Random observation: If E denotes a collection of vectors of a vector space V, then we can write a judgment of the form E ⊢ v, to mean that v is in the span of E. This satisfies the structural rules of logic, for instance {v} ⊢ v and we have cut elimination since we can expand out brackets. This also satisfies a kind of compactness property - any spanning judgment will only involve a finite number of vectors since that is what it means to be in a span.
Is this kind of observation (in a more general context of a monad on a category maybe) made explicit by some well-known type theory in categorical logic?
@antopatriarca which (distributive?) lattice do you have in mind? maybe the lattice of subspaces of a vector space (though this is famously not distributive)
@boarders It was just an idea since I now tried to work on your construction and I met some difficulties. So what does E, F ⊢ v, w means in your context? Are the two spaces supposed to be intersected? Is "v, w" the span of the two vectors? If that is the case then the cut elimination would read as "if the span of A and v is included in E and w is in the intersection of F and A, then the union of v and w is contained in the intersection of E and F." This doesn't work, as we can for example have v ⊈ A and 𝐸 ∩ 𝐹 = A ∩ 𝐹 = 𝐴. I guess we can have "v, w" means disjoint union. In this case, I think it would work, but it obviously isn't the usual lattice of vector spaces. In fact, I would say the fact they are vectors has nothing to do with this construction.
Zermelo formulated a version of "second-order" set theory in which one uses the ZFC axioms, but instead of a relation ∈, we quantify each statement over some given relation R e.g.
the axiom of extensionaliity: x R A ⇔ x R B ⇒ A = B
and then we can write down the property that R satisfies the ZFC axioms ZFC(R). This satisfies a certain categoricity property that says that all such models of second-order set theory are grothendieck universes (equal to the cumulative hierarchy up to some inaccessible cardinal). It follows that for any two such models one is an initial segment of the other. Such a cumulative view of the set-theoretic universe seems to rely in some sense on the idea that the category of ordinals behaves like an ordinal - in the sense that for any two ordinals one is uniquely isomorphic to some initial segment of the other. Such a principle relies on some background of excluded middle, the category of ordinals in a topos doesn't necessarily behave like that. I wonder then if one can show a version of Zermelo's theorem in a constructive meta-theory in which the collection of models is still isomorphic to the category of ordinals?
where f : ℝ → ℝ, are of the form f = x ↦ c x for some c ∈ ℝ. Such maps must also be ℚ-linear and so if we can choose a basis for ℝ over ℚ then we can also get uncountably many discontinuous solutions to the equation. Such bases require something like the well-ordering principle and so I wonder if in constructive mathematics / topos theory if the question can have interesting alternative answers (e.g. if it is possible that there are only finitely many discontinuous solutions or something like that).
Can you use a theory of generalized differential equations to find the “space of solutions” to a regular expression problem? I have in mind something like finding the most general regular expression for which it accepts a given set of strings? I think if you do this naively and you wanted something such that it accepts:
“hallo” and “hello” then it’ll give “h(e|a)llo” and there is an easy algorithm to compute that, but I suppose I am interested in ways to make such input strings give back “h[a-z]llo” or something closer to that
@rileyshahar It is the most general solution, of course - my question is about asking what is the right framework for asking about the space of solutions to such questions - there is a most permissive solution (.) and a least permissive solution (h(a|e)llo) and a family of solutions in between ('hllo' etc.)
In axiomatic propositional logic (or even minimal logic), the axioms (really axiom schema) for → are usually given by:
(A1) A → (B → A)
(A2) (A → (B → C)) → ((A → B) → (A → C))
One also has a rule of modus ponens:
(a) A, (b) A → B
------------------------ MP a, b
B
[In this context it is impossible to care about the distinction between "rule" and "axiom" but everyone mentions it anyway and then proves that it doesn't matter]
One then shows in propositional [minimal] logic one can prove the theorem Id:
Lemma (Id)
A → A
Proof
A → ((A → A) → A) by (A1)
A → (A → A) by (A1)
(A → ((A → A) → A)) → ((A → (A → A)) → (A → A)) by (A2)
((A → (A → A)) → (A → A)) by MP 3,1
(A → A) by MP 4, 2
This seems a bit magical unless one knows that (A1) is just a schema for the K combinator, (A2) for the S combinator [which in turn is the applicative function application <*> for (e → _)] and this is the usual combinator identity:
I = S K K
which is plausible if we think of S as function application with access to some shared environment and K as the function that ignores everything but gives back the shared environment.
[Note that each K has to be instantiated at a different type much like typing exponential in the simply typed lambda calculus]
It is interesting that in these axiomatic proofs one gives "types" and axiom schemas but usually doesn't mention how the schema and the "type" unify. Using lambda or combinatory terms has a massive advantage since we condense 5 lines to 1, but strictly speaking we should check (or rather a typechecker should) that the types can be inferred/provided and it is correctly typed with the given types.
I have these definitions in agda (which is meant to show that the lexical product of two well-ordered relations is well-ordered):
module WellOrderedLex {ℓ : Level} (A B : Set ℓ) where
-- [skipped imports / standard defs]
data Desc (R : Rel A) (y : A) : Set ℓ where
step : (∀ (x : A) → R x y → Desc R x) → Desc R y
data Lex (R₀ : Rel A) (R₁ : Rel B) : Rel (A × B) where
FstR : ∀ {a₀ a₁ : A} {b₀ b₁ : B} → R₀ a₀ a₁ → Lex R₀ R₁ (a₀ , b₀) (a₁ , b₁)
SndR : ∀ {a : A} {b₀ b₁ : B} → R₁ b₀ b₁ → Lex R₀ R₁ (a , b₀) (a , b₁)
{-# TERMINATING #-}
desc-lem : {R₀ : Rel A} {R₁ : Rel B} →
(a : A) (b : B) →
Desc R₀ a →
DescR R₁ →
Desc R₁ b →
Desc (Lex R₀ R₁) (a , b)
desc-lem {R₀ = R₀} {R₁ = R₁} a b (step a-step) dB (step b-step) =
step (λ {
.(_ , _) (FstR Ra'a) →
desc-lem _ _ (a-step _ Ra'a) dB (dB _) ;
.(a , _) (SndR Rb'b) →
desc-lem a _ (step a-step) dB (b-step _ Rb'b)}
)
Desc-Lex : {R₀ : Rel A} {R₁ : Rel B} →
DescR R₀ →
DescR R₁ →
DescR (Lex R₀ R₁)
Desc-Lex desc-R₀ desc-R₁ (a , b) =
desc-lem a b (desc-R₀ a) desc-R₁ (desc-R₁ b)
Any ideas for what to try to convince agda that this definition is actually terminating? Would also appreciate pointers towards proofs that show this fact using possibly different definitions (but still fully formalized in a constructive setting).
Note: please skip tedious comments about hyphens and prescriptive grammar, I couldn't care less
Towards the beginning he mentions some bad reasons for not believing in excluded middle include the undecidability of CH. This is true, but I don’t think it is a bad thing to mention (or perhaps I just feel bad since I am guilty of having done so) since:
CH ∨ ¬CH - “CH is either true or false” is a theorem of ZFC since it is just an instance of LEM. This is obviously not a solution to Hilbert’s first problem
Pr(CH) ∨ Pr(¬CH)- “there is a proof of CH or a proof of its negation in ZFC”. This is is not true, as shown by Cohen + Gödel (this is not an internal statement in ZFC, it is meta-theoretical)
Dec(Pr(CH)) - it is decidable that we can give a proof of CH, or that we can’t give a proof. This is also true, but this time we can’t appeal to LEM so we must be appealing to something else (in this case we appeal again to Cohen + Gödel). But this means we don’t accept the meta-theoretic principle LEM when it comes to statements about provability
The thing he emphasizes is different models and this I strongly agree with.
In ZFC, any vector space has a basis as a result of the AOC (axiom of choice). Debating whether every vector space has a basis by arguing about matching socks or Banach—Tarski is a waste of time from a bygone age. Instead, we should realize the mathematical fact that in a sheaf topos on a space X, if we consider a vector space then this is a continuous family of vector spaces on X and a choice of basis amounts to a global trivialization of the corresponding bundle. There exists non-trivial vector bundles however (in any kind of mathematics we choose!), and so we have reasons to not believe in the AOC.
Rust + serde ecosystem is just way too good if you are writing anything that is mostly just data mangling against some known schema, no need to be using python for these tasks which makes me only ever regret the choice
I think “active learning”/“student-centred learning” and other new ideas for how university teaching might work are great. A model for learning based too much around “propositional knowledge” and too little around capacities and practices leaves us in the same decrepit situation as analytic philosophy’s view of epistemology (“justified true belief”). It is slightly sobering however that the gold standard of a “flipped classroom” is how high school mathematics works, and I don’t think many people would view that as any kind of ideal of education, to say the least
"You cannot plonk someone in front of a computer screen for an hour and expect them to become a better person. Well-meaning researchers have tried way, way harder than that and gotten way, way less."
Moderately interesting (to me!) that in mathematics a magma is basically a useless idea that you wouldn’t even define in an undergraduate degree, but the typed analog - an applicative structure - is a very useful starting point for realizability, semantics of type theory / HOL etc.
Applied category theory would probably be significantly better if it gave more actual examples of “compositionality” and the main proponents of it sounded less like people trying to get know-nothing VC funding - the main exception I know is Tai Danae Bradley, who has a deep appreciation for CT as a unifying concept