boarders

boarders, 6 days ago (edited 3 days ago) to random

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?

boarders, 7 days ago to random

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?

boarders, 7 days ago to random

The continuous solutions to the equation:

f (x + y) = f(x) + f(y)

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).

boarders, 7 days ago to random

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

boarders, 8 days ago to random

Just landed in Switzerland for Zurihac if anyone would like to meet up this week

consequently, 9 days ago to random

My anticipation is building for next week’s Nordic Logic Summer School and my class on proof theory. (The fact that I get to visit Reykjavík is to teach is a cool bonus.)

https://consequently.org/class/2024/nls-proof-theory/

#prooftheory

jonmsterling, 13 days ago to random

God I am so frustrated with opam... I am ready to jump.

boarders, 14 days ago to random

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

1. A → ((A → A) → A) by (A1)
2. A → (A → A) by (A1)
3. (A → ((A → A) → A)) → ((A → (A → A)) → (A → A)) by (A2)
4. ((A → (A → A)) → (A → A)) by MP 3,1
5. (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.

boarders, 14 days ago to random

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

joey, 18 days ago to random

I think I asked this before but:

Is there an analog of "locality" when moving from topological spaces sheaves to sheaves on a site? Or was it something specific to spaces that was generalized away when moving to sites?

antidote, 18 days ago to random

Can someone give me a really good excuse to learn (algebraic) geometry? As an outsider, the maths sounds like a real challenge and something I’d probably get a lot out of learning, but I’ve not got any real motivations to step on the ladder!

deech, 19 days ago to random

Git reflog should be taught on day 0. It is the easiest way of getting out of jams which is basically your life with Git.

pkhuong, 19 days ago to random

Work is both performance and liability^Wcorrectness oriented, and I noticed a common pattern is that we'll generate commands with a fully deterministic program (i.e., a function), reify the command stream, and act on the commands.The IO monad is real!

codyroux, 19 days ago to random

The amount of people claiming to hate math but love sudoku is alarming.

Reminds me of people who love poetry but hate rap.

boarders, 20 days ago (edited 20 days ago) to random

Andrej Bauer gave an excellent recent talk “How to not believe in the law of excluded middle”: https://youtu.be/96iHUx0aGDs?si=y9j8Kc9znPs-cS1U

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

jonmsterling, 20 days ago to random

https://www.fpcomplete.com/blog/type-safety-doesnt-matter/

Ah, the old "Kill yourself in order to gain sympathy from the dead" rhetorical trick... Honestly it is hard to believe that this kind of opportunism still walks.

No, the goal of types is not to get rid of as many runtime errors as possible. next, please!