From Newsgroup: sci.lang

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:

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.

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.
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.
--
Copyright 2026 Olcott<br><br>

My 28 year goal has been to make <br>
"true on the basis of meaning expressed in language"<br>
reliably computable.<br><br>

This required establishing a new foundation<br>
--- Synchronet 3.21a-Linux NewsLink 1.2

From Newsgroup: sci.lang

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

From Newsgroup: sci.lang

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)
--
Copyright 2026 Olcott

My 28 year goal has been to make
"true on the basis of meaning expressed in language"
reliably computable.

This required establishing a new foundation
for correct reasoning.
--- Synchronet 3.21a-Linux NewsLink 1.2

From Newsgroup: sci.lang

On 11/01/2026 16:32, olcott wrote:

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:

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.

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

That is a very restricted scope. For example, neither operator is in
the language of the first order Peano arithmetic. In addition, in
langages that have := don't have it as a symbol for a function or a
predicate but as sui generis with specific syntax rules, one of which
usually is that the symbol on the left side of := must not be used on
the right side. Therefore G := (F re4 G) is not in typical languages that
have := and re4.
--
Mikko
--- Synchronet 3.21a-Linux NewsLink 1.2