A
Anonymous01/26/26, 05:56No.16899466
is the diagonal argument intuitionistically valid?
60
Replies
A
Anon01/26/26, 06:15No.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.
A
Anon01/26/26, 06:26No.16899472
no it’s impossible to complete.
A
Anon01/26/26, 06:36No.16899475
If it isn't, then all inductive arguments are invalid.
A
Anon01/26/26, 06:43No.16899481
The binary tree gives visual intuition. Branches like are countable, but there's no way of counting the branches.
A
Anon01/26/26, 07:10No.16899496
It still proves that the functions bool -> nat are not countable. But it doesn't prove that that they are not subcountable.
A
Anon01/26/26, 07:57No.16899501
Yes, 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"
A
Anon01/26/26, 07:59No.16899502
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]
A
Anon01/26/26, 14:00No.16899602
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
A
Anon01/26/26, 17:29No.16899690
(** 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 text
below. *)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.
A
Anon01/26/26, 17:31No.16899693
COQ/ROCQ is intuitionnist for the record, and thus of course the above formalized proof is.
A
Anon01/26/26, 17:53No.16899701
What is it
A
Anon01/26/26, 18:30No.16899724
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
A
Anon01/26/26, 20:52No.16899807
yeah, what
A
Anon01/26/26, 21:19No.16899819
> 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.
A
Anon01/26/26, 21:48No.16899832
itt: 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.
A
Anon01/26/26, 21:51No.16899833
The question has been answered in good detail, but this thread will still survive all of February.
Quote me in March.
A
Anon01/27/26, 02:54No.16899929
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.
A
Anon01/27/26, 03:26No.16899952
I 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.
A
Anon01/28/26, 02:29No.16900535
[math]sheeeeeiiit[/math]
A
Anon01/28/26, 19:44No.16900852
That is a retarded way to write x < 2^x.