The first time I saw it was in Stan Wagon's book, The Banach-Tarski paradox. I found it confusing and had to devote brain cycles to figuring out what it meant, let alone what the mathematical argument was. I don't like it, it's pretentious and confusing. You could say "2 witnesses the falsity of the claim that all primes are odd"; but why make a statement harder to read? It's a pretty common locution but I'm not a fan.

I will say that it's a stretch to go from the colloquial meaning of witness to Boolean satisfiability. I don't think there's necessarily a functor from, "While Googling X I ran across Y" to "X and Y are deeply related." If anything, it's the opposite. Google knowledge is all surface, no depth. It gives the illusion of understanding.

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.

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

Agreed. The issue may actually be elsewhere, though. A witness is sometimes a proof and sometimes it isn't. For example, For S1="Oranges exist", showing an orange is a witness that proves S1. For S2="Oranges are juicy", showing an orange that happens to be juicy is not a witness that proves S2. I wanted to confirm my understanding of "witness as proof" by looking at more examples of witnesses.

For S2="Oranges are juicy", — alcontali

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.

Banach-Tarski paradox — fishfry

The explanations for the Banach-Tarski paradox in the following video are very intuitive:



It really helps understanding the set-theoretical symbol manipulations in the proof. Of course, the section in Wikipedia is called "sketch of the proof" instead of "proof". It is some kind of disclaimer with which they very often label a proof. Maybe they use the disclaimer because the proof is not expressed in strictly and rigorous first-order logic language only? Not sure ...

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.

In any event, the subject was the use of the word witness, and my reference to that book was incidental.

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

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.

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. It is interesting, though. If the proof were about formal language, I would probably keep drilling down in order to figure it out.

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? 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?

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.

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! ;-)

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

Certainly, if S is such that S implies ~S, then an axiomatic derivation of S entails inconsistency. And Godel exhibited an arithmetical proposition of this form. But here, S should not be formally interpreted as a referring to its lack of provability. For this heuristic interpretation of S is terribly misleading, 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.

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). Godel wrote elsewhere The Length of Proofs, just two pages: this from that: "The transition to the logic of the next higher type not only results in certain previously unprovable propositions becoming provable, but also in it becoming possible to shorten extraordinarily infinitely many of the proofs already available."

By this he means that if P is not provable in logical system S(i), then it may well be in S(i+1), and, if the proof of P in S(i) is infinitely long, then in S(i+1) it may just be tractable.

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

It is precisely because Peano arithmetic might be ω-inconsistent that Godel's constructed sentence 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.

I 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.

I have found another example, and actually a quite interesting one, from the cryptography subdomain at stack exchange:

What is a “witness” in zero knowledge proof? A witness for an NP statement is a piece of information that allows you to efficiently verify that the statement is true. For example, if the statement is that there exists a Hamiltonian cycle in some graph, a witness would be such cycle. Given a cycle, one can efficiently check whether it is a valid Hamiltonian cycle, but finding such cycle is difficult. Knowledge extractors are used in the definition of proofs of knowledge. There, you don't just prove that some statement is true, but that you know a witness for this statement.

In upstream pure mathematics, computation in its entirely abstract, Platonic worlds is deemed effortless. Downstream cryptography cannot assume that, and must also take into account issues of computation effort. Hence, the requirement that the witness must be efficiently verifiable. 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.

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

That's why they call it pure and applied math! And likewise the theory of computation. I hope you will agree that although Turing machines have an unbounded tape, no physical computer does. So I think you are making a rather commonplace observation. And also of course drawing the distinction between computability theory, the study of what is computable by a machine; and complexity theory, the study of how efficiently things may be computed. Again, true but not entirely earth-shaking. Yes?

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

You hit a lot of really cool topics. I'll keep my answers brief. I hope we can focus on one or two things instead of branching out into too many diverse topics. You uptake new information rapidly but have a hard time staying focussed. Is that a good guess?

