On 06/01/2026 02:24, Oleksiy Gapotchenko wrote:
Just an external observation:
A lot of tech innovations in software optimization area get discarded
from the very beginning because people who work on them perceive the
halting problem as a dogma.
It is a dogma in the same sense as 2 * 3 = 6 is a dogma: a provably
true sentence of a certain theory.
On 1/6/2026 7:23 AM, Mikko wrote:
On 06/01/2026 02:24, Oleksiy Gapotchenko wrote:
Just an external observation:
A lot of tech innovations in software optimization area get discarded
from the very beginning because people who work on them perceive the
halting problem as a dogma.
It is a dogma in the same sense as 2 * 3 = 6 is a dogma: a provably
true sentence of a certain theory.
...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
F reo G_F rao -4Prov_F (riLG_FriY)
"F proves that: G_F is equivalent to
G||del_Number(G_F) is not provable in F" https://plato.stanford.edu/entries/goedel-incompleteness/#FirIncTheCom
Stripping away the inessential baggage using a formal
language with its own self-reference operator and
provability operator (thus outside of arithmetic)
G := (F re4 G)-a-a // G asserts its own unprovability in F
A proof of G in F would be a sequence of inference
steps in F that prove that they themselves do not exist.
On 06/01/2026 16:02, olcott wrote:
On 1/6/2026 7:23 AM, Mikko wrote:
On 06/01/2026 02:24, Oleksiy Gapotchenko wrote:
Just an external observation:
A lot of tech innovations in software optimization area get
discarded from the very beginning because people who work on them
perceive the halting problem as a dogma.
It is a dogma in the same sense as 2 * 3 = 6 is a dogma: a provably
true sentence of a certain theory.
...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
F reo G_F rao -4Prov_F (riLG_FriY)
"F proves that: G_F is equivalent to
G||del_Number(G_F) is not provable in F"
https://plato.stanford.edu/entries/goedel-incompleteness/#FirIncTheCom
Stripping away the inessential baggage using a formal
language with its own self-reference operator and
provability operator (thus outside of arithmetic)
G := (F re4 G)-a-a // G asserts its own unprovability in F
A proof of G in F would be a sequence of inference
steps in F that prove that they themselves do not exist.
From the way G is constructed it can be meta-proven that either
G is true and unprovable in F (which means that F is incomplete)
or G is false and provable in F (which means that F is inconsistent).
On 1/7/2026 6:10 AM, Mikko wrote:
On 06/01/2026 16:02, olcott wrote:
On 1/6/2026 7:23 AM, Mikko wrote:
On 06/01/2026 02:24, Oleksiy Gapotchenko wrote:
Just an external observation:
A lot of tech innovations in software optimization area get
discarded from the very beginning because people who work on them
perceive the halting problem as a dogma.
It is a dogma in the same sense as 2 * 3 = 6 is a dogma: a provably
true sentence of a certain theory.
...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
F reo G_F rao -4Prov_F (riLG_FriY)
"F proves that: G_F is equivalent to
G||del_Number(G_F) is not provable in F"
https://plato.stanford.edu/entries/goedel-incompleteness/#FirIncTheCom
Stripping away the inessential baggage using a formal
language with its own self-reference operator and
provability operator (thus outside of arithmetic)
G := (F re4 G)-a-a // G asserts its own unprovability in F
A proof of G in F would be a sequence of inference
steps in F that prove that they themselves do not exist.
-aFrom the way G is constructed it can be meta-proven that either
Did you hear me stutter ?
A proof of G in F would be a sequence of inference
steps in F that prove that they themselves do not exist.
On 07/01/2026 15:06, olcott wrote:
On 1/7/2026 6:10 AM, Mikko wrote:
On 06/01/2026 16:02, olcott wrote:
On 1/6/2026 7:23 AM, Mikko wrote:
On 06/01/2026 02:24, Oleksiy Gapotchenko wrote:
Just an external observation:
A lot of tech innovations in software optimization area get
discarded from the very beginning because people who work on them >>>>>> perceive the halting problem as a dogma.
It is a dogma in the same sense as 2 * 3 = 6 is a dogma: a provably
true sentence of a certain theory.
...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
F reo G_F rao -4Prov_F (riLG_FriY)
"F proves that: G_F is equivalent to
G||del_Number(G_F) is not provable in F"
https://plato.stanford.edu/entries/goedel-incompleteness/#FirIncTheCom >>>>
Stripping away the inessential baggage using a formal
language with its own self-reference operator and
provability operator (thus outside of arithmetic)
G := (F re4 G)-a-a // G asserts its own unprovability in F
A proof of G in F would be a sequence of inference
steps in F that prove that they themselves do not exist.
-aFrom the way G is constructed it can be meta-proven that either
Did you hear me stutter ?
A proof of G in F would be a sequence of inference
steps in F that prove that they themselves do not exist.
An F where such sequence really exists then in that F both G and
the negation of G are provable.
In an F where such sequn|-nce does not exist G is unprovable by
definition. However it is meta-provable frome the way it is
constructed and therefore true in every interpretation where
the natural numbers contained in F have their standard properties.
On 1/8/2026 4:21 AM, Mikko wrote:
On 07/01/2026 15:06, olcott wrote:G := (F re4 G)-a-a // G asserts its own unprovability in F
On 1/7/2026 6:10 AM, Mikko wrote:
On 06/01/2026 16:02, olcott wrote:
On 1/6/2026 7:23 AM, Mikko wrote:
On 06/01/2026 02:24, Oleksiy Gapotchenko wrote:
Just an external observation:
A lot of tech innovations in software optimization area get
discarded from the very beginning because people who work on them >>>>>>> perceive the halting problem as a dogma.
It is a dogma in the same sense as 2 * 3 = 6 is a dogma: a provably >>>>>> true sentence of a certain theory.
...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
F reo G_F rao -4Prov_F (riLG_FriY)
"F proves that: G_F is equivalent to
G||del_Number(G_F) is not provable in F"
https://plato.stanford.edu/entries/goedel-incompleteness/#FirIncTheCom >>>>>
Stripping away the inessential baggage using a formal
language with its own self-reference operator and
provability operator (thus outside of arithmetic)
G := (F re4 G)-a-a // G asserts its own unprovability in F
A proof of G in F would be a sequence of inference
steps in F that prove that they themselves do not exist.
-aFrom the way G is constructed it can be meta-proven that either
Did you hear me stutter ?
A proof of G in F would be a sequence of inference
steps in F that prove that they themselves do not exist.
An F where such sequence really exists then in that F both G and
the negation of G are provable.
A proof of G in F would be a sequence of inference
steps in F that prove that they themselves do not exist.
Does not exist because is contradicts itself.
On 08/01/2026 16:18, olcott wrote:
On 1/8/2026 4:21 AM, Mikko wrote:
On 07/01/2026 15:06, olcott wrote:G := (F re4 G)-a-a // G asserts its own unprovability in F
On 1/7/2026 6:10 AM, Mikko wrote:
On 06/01/2026 16:02, olcott wrote:
On 1/6/2026 7:23 AM, Mikko wrote:
On 06/01/2026 02:24, Oleksiy Gapotchenko wrote:
Just an external observation:
A lot of tech innovations in software optimization area get
discarded from the very beginning because people who work on
them perceive the halting problem as a dogma.
It is a dogma in the same sense as 2 * 3 = 6 is a dogma: a provably >>>>>>> true sentence of a certain theory.
...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
F reo G_F rao -4Prov_F (riLG_FriY)
"F proves that: G_F is equivalent to
G||del_Number(G_F) is not provable in F"
https://plato.stanford.edu/entries/goedel-incompleteness/
#FirIncTheCom
Stripping away the inessential baggage using a formal
language with its own self-reference operator and
provability operator (thus outside of arithmetic)
G := (F re4 G)-a-a // G asserts its own unprovability in F
A proof of G in F would be a sequence of inference
steps in F that prove that they themselves do not exist.
-aFrom the way G is constructed it can be meta-proven that either
Did you hear me stutter ?
A proof of G in F would be a sequence of inference
steps in F that prove that they themselves do not exist.
An F where such sequence really exists then in that F both G and
the negation of G are provable.
A proof of G in F would be a sequence of inference
steps in F that prove that they themselves do not exist.
Does not exist because is contradicts itself.
That conclusion needs the additional assumption that F is consistent,
which requires that the first order Peano arithmetic is consistent.
If F is not consistent then both G and its negation are provable in F.
The first order Peano arithmetic is believed to be sonsistent but its consistency is not proven.
On 1/10/2026 3:25 AM, Mikko wrote:
On 08/01/2026 16:18, olcott wrote:
On 1/8/2026 4:21 AM, Mikko wrote:
On 07/01/2026 15:06, olcott wrote:G := (F re4 G)-a-a // G asserts its own unprovability in F
On 1/7/2026 6:10 AM, Mikko wrote:
On 06/01/2026 16:02, olcott wrote:
On 1/6/2026 7:23 AM, Mikko wrote:
On 06/01/2026 02:24, Oleksiy Gapotchenko wrote:
Just an external observation:
A lot of tech innovations in software optimization area get >>>>>>>>> discarded from the very beginning because people who work on >>>>>>>>> them perceive the halting problem as a dogma.
It is a dogma in the same sense as 2 * 3 = 6 is a dogma: a provably >>>>>>>> true sentence of a certain theory.
...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
F reo G_F rao -4Prov_F (riLG_FriY)
"F proves that: G_F is equivalent to
G||del_Number(G_F) is not provable in F"
https://plato.stanford.edu/entries/goedel-incompleteness/
#FirIncTheCom
Stripping away the inessential baggage using a formal
language with its own self-reference operator and
provability operator (thus outside of arithmetic)
G := (F re4 G)-a-a // G asserts its own unprovability in F
A proof of G in F would be a sequence of inference
steps in F that prove that they themselves do not exist.
-aFrom the way G is constructed it can be meta-proven that either
Did you hear me stutter ?
A proof of G in F would be a sequence of inference
steps in F that prove that they themselves do not exist.
An F where such sequence really exists then in that F both G and
the negation of G are provable.
A proof of G in F would be a sequence of inference
steps in F that prove that they themselves do not nexist.
Does not exist because is contradicts itself.
That conclusion needs the additional assumption that F is consistent,
which requires that the first order Peano arithmetic is consistent.
It remains true for any proof system that does not
contradict itself.
If F is not consistent then both G and its negation are provable in F.
The first order Peano arithmetic is believed to be sonsistent but its
consistency is not proven.
The point is that after all these years no one ever
bothered to notice WHY G is unprovable in F. When
we do that then G||del Incompleteness falls apart.
*G is unprovable in F because its proof would contradict itself*
*G is unprovable in F because its proof would contradict itself*
*G is unprovable in F because its proof would contradict itself*
On 1/10/26 11:19 AM, olcott wrote:
On 1/10/2026 3:25 AM, Mikko wrote:
On 08/01/2026 16:18, olcott wrote:
On 1/8/2026 4:21 AM, Mikko wrote:
On 07/01/2026 15:06, olcott wrote:G := (F re4 G)-a-a // G asserts its own unprovability in F
On 1/7/2026 6:10 AM, Mikko wrote:
On 06/01/2026 16:02, olcott wrote:Did you hear me stutter ?
On 1/6/2026 7:23 AM, Mikko wrote:
On 06/01/2026 02:24, Oleksiy Gapotchenko wrote:
Just an external observation:
A lot of tech innovations in software optimization area get >>>>>>>>>> discarded from the very beginning because people who work on >>>>>>>>>> them perceive the halting problem as a dogma.
It is a dogma in the same sense as 2 * 3 = 6 is a dogma: a
provably
true sentence of a certain theory.
...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
F reo G_F rao -4Prov_F (riLG_FriY)
"F proves that: G_F is equivalent to
G||del_Number(G_F) is not provable in F"
https://plato.stanford.edu/entries/goedel-incompleteness/
#FirIncTheCom
Stripping away the inessential baggage using a formal
language with its own self-reference operator and
provability operator (thus outside of arithmetic)
G := (F re4 G)-a-a // G asserts its own unprovability in F
A proof of G in F would be a sequence of inference
steps in F that prove that they themselves do not exist.
-aFrom the way G is constructed it can be meta-proven that either >>>>>>
A proof of G in F would be a sequence of inference
steps in F that prove that they themselves do not exist.
An F where such sequence really exists then in that F both G and
the negation of G are provable.
A proof of G in F would be a sequence of inference
steps in F that prove that they themselves do not nexist.
Does not exist because is contradicts itself.
That conclusion needs the additional assumption that F is consistent,
which requires that the first order Peano arithmetic is consistent.
It remains true for any proof system that does not
contradict itself.
If F is not consistent then both G and its negation are provable in F.
The first order Peano arithmetic is believed to be sonsistent but its
consistency is not proven.
The point is that after all these years no one ever
bothered to notice WHY G is unprovable in F. When
we do that then G||del Incompleteness falls apart.
*G is unprovable in F because its proof would contradict itself*
*G is unprovable in F because its proof would contradict itself*
*G is unprovable in F because its proof would contradict itself*
Right. so you can only have two of the following, and not all three:
1) Consistent.
2) Complete
3) Capable of supporting the Natural Numbers.
It seems the logic you can handle can't do the last, so yo are fine with your limited, but Complete and Consistant system.
On 1/10/2026 5:19 PM, Richard Damon wrote:
On 1/10/26 11:19 AM, olcott wrote:
On 1/10/2026 3:25 AM, Mikko wrote:
On 08/01/2026 16:18, olcott wrote:
On 1/8/2026 4:21 AM, Mikko wrote:
On 07/01/2026 15:06, olcott wrote:G := (F re4 G)-a-a // G asserts its own unprovability in F
On 1/7/2026 6:10 AM, Mikko wrote:
On 06/01/2026 16:02, olcott wrote:Did you hear me stutter ?
On 1/6/2026 7:23 AM, Mikko wrote:
On 06/01/2026 02:24, Oleksiy Gapotchenko wrote:
Just an external observation:
A lot of tech innovations in software optimization area get >>>>>>>>>>> discarded from the very beginning because people who work on >>>>>>>>>>> them perceive the halting problem as a dogma.
It is a dogma in the same sense as 2 * 3 = 6 is a dogma: a >>>>>>>>>> provably
true sentence of a certain theory.
...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
F reo G_F rao -4Prov_F (riLG_FriY)
"F proves that: G_F is equivalent to
G||del_Number(G_F) is not provable in F"
https://plato.stanford.edu/entries/goedel-incompleteness/
#FirIncTheCom
Stripping away the inessential baggage using a formal
language with its own self-reference operator and
provability operator (thus outside of arithmetic)
G := (F re4 G)-a-a // G asserts its own unprovability in F
A proof of G in F would be a sequence of inference
steps in F that prove that they themselves do not exist.
-aFrom the way G is constructed it can be meta-proven that either >>>>>>>
A proof of G in F would be a sequence of inference
steps in F that prove that they themselves do not exist.
An F where such sequence really exists then in that F both G and
the negation of G are provable.
A proof of G in F would be a sequence of inference
steps in F that prove that they themselves do not nexist.
Does not exist because is contradicts itself.
That conclusion needs the additional assumption that F is consistent,
which requires that the first order Peano arithmetic is consistent.
It remains true for any proof system that does not
contradict itself.
If F is not consistent then both G and its negation are provable in F. >>>> The first order Peano arithmetic is believed to be sonsistent but its
consistency is not proven.
The point is that after all these years no one ever
bothered to notice WHY G is unprovable in F. When
we do that then G||del Incompleteness falls apart.
*G is unprovable in F because its proof would contradict itself*
*G is unprovable in F because its proof would contradict itself*
*G is unprovable in F because its proof would contradict itself*
Right. so you can only have two of the following, and not all three:
1) Consistent.
2) Complete
3) Capable of supporting the Natural Numbers.
It seems the logic you can handle can't do the last, so yo are fine
with your limited, but Complete and Consistant system.
Not at all. G||del incorrectly conflates true in meta-math
with true in math. Proof Theoretic Semantics rejects this.
Proof Conditional Semantics is misguided.
On 1/10/26 7:16 PM, olcott wrote:
On 1/10/2026 5:19 PM, Richard Damon wrote:
On 1/10/26 11:19 AM, olcott wrote:
On 1/10/2026 3:25 AM, Mikko wrote:
On 08/01/2026 16:18, olcott wrote:
On 1/8/2026 4:21 AM, Mikko wrote:
On 07/01/2026 15:06, olcott wrote:G := (F re4 G)-a-a // G asserts its own unprovability in F
On 1/7/2026 6:10 AM, Mikko wrote:
On 06/01/2026 16:02, olcott wrote:Did you hear me stutter ?
On 1/6/2026 7:23 AM, Mikko wrote:
On 06/01/2026 02:24, Oleksiy Gapotchenko wrote:
Just an external observation:
A lot of tech innovations in software optimization area get >>>>>>>>>>>> discarded from the very beginning because people who work on >>>>>>>>>>>> them perceive the halting problem as a dogma.
It is a dogma in the same sense as 2 * 3 = 6 is a dogma: a >>>>>>>>>>> provably
true sentence of a certain theory.
...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
F reo G_F rao -4Prov_F (riLG_FriY)
"F proves that: G_F is equivalent to
G||del_Number(G_F) is not provable in F"
https://plato.stanford.edu/entries/goedel-incompleteness/ >>>>>>>>>> #FirIncTheCom
Stripping away the inessential baggage using a formal
language with its own self-reference operator and
provability operator (thus outside of arithmetic)
G := (F re4 G)-a-a // G asserts its own unprovability in F >>>>>>>>>>
A proof of G in F would be a sequence of inference
steps in F that prove that they themselves do not exist.
-aFrom the way G is constructed it can be meta-proven that either >>>>>>>>
A proof of G in F would be a sequence of inference
steps in F that prove that they themselves do not exist.
An F where such sequence really exists then in that F both G and >>>>>>> the negation of G are provable.
A proof of G in F would be a sequence of inference
steps in F that prove that they themselves do not nexist.
Does not exist because is contradicts itself.
That conclusion needs the additional assumption that F is consistent, >>>>> which requires that the first order Peano arithmetic is consistent.
It remains true for any proof system that does not
contradict itself.
If F is not consistent then both G and its negation are provable in F. >>>>> The first order Peano arithmetic is believed to be sonsistent but its >>>>> consistency is not proven.
The point is that after all these years no one ever
bothered to notice WHY G is unprovable in F. When
we do that then G||del Incompleteness falls apart.
*G is unprovable in F because its proof would contradict itself*
*G is unprovable in F because its proof would contradict itself*
*G is unprovable in F because its proof would contradict itself*
Right. so you can only have two of the following, and not all three:
1) Consistent.
2) Complete
3) Capable of supporting the Natural Numbers.
It seems the logic you can handle can't do the last, so yo are fine
with your limited, but Complete and Consistant system.
Not at all. G||del incorrectly conflates true in meta-math
with true in math. Proof Theoretic Semantics rejects this.
Proof Conditional Semantics is misguided.
Nope, it weems you think math doesn't work.
On 1/10/2026 3:25 AM, Mikko wrote:
On 08/01/2026 16:18, olcott wrote:
On 1/8/2026 4:21 AM, Mikko wrote:
On 07/01/2026 15:06, olcott wrote:G := (F re4 G)-a-a // G asserts its own unprovability in F
On 1/7/2026 6:10 AM, Mikko wrote:
On 06/01/2026 16:02, olcott wrote:
On 1/6/2026 7:23 AM, Mikko wrote:
On 06/01/2026 02:24, Oleksiy Gapotchenko wrote:
Just an external observation:
A lot of tech innovations in software optimization area get >>>>>>>>> discarded from the very beginning because people who work on >>>>>>>>> them perceive the halting problem as a dogma.
It is a dogma in the same sense as 2 * 3 = 6 is a dogma: a provably >>>>>>>> true sentence of a certain theory.
...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
F reo G_F rao -4Prov_F (riLG_FriY)
"F proves that: G_F is equivalent to
G||del_Number(G_F) is not provable in F"
https://plato.stanford.edu/entries/goedel-incompleteness/
#FirIncTheCom
Stripping away the inessential baggage using a formal
language with its own self-reference operator and
provability operator (thus outside of arithmetic)
G := (F re4 G)-a-a // G asserts its own unprovability in F
A proof of G in F would be a sequence of inference
steps in F that prove that they themselves do not exist.
-aFrom the way G is constructed it can be meta-proven that either
Did you hear me stutter ?
A proof of G in F would be a sequence of inference
steps in F that prove that they themselves do not exist.
An F where such sequence really exists then in that F both G and
the negation of G are provable.
A proof of G in F would be a sequence of inference
steps in F that prove that they themselves do not exist.
Does not exist because is contradicts itself.
That conclusion needs the additional assumption that F is consistent,
which requires that the first order Peano arithmetic is consistent.
It remains true for any proof system that does not
contradict itself.
On 1/10/2026 6:35 PM, Richard Damon wrote:
On 1/10/26 7:16 PM, olcott wrote:
On 1/10/2026 5:19 PM, Richard Damon wrote:
On 1/10/26 11:19 AM, olcott wrote:
On 1/10/2026 3:25 AM, Mikko wrote:
On 08/01/2026 16:18, olcott wrote:It remains true for any proof system that does not
On 1/8/2026 4:21 AM, Mikko wrote:
On 07/01/2026 15:06, olcott wrote:G := (F re4 G)-a-a // G asserts its own unprovability in F
On 1/7/2026 6:10 AM, Mikko wrote:
On 06/01/2026 16:02, olcott wrote:Did you hear me stutter ?
On 1/6/2026 7:23 AM, Mikko wrote:
On 06/01/2026 02:24, Oleksiy Gapotchenko wrote:
Just an external observation:
A lot of tech innovations in software optimization area get >>>>>>>>>>>>> discarded from the very beginning because people who work >>>>>>>>>>>>> on them perceive the halting problem as a dogma.
It is a dogma in the same sense as 2 * 3 = 6 is a dogma: a >>>>>>>>>>>> provably
true sentence of a certain theory.
...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
F reo G_F rao -4Prov_F (riLG_FriY)
"F proves that: G_F is equivalent to
G||del_Number(G_F) is not provable in F"
https://plato.stanford.edu/entries/goedel-incompleteness/ >>>>>>>>>>> #FirIncTheCom
Stripping away the inessential baggage using a formal
language with its own self-reference operator and
provability operator (thus outside of arithmetic)
G := (F re4 G)-a-a // G asserts its own unprovability in F >>>>>>>>>>>
A proof of G in F would be a sequence of inference
steps in F that prove that they themselves do not exist.
-aFrom the way G is constructed it can be meta-proven that either >>>>>>>>>
A proof of G in F would be a sequence of inference
steps in F that prove that they themselves do not exist.
An F where such sequence really exists then in that F both G and >>>>>>>> the negation of G are provable.
A proof of G in F would be a sequence of inference
steps in F that prove that they themselves do not nexist.
Does not exist because is contradicts itself.
That conclusion needs the additional assumption that F is consistent, >>>>>> which requires that the first order Peano arithmetic is consistent. >>>>>
contradict itself.
If F is not consistent then both G and its negation are provable
in F.
The first order Peano arithmetic is believed to be sonsistent but its >>>>>> consistency is not proven.
The point is that after all these years no one ever
bothered to notice WHY G is unprovable in F. When
we do that then G||del Incompleteness falls apart.
*G is unprovable in F because its proof would contradict itself*
*G is unprovable in F because its proof would contradict itself*
*G is unprovable in F because its proof would contradict itself*
Right. so you can only have two of the following, and not all three:
1) Consistent.
2) Complete
3) Capable of supporting the Natural Numbers.
It seems the logic you can handle can't do the last, so yo are fine
with your limited, but Complete and Consistant system.
Not at all. G||del incorrectly conflates true in meta-math
with true in math. Proof Theoretic Semantics rejects this.
Proof Conditional Semantics is misguided.
Nope, it weems you think math doesn't work.
Proof Theoretic Semantics agrees with me you are
going by Proof Conditional Semantics.
On 10/01/2026 18:19, olcott wrote:
On 1/10/2026 3:25 AM, Mikko wrote:
On 08/01/2026 16:18, olcott wrote:
On 1/8/2026 4:21 AM, Mikko wrote:
On 07/01/2026 15:06, olcott wrote:G := (F re4 G)-a-a // G asserts its own unprovability in F
On 1/7/2026 6:10 AM, Mikko wrote:
On 06/01/2026 16:02, olcott wrote:Did you hear me stutter ?
On 1/6/2026 7:23 AM, Mikko wrote:
On 06/01/2026 02:24, Oleksiy Gapotchenko wrote:
Just an external observation:
A lot of tech innovations in software optimization area get >>>>>>>>>> discarded from the very beginning because people who work on >>>>>>>>>> them perceive the halting problem as a dogma.
It is a dogma in the same sense as 2 * 3 = 6 is a dogma: a
provably
true sentence of a certain theory.
...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
F reo G_F rao -4Prov_F (riLG_FriY)
"F proves that: G_F is equivalent to
G||del_Number(G_F) is not provable in F"
https://plato.stanford.edu/entries/goedel-incompleteness/
#FirIncTheCom
Stripping away the inessential baggage using a formal
language with its own self-reference operator and
provability operator (thus outside of arithmetic)
G := (F re4 G)-a-a // G asserts its own unprovability in F
A proof of G in F would be a sequence of inference
steps in F that prove that they themselves do not exist.
-aFrom the way G is constructed it can be meta-proven that either >>>>>>
A proof of G in F would be a sequence of inference
steps in F that prove that they themselves do not exist.
An F where such sequence really exists then in that F both G and
the negation of G are provable.
A proof of G in F would be a sequence of inference
steps in F that prove that they themselves do not exist.
Does not exist because is contradicts itself.
That conclusion needs the additional assumption that F is consistent,
which requires that the first order Peano arithmetic is consistent.
It remains true for any proof system that does not
contradict itself.
Only for those where G can be constructed so that G is true if and
only if it is not provable. Such construction is prosible in Peano
arithmetic and many other systems but not in every system.
Any Formal System having an unprovability operator re4
On 11/01/2026 14:32, olcott wrote:
Any Formal System having an unprovability operator re4
It's odd to use that as unprovability[sic], but at least you have a
reference to the system in your expression so we could meaningfully read
it as a negation.
On 1/11/2026 10:16 AM, Tristan Wibberley wrote:
On 11/01/2026 14:32, olcott wrote:
Any Formal System having an unprovability operator re4
It's odd to use that as unprovability[sic], but at least you have a
reference to the system in your expression so we could meaningfully read
it as a negation.
(F re4 G) rei -4(F reo G)
On 1/11/2026 4:34 AM, Mikko wrote:
On 10/01/2026 18:19, olcott wrote:
On 1/10/2026 3:25 AM, Mikko wrote:
On 08/01/2026 16:18, olcott wrote:
On 1/8/2026 4:21 AM, Mikko wrote:
On 07/01/2026 15:06, olcott wrote:G := (F re4 G)-a-a // G asserts its own unprovability in F
On 1/7/2026 6:10 AM, Mikko wrote:
On 06/01/2026 16:02, olcott wrote:Did you hear me stutter ?
On 1/6/2026 7:23 AM, Mikko wrote:
On 06/01/2026 02:24, Oleksiy Gapotchenko wrote:
Just an external observation:
A lot of tech innovations in software optimization area get >>>>>>>>>>> discarded from the very beginning because people who work on >>>>>>>>>>> them perceive the halting problem as a dogma.
It is a dogma in the same sense as 2 * 3 = 6 is a dogma: a >>>>>>>>>> provably
true sentence of a certain theory.
...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
F reo G_F rao -4Prov_F (riLG_FriY)
"F proves that: G_F is equivalent to
G||del_Number(G_F) is not provable in F"
https://plato.stanford.edu/entries/goedel-incompleteness/
#FirIncTheCom
Stripping away the inessential baggage using a formal
language with its own self-reference operator and
provability operator (thus outside of arithmetic)
G := (F re4 G)-a-a // G asserts its own unprovability in F
A proof of G in F would be a sequence of inference
steps in F that prove that they themselves do not exist.
-aFrom the way G is constructed it can be meta-proven that either >>>>>>>
A proof of G in F would be a sequence of inference
steps in F that prove that they themselves do not exist.
An F where such sequence really exists then in that F both G and
the negation of G are provable.
A proof of G in F would be a sequence of inference
steps in F that prove that they themselves do not exist.
Does not exist because is contradicts itself.
That conclusion needs the additional assumption that F is consistent,
which requires that the first order Peano arithmetic is consistent.
It remains true for any proof system that does not
contradict itself.
Only for those where G can be constructed so that G is true if and
only if it is not provable. Such construction is prosible in Peano
arithmetic and many other systems but not in every system.
Any Formal System having an unprovability operator re4
and A := B // A [is defined as] B (self-reference operator)
can reject this expression G := (F re4 G) as non-well-founded
using Proof Theoretic Semantics.
| Sysop: | Amessyroom |
|---|---|
| Location: | Fayetteville, NC |
| Users: | 54 |
| Nodes: | 6 (0 / 6) |
| Uptime: | 17:54:19 |
| Calls: | 742 |
| Files: | 1,218 |
| D/L today: |
4 files (8,203K bytes) |
| Messages: | 184,414 |
| Posted today: | 1 |