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.
| Sysop: | datGSguy |
|---|---|
| Location: | Eugene, OR |
| Users: | 7 |
| Nodes: | 4 (0 / 4) |
| Uptime: | 219:17:14 |
| Calls: | 361 |
| Calls today: | 34 |
| Files: | 14 |
| D/L today: |
65 files (1,067K bytes) |
| Messages: | 5,751 |
| Posted today: | 1 |