* Now re Banach-Tarski. First, a machine-formalizable proof would not be remotely understandable to a person who didn't already understand the standard proof. So that's not the way to go. 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.

Secondly, it turns out that the proof of Banach-Tarski is very straightforward. The outline on Wiki is very good. And as I said, it is at heart a syntactic matter that could be programmed into a computer. Not the entire proof, but the core idea. 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.

But you know -- the fact is that Banach-Tarski is at heart a logical paradox. You lay out some very sensible axioms, and they lead to a non-sensible yet logically correct conclusion. Tarski and von Neumann and others were all interested in applying group theory to geometry. So this is a paradox in "geometric group theory." That's yet another buzzwordy way to say it. But Tarski was in the middle of all that.

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

No no no!! It's not NEARLY so bad. I could fully explain the proof of the Banach-Tarski theorem to you in a perfectly understandable way. Just not here, because it's a little lengthy. There are several moving parts. But each part of the proof is quite straightforward.

You don't have to make your life difficult by wondering what those buzzwords mean. You could ask me, for example. But not in this thread. If someone starts a B-T thread that would be more appropriate. But the buzzwords are easy once they're explained.

The think about the Tarski theorem you quoted is that professional mathematicians can always summarize the proof in a sentence or two of jargon. The idea isn't to understand the jargon from the top down. You can understand the proof from the basic ideas on up. It's long but each part is surprisingly straightforward.

I can tell you want the buzzwords mean, but they won't shed light on the paradox until AFTER you understand the paradox. Tarski's using professional jargon.

It is interesting, though. If the proof were about formal language, I would probably keep drilling down in order to figure it out. — alcontali

I could lay that out for you in a page of exposition. Start a new thread, I feel bad enough about hijacking this one. 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. We then apply the paradox to Euclidean three-space.

But nevermind, this is not a forum for lengthy mathematical exposition. You can just google "Free group on 2 letters paradoxical" and there are a bunch of interrelated Wiki pages. That's probably better than my posting an exposition here.

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

These days logic is geometry. It's all come out via the mysterious categorical point of view. Buzzword: "topos theory."

But a lot of these old guys did a lot of different things.

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

Hilbert did much more than that. He's regarded as the number one mathematician of the first half of the 20th century. (Grothendieck wins the second half). He almost beat Einstein to general relativity. He's famous for a lot of deep work in a lot of areas. Very interesting guy, I'm sure you've seen the famous picture of him in his hat.

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

That's something else I could put in context for you in fifteen minutes, but not this fifteen minutes. Make a thread so we don't go in all directions here.

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

I hope you will allow me to a suggestion. It's not about showing off. It's about learning. You happen to be interested in a lot of things I know a little about (and some I know a lot about). I'm happy to yack about them. I'm pretty ignorant about most other things. Ask anyone.

There's a Zen saying. Beginner's mind.

You uptake new information rapidly but have a hard time staying focussed. Is that a good guess? — fishfry

It's complicated. If there is nobody is waiting for me to finish some work, I know from experience that I will abandon ship within one month, because I will get distracted by some other shiny toy that I will have run into.

My longest time on a project has been 2.5 years up till now. Still, it was very interactive, with lots of feedback, and with people who were waiting for the job to be done, and in a situation where I would have felt embarrassed to flake out on my commitment to get something going.

So, yes, serious levels of perseverance are for me often about not losing face and not letting key people down.

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

I have always had it somewhere in the back of my head that I would want to figure out and elaborate on Coq and/or Isabelle. Still, if there is nobody else who really needs my Coq scripts, I will probably fail to keep pursuing it.

Run-off-the-mill software scripting projects automatically include that kind of incentives, because there is someone paying for the result that he is waiting to see. Or at least there is an open-source team waiting for the job to be done. Otherwise, I will indeed just be flaneuring from one topic to the other. There needs to be a deliverable to be shipped to someone, for me to decisively lock in on a target. This is just a hobby, really.

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

