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 … (Gödel 1931:40-41)
Gödel, Kurt 1931.
On Formally Undecidable Propositions of
Principia Mathematica And Related Systems
F ⊢ G_F ↔ ¬Prov_F (⌜G_F⌝)
"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 ⊬ G) // 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
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 … (Gödel 1931:40-41)
Gödel, Kurt 1931.
On Formally Undecidable Propositions of
Principia Mathematica And Related Systems
F ⊢ G_F ↔ ¬Prov_F (⌜G_F⌝)
"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 ⊬ G) // 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
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 ⊬ G) // 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 … (Gödel 1931:40-41)
Gödel, Kurt 1931.
On Formally Undecidable Propositions of
Principia Mathematica And Related Systems
F ⊢ G_F ↔ ¬Prov_F (⌜G_F⌝)
"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 ⊬ G) // 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
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 ⊬ G) // 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 … (Gödel 1931:40-41)
Gödel, Kurt 1931.
On Formally Undecidable Propositions of
Principia Mathematica And Related Systems
F ⊢ G_F ↔ ¬Prov_F (⌜G_F⌝)
"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 ⊬ G) // 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
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 ⊬ G) // 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 … (Gödel 1931:40-41)
Gödel, Kurt 1931.
On Formally Undecidable Propositions of
Principia Mathematica And Related Systems
F ⊢ G_F ↔ ¬Prov_F (⌜G_F⌝)
"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 ⊬ G) // 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
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 ⊬ G) // 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 … (Gödel 1931:40-41)
Gödel, Kurt 1931.
On Formally Undecidable Propositions of
Principia Mathematica And Related Systems
F ⊢ G_F ↔ ¬Prov_F (⌜G_F⌝)
"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 ⊬ G) // 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 >>>>>>
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 ⊬ G) // 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 … (Gödel 1931:40-41)
Gödel, Kurt 1931.
On Formally Undecidable Propositions of
Principia Mathematica And Related Systems
F ⊢ G_F ↔ ¬Prov_F (⌜G_F⌝)
"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 ⊬ G) // 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 >>>>>>>
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 ⊬ G) // 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 … (Gödel 1931:40-41)
Gödel, Kurt 1931.
On Formally Undecidable Propositions of
Principia Mathematica And Related Systems
F ⊢ G_F ↔ ¬Prov_F (⌜G_F⌝)
"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 ⊬ G) // 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 >>>>>>>>
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 ⊬ G) // 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 … (Gödel 1931:40-41)
Gödel, Kurt 1931.
On Formally Undecidable Propositions of
Principia Mathematica And Related Systems
F ⊢ G_F ↔ ¬Prov_F (⌜G_F⌝)
"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 ⊬ G) // 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
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 ⊬ G) // 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 … (Gödel 1931:40-41) >>>>>>>>>>>
Gödel, Kurt 1931.
On Formally Undecidable Propositions of
Principia Mathematica And Related Systems
F ⊢ G_F ↔ ¬Prov_F (⌜G_F⌝)
"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 ⊬ G) // 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 >>>>>>>>>
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 ⊬ G) // 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 … (Gödel 1931:40-41)
Gödel, Kurt 1931.
On Formally Undecidable Propositions of
Principia Mathematica And Related Systems
F ⊢ G_F ↔ ¬Prov_F (⌜G_F⌝)
"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 ⊬ G) // 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 >>>>>>
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 ⊬
On 11/01/2026 14:32, olcott wrote:
Any Formal System having an unprovability operator ⊬
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 ⊬
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 ⊬ G) ≡ ¬(F ⊢ 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 ⊬ G) // 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 … (Gödel 1931:40-41)
Gödel, Kurt 1931.
On Formally Undecidable Propositions of
Principia Mathematica And Related Systems
F ⊢ G_F ↔ ¬Prov_F (⌜G_F⌝)
"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 ⊬ G) // 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 >>>>>>>
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 ⊬
and A := B // A [is defined as] B (self-reference operator)
can reject this expression G := (F ⊬ G) as non-well-founded
using Proof Theoretic Semantics.
| Sysop: | datGSguy |
|---|---|
| Location: | Eugene, OR |
| Users: | 7 |
| Nodes: | 4 (0 / 4) |
| Uptime: | 219:22:54 |
| Calls: | 361 |
| Calls today: | 34 |
| Files: | 14 |
| D/L today: |
73 files (1,158K bytes) |
| Messages: | 5,781 |
| Posted today: | 1 |