Anonymous at Sun, 28 Jul 2024 08:18:05 UTC No. 16300087

>>16299720
Check this out, OP:
https://us.metamath.org/

Intuitionism is a believe system that the theorem of the excluded middle doesn't hold.
"New Foundation" is a set of set theory and logic from the Philosopher Quine.

Anonymous at Sun, 28 Jul 2024 14:44:52 UTC No. 16300430

>>16299720
cool tool OP, i'll check it out

>TND
heh

Anonymous at Sun, 28 Jul 2024 17:58:21 UTC No. 16300605

>>16299720
This is really cool. Great find

Anonymous at Sun, 28 Jul 2024 18:49:06 UTC No. 16300675

>>16300087
Oh I've seen Metamath before, it's cool but there are others that are in my opinion better, in particular I prefer Isabelle. I remember when I first discovered proof checkers I wanted to do something with it, so I decided to write a proof of something as my undergrad thesis, I decided to write a proof of the correctness of the aho-corasick algorithm for pattern search. In the end it never worked out, but I still have hope I can make a project out of using a proof checker. Although I would probably use Isabelle or Coq rather than Metamath.

Anonymous at Sun, 28 Jul 2024 20:02:38 UTC No. 16300805

>>16299720
damn, wth? Someone guide me through that proof, or a simpler statement maybe

Anonymous at Sun, 28 Jul 2024 20:18:38 UTC No. 16300835

>>16300805
This video https://www.youtube.com/watch?v=skPuu8Zt1hU explains the proof. I just transcribed the argument using the rules that the website has.
>>16300430
What's the deal with Law of Excluded Middle? Why do people hate it so much? It seems fine to me.... At least when what you're trying to model is bivalent (such as math statements)

Anonymous at Mon, 29 Jul 2024 11:23:41 UTC No. 16301669

>>16300835
It allows for nonconstructive proofs, but that's not what that poster was commenting on.

Anonymous at Mon, 29 Jul 2024 12:00:53 UTC No. 16301700

>>16300835
Love that guy, he makes great videos. Clearly autismo, but to be fair if you're interested in formal logic then you most likely are too.

Anonymous at Mon, 29 Jul 2024 17:28:49 UTC No. 16302052

>>16301669
What was he commenting on then? Isn't that what TND means?

Anonymous at Mon, 29 Jul 2024 17:50:24 UTC No. 16302084

>>16299720
This proof seems false. It is not a given that an object exists. So those exists-introduction steps on line 5 and 13 are unsound.

Anonymous at Mon, 29 Jul 2024 18:12:34 UTC No. 16302124

>>16302084
>It is not a given that an object exists
What do you mean? It is always assumed that the domain of discourse is non empty, so an object does exist. Or do you mean the rule exist introduction is not valid?

Anonymous at Mon, 29 Jul 2024 18:20:20 UTC No. 16302132

So, what is the difference between
>[math]\exists x \text{ s.t. this statement } (Px \rightarrow \exists y Py) \text{ is true}[/math]
and
>[math]\exists x \text{ s.t. if } Px \text{ is true, then } \exists y Py[/math]
OP's is the former, but the latter is what low math people are used to. The former is an always true, whereas the latter is usually proved by showing that if Px is true, this leads to the remainder of the statement (or proven by the equivalent contrapositive).

>>16299720
>>16300835
I see, thanks for the video

Anonymous at Mon, 29 Jul 2024 18:21:25 UTC No. 16302134

>>16302132
also, how do you write the second statement in logic math then, if they are genuinely different?

Anonymous at Mon, 29 Jul 2024 18:22:52 UTC No. 16302138

>>16302132
ugh, sorry, change the "there exists y" into a "for all y"

Anonymous at Mon, 29 Jul 2024 18:52:06 UTC No. 16302187

>>16302124
>It is always assumed that the domain of discourse is non empty, so an object does exist.
Why would you assume this?

Anonymous at Mon, 29 Jul 2024 18:57:42 UTC No. 16302198

>>16302187
It's a historical thing. It's obviously not a good idea to assume that, but older versions of first-order logic typically did make that assumption. Hopefully the meme will die out as type theory becomes more popular.

Anonymous at Mon, 29 Jul 2024 19:14:27 UTC No. 16302243

>>16302132
They look like the same statement to me ngl

Anonymous at Mon, 29 Jul 2024 19:16:08 UTC No. 16302248

>>16302187
I don't really know why they do so, but it's just something I see textbooks assume. Plus what could you possibly want to model where the domain of discourse might be empty? Pretty much everything we want to talk about has a non empty domain of discourse.

Anonymous at Mon, 29 Jul 2024 19:17:16 UTC No. 16302250

>>16300835
>What's the deal with Law of Excluded Middle?
It allows for non-constructive existence claims.

Example: Choose a theory T, say T=ZFC. Further, let CT denote a proposition that's independent of T, i.e. one such that T can't prove or disprove it. E.g. for ZFC you may choose the contiunuum hypothesis, or for any theory stronger than arithmetic you may choose the arithmetized consistency claim of your theory.

Now consider the class
S := {n in {0,1} | CT or x=1}

Facts:
S is provenly a subset of the naturals N.
More specifically, members of S come from {0,1}. Yet more, we know that if m is a member of S, then provenly
(m is 0 and CT) or (m is 1).
Clearly 1 is a member of S, meaning S is provably inhabited.
If CT holds, then S={0,1}.
If CT does not hold, then S={1}.

Consider the contrapositive of the Induction principle in N, for any subset V of N. (More explicitly, we're interested in subsets defined negatively alla V:=N\U for some other subset U. Note that in this way, in total, we deal with double negation.)
Doing this, we find that V being non-empty is equivalent for it to be inconsistent that there does not exist a least member of V.
Adopting the law of excluded middle (resp double negation elimination), this is exactly the proof of the least number principle - the idea that each non-empty subset of N has a least member.

But let's go back to S:
Again:
ZFC proves all members of S are members from {0,1}.
Further:
ZFC can't prove 0 is the least member of S.
ZFC can't prove 1 is the least member of S.

But (using excluded middle LEM), ZFC prove "there exists" a least member of S.
So LEM just means your existence claims become elusive.
Not having LEM just rules this out. If your constructive theory proves a number "exists" that has property Q, then indeed you can find a _particular_ number number with that property.

Good constructive set theories not only have this for numbers (models), but all kinds of sets.

Anonymous at Mon, 29 Jul 2024 19:28:10 UTC No. 16302270

(That "mathematical statements are bivalent" is more a metaphysical wish or perspective. Ofc you can take the syntatic construct that is a theory for itself and not speak of models or the Platonic real. In the hard constructivist cast, we might interpret the symbols in terms of provability and computation. That said, there's dozens of constructive interpretations, all not simply bivalent/Platonic. And also many more possible axioms, some contradicting classical logic. Per default, it's however a strictly weaker system (meaning it proves "less" but has richer semantics). That said, all classical arithmetic statements up to double-negations in their formulations have constructive proofs. (Gödel-Gentzen translation), so for arithmetic nothing is lost by dropping LEM. Except proof shortcuts ofc.)