That sounds interesting! Looking into it.

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" and ""topos theory". Hopefully the vocabulary pyramid will not insurmountable!

Ok, I'm reading up on "free group on two letters — alcontali

That's the heart of Banach-Tarski and it's purely syntactic, nothing to do with spheres. It's amazing. I hope you will look into this. I have a little writeup but I'm not sure this is the place for it. Depends on your level of interest. I notice that you're the thread starter here so perhaps it would be ok.

So, yes, serious levels of perseverance are for me often about not losing face and not letting key people down. — alcontali

Well see, that's a point I'm trying to make. It's not about face, it's just about learning what someone else happens to know. Your curiosity is wide so you shouldn't expect to master all this stuff in a few minutes of Wiki-ing. Especially topos theory and categorical logic. Grad students struggle with that stuff.

But Banach-Tarski, that's actually very approachable. The proof is long but the parts are simple. And the free group on two letters, the Wiki pages are good and it's a true veridical paradox, incredibly counterintuitive but requiring no questionable principles, not even the axiom of choice. No set-theoretic principles deeper than the union of five sets are used; and all the objects considered are finite strings and sets of finite strings.

I don't know what's the value of Coq or other proof assistants for someone who's trying to learn modern math. Better perhaps to just learn the math IMO.

↪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

Peano's axiom of induction isn't an axiom of logic, and plays no part in standard proofs of Godel's incompleteness theorem. It can however be shown to be responsible for causing incompleteness, in the presence of the other axioms of peano arithmetic.

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".

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.

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

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.

And the universal quantifier is both part of the proof, and proved separately within the proof.

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

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"? What does it even mean to "prove" "for all"? It amounts to saying that 2+2=4 is meaningless absent a proof of "+" and "=".

And there may be cases that rigor require reference to the legitimacy and meaning of "+" and "=", as well as "for all" and "there exists," - but I should think only in cases where the question either arises or might arise as to whether these terms and others like them are being used in a way that requires clarification as to any peculiar usage of them.

It seems to me a quantifier says what it says: it qualifies. The fact or act of qualification itself is not susceptible of proof, it just is. What follows, then, either accords or does not accord with the qualification.

Godel is saying, in effect, that no recursive process (i.e., "for all") over the natural numbers will yield a natural number that encodes his particular expression. The "for all" in this case only means that there is a recursive process for generating the natural numbers - which is not in question.

In short, I think you're not making sense. But I shall trust you to be clear in reply as to exactly what you mean, for my correction.

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

Sorry, that was actually a typo. Nevertheless this exchange perhaps serves as a useful reminder that any number represents a legitimate theorem relative to the provability-predicate of some Godel-numbering system.

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, 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. Neither humans nor God can ever claim knowledge of PA's consistency, for all we can have are proofs of consistency relative to the consistency of other systems, which begs the question.

Of course, it is standard practice to explicitly state consistency as an assumption when we informally interpret PA and discussing incompleteness, so your remark is valid, after a bit of clarification. My political agenda here is actually concerned with how to interpret PA without assuming consistency, in light of Godel's results. For there are arguably many conceptual benefits to be had by dropping the consistency assumption, that demonstrate the fundamentally empirically contigent, vague and indeterminate nature of logic and mathematics that is better understood as being a posteriori in nature.

Incompleteness is the result of unlimited universal quantification in Peano's axiom of induction, that takes us from the non-controversial constructive semantics of quantifier-free Primitive Recursive Arithmetic that represents the predictably terminating algorithms, to the controversial non-constructive interpretations of PA that represents every possible algorithm. Logic should therefore replace the simplistic sign of universal quantification for a richer collection of signs that distinguishes the different use-cases of the original sign, whilst also making explicit the relation of the Axiom of choice to universal quantification. David Hilbert in fact did use a system closer to this, called the epsilon-calculus during his attempts to prove consistency, and it is in fact making a come back.

