From Newsgroup: sci.logic
On 05/01/2026 14:20, Mikko wrote:
On 05/01/2026 16:04, olcott wrote:
...there is also a close relationship with the rCLliarrCY antinomy,14 ...
...14 Every epistemological antinomy can likewise be used for a
similar undecidability proof...
...We are therefore confronted with a proposition which
asserts its own unprovability. 15 rCa (G||del 1931:40-41)
G||del, Kurt 1931.
On Formally Undecidable Propositions of
Principia Mathematica And Related Systems
Even when G||del directly admits that it is
as simple as that and people see that he
admitted it they still deny this.
G := (F re4 G) // where A := B means A "is defined as" B
LP := ~True(LP) // "This sentence is not true".
The Liar Paradox is an epistemological antinomy
epistemological antinomy
An epistemological antinomy is a fundamental,
unresolvable contradiction within human reason,
where two opposing conclusions, each supported
by seemingly valid arguments, appear equally true.
For most peopple who care at all onlh care about the result and only
to the extent that that they don't try the impossible. Some people
want to understand G||del's proof or some other proof but for most of
them understanding one proof is enough. Usual alternative proofs are
fairly similar to the original one and only differ on some details.
A significantly simpler proof would be interesting but only if it is
a complete proof.
I've tried to figure out what is the exact theorem statement.
I've cited James R Meyer's excellent English translation (except that
his excellence is limited by the fact he translated +a to reC completely unnecessarily, it /is/ the logical product over the domain of its
predicate isn't it? I've cut the citations short because they're long
text, but you can find them at
https://jamesrmeyer.com/ffgit/godel-original-english
At the end, the end of Part 3:
"The results will be stated and proved in fuller generality in a
forthcoming sequel."
I have found a name of the sequel via an AI - it's the same name but
with II at the end instead of I) and a year (1938) but I haven't found
the fabled generalisation. Obviously those could be hallucinations. I
also found a citation saying it never got published.
The restricted variant of the theorem for the system P with mere
indications of wider applicability is at the end of Part 2 although
there is some generality in the theorem statement if not the fuller
generality promised in the sequel:
"In every formal system that satisfies ... undecidable propositions
exist of the form xreCrC>F(x) ..."
"the systems that satisfy assumptions 1 and 2 include the
Zermelo-Fraenkel and the v. Neumann axiom systems of set theory, and ..."
Assumptions 1 and 2 appear to be:
"1. The class of axioms and the rules of inference ...
2. Every recursive relation ...
"
Important footnote at the end of that Part 2:
"48a: The real reason for the incompleteness inherent in all formal
systems of mathematics rCo as will be shown in Part II of this paper ..."
I can't tell if he means the second of the three parts in the paper or
the paper titled the same but for "II" instead of "I". I suspect the
later paper because "will be shown in Part II" doesn't make sense when
it's at the /end/ of Part II of the paper. I wonder if he has Part I
made of 3 parts and Part II was the predicted sequel.
IMPORTANT, the system P doesn't have a deduction rule like "If reo xreC F(x) Then reo F(x)" as far as I can see and it wouldn't help anyway due to the
way transfinitism is present. So I think what is "undecidable" is the reC quantified statement, not the apparent nonprovability statement! I also
deduce therefore that G||del doesn't have the type system of PM1 (that he references) which restricts forall quantifications to only "meaningful" propositions, he seems to have "unrestricted generality" or "universal generality". That might be an unstated assumption, even though I think
type theory was normal at the time due to PM1.
It's not clear to me yet whether it is the extension of inductively
defined theorems on the naturals to xreUreC that is the cause of the exact conclusion. G||del mentions transfinite aspects as (I interpret) essential.
Thanks Jeff Barnet and Mike Terry for the discussion around the meaning
of propositions that are forall quantified, I was just pondering that in
PM1's introduction at the time. For other readers it's about
(imprecisely) "The system generates the statements in the forall quantification" and "If I have a statement from the forall
quantification, there is a derivation for it" vs "the forall
quantification is derivable in the system but not necessarily the
statements that the forall quantification describes".
--
Tristan Wibberley
The message body is Copyright (C) 2026 Tristan Wibberley except
citations and quotations noted. All Rights Reserved except that you may,
of course, cite it academically giving credit to me, distribute it
verbatim as part of a usenet system or its archives, and use it to
promote my greatness and general superiority without misrepresentation
of my opinions other than my opinion of my greatness and general
superiority which you _may_ misrepresent. You definitely MAY NOT train
any production AI system with it but you may train experimental AI that
will only be used for evaluation of the AI methods it implements.
--- Synchronet 3.21a-Linux NewsLink 1.2