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

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, 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, 8 days ago to random

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

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

boarders, 20 days ago (edited 19 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

boarders, 1 month ago to random

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.

boarders, 1 month ago to random

So many aspects of current culture are simply different versions of: “lottery winner endorses lottery as path to success”

boarders, 1 month ago to random

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

boarders, 1 month ago to random

"Double negation elimination (DNE) states that if a proposition is not false (¬¬P), then it must be true (P). This principle is accepted in constructive logic."

boarders, 2 months ago to random

What Scott calls the "first-order disease" - the absolute dominance of thinking the only truly worthwhile quantificational logics are first-order logics - has only confused me more over time. From a philosophical point of view only quantifying over "individuals" and the Quinian worry that quantifying over "properties" or "functions" represents a kind of platonism due to "ontological commitment" sounds like something from the scholastics and I am taken aback anyone takes it seriously. From a model theory point of view first-order logic is in some sense characterized by the Lowenheim--Skolem theorem and the compactness theorem (Lindström's theorem essentially says it is the strongest logic with these properties), guaranteeing both that it cannot prove categoricity results (so cannot hope to give any account of structuralism in mathematics), but also cannot talk directly about infinite or finite theories.

The most persistent version of this disease to me is the the intense focus in computability theory to think the only (partial) functions we care to discuss are those from ℕ → ℕ - bizarre that the failure of the higher-order Church--Turing thesis is not more widely studied

boarders, 2 months ago to random

Topos theory confusion: If I consider the topos Set/ℕ then this has a global element n : ℕ (generic natural number), and I think you shouldn't be able to prove: n = 0 ∨ n ≠ 0 since this number is 'generic'

On the other hand, this topos is classical as it is isomorphic to Set^|ℕ| - so the law of excluded middle should hold. how do I resolve these two things? Is it something to do with internal vs external interpretations of a logical statement?

boarders, 2 months ago to random

Type theorists and set theorists both frequently agree with a kind of tacit formalist idea - “if mathematics is not written in our language then it is not mathematics” - category theory did not become mathematics when people decided universes / reflection / classes made it set theoretically respectable, your proof development did not become mathematics when agda finished typechecking

boarders, 2 months ago to random

"Finally, yes, every generation thinks the younger generation is failing to make the grade—except for the current cohort of professors, who are by and large more invested in their students’ success and mental health and more responsive to student needs than any group of educators in human history. We are not complaining about our students. We are complaining about what has been taken from them."

https://slate.com/human-interest/2024/02/literacy-crisis-reading-comprehension-college.html

boarders, 3 months ago to random

Quine and Kripke both said that intuitionists don’t really disagree with classical mathematicians about logical principles since they mean different things by the connectives, are there any good starting points that discuss this sort of meta-logical question about adjudicating between different systems? Personally, I think this view is quite wrong, since classical logicians think constructivists are confusing truth with proof (i.e. they think intuitionistic logic is part of classical modal logic where box is provability), and constructivists think of classical logic a subset of constructive logic - either under the double negation operator, where classical truth is about irrefutability, or using HoTT’s squash operator where classical truth is about mere existence.

boarders, 3 months ago to random

Reminded again at work that Fortran doesn’t have short circuiting for Boolean operations. Some of the compilers (intel) will implicitly convert TRUE to -1 (all bits set) and FALSE to 0 and they will convert an Int to a bool based on whether the first bit is set (depends on endianness of hardware). Fortran77 ignores any characters after column 72 and so if you have “*100” and the 0 is at that column then the compiler will read it as “*1” followed by a comment.

boarders, 3 months ago to random

How do you motivate the stable part of stable homotopy theory to a layperson? I think I would lean towards Thom’s computation of the unoriented cobordism ring, but even that is quite challenging to get at. The homotopy groups of spheres are hard to motivate as a fundamental object to someone outside mathematics.

boarders, 3 months ago to random

does the category Set have more than one elementary topos structure? In the definition we have to pick a representable object for Sub(-), but Sub(-) has typically had an automorphism which flips the ordering and so there are different choices of how 2 represents it (corresponding to not : 2 -> 2). Maybe the structure of a power set object only says there is some choice, but any choice will do.

boarders, 4 months ago to random

https://www.experimental-history.com/p/i-wanted-to-be-a-teacher-but-they - the amount student evaluation operates as a legitimating factor for “meritocratic” ranking and the “just deserts” model is a shameful part of how we approach education

boarders, 4 months ago to random

Idle question: does every infinite set have a bijection with a proper subset without choice?

boarders, 4 months ago to random

What are some compelling ways to explain type theory to someone without a mathematics background, are there some particular interesting results one could showcase?

boarders, 4 months ago to random

Rather than stating the truth conditions of logical operators as material truth conditionals - for example, A ∧ B is true if A is true and if B is true - we can re-phrase them in terms of at least or at most:

A ∧ B is at most as true as both A and B

A ∨ B is at least as true as A and at least as true as B

A ⊃ B holds if B is at least as true as A

This now makes sense in an intuitionistic setting without bivalence

boarders, 5 months ago to random

Reasons I dislike formalism in the philosophy of mathematics:

1. Those that follow it tend to have the view that mathematics as a human practice should cause no philosophical puzzlement, that this perennial question about the nature of mathematics as “synthetic a priori” is not just a question in need of disillusion - but one that couldn’t possibly rouse some deep sense of mysticism.

2. Explaining mathematical practice as the making of certain meaningless marks in certain orders is like explaining language as certain movements of air caused by certain manipulations of the throat.

3. Formalism ultimately seeks to find some “autonomous discursive practice” - a language game one could play though one plays no other - which emerges spontaneously from nothing, which is deeply misguided to anyone who had read Quine or Sellar’s criticism of logical positivism.

4. Taking formalism seriously means that, perhaps, someone like Frege is the first mathematician - what were Gauss, Euler and Galois doing before them? Funnily enough, Bertrand Russell says something like this somewhere (which one should probably take as no endorsement)

boarders, 7 months ago to random

This quote of Rosenzweig (especially the ending) speaks to how to approach mathematics:

“The first pages of philosophical books are met by the reader with special reverence. He believes that they are to be the basis for all that follows. Therefore he also thinks that it would suffice to refute them, in order to have refuted the whole. Hence the enormous interest in Kant’s doctrine of space and time in the form in which he developed it in the beginning of the Critique; hence the comical attempts to “refute” Hegel with respect to the first triple-step of his Logic, and Spinoza with respect to his definitions. And hence the helplessness of the “general reader” [Rosenzweig uses the English words here] before philosophical books. He thinks they must be “especially logical,” by which he means the dependence of each subsequent sentence on each preceding one, such that when the famous one stone is pulled out “the whole comes tumbling down.” In truth, this is nowhere less the case than in philosophical books. Here a sentence does not follow from its predecessor, but, much more likely, from its successor. It will be of little help to whomever has not understood a sentence or paragraph if, in his conscientious belief that he may leave nothing behind uncomprehended, he reads it over and over again, or even starts once more from the beginning. Philosophical books defy the ancien regime strategy that thinks it may not leave any unconquered fortresses in the rear; they want to be conquered in a Napoleonic manner, in a bold advance on the enemy’s main force, after whose defeat the small border fortresses will fall on their own.”

boarders, 8 months ago to random

Lorna Finlayson on the problems facing academics in the UK: https://newleftreview.org/sidecar/posts/the-sycophant

“It is teacher’s pet syndrome: an ingrained trust in authority – the conviction that those in power are basically reasonable people who have our interests at heart – and an equally ingrained fear of getting in trouble.”