assuming you believe in the non-emptiness of the domain of first-order quantification! Which I surmise in this case you do, and `someone()` obtains a witness for that?
If either everyone drinks or someone doesn't, then there is a person such that, if they drink, then everyone drinks.pic.twitter.com/rlH7qswPA9
-
-
-
Yeah, my editor currently lets you dream up arbitrary function symbols to use as you like. I'm planning to close that loophole soon.
- Još 4 druga odgovora
Novi razgovor -
-
-
Is this editor available outside of Glasgow institutions (and Edinburgh apartments)?
- Još 3 druga odgovora
Novi razgovor -
-
-
Raymond Smullyan came up with this, right?
-
I think I first saw it in the old Coq tutorial https://coq.inria.fr/tutorial/1-basic-predicate-calculus … (Section 1.4.3 "Paradoxes of classical predicate calculus"), which credits it to Smullyan.
Kraj razgovora
Novi razgovor -
-
-
I may be missing something obvious, but isn't this just wrong? (What if two people don't drink?) Are you showing a tricky example for proof systems? Is d (as a set of elements x that make d(x) true) treated as empty until you assume entry?
-
I'm pretty sure it isn't wrong (as in, it is a valid proof in a widely accepted variant of FOL). It is usually presented in classical logic, without the '(all x. d(x)) \/ (ex x. ~d(x))' assumption. I originally got it from the old Coq tutorial: https://coq.inria.fr/tutorial/1-basic-predicate-calculus … (Sec 1.4.3)
- Još 2 druga odgovora
Novi razgovor -
-
-
I'm reminded of a friend's proof of the Pigeonhole Principle in which the existential witnesses were called Sid and Gladys.
Hvala. Twitter će to iskoristiti za poboljšanje vaše vremenske crte. PoništiPoništi
-
Čini se da učitavanje traje već neko vrijeme.
Twitter je možda preopterećen ili ima kratkotrajnih poteškoća u radu. Pokušajte ponovno ili potražite dodatne informacije u odjeljku Status Twittera.