And the universal quantifier is both part of the proof, and proved separately within the proof. — tim wood

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. We also know that for any particular 'S' and 'G', PA can decide whether or not 'S' derives 'G'.

Therefore the universal quantifier above cannot have the ordinary meaning of every, which ought to have been the central conclusion of Godel's incompleteness theorem. In stark contrast to the commonly accepted idea that Godels' sentence is self-referential with definite meaning.

So we have two choices. Either we stick to our a priori philosophical concepts and abandon mathematical logic and it's physical embodiment as being an unsuitable language for expressing and justifying philosophical truth. Or we revise our philosophical intuitions to match what PA and its physical embodiment can and cannot express. I'm saying the latter.

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

This is acceptable, because the contradiction it expresses can be represented without universal quantifiers. It is analogous to having a function that by design terminates, and that converts an arbitrary number into a number or another arbitrary number. the conflation of all with arbitrary is perhaps the central source of controversy and misunderstanding in logic.

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

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:

...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

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.

It's as if you cannot prove you're you, so we ask your mum. Your mum says, "Yep, that's him" And done, proved. Is your mum respectable? That much is accepted as granted.

Or it may be that you're not really reconciled either to the notion that systems are built on axioms, or axioms themselves, granted but themselves unprovable except by some meta- argument. [iEverything[/i] can be shoveled down this rabbit-hole; its just not useful to do so. Your mum gets a pass - I'm sure she has no need of one.

Incompleteness is the result of unlimited universal quantification in Peano's axiom of induction, — 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.

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

Sure it does! Godel gives it us, carefully built. The argument, in meta-mathematical terms, is, "'G' is this weird sentence: if provable, then PA is inconsistent (and every sentence becomes provable), and if not provable, then PA in incomplete, meaning that there are sentences G, G', G'', G'''..., in PA that are not provable, (but true, because they assert their own unprovability).

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,

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

That is indeed Gödel's original proof, which certainly has its merits, but in the meanwhile various alternatives have emerged, some of which can possibly be considered more straightforward. I specifically like Alan Turing's alternative based on the Halting problem:

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. This means that there is an algorithm N(n) that, given a natural number n, computes a true first-order logic statement about natural numbers, and that for all true statements, there is at least one n such that N(n) yields that statement. Now suppose we want to decide if the algorithm with representation a halts on input i. We know that this statement can be expressed with a first-order logic statement, say H(a, i). Since the axiomatization is complete it follows that either there is an n such that N(n) = H(a, i) or there is an n' such that N(n') = ¬ H(a, i). So if we iterate over all n until we either find H(a, i) or its negation, we will always halt, and furthermore, the answer it gives us will be true (by soundness). This means that this gives us an algorithm to decide the halting problem. Since we know that there cannot be such an algorithm, it follows that the assumption that there is a consistent and complete axiomatization of all true first-order logic statements about natural numbers must be false.

As you undoubtedly noticed, Alan Turing's version does not make use of any particular witness theorem. To some extent, that is a good thing because it spares us from overly focusing on that one witness in Gödel's original proof.

As you undoubtedly noticed, Alan Turing's version does not make use of any particular witness theorem. — alcontali

Are you quite sure? Asking, not a challenge. It seems to me that within your first two sentences alone:

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.

As to recursion, I'm thinking that the essence of recursion is that the task can be done "blind"; that is, without reference to some or all, but rather only to the question as to whether the task is done. And recursion is what (I'm claiming here) makes Godel's theorem work.

But there is a postulatory argument in hypothetical form that applies here. if you wish to argue coherently about all or some, you have to have some way to refer to them. If you cannot do that, then you cannot argue coherently about all or some (maybe via recursion?). But we like to be able to argue about some or all. Therefore (modus tollens) we must (had better) be able to refer to them.

