is the diagonal argument intuitionistically valid?
>>16899466It's just invalid altogether. You cannot prove the existence of an infinite number of things while using a finite amount of reason without your proof being circular.
>>16899466no it’s impossible to complete.
>>16899472But Cantor specifically constructs a method for showing that the set in pic rel is uncountable, and his proof by contradiction does not fail intuitionistically because it doesn't rely on double negation and therefore does not include any hidden assumptions about LEM.
If it isn't, then all inductive arguments are invalid.
>>16899474he never finished it lol
>>16899475induction works fine as long as it’s done in a finite amount of steps.
>>16899476How so?
>>16899466The binary tree gives visual intuition. Branches like are countable, but there's no way of counting the branches.
It still proves that the functions bool -> nat are not countable. But it doesn't prove that that they are not subcountable.
>>16899466Yes, at least in the form "there is no bijection between natural numbers and infinite strings of 0's and 1's". You're intuistionistically allowed to conclude not-P from "P implies contradiction". You just can't conclude P from "not-P implies contradiction"
As you can clearly see, no excluded middle is required:[code]def surjective (f: α ω) : Prop := ∀y, ∃x, f x = ytheorem lwfix (f: α α ω)(sj: surjective f)(u: ω ω): ∃x, u x = x := let d x := u (f x x) let ⟨c, (fp: f c = d)⟩ := sj d have := calc d c = u (f c c) := rfl _ = u (d c) := by rw[fp] ⟨d c, this.symm⟩[/code]
>>168995024chan ate some arrows, so here's a link: https://live.lean-lang.org/#codez=CYUwZgBAzgrgTgKxAYwC4EsBuIIAowBcEgjcASBJhBIJPAAlBEQApwD2ADnQLwQSAARAJ4A0EQMBEAD0GQRETrwBQM1AAsQTOCAC2EADYB3MOkn4ipCsarVcUBEViIUGbBDDmYRSuTNFRgmBEmdJBOwyXJogqBDAvhwQPvhRItTBWmEQgBfkyIL4LESQyFIR1ICX5NGWEUkKAIYOgRDIFZrISVyReZyxubW0NXBgmk0QAPpc+bEttFw1AEa8EHDaANpgLAC6SaktgoroUAB0ULxqaoVAA
>>16899478this
As some anons have pointed out, there's various diagonal constructions and not all use the same principles or are equivalent.You say "intuitionistically", I take it to mean vanilla constructive, but if you look at different schools (Brouwer, Markov Jr, more modern models of set theories in topoi), you 'll also get different answers.Two years ago I made a breakdown on set theoretical failures and anti-classical results. I also set down and go through it in a video, with an emphasis on trying to motivate why classical results can be broken and in what sense it's this is. Very relatedly, in the logic playlist I have one where I discuss how the Königs lemma fails, and how the constructive/formal Church Turing thesis breaks LEM (even WLPO). This or next week I'll also do on on locally constant choice in the Brouwerian school.https://youtu.be/q-mjO9Uxvy0
>>16899602This is the second half from that bullet point list, from the script go through use that's also on gist. Since I studied this fairly fringe corner of logic quite a bit, feel free to ask something not on thiere.
>>16899603>{X,X} surjects onto {0,1}^Xexcuse me what the fuck?
>>16899642https://arxiv.org/pdf/2207.13300It's a strong form of breaking withhttps://en.wikipedia.org/wiki/Tarski%27s_theorem_about_choiceI think very roughly, for [math]X[/math] you take the union over all the ordinals [math]ω_n[/math], which is a limit ordinal of size [math]\aleph_\omega[/math]. You stratify the whole thing into layers, in a complete graph kind of way, and the [math]X\times X[/math] represent edges. And the surjection from the edges map down on what's below that edge. (This is my vague impression, likely very blurry)---Vaguely related, there's a nice breakdown of possibilities in ZF in functional analysis athttps://karagila.org/wp-content/uploads/2016/10/axiom-of-choice-in-analysis.pdfI'll next steelman Brouwerian choice, the (weakest?) consequence being that all functions [math] ({\mathbb N}\to{\mathbb N})\to{\mathbb N} [/math] are locally constantLCP fromhttps://www.jucs.org/jucs_11_12/constructive_set_theory_and/jucs_11_12_2008_2033_rathjen.pdf
>>16899665>ZF without Cwhat possible use could anyone have for such an abomination?
>>16899667There not being a discontinuous linear map in every vector space :PNa, I donno, maybe people want all subsets of R be Lebesgue measure.I know some anti-choice set theorists, I could ask em.But that's not my battle - everything I care for and worry about lives in [math]V_{\omega+7}[/math]
>>16899466(** The diagonal argument is 100% valid and in fact is a COQ/ROCQ theorem that you can compile online or wih coqc installed on your computer. Just copypaste the textbelow. *)Theorem diagonal: forall f: nat -> nat -> bool, exists g: nat -> bool, ~ (exists p: nat, forall q: nat, f p q = g q).Proof. intro f. exists (fun k: nat => negb (f k k)). intro F. destruct F as (i, G). absurd (f i i = negb (f i i)). destruct (f i i); discriminate. apply G.Defined.
>>16899466>>16899690COQ/ROCQ is intuitionnist for the record, and thus of course the above formalized proof is.
>>16899668You cannot be a set theorist and be an "anti choice"; not because you'd be a pro-choice but because in that situation you would probably have mastered the tools that makes that kind of position meaningless, for instance: starting from any model U of ZF you can bechanically build:1°) a submodel L of ZF+global choice (stronger than AC: L is Gödel constructible universe)+ GHC; and from that L you can build three models M, X, M[G] and a map j: V -> M (through forcing, via boolean valued model technique described in Takeuti set theory books) such that j is elementary (L and M satisfy the exact same sentences), X is a transitive submodel of M[G] and M is a transtitive submodel of X (X is the model Paul Cohen used to refute AC) and:M,X and M[G] all have exactly the same iintegers and satisfy the same arithmetical sentences!! So arithmetic (including whether a Turing machine halts or not and thus anything from math which has a concrete meaning) is IMMUNE to switching AC on/off; this vbesides can be extended to some sentences including certain subsets of P(N) (see Shoenfield absoluteness theorem).
>>16899466What is it
>>16899700Well ofc those guys know the ins and outs of Shoenfield absoluteness and forcing arguments for what you can patch on top of this and that model. All I can report is that there's people working in set theory who say and mean "the axiom of choice is false." I can't explain their full position better to you, but you likewise see people looking you straight in the face and making consistency claims about this and that theory because reasons/Platonist conviction. In and out knowledge of quantifier stratifications and reflection principles doesn't seem to sway some away from reading some sort of ontological truth into sets, and some rules for them, one big. As for me, I don't care too deeply (and even if I was writing papers in the field myself, I think I'd not by a Platonist, nor multiverse guy nor even a convinced formalist.) I'm not the one to argue about this.
>>16899471That’s ridiculous. What if I just start counting, 1..2..3. Are you telling me I’ll hit the limit, find the highest number possible?Many proofs of infinite prove by contradiction; showing it’s impossible for the answer not to be infinite
>>16899702This looks like some eager AD propagandist position (maybe I'm mistaken but yes I'd like to interact with these people a bit). Again we have some serious improvements on the result above: let P be any sentence of second order arithmetic (i.e. with quantifiers restricted on N or P(N)). Then from forcing techniques we have ZF + global choice + HGC proves P if and only if ZF+DC proves P (folklore forcing argument seen in an Ali Enayat FOM mail list message but also here at pages 7-8: https://www.irif.fr/~krivine/articles/Forcing.pdf)What does that mean? Virtually every piece of math that is not pure algebra or foundational can be readily formalized and proven in second order arithmetic (with full comprehension and DC). If you have a PHD in engineer math it fits in SOA unless some miracle. And even ADist prefer DC (people don't want to deal with omega_1 having a countable cofinality I guess). It is pointless to force people to adopt some very risky axiom that is equiconsistent to some mammoothly gigantic cardinals just because of the entertainment value and removing the fruitful AC.
my understanding of what the diagonal argument actually proves is "if this system of axioms allows countable infinities (i.e. you can count to infinity by induction), the system also has uncountable infinities"but i've always been a bit put off by the way Cantor's construction works - if you put the enumeration in unary, the length of the label is the same as the number of differing infinite binary strings... which by definition of the natural numbers is always finite. Cantor never gets to a point, even by induction, where he can add a binary number different from an infinite length subset of infinite length binary strings unless you only induct the list of binary strings to infinity but not the enumeration.... you can't induct the enumeration to infinite length at all by definition, so how does it work for the binary strings with a "maximum number of differing digits" that is exactly as finite as the length of a natural number?idk maybe i'm just psyoping myself here
>>16899709I'm very SOA pilled. I just said [math]V_{\omega+7}[/math] to make integral transform type and results on that level easy to deal with. (I might even be FOL arithmetic with all finite types [math] {\mathbb N}\to\ast [/math] and [math] \ast \to {\mathbb N} [/math] pilled, although I only see that in truth theory books. I haven't checked if this lacks anything, I don't know how higher order statements are formulated there.)Likely a dependent type theory would be even smoother, but as long as the books aren't being written like this, I'll not start writing in a language many people don't understand.[math]V_{\omega+\omega}[/math] is a topos and iirc a model of ZFC-Replacement. It has categories of Hilbert spaces. The working math of QM is one of the reason why I'd not start the conversation with SOA.>>16899724If you got N and function spaces out of N, then you got uncountability.(N is generally taken to be the inductive set. "Count to infinity" is language you want to avoid, but I catch your drift.)As for buying into a proof of uncountability, it's much smoother to just look at the purely set theoretical argument that any X can't be surjected into {0,1}^X. If you're just looking for uncountability, then talking about reals, let along digit expansions, just makes things more complicated. Not that they aren't relevant, but just messier. And digit expansion talk needs a lot more logical/theory axioms than just plain sets - which you need anyway.
>>16899496>the functions bool -> nat are not countableSorry, I meant*the functions nat -> bool
>>16899705Yes, it's possible. Just because you don't find intuitive doesn't make it impossible.
>>16899747Wait, you actually think that natural numbers might stop at some magical number?
>>16899773obviously there's nothing "natural" about those so-called "natural numbers" and subitizing stops at ..... so that's the last properly natural number
>>16899466yeah, what >>16899501 said
>>16899773If the universe has only finitely many states, it's possible. The maximum number will be the number of states.
>>16899472 >>16899476nigger, intuitionism=/=constructivism
> You cannot prove the existence of an infinite number of things while using a finite amount of reason without your proof being circular.You don't have to. A type is not a collection of things, it's a class of values by construction. A value is value of a natural number type if it is constructed in a particular way.Induction also has little to do with infinity: it descents. It's about reducing a proof of P(n+1) to a proof of P(n) and so on until you inevitably reach P(0).And a diagonal argument is not about infinte number of things. It merely states that some function cannot possibly exist.
>>16899773No obviously not since there is no natural number that is greater than or equal to every natural number. But there are infinite numbers called transfinite numbers, the first of which is the number ω, which is greater than literally every natural number. You can continue to count uperwards with it too, ω+1, ω+2, ω+3 .... Infinity is weird man.
>>16899466itt: bunch of mathlet rednecks and Normie Wild-burger failsons seething that the Good Lord gave Georg Cantor, a Christian of Jewish descent, this remarkable insight into the divine infinite.
The question has been answered in good detail, but this thread will still survive all of February.Quote me in March.
>>16899733yeah i just want to be clear my issue isn't really with the conclusions at all, but more specifically with the fact that there's more than one axiom independent of the rest of ZF that Cantor is relying on.set theory only allows this argument to work via the independent Axiom of Infinity; ZF - Infinity can't actually prove Infinity or (not)Infinity. ZF can't prove Choice either, but funnily enough ZF - Infinity + (not)Infinity DOES prove Choice. regardless, the argument is a "smoother" result in set theoretic arguments literally because it's restating axioms, lol.this all in turn is why i think a more accurate framing of the diagonal argument is that "if a countably infinite set exists (provided Axiom of Choice), uncountably infinite sets exist." and you can simplify by ignoring the countability of the first set, so the real formulation is:"if (Axiom of Infinity) + (Axiom of Choice), there exist uncountably infinite sets."tl;dr: not enough of a deal is made of the fact that Infinity and Choice are both independent of the other axioms, or that Infinity is the reason Choice is necessary as an independent axiom in the first place....for the record i am not a finitist, just to make that clear.
>>16899832> divine infiniteSo you confirm it's all theology.
>>16899853The divine 1 didn't stop the concept of 1 having mundane applications.
>>16899853Yes, according to Cantor, God is the absolute infinite, as distinguished from actual infinities. Mathematics is theology.
>>16899853Indeed. All the independence results in set theory confirm that. You can make up answers to the set theory questions as you go along, just like you do in theology. In the other sciences, that would make it unfalsifiable nonsense.
>>16899851Mhm, yeah I mean theories are generally chosen in a fashion not full of redundancies, so usually all axioms of a theory, as presented, are independent of the others. (For Z vs ZF, there's the accident that Collection is redundant if you got LEM, Pairing and Replacement, but that's due to historical reasons. Replacement and Regularity came with Franklin and Neumann. Indeed as I write above, iirc V_\omega·2 is a model of Z, which goes to show how small the original set theory of Zermelo was. Anyway.)The hereditarily finite sets (of which you can loop through all the names via 3 lines of code) model ZF-Infinity. So indeed, ZF + not Infinity has a good relation to choice. I think the best way to grok it is by realizing that "the spine" of the universe V, the ordinals, in case of those small models is just \omega_0. The original \omega_0 is not a set in the theory without infinite, so \omega_0 is On, the class of all ordinals. In other words, the ordinals are just the numbers n={0,1,...,n-1}. Every set being finite exactly means every set is in bijection with an n, which (funny part) all sets are well-ordered, which is the classical ZF equivalent to the axiom of choice.If you want to see a rather technical text that does all of this also constructively, there'shttps://arxiv.org/pdf/2010.04270If you (or anyone) want to see the hereditariy finite world in a very lean type theory, there'shttps://www.ps.uni-saarland.de/Publications/documents/SmolkaStark_2016_Hereditarily.pdfThe "negative core" of many (not really all, but various) diagonalization arguments is also worked out in Lawvere's proof (usually done category theoretically). This is 1 step before you make a contraposition to turn it into a nogo theorem. The nice core about it is really a fixed point theorem: You get that a surjection onto a function space with image being some set/type V induces a fixed point in a map n:V->V. I spell it out in more logical terms in the pic (that's also a vid).
>>16899923(forgot to mention that you get Cantor from this Lawyere fixed point theorem by choosing V={0,1} and n(v):=1-v, or said differently V=Bool and n=\neg)
>>16899923Want to repeat this since it was maybe more obscurely formulated than intended:No set being infinite classically means every set being finite. Every set being finite classically always just means all sets being in bijection with a finite ordinal, the member of the smallest infinite ordinal (here a proper class). Those finite ordinals are even cardinal numbers. Being in bijection with an ordinal means you're well-ordered. So there not being an infinite set is another way of saying all sets are well-ordered. The prove that a well-order implies a choice function (leaving out the empty set ofc) is here every simpler than in the general case.
yes they are. it's also constructively valid. anyone saying otherwise is on par with midwits thinking negative latitudes don't exist and that the earth is just a northern hemisphere, simply because negative numbers can't exist.
>>16899466I think you're taking about type theory and my uninformed answer is no. Intuitionist type theory doesn't allow you to use these kinds of infinite sets.
>>16899899There are no theorems about Cantor's absolute infinite, as opposed to many theorems about actual infinities. There is a theorem in modal logic about a Gödel formalization that has nothing to do with Cantor's
>>16899903it is unfalsifiable nonsensehistorically set theorists just kept adding axioms until they had something that was not trivially self-contradictorygenerally speaking, mathematics is not science
>>16899471>It's just invalid altogether.>You cannot prove the existence of an infinite number of things while using a finite amount of reason without your proof being circular.Okay. One problem. Circular arguments are definitionally valid.
>>16900056exactly, which is why a monad is just a monoid in the category of endofunctors.
>>16899705>That’s ridiculous. What if I just start counting, 1..2..3. Are you telling me I’ll hit the limit, find the highest number possible?You won't find the highest number, but you will run out of memory by either dying first or getting to some arbitrarily large number where you lose your count.
>>16899733>It has categories of Hilbert spaces. The working math of QM is one of the reason why I'd not start the conversation with SOA.Do Non-second countable Hilbert spaces occur in QM? If not, then you're in l^2 all the time and this space is well managed by SOA (like any polish space, with the help of long and tedious encodings though).
>>16900174I mean it's physics, you don't want to pin down a theory you can't break from. (It's not like algebraic geometry where you pin down a setting an explore it. Rather you got some "experimental facts" and try to compress the observation info a new framework that also makes predictions. New ideas need freedom from formalities, albeit someone better clean up the mess eventually. If you do a 20 page manual QFT scattering integral, you might even want to make ad hoc assumption/hypothesis at the get go, so technically you're moving to another theory mid calculation, lel.)But in any case, while nice spaces might be well codable in SOA, and people who just do QM for semicondutor models and such will be satisfied with a single Hilbert space, I do quite explicitly mean that people (not just nLab shizo level) also do use categories and functors to speak about many Hilbert spaces at once. I'm confident that certain things are codable, but once you talk of functors with codomain some big category of Hilbert spaces, having some quantifiers over such objects is just more convenient. I'm not saying you can't get far, I'm just saying I don't start defending second order arithmetic without any more types, as foundations, when I face theoreticians.
