So, for the claim that something exists, if you give an example for that, then such example is a "witness" for the claim. Is that enough as a definition? — alcontali
As a definition? It sure seems so. But definitions in themselves can satisfy themselves insofar as they can consistently reach. It appears you're looking to test the "granularity" of this one to see if it holds "all the way down." And again, as expressed, it seems it must. You need a counterexample, and in terms of the definition, it would have to be something that at the same time both does and does not exist - or so it seems. — tim wood
Good point. I observe that some qualifications are categorical, others of degree, and perhaps some even arbitrary. The juicy orange is witness to the "theorem" that some oranges are juicy. And this seems just a matter of aligning what can be said with what is said. I'll leave it here because I'm out of my depth, but it's an interesting topic.For S2="Oranges are juicy", — alcontali
Banach-Tarski paradox — fishfry
The explanations for the Banach-Tarski paradox in the following video are very intuitive: — alcontali
What's interesting about Banach-Tarski is that it's a purely syntactic paradox. The free group on two letters has a paradoxical decomposition, and this is purely a matter of meaningless syntax. One then lifts the paradox to Euclidean 3-space since the isometry group of 3-space (that is, the group of rigid transformations) contains a copy of the free group on two letters by virtue of the existence of a pair of independent, non-commuting rotations. — fishfry
In another example, there is the canonical witness for Gödel's first incompleteness theorem:
S = "S is not provable in T"
It is a witness for the theorem that says that there exist expressions in the language of first-order logic that are not provable from any possible choice of axioms (phrased in the same language).
S happens to be formally not provable from T. Well, that is what S says. So, in a sense, S is even logically true. — alcontali
because the universal quantifier in S that supposedly ranges over the godel numbers of every proof, isn't obtained by mathematical induction. Therefore it's interpretation as referring to every proof isn't justified. — sime
Sure it is: 1 is not a proof, 2 is not a proof,..., n+1 is not a proof,... The limitation is against going on into the transfinite. I'm not looking at the moment - subject to correction - but I think the relevant qualification is call ω-consistency (omega-consistency) — tim wood
should not be informally interpreted as saying "n is not a proof of S for n < ω".
.... and this should not feel in the least bit troubling or surprising , for there is no formal justification to support the heuristic and informal interpretation of universal-quantifiers as denoting each and every member of an infinite domain , unless that is to say, the universal quantifier in question was constructed using the axiom of induction. — sime
Still, this twist is obviously not needed in upstream pure mathematics. So, it is a matter of correctly switching between both context-dependent views on the concept of witness. — alcontali
I've found a machine-verifiable version of the Banach-Tarski proof for the Coq proof assistant. It looks endless. I first thought that this is because the Coq formalisms are excruciatingly lengthy, but the classical, annotated first-order-logic version is also 30 pages long. — alcontali
It uses pyramidal vocabulary. For example:
Theorem 22 (Tarski’s Theorem)Let G act on X, and let E ⊆ X. Then there exists a finitely additive, G-invariant measure on X defined for all subsets of X and normalizing E if and only i fE is not G-paradoxical.
So, it requires figuring out what "G-invariant measure" and " normalizing" means. Otherwise, Tarski's theorem 22 will remain inaccessible. — alcontali
It is interesting, though. If the proof were about formal language, I would probably keep drilling down in order to figure it out. — alcontali
Actually, Tarski does have theorems in the realm of formal languages, e.g. his undefinability theorem. I wonder how he ended up also working on abstract algebraic geometry and topology? — alcontali
Hilbert is also like that. He did his language-oriented Hilbert calculi but also his geometry-oriented Hilbert spaces. I wonder how people manage to not only handle both domains but even be original in both? — alcontali
There could actually even be a deeper link between geometry and formal language, because the late Voevodsky saw homeomorphisms everywhere in formal language domains, while those are clearly a geometry concept. I still don't understand Voevodsky's univalent foundations. Everybody seems to be raving and hyping that stuff, but I still cannot wrap my head around it. — alcontali
There is of course nothing more fashionable than being able to come up with a finer point in the Voevodsky stuff. I cannot "show off" because I unfortunately don't get it! ;-) — alcontali
You uptake new information rapidly but have a hard time staying focussed. Is that a good guess? — fishfry
Coq and machine-assisted proofs in general are an interesting subject, but let's hopefully not get sidetracked into that. To that end, you should definitely read the Mephist I linked earlier. He knows a lot more about Coq and constructive math than I do if he's around. — fishfry
If you are interested, the key buzzphrase is: "The free group on two letters has a paradoxical decomposition." That phrase leads to a web of interrelated Wiki pages that are very good. You'll halfway understand B-T from those. The heart of the proof is about formal language. It's about all the finite strings you can make using two symbols and their inverses. It is the most syntactic thing you ever saw. It's a very natural construction that contains a surprising paradox. — fishfry
These days logic is geometry. It's all come out via the mysterious categorical point of view. Buzzword: "topos theory." — fishfry
Ok, I'm reading up on "free group on two letters — alcontali
So, yes, serious levels of perseverance are for me often about not losing face and not letting key people down. — alcontali
↪simeI have to refer you to the proof itself. It relies on recursion and ω-consistency. I quote this: "Every ω-consistent system is obviously also consistent. However, as will be shown later, the converse does not hold." (The Undecidable, Ed. Martin Davis, 1965, p. 24).
PA may be inconsistent, but I take Godel's qualifications on his system P, of which he says, "P is essentially the system which one obtains by building the logic of PM around Peano's axioms.." (10), & ff., as sufficient to regard his claims as rigorous. As he observes later (p. 36), "In particular, the consistency of P is unprovable in P, assuming P is consistent (in the contrary case, of course, every statement is provable).
should not be informally interpreted as saying "n is not a proof of S for n < ω".
.... and this should not feel in the least bit troubling or surprising , for there is no formal justification to support the heuristic and informal interpretation of universal-quantifiers as denoting each and every member of an infinite domain , unless that is to say, the universal quantifier in question was constructed using the axiom of induction.
— sime
Agreed. Informal remarks about his proof are often not quite right. But I think it's pretty clear that the axiom of induction or something like is a main piece of his proof. — tim wood
The universal quantifier in "Godel's sentence" G which supposedly says "For all Godel numbers p, p does not encode a proof of Godel sentence G", isn't an abbreviation of an independent proof of G's non-provability. Therefore this quantifier should not be given this common (mis)interpretation. — sime
The reason this matters, is because in logic the use of an existential quantifier should not be informally interpreted as bearing witness to a fact, unless the quantifier is used to abbreviate an independent proof of the fact concerned that does not beg the use of this quantifier in a circular fashion.
For otherwise we might just as well say that "a universal quantifier has proved a universal truth, because the universal quantifier says so". — sime
Not quite. Not "For all Godel numbers p," but instead, for all x, x being any natural number. Some xs will be ps, most not. Them that aren't won't be (encode) a proof, and them that are also won't be a proof. — tim wood
And the universal quantifier is both part of the proof, and proved separately within the proof. — tim wood
I read this as your taking exception to the use of existential (i.e., existential and universal) quantifiers unless it/they "abbreviate an independent proof of the fact concerned...". So, if I say x>3 is true for all x greater than three, this is neither true nor valid, subject to a proof of the "for all"? — tim wood
Sure you do. That's in part what the proof is all about. In technical mathematical language, it's, "You can get theah, from heah." You just have to exercise some care in your heahs and theahs, which is done via recursion and ω-consistency. But you qualify this:Furthermore, for any provability predicate Prov('X','S') interpreted as saying 'X' encodes a proof of 'S', it isn't actually knowable which numbers represent legitimate proofs,... — sime
That for a certain broad class of systems with certain qualities the consistency of same cannot be proved within the system is demonstrated as a consequence of Godel's theorem's. But you do not appear to be acknowledging that the proofs in question are meta-mathematical....due the possibility that Peano-arthmetic is inconsistent and proves absurdity, together with Godel's second incompleteness theorem which forbids the possibility of PA representing it's own consistency. — sime
No it isn't. I'm thinking you've read the proof and worked through it at least some - but maybe not. The universal quantifiers are then qualified via recursion schema. And significantly, while your Prov("X," "S") is recursive, according to Godel, Godel also says the related Provable ("S"); that is, "S is a provable theorem," is not recursive. The trick of the thing, imo and apart from details, is in its back-and-forth movement between mathematical-logical argument and meta-mathematical-logical argument.Incompleteness is the result of unlimited universal quantification in Peano's axiom of induction, — sime
Consider universal quantification over the negative-provability predicate in PA, that is informally interpreted as saying " For every 'S', 'S' doesn't prove 'G' ".
We know for a fact that this has no syntactical expression in PA, since if PA is consistent then the statement isn't decidable (via the Diagonalization lemma) and if PA is inconsistent then PA is unsound and has no interpretation whatsoever. — sime
My political agenda here is actually concerned with how to interpret PA without assuming consistency, in light of Godel's results. — sime
I'm thinking you've read the proof and worked through it at least some - but maybe not. The universal quantifiers are then qualified via recursion schema. And significantly, while your Prov("X," "S") is recursive, according to Godel, Godel also says the related Provable ("S"); that is, "S is a provable theorem," is not recursive. — tim wood
Are you quite sure? Asking, not a challenge. It seems to me that within your first two sentences alone:As you undoubtedly noticed, Alan Turing's version does not make use of any particular witness theorem. — alcontali
, that you have got to use some sort of quantification.Assume that we have a sound (and hence consistent) and complete axiomatization of all true first-order logic statements about natural numbers. Then we can build an algorithm that enumerates all these statements. — alcontali
that you have got to use some sort of quantification. — tim wood
That for a certain broad class of systems with certain qualities the consistency of same cannot be proved within the system is demonstrated as a consequence of Godel's theorem's. But you do not appear to be acknowledging that the proofs in question are meta-mathematical. — tim wood
No it isn't. I'm thinking you've read the proof and worked through it at least some - but maybe not. The universal quantifiers are then qualified via recursion schema. . — tim wood
And significantly, while your Prov("X," "S") is recursive, according to Godel, Godel also says the related Provable ("S"); that is, "S is a provable theorem," is not recursive. — tim wood
So it appears to me, so far, that you're the guy that says "prove it" to the respective proofs until they're driven into their own grounding in axioms and sense, at which level the call for proof is an error. Are you that guy?
That is, I do not take you to be challenging or disqualifying Godel, but rather making some assumptions both counter-to and beyond it, for other purposes. As you say above, — tim wood
Get involved in philosophical discussions about knowledge, truth, language, consciousness, science, politics, religion, logic and mathematics, art, history, and lots more. No ads, no clutter, and very little agreement — just fascinating conversations.