None of this gainsays your ambition to see what order may be discerned in the chaos resulting from the suspension of ordinary qualification or other axioms, but to my way of thinking, that thinking is forever coralled and can never escape to disinform such propositions as "for all," or "there exists," or even 2+2=4.

that you have got to use some sort of quantification. — tim wood

Yes, Alan Turing's version uses quantification, but not a witness such as S = "S is not provable" as in Gödel's original proof.

I also believe that the problem is somehow fundamentally caused by extending propositional logic into first-order logic by adding universal quantifiers, but there is not necessarily a direct relationship in Alan Turing's proof, which merely states that it would ex absurdo solve the Halting Problem. The Halting Problem itself also uses universal quantification. So, some kind of relationship could already occur there.

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

Well any demonstration of axiomatic incompleteness is a purely syntactical demonstration, in spite of any semantic or meta-logical pretenses to the contrary. It purely consists in the exhibition of a well-formed formula f and it's negation ~f , in a circumstance where neither is currently known to be syntactically inconsistent in relation to a given set of axioms.

The fact that it is possible to prove the relative consistency of PA in relation to the relative consistency of another system, is again, an equally syntactical derivation, whilst the syntactical notion of absolute inconsistency is also potentially observable by deriving f & ~f. But i don't understand the notion called absolute consistency. For that seems akin to the idea of 'completed infinity'; both of these notions are impossible to determine, or even to define in a non-circular fashion, and only serve to disguise the under-determined semantics of logic that is actually decided a posteriori when a sentence is actually derived, proved, or else used in a fashion unrelated to logic.

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

I was referring to the cause of incompleteness, which is due to unbounded universal quantification in cases where universal quantifiers cannot be eliminated. Although here I made a mistake, in that the origin of incompleteness in weaker systems than Peano Arithmetic lies with the universal quantifiers in the other arithmetic axioms, as opposed to the axiom of induction - as evidenced by the incompleteness of Robinson arithmetic that does not possess the induction axiom. None of this changes anything of significance tho..

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

And hence the reason why the universal quantifier over ~Prov('S','G') to form ~prov('G') should not be interpreted as literally "passing over"every number, which was my original point. For Prov('G') might still be derivable, even though Prov('S','G') isn't actually derivable for any 'S', if PA turns out to be omega inconsistent. Likewise, ~Prov('G') cannot express the fact that Prov('S','G') is not derivable for some 'S', for then the diagonalisation lemma yields the contradiction t => ~Prov(''t') for some t.

The sentence t => ~Prov("t") has an infinitely expandable fractal-like structure due to the sentence being fed it's own godel number, and there is no known reduction of it's quantifiers to those of the axioms. Therefore, whether or not PA is consistent, we don't have a semantically interpretable sentence. All we have is a syntactically verifiable self-negating sentence that has no meaningful interpretation.

The ultimate mistake is this: In logic, the absence of a witness should not be equivocated with the witnessing of an absence. Only by making this conflation, as is done in classical logic, can Godel's sentence assume its controversial and illogical interpretation as proving it's non-provability.

It is disingenuous sophistry of textbooks to suggest that t => ~Prov("t") has the high-level interpretation "t implies that t doesn't have a proof", even with the consistency disclaimers. Worse, it disguises the synthetic a posteriori nature of reasoning.

An existential quantifier cannot make a non-trivial existential claim. Either the quantifier concerned is analytically reducible to an instance of the axioms, else the quantifier is logically meaningless and should not even be informally interpreted.

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

On the contrary, I'm about eliminating unprovable assumptions from popular understandings of logic.

S = "S is not provable in T"
A proof of S in T requires a sequence of inference steps in T
that prove that they themselves do not exist.

Copyright 2023 PL Olcott

Curious. I never came across "witness" in math before this thread. Mostly Foundations I suppose. But, loosely, it seems to be a sort of example. Normally, when a mathematician proves a conjecture they might demonstrate by citing an example to make it more "real". "Under certain circumstances there exist certain things of which the following is an example", etc.