• =?UTF-8?B?UmU6IEfDtmRlbCdzIEcgOj0gKEYg4oqsIEcp?=

    From olcott@[email protected] to comp.theory on Mon Nov 3 17:40:06 2025
    From Newsgroup: comp.theory

    On 11/2/2025 6:41 AM, Mikko wrote:
    On 2025-11-01 13:50:53 +0000, olcott said:

    On 11/1/2025 4:10 AM, Mikko wrote:
    On 2025-10-31 12:09:48 +0000, olcott said:

    On 10/31/2025 6:02 AM, Mikko wrote:
    On 2025-10-30 12:54:57 +0000, olcott said:

    On 10/30/2025 5:37 AM, Mikko wrote:
    On 2025-10-29 16:22:11 +0000, olcott said:

    On 10/29/2025 5:43 AM, Mikko wrote:
    On 2025-10-28 15:07:18 +0000, olcott said:

    On 10/28/2025 4:54 AM, Mikko wrote:
    On 2025-10-27 13:56:21 +0000, olcott said:

    On 10/27/2025 4:45 AM, Mikko wrote:
    On 2025-10-26 17:57:16 +0000, Richard Damon said:

    On 10/26/25 7:44 AM, Mikko wrote:
    On 2025-10-25 19:57:19 +0000, olcott said:

    On 10/25/2025 6:59 AM, Mikko wrote:
    On 2025-10-24 17:37:43 +0000, olcott said:

    On 10/24/2025 2:46 AM, Mikko wrote:
    On 2025-10-23 15:39:13 +0000, olcott said: >>>>>>>>>>>>>>>>>>>
    On 10/23/2025 5:02 AM, Mikko wrote:
    On 2025-10-22 12:39:31 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>>
    On 10/22/2025 4:23 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>> On 2025-10-21 15:11:19 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>>>>
    On 10/21/2025 4:31 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>>>> On 2025-10-20 16:24:46 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>>>>>>
    On 10/20/2025 3:55 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>> On 2025-10-19 15:03:34 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>>>>>>>>
    On 10/19/2025 3:44 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>>>> On 2025-10-18 10:58:15 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    On 10/18/2025 4:30 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    That is not a sense of "proof". >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    That is the correct way to do a proof. >>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    A way to do is not a sense. >>>>>>>>>>>>>>>>>>>>>>>>>>>>
    The conventional way to do proofs concludes >>>>>>>>>>>>>>>>>>>>>>>>>>>> that
    within its rules if the Moon is made from green >>>>>>>>>>>>>>>>>>>>>>>>>>>> cheese and the Moon is not made from green >>>>>>>>>>>>>>>>>>>>>>>>>>>> cheese
    this proves that Donald Trump is the Lord >>>>>>>>>>>>>>>>>>>>>>>>>>>> and savior Jesus Christ. >>>>>>>>>>>>>>>>>>>>>>>>>>>
    Right, and the empirical falct that nobody >>>>>>>>>>>>>>>>>>>>>>>>>>> has verified all of
    1. the Moon is made from green cheese >>>>>>>>>>>>>>>>>>>>>>>>>>> 2. the Moon is not made from grenn cheese >>>>>>>>>>>>>>>>>>>>>>>>>>> 3. Donald Trump is not the Lord and saviour >>>>>>>>>>>>>>>>>>>>>>>>>>> Jesus Christ
    at the same time supports the idea that the >>>>>>>>>>>>>>>>>>>>>>>>>>> conventiona wya to
    do proofs is correct and trustworthy. >>>>>>>>>>>>>>>>>>>>>>>>>>
    When we require that correct reasoning is only >>>>>>>>>>>>>>>>>>>>>>>>>> semantic
    logical entailment from basic facts the >>>>>>>>>>>>>>>>>>>>>>>>>> Principle of
    Explosion ceases to exist.

    Only if you exclude from "correct reasioning" >>>>>>>>>>>>>>>>>>>>>>>>> some reasning that
    actually is correct.

    There is no counter-example that can possibly exist >>>>>>>>>>>>>>>>>>>>>>>> that can show there are any gaps in the body of >>>>>>>>>>>>>>>>>>>>>>>> human
    knowledge that can be expressed in language that >>>>>>>>>>>>>>>>>>>>>>>> begins
    with a consistent set of basic facts and only >>>>>>>>>>>>>>>>>>>>>>>> applies
    semantic logical entailment to these facts. >>>>>>>>>>>>>>>>>>>>>>>
    There is no language that begins with a >>>>>>>>>>>>>>>>>>>>>>> consistent set of basic facts
    and only applies semantic logical entailment to >>>>>>>>>>>>>>>>>>>>>>> those facts and can
    express all of human knowledge without any gaps. >>>>>>>>>>>>>>>>>>>>>>
    A subset of formalized English does do this. >>>>>>>>>>>>>>>>>>>>>
    Nobody has ever presented such subset. >>>>>>>>>>>>>>>>>>>>
    ChatGPT rewords my words into that subset. >>>>>>>>>>>>>>>>>>>
    Your words have much less material than all human >>>>>>>>>>>>>>>>>>> knowledge without
    any gaps. Therefore it is impossible to verify that >>>>>>>>>>>>>>>>>>> you have told
    every necessary word to it.

    Categorically exhaustive reasoning reverse-engineers >>>>>>>>>>>>>>>>>> the required architecture of the system. Wittgenstein >>>>>>>>>>>>>>>>>> did this on Gödel https://www.liarparadox.org/ >>>>>>>>>>>>>>>>>> Wittgenstein.pdf
    and he was so succinct eliminate the convoluted mess >>>>>>>>>>>>>>>>>> of Gödel
    numbers that people mistook his succinct analysis as >>>>>>>>>>>>>>>>>> simplistic
    not understanding what Gödel was really saying. >>>>>>>>>>>>>>>>>
    Yes, an expectable consequence of ignoring essential >>>>>>>>>>>>>>>>> aspects is
    not understanding.

    Gödel numbers are merely the ridiculously convoluted >>>>>>>>>>>>>>>> way that Gödel added the functionality of this simple >>>>>>>>>>>>>>>> operator: ⊢ to a formal language woefully too inexpressive. >>>>>>>>>>>>>>>
    Natural numbers are one of the best understood topics of >>>>>>>>>>>>>>> mathematics.
    Therefore restricting the assumptions to natural numbers >>>>>>>>>>>>>>> provdes the
    basis for the most interesting result.

    Of course one can ask whether one can prove a similar >>>>>>>>>>>>>>> theorem about
    finite strings. It is much simpler to express claims and >>>>>>>>>>>>>>> proofs as
    fimite strings as thats how they are usually expressed >>>>>>>>>>>>>>> anyway. But
    that requires that one first constructs a theory of >>>>>>>>>>>>>>> finite strings.

    But we can show a direct one-to-one mapping of finite >>>>>>>>>>>>>> strings in a finite alphabet to natural numbers (it just >>>>>>>>>>>>>> becomes the notational base for the numbers).

    That's true, and I would prefer that rather than Gödel's >>>>>>>>>>>>> mapping. But
    the proof of Gödel's theorem is simpler if the number of >>>>>>>>>>>>> symbols in
    the alphabet is prime even if that would mean that some of >>>>>>>>>>>>> the symbols
    are unused.

    Gödel numbers hide this simple essence behind a convoluted >>>>>>>>>>>> mess:
    G := (F ⊬ G)

    No, that is not the sentence. For Gödel's purposes it was >>>>>>>>>>> important to
    cover languages that have no symbol for ':=' or '⊬'.

    But that is irrelevant to my preference for the numbering >>>>>>>>>>> method.

    His result is supposed to apply to any formal language
    as expressive as PA or above.

    Yes, includint PA itself. Therefore his proof could not assume any >>>>>>>>> symbols other than those of PA. A proof that requires other >>>>>>>>> symbols
    proves nothing about PA.

    If he started with Minimal Type Theory and the understanding
    that cycles in the evaluation sequence of expressions indicate >>>>>>>> that they are semantically unsound we would have never heard
    of Incompleteness.

    Sooner or later someone would have found incompleteness anyway.

    Incompleteness is a misconception nothing more.

    No, it is a part of analytic knowledge. You have not shown any error >>>>> in Gödel's and other proofs that every theory of natural numbers is >>>>> incomplete. All you have shown is that you don't like the fact and
    some rationale for your dislike.

    His incompleteness applies to PA or above, thus
    applies to MTT.

    You have never shown the full theory of MTT so hard to tell. But if
    MTT is consistent it should be provably incomplete.

    I showed the entire language specification you just
    didn't pay attention.

    Irrelevant to my comment that some parts of the theory are not yet
    shown.

    Its exactly the same thing a FOL with additional operators
    to make it much more expressive. For example it can directly
    expression any HOL logic expression.

    You mean it includes "tertium non datur" and "the principle of explosion"?

    I give an example.

    Thank's but the definition of the theory is still missing.


    The theory is entirely expressed by the conventional
    meaning of it operators and the syntax that I provided.

    G := (F ⊬ G)
    G is defined as unprovable from F.
    That is the ordinary "defined as" operator.
    --
    Copyright 2025 Olcott "Talent hits a target no one else can hit; Genius
    hits a target no one else can see." Arthur Schopenhauer
    --- Synchronet 3.21a-Linux NewsLink 1.2
  • From olcott@[email protected] to comp.theory on Mon Nov 3 17:41:35 2025
    From Newsgroup: comp.theory

    On 11/2/2025 6:43 AM, Mikko wrote:
    On 2025-11-01 13:52:41 +0000, olcott said:

    On 11/1/2025 4:16 AM, Mikko wrote:
    On 2025-10-31 12:18:16 +0000, olcott said:

    On 10/31/2025 6:10 AM, Mikko wrote:
    On 2025-10-30 13:01:34 +0000, olcott said:

    On 10/30/2025 5:44 AM, Mikko wrote:
    On 2025-10-29 16:26:58 +0000, olcott said:

    On 10/29/2025 5:53 AM, Mikko wrote:
    On 2025-10-29 01:57:07 +0000, Richard Damon said:

    On 10/28/25 11:12 AM, olcott wrote:
    On 10/28/2025 4:58 AM, Mikko wrote:
    On 2025-10-28 01:22:21 +0000, Richard Damon said:

    On 10/27/25 5:45 AM, Mikko wrote:
    On 2025-10-26 17:57:16 +0000, Richard Damon said:

    On 10/26/25 7:44 AM, Mikko wrote:
    On 2025-10-25 19:57:19 +0000, olcott said:

    On 10/25/2025 6:59 AM, Mikko wrote:
    On 2025-10-24 17:37:43 +0000, olcott said: >>>>>>>>>>>>>>>>>>
    On 10/24/2025 2:46 AM, Mikko wrote:
    On 2025-10-23 15:39:13 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>
    On 10/23/2025 5:02 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>> On 2025-10-22 12:39:31 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>>>
    On 10/22/2025 4:23 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>>> On 2025-10-21 15:11:19 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>>>>>
    On 10/21/2025 4:31 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>>>>> On 2025-10-20 16:24:46 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>>>>>>>
    On 10/20/2025 3:55 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>>> On 2025-10-19 15:03:34 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>>>>>>>>>
    On 10/19/2025 3:44 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>> On 2025-10-18 10:58:15 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    On 10/18/2025 4:30 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    That is not a sense of "proof". >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    That is the correct way to do a proof. >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    A way to do is not a sense. >>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    The conventional way to do proofs concludes >>>>>>>>>>>>>>>>>>>>>>>>>>>>> that
    within its rules if the Moon is made from >>>>>>>>>>>>>>>>>>>>>>>>>>>>> green
    cheese and the Moon is not made from green >>>>>>>>>>>>>>>>>>>>>>>>>>>>> cheese
    this proves that Donald Trump is the Lord >>>>>>>>>>>>>>>>>>>>>>>>>>>>> and savior Jesus Christ. >>>>>>>>>>>>>>>>>>>>>>>>>>>>
    Right, and the empirical falct that nobody >>>>>>>>>>>>>>>>>>>>>>>>>>>> has verified all of
    1. the Moon is made from green cheese >>>>>>>>>>>>>>>>>>>>>>>>>>>> 2. the Moon is not made from grenn cheese >>>>>>>>>>>>>>>>>>>>>>>>>>>> 3. Donald Trump is not the Lord and saviour >>>>>>>>>>>>>>>>>>>>>>>>>>>> Jesus Christ
    at the same time supports the idea that the >>>>>>>>>>>>>>>>>>>>>>>>>>>> conventiona wya to
    do proofs is correct and trustworthy. >>>>>>>>>>>>>>>>>>>>>>>>>>>
    When we require that correct reasoning is >>>>>>>>>>>>>>>>>>>>>>>>>>> only semantic
    logical entailment from basic facts the >>>>>>>>>>>>>>>>>>>>>>>>>>> Principle of
    Explosion ceases to exist. >>>>>>>>>>>>>>>>>>>>>>>>>>
    Only if you exclude from "correct reasioning" >>>>>>>>>>>>>>>>>>>>>>>>>> some reasning that
    actually is correct.

    There is no counter-example that can possibly >>>>>>>>>>>>>>>>>>>>>>>>> exist
    that can show there are any gaps in the body of >>>>>>>>>>>>>>>>>>>>>>>>> human
    knowledge that can be expressed in language >>>>>>>>>>>>>>>>>>>>>>>>> that begins
    with a consistent set of basic facts and only >>>>>>>>>>>>>>>>>>>>>>>>> applies
    semantic logical entailment to these facts. >>>>>>>>>>>>>>>>>>>>>>>>
    There is no language that begins with a >>>>>>>>>>>>>>>>>>>>>>>> consistent set of basic facts
    and only applies semantic logical entailment to >>>>>>>>>>>>>>>>>>>>>>>> those facts and can
    express all of human knowledge without any gaps. >>>>>>>>>>>>>>>>>>>>>>>
    A subset of formalized English does do this. >>>>>>>>>>>>>>>>>>>>>>
    Nobody has ever presented such subset. >>>>>>>>>>>>>>>>>>>>>
    ChatGPT rewords my words into that subset. >>>>>>>>>>>>>>>>>>>>
    Your words have much less material than all human >>>>>>>>>>>>>>>>>>>> knowledge without
    any gaps. Therefore it is impossible to verify that >>>>>>>>>>>>>>>>>>>> you have told
    every necessary word to it.

    Categorically exhaustive reasoning reverse-engineers >>>>>>>>>>>>>>>>>>> the required architecture of the system. Wittgenstein >>>>>>>>>>>>>>>>>>> did this on Gödel https://www.liarparadox.org/ >>>>>>>>>>>>>>>>>>> Wittgenstein.pdf
    and he was so succinct eliminate the convoluted mess >>>>>>>>>>>>>>>>>>> of Gödel
    numbers that people mistook his succinct analysis as >>>>>>>>>>>>>>>>>>> simplistic
    not understanding what Gödel was really saying. >>>>>>>>>>>>>>>>>>
    Yes, an expectable consequence of ignoring essential >>>>>>>>>>>>>>>>>> aspects is
    not understanding.

    Gödel numbers are merely the ridiculously convoluted >>>>>>>>>>>>>>>>> way that Gödel added the functionality of this simple >>>>>>>>>>>>>>>>> operator: ⊢ to a formal language woefully too >>>>>>>>>>>>>>>>> inexpressive.

    Natural numbers are one of the best understood topics of >>>>>>>>>>>>>>>> mathematics.
    Therefore restricting the assumptions to natural numbers >>>>>>>>>>>>>>>> provdes the
    basis for the most interesting result.

    Of course one can ask whether one can prove a similar >>>>>>>>>>>>>>>> theorem about
    finite strings. It is much simpler to express claims and >>>>>>>>>>>>>>>> proofs as
    fimite strings as thats how they are usually expressed >>>>>>>>>>>>>>>> anyway. But
    that requires that one first constructs a theory of >>>>>>>>>>>>>>>> finite strings.

    But we can show a direct one-to-one mapping of finite >>>>>>>>>>>>>>> strings in a finite alphabet to natural numbers (it just >>>>>>>>>>>>>>> becomes the notational base for the numbers).

    That's true, and I would prefer that rather than Gödel's >>>>>>>>>>>>>> mapping. But
    the proof of Gödel's theorem is simpler if the number of >>>>>>>>>>>>>> symbols in
    the alphabet is prime even if that would mean that some of >>>>>>>>>>>>>> the symbols
    are unused.

    Godel's Theorem doesn't need the number of symbols to be >>>>>>>>>>>>> prime, it uses prime numbers to number the symbols, and >>>>>>>>>>>>> prime powers for the position.

    And consequently Gödel's example of an undecidable formula >>>>>>>>>>>> is more complex
    than needed. Which doesn't really matter as the complex >>>>>>>>>>>> details can be
    hidden behind definitions.


    ...We are therefore confronted with a proposition which >>>>>>>>>>> asserts its own unprovability. 15 ...
    (Gödel 1931:40-41)

    Which is a statement in the meta-logic, not in the logic.

    G asserts it isn't provable, but asserting that there can be >>>>>>>>>> no number which can encode a proof of itself.

    This statement MUST be either true of false.

    It's actually both.

    It is a lie that it is even a statement.
    I could equally say this statement is true or false: "What time >>>>>>>> is it?"

    You cant say that in the language of Peano arithmetic.

    PA is ridiculously inexpressive so that the key
    essence is hidden bu far too many purely extraneous
    details.

    PA can express everything we need to know about natural numbers.
    Complexities can be hidden behind definitions.

    MTT can express anything that we way to know about
    formal expressions of language.

     Since Incompleteness applies to PA OR ABOVE.
    I go with above.

    You may need to rewrite the proof for the language of the theory you >>>>> want to use, especially if you don't want to use the ordinary logic.

    All that I did was get rid of the purely extraneous
    complexity of Gödel's G

    All that complexity is in Gödel's proof. You need to rewrite the proof
    and verify its equivalence to the original if you want to ger rid of
    the complexity.

    But the complexity affects only the verification of the correctness of
    the proof. The meaning of the conclusion is simple.

    *Gödel already said that it is equivalent*

    Not about my comment.


    I am not going to do any useless busy work.
    --
    Copyright 2025 Olcott "Talent hits a target no one else can hit; Genius
    hits a target no one else can see." Arthur Schopenhauer
    --- Synchronet 3.21a-Linux NewsLink 1.2
  • From olcott@[email protected] to comp.theory on Mon Nov 3 17:45:57 2025
    From Newsgroup: comp.theory

    On 11/2/2025 6:45 AM, Mikko wrote:
    On 2025-11-01 13:54:09 +0000, olcott said:

    On 11/1/2025 4:18 AM, Mikko wrote:
    On 2025-10-31 12:20:13 +0000, olcott said:

    On 10/31/2025 6:15 AM, Mikko wrote:
    On 2025-10-30 13:03:23 +0000, olcott said:

    On 10/30/2025 5:50 AM, Mikko wrote:
    On 2025-10-29 16:25:00 +0000, olcott said:

    On 10/29/2025 5:45 AM, Mikko wrote:
    On 2025-10-28 15:12:29 +0000, olcott said:

    On 10/28/2025 4:58 AM, Mikko wrote:
    On 2025-10-28 01:22:21 +0000, Richard Damon said:

    On 10/27/25 5:45 AM, Mikko wrote:
    On 2025-10-26 17:57:16 +0000, Richard Damon said:

    On 10/26/25 7:44 AM, Mikko wrote:
    On 2025-10-25 19:57:19 +0000, olcott said:

    On 10/25/2025 6:59 AM, Mikko wrote:
    On 2025-10-24 17:37:43 +0000, olcott said:

    On 10/24/2025 2:46 AM, Mikko wrote:
    On 2025-10-23 15:39:13 +0000, olcott said: >>>>>>>>>>>>>>>>>>>
    On 10/23/2025 5:02 AM, Mikko wrote:
    On 2025-10-22 12:39:31 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>>
    On 10/22/2025 4:23 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>> On 2025-10-21 15:11:19 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>>>>
    On 10/21/2025 4:31 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>>>> On 2025-10-20 16:24:46 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>>>>>>
    On 10/20/2025 3:55 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>> On 2025-10-19 15:03:34 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>>>>>>>>
    On 10/19/2025 3:44 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>>>> On 2025-10-18 10:58:15 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    On 10/18/2025 4:30 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    That is not a sense of "proof". >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    That is the correct way to do a proof. >>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    A way to do is not a sense. >>>>>>>>>>>>>>>>>>>>>>>>>>>>
    The conventional way to do proofs concludes >>>>>>>>>>>>>>>>>>>>>>>>>>>> that
    within its rules if the Moon is made from green >>>>>>>>>>>>>>>>>>>>>>>>>>>> cheese and the Moon is not made from green >>>>>>>>>>>>>>>>>>>>>>>>>>>> cheese
    this proves that Donald Trump is the Lord >>>>>>>>>>>>>>>>>>>>>>>>>>>> and savior Jesus Christ. >>>>>>>>>>>>>>>>>>>>>>>>>>>
    Right, and the empirical falct that nobody >>>>>>>>>>>>>>>>>>>>>>>>>>> has verified all of
    1. the Moon is made from green cheese >>>>>>>>>>>>>>>>>>>>>>>>>>> 2. the Moon is not made from grenn cheese >>>>>>>>>>>>>>>>>>>>>>>>>>> 3. Donald Trump is not the Lord and saviour >>>>>>>>>>>>>>>>>>>>>>>>>>> Jesus Christ
    at the same time supports the idea that the >>>>>>>>>>>>>>>>>>>>>>>>>>> conventiona wya to
    do proofs is correct and trustworthy. >>>>>>>>>>>>>>>>>>>>>>>>>>
    When we require that correct reasoning is only >>>>>>>>>>>>>>>>>>>>>>>>>> semantic
    logical entailment from basic facts the >>>>>>>>>>>>>>>>>>>>>>>>>> Principle of
    Explosion ceases to exist.

    Only if you exclude from "correct reasioning" >>>>>>>>>>>>>>>>>>>>>>>>> some reasning that
    actually is correct.

    There is no counter-example that can possibly exist >>>>>>>>>>>>>>>>>>>>>>>> that can show there are any gaps in the body of >>>>>>>>>>>>>>>>>>>>>>>> human
    knowledge that can be expressed in language that >>>>>>>>>>>>>>>>>>>>>>>> begins
    with a consistent set of basic facts and only >>>>>>>>>>>>>>>>>>>>>>>> applies
    semantic logical entailment to these facts. >>>>>>>>>>>>>>>>>>>>>>>
    There is no language that begins with a >>>>>>>>>>>>>>>>>>>>>>> consistent set of basic facts
    and only applies semantic logical entailment to >>>>>>>>>>>>>>>>>>>>>>> those facts and can
    express all of human knowledge without any gaps. >>>>>>>>>>>>>>>>>>>>>>
    A subset of formalized English does do this. >>>>>>>>>>>>>>>>>>>>>
    Nobody has ever presented such subset. >>>>>>>>>>>>>>>>>>>>
    ChatGPT rewords my words into that subset. >>>>>>>>>>>>>>>>>>>
    Your words have much less material than all human >>>>>>>>>>>>>>>>>>> knowledge without
    any gaps. Therefore it is impossible to verify that >>>>>>>>>>>>>>>>>>> you have told
    every necessary word to it.

    Categorically exhaustive reasoning reverse-engineers >>>>>>>>>>>>>>>>>> the required architecture of the system. Wittgenstein >>>>>>>>>>>>>>>>>> did this on Gödel https://www.liarparadox.org/ >>>>>>>>>>>>>>>>>> Wittgenstein.pdf
    and he was so succinct eliminate the convoluted mess >>>>>>>>>>>>>>>>>> of Gödel
    numbers that people mistook his succinct analysis as >>>>>>>>>>>>>>>>>> simplistic
    not understanding what Gödel was really saying. >>>>>>>>>>>>>>>>>
    Yes, an expectable consequence of ignoring essential >>>>>>>>>>>>>>>>> aspects is
    not understanding.

    Gödel numbers are merely the ridiculously convoluted >>>>>>>>>>>>>>>> way that Gödel added the functionality of this simple >>>>>>>>>>>>>>>> operator: ⊢ to a formal language woefully too inexpressive. >>>>>>>>>>>>>>>
    Natural numbers are one of the best understood topics of >>>>>>>>>>>>>>> mathematics.
    Therefore restricting the assumptions to natural numbers >>>>>>>>>>>>>>> provdes the
    basis for the most interesting result.

    Of course one can ask whether one can prove a similar >>>>>>>>>>>>>>> theorem about
    finite strings. It is much simpler to express claims and >>>>>>>>>>>>>>> proofs as
    fimite strings as thats how they are usually expressed >>>>>>>>>>>>>>> anyway. But
    that requires that one first constructs a theory of >>>>>>>>>>>>>>> finite strings.

    But we can show a direct one-to-one mapping of finite >>>>>>>>>>>>>> strings in a finite alphabet to natural numbers (it just >>>>>>>>>>>>>> becomes the notational base for the numbers).

    That's true, and I would prefer that rather than Gödel's >>>>>>>>>>>>> mapping. But
    the proof of Gödel's theorem is simpler if the number of >>>>>>>>>>>>> symbols in
    the alphabet is prime even if that would mean that some of >>>>>>>>>>>>> the symbols
    are unused.

    Godel's Theorem doesn't need the number of symbols to be >>>>>>>>>>>> prime, it uses prime numbers to number the symbols, and >>>>>>>>>>>> prime powers for the position.

    And consequently Gödel's example of an undecidable formula is >>>>>>>>>>> more complex
    than needed. Which doesn't really matter as the complex >>>>>>>>>>> details can be
    hidden behind definitions.


    ...We are therefore confronted with a proposition which
    asserts its own unprovability. 15 ...
    (Gödel 1931:40-41)

    G := (F ⊬ G) // Olcott's Minimal Type Theory
    https://philarchive.org/archive/PETMTT-4v2 // YACC BNF of MTT >>>>>>>>>>
    ?- G = not(provable(F, G)).
    G = not(provable(F, G)).

    ?- unify_with_occurs_check(G, not(provable(F, G))).
    false.

    Gödel, Kurt 1931.
    On Formally Undecidable Propositions of Principia Mathematica >>>>>>>>>> And Related Systems

    Nice to see that you don't disagree.

    In other words you agree that I proved 1931 Incompleteness is >>>>>>>> incorrect.
    Gödel's G when boiled down to its barest essence is simply
    semantically
    unsound the same way the Liar Paradox is unsound.

    As yousually your "in other words" is a lie. Existence of a
    simpler proof
    does not make the original one incorrect.

    My words are true within your words:
       "Nice to see that you don't disagree."
    If you didn't mean that then you should not have said that.

    I did not say nor mean "you did not disagree with anything". The usual >>>>> meaning of what I said is that you don't disagree with what I said in >>>>> my previous message about the complexity of Gödel's sentence.

    The complexity of Gödel's sentence is nuts.
    G := (F ⊬ G) Just detect the cycle in this
    and Gödel is refuted.

    Nice to see that you still don't disagree with my comment about the
    complexity of Gödel's sentence.

    Yet I absolutely do disagree.

    OK, you think Gödel's numbering scheme is simple.



    ...We are therefore confronted with a proposition which asserts its own unprovability. 15 ... (Gödel 1931:40-41)

    It totally hides the details that proof his theorem is unsound.
    What does it mean for an expression to assert its own unprovability?

    It means semantic gibberish that Prolog can spot and reject.

    ?- G = not(provable(F, G)).
    G = not(provable(F, G)).
    ?- unify_with_occurs_check(G, not(provable(F, G))).
    false.





    *Gödel already said that it is equivalent*

    That doesn't mean 'equally complex'.

    --
    Copyright 2025 Olcott "Talent hits a target no one else can hit; Genius
    hits a target no one else can see." Arthur Schopenhauer
    --- Synchronet 3.21a-Linux NewsLink 1.2
  • From Tristan Wibberley@[email protected] to comp.theory on Tue Nov 4 00:29:02 2025
    From Newsgroup: comp.theory

    On 03/11/2025 23:40, olcott wrote:

    [the snip of the century]

    G := (F ⊬ G)
    G is defined as unprovable from F.
    That is the ordinary "defined as" operator.

    That's "definitionally reduces to", I think. If "(F ⊬ G)" is not
    ultimately defined then G can still be not defined.

    "define" /is/ a funny word isn't it? Several fields have mixed it up in different ways.

    --
    Tristan Wibberley

    The message body is Copyright (C) 2025 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 olcott@[email protected] to comp.theory on Mon Nov 3 18:32:51 2025
    From Newsgroup: comp.theory

    On 11/3/2025 6:29 PM, Tristan Wibberley wrote:
    On 03/11/2025 23:40, olcott wrote:

    [the snip of the century]

    G := (F ⊬ G)
    G is defined as unprovable from F.
    That is the ordinary "defined as" operator.

    That's "definitionally reduces to", I think. If "(F ⊬ G)" is not
    ultimately defined then G can still be not defined.

    "define" /is/ a funny word isn't it? Several fields have mixed it up in different ways.


    ?- G = not(provable(F, G)).
    G = not(provable(F, G)).

    ?- unify_with_occurs_check(G, not(provable(F, G))).
    false.

    The point is that Prolog determines it is semantically
    unsound because it has a cycle in the directed graph of
    its evaluation sequence.

    --
    Tristan Wibberley

    The message body is Copyright (C) 2025 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.

    --
    Copyright 2025 Olcott "Talent hits a target no one else can hit; Genius
    hits a target no one else can see." Arthur Schopenhauer
    --- Synchronet 3.21a-Linux NewsLink 1.2
  • From Kaz Kylheku@[email protected] to comp.theory on Tue Nov 4 01:59:59 2025
    From Newsgroup: comp.theory

    On 2025-11-04, olcott <[email protected]> wrote:
    On 11/3/2025 6:29 PM, Tristan Wibberley wrote:
    On 03/11/2025 23:40, olcott wrote:

    [the snip of the century]

    G := (F ⊬ G)
    G is defined as unprovable from F.
    That is the ordinary "defined as" operator.

    That's "definitionally reduces to", I think. If "(F ⊬ G)" is not
    ultimately defined then G can still be not defined.

    "define" /is/ a funny word isn't it? Several fields have mixed it up in
    different ways.


    ?- G = not(provable(F, G)).
    G = not(provable(F, G)).

    ?- unify_with_occurs_check(G, not(provable(F, G))).
    false.

    The point is that Prolog determines it is semantically
    unsound because it has a cycle in the directed graph of
    its evaluation sequence.

    Idiot, you can't do it that way. You have to encode it:

    G := not(is_theorem_numbrer(F, G_number))

    Where G_number is not a symbol but an actual numeric literal which is
    the Gödel numbering of "not(godel_number_of_theorem(F, G_number))".

    It's not quite that simple, but that's the gist.

    Statements of number theory have to be encoded as numbers, giving
    rise to a the predicate is_theorem_number.

    You cannot simply have a direct symbolic reference that is circular; of
    course Prolog chokes on that.
    --
    TXR Programming Language: http://nongnu.org/txr
    Cygnal: Cygwin Native Application Library: http://kylheku.com/cygnal
    Mastodon: @[email protected]
    --- Synchronet 3.21a-Linux NewsLink 1.2
  • From Mikko@[email protected] to comp.theory on Tue Nov 4 11:46:25 2025
    From Newsgroup: comp.theory

    On 2025-11-03 23:40:06 +0000, olcott said:

    On 11/2/2025 6:41 AM, Mikko wrote:
    On 2025-11-01 13:50:53 +0000, olcott said:

    On 11/1/2025 4:10 AM, Mikko wrote:
    On 2025-10-31 12:09:48 +0000, olcott said:

    On 10/31/2025 6:02 AM, Mikko wrote:
    On 2025-10-30 12:54:57 +0000, olcott said:

    On 10/30/2025 5:37 AM, Mikko wrote:
    On 2025-10-29 16:22:11 +0000, olcott said:

    On 10/29/2025 5:43 AM, Mikko wrote:
    On 2025-10-28 15:07:18 +0000, olcott said:

    On 10/28/2025 4:54 AM, Mikko wrote:
    On 2025-10-27 13:56:21 +0000, olcott said:

    On 10/27/2025 4:45 AM, Mikko wrote:
    On 2025-10-26 17:57:16 +0000, Richard Damon said:

    On 10/26/25 7:44 AM, Mikko wrote:
    On 2025-10-25 19:57:19 +0000, olcott said:

    On 10/25/2025 6:59 AM, Mikko wrote:
    On 2025-10-24 17:37:43 +0000, olcott said: >>>>>>>>>>>>>>>>>>
    On 10/24/2025 2:46 AM, Mikko wrote:
    On 2025-10-23 15:39:13 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>
    On 10/23/2025 5:02 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>> On 2025-10-22 12:39:31 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>>>
    On 10/22/2025 4:23 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>>> On 2025-10-21 15:11:19 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>>>>>
    On 10/21/2025 4:31 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>>>>> On 2025-10-20 16:24:46 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>>>>>>>
    On 10/20/2025 3:55 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>>> On 2025-10-19 15:03:34 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>>>>>>>>>
    On 10/19/2025 3:44 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>> On 2025-10-18 10:58:15 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    On 10/18/2025 4:30 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    That is not a sense of "proof". >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    That is the correct way to do a proof. >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    A way to do is not a sense. >>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    The conventional way to do proofs concludes that >>>>>>>>>>>>>>>>>>>>>>>>>>>>> within its rules if the Moon is made from green >>>>>>>>>>>>>>>>>>>>>>>>>>>>> cheese and the Moon is not made from green cheese >>>>>>>>>>>>>>>>>>>>>>>>>>>>> this proves that Donald Trump is the Lord and savior Jesus Christ.

    Right, and the empirical falct that nobody has verified all of
    1. the Moon is made from green cheese >>>>>>>>>>>>>>>>>>>>>>>>>>>> 2. the Moon is not made from grenn cheese >>>>>>>>>>>>>>>>>>>>>>>>>>>> 3. Donald Trump is not the Lord and saviour Jesus Christ
    at the same time supports the idea that the conventiona wya to
    do proofs is correct and trustworthy. >>>>>>>>>>>>>>>>>>>>>>>>>>>
    When we require that correct reasoning is only semantic
    logical entailment from basic facts the Principle of
    Explosion ceases to exist. >>>>>>>>>>>>>>>>>>>>>>>>>>
    Only if you exclude from "correct reasioning" some reasning that
    actually is correct.

    There is no counter-example that can possibly exist >>>>>>>>>>>>>>>>>>>>>>>>> that can show there are any gaps in the body of human >>>>>>>>>>>>>>>>>>>>>>>>> knowledge that can be expressed in language that begins
    with a consistent set of basic facts and only applies >>>>>>>>>>>>>>>>>>>>>>>>> semantic logical entailment to these facts. >>>>>>>>>>>>>>>>>>>>>>>>
    There is no language that begins with a consistent set of basic facts
    and only applies semantic logical entailment to those facts and can
    express all of human knowledge without any gaps. >>>>>>>>>>>>>>>>>>>>>>>
    A subset of formalized English does do this. >>>>>>>>>>>>>>>>>>>>>>
    Nobody has ever presented such subset. >>>>>>>>>>>>>>>>>>>>>
    ChatGPT rewords my words into that subset. >>>>>>>>>>>>>>>>>>>>
    Your words have much less material than all human knowledge without
    any gaps. Therefore it is impossible to verify that you have told
    every necessary word to it.

    Categorically exhaustive reasoning reverse-engineers >>>>>>>>>>>>>>>>>>> the required architecture of the system. Wittgenstein >>>>>>>>>>>>>>>>>>> did this on Gödel https://www.liarparadox.org/ Wittgenstein.pdf
    and he was so succinct eliminate the convoluted mess of Gödel
    numbers that people mistook his succinct analysis as simplistic
    not understanding what Gödel was really saying. >>>>>>>>>>>>>>>>>>
    Yes, an expectable consequence of ignoring essential aspects is
    not understanding.

    Gödel numbers are merely the ridiculously convoluted >>>>>>>>>>>>>>>>> way that Gödel added the functionality of this simple >>>>>>>>>>>>>>>>> operator: ⊢ to a formal language woefully too inexpressive. >>>>>>>>>>>>>>>>
    Natural numbers are one of the best understood topics of mathematics.
    Therefore restricting the assumptions to natural numbers provdes the
    basis for the most interesting result.

    Of course one can ask whether one can prove a similar theorem about
    finite strings. It is much simpler to express claims and proofs as
    fimite strings as thats how they are usually expressed anyway. But
    that requires that one first constructs a theory of finite strings.

    But we can show a direct one-to-one mapping of finite strings in a
    finite alphabet to natural numbers (it just becomes the notational base
    for the numbers).

    That's true, and I would prefer that rather than Gödel's mapping. But
    the proof of Gödel's theorem is simpler if the number of symbols in
    the alphabet is prime even if that would mean that some of the symbols
    are unused.

    Gödel numbers hide this simple essence behind a convoluted mess: >>>>>>>>>>>>> G := (F ⊬ G)

    No, that is not the sentence. For Gödel's purposes it was important to
    cover languages that have no symbol for ':=' or '⊬'. >>>>>>>>>>>>
    But that is irrelevant to my preference for the numbering method. >>>>>>>>>>>
    His result is supposed to apply to any formal language
    as expressive as PA or above.

    Yes, includint PA itself. Therefore his proof could not assume any >>>>>>>>>> symbols other than those of PA. A proof that requires other symbols >>>>>>>>>> proves nothing about PA.

    If he started with Minimal Type Theory and the understanding >>>>>>>>> that cycles in the evaluation sequence of expressions indicate >>>>>>>>> that they are semantically unsound we would have never heard >>>>>>>>> of Incompleteness.

    Sooner or later someone would have found incompleteness anyway. >>>>>>>
    Incompleteness is a misconception nothing more.

    No, it is a part of analytic knowledge. You have not shown any error >>>>>> in Gödel's and other proofs that every theory of natural numbers is >>>>>> incomplete. All you have shown is that you don't like the fact and >>>>>> some rationale for your dislike.

    His incompleteness applies to PA or above, thus
    applies to MTT.

    You have never shown the full theory of MTT so hard to tell. But if >>>>>> MTT is consistent it should be provably incomplete.

    I showed the entire language specification you just
    didn't pay attention.

    Irrelevant to my comment that some parts of the theory are not yet shown. >>>
    Its exactly the same thing a FOL with additional operators
    to make it much more expressive. For example it can directly
    expression any HOL logic expression.

    You mean it includes "tertium non datur" and "the principle of explosion"? >>
    I give an example.

    Thank's but the definition of the theory is still missing.

    The theory is entirely expressed by the conventional
    meaning of it operators and the syntax that I provided.

    They don't express any theory. Shall we conclude that there is no theory?
    --
    Mikko

    --- Synchronet 3.21a-Linux NewsLink 1.2
  • From Mikko@[email protected] to comp.theory on Tue Nov 4 11:51:54 2025
    From Newsgroup: comp.theory

    On 2025-11-04 00:32:51 +0000, olcott said:

    On 11/3/2025 6:29 PM, Tristan Wibberley wrote:
    On 03/11/2025 23:40, olcott wrote:

    [the snip of the century]

    G := (F ⊬ G)
    G is defined as unprovable from F.
    That is the ordinary "defined as" operator.

    That's "definitionally reduces to", I think. If "(F ⊬ G)" is not
    ultimately defined then G can still be not defined.

    "define" /is/ a funny word isn't it? Several fields have mixed it up in
    different ways.


    ?- G = not(provable(F, G)).
    G = not(provable(F, G)).

    ?- unify_with_occurs_check(G, not(provable(F, G))).
    false.

    The point is that Prolog determines it is semantically
    unsound because it has a cycle in the directed graph of
    its evaluation sequence.

    Prolog does not deremine it semantically unsound. The library predicate unify_with_occurs_check is required fail if the unification would produce
    a loop as a special feature of that feature. It is there for programmers
    that want to ensure that they don't create loops were they don't want
    loops. A loop in a data structure is a syntactic feature. There is no
    semantic considerations in unify_with_occurs_check.
    --
    Mikko

    --- Synchronet 3.21a-Linux NewsLink 1.2
  • From Mikko@[email protected] to comp.theory on Tue Nov 4 11:53:38 2025
    From Newsgroup: comp.theory

    On 2025-11-03 23:41:35 +0000, olcott said:

    On 11/2/2025 6:43 AM, Mikko wrote:
    On 2025-11-01 13:52:41 +0000, olcott said:

    On 11/1/2025 4:16 AM, Mikko wrote:
    On 2025-10-31 12:18:16 +0000, olcott said:

    On 10/31/2025 6:10 AM, Mikko wrote:
    On 2025-10-30 13:01:34 +0000, olcott said:

    On 10/30/2025 5:44 AM, Mikko wrote:
    On 2025-10-29 16:26:58 +0000, olcott said:

    On 10/29/2025 5:53 AM, Mikko wrote:
    On 2025-10-29 01:57:07 +0000, Richard Damon said:

    On 10/28/25 11:12 AM, olcott wrote:
    On 10/28/2025 4:58 AM, Mikko wrote:
    On 2025-10-28 01:22:21 +0000, Richard Damon said:

    On 10/27/25 5:45 AM, Mikko wrote:
    On 2025-10-26 17:57:16 +0000, Richard Damon said: >>>>>>>>>>>>>>>
    On 10/26/25 7:44 AM, Mikko wrote:
    On 2025-10-25 19:57:19 +0000, olcott said:

    On 10/25/2025 6:59 AM, Mikko wrote:
    On 2025-10-24 17:37:43 +0000, olcott said: >>>>>>>>>>>>>>>>>>>
    On 10/24/2025 2:46 AM, Mikko wrote:
    On 2025-10-23 15:39:13 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>>
    On 10/23/2025 5:02 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>> On 2025-10-22 12:39:31 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>>>>
    On 10/22/2025 4:23 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>>>> On 2025-10-21 15:11:19 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>>>>>>
    On 10/21/2025 4:31 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>> On 2025-10-20 16:24:46 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>>>>>>>>
    On 10/20/2025 3:55 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>>>> On 2025-10-19 15:03:34 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    On 10/19/2025 3:44 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> On 2025-10-18 10:58:15 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    On 10/18/2025 4:30 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    That is not a sense of "proof". >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    That is the correct way to do a proof. >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    A way to do is not a sense. >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    The conventional way to do proofs concludes that >>>>>>>>>>>>>>>>>>>>>>>>>>>>>> within its rules if the Moon is made from green >>>>>>>>>>>>>>>>>>>>>>>>>>>>>> cheese and the Moon is not made from green cheese
    this proves that Donald Trump is the Lord and savior Jesus Christ.

    Right, and the empirical falct that nobody has verified all of
    1. the Moon is made from green cheese >>>>>>>>>>>>>>>>>>>>>>>>>>>>> 2. the Moon is not made from grenn cheese >>>>>>>>>>>>>>>>>>>>>>>>>>>>> 3. Donald Trump is not the Lord and saviour Jesus Christ
    at the same time supports the idea that the conventiona wya to
    do proofs is correct and trustworthy. >>>>>>>>>>>>>>>>>>>>>>>>>>>>
    When we require that correct reasoning is only semantic
    logical entailment from basic facts the Principle of
    Explosion ceases to exist. >>>>>>>>>>>>>>>>>>>>>>>>>>>
    Only if you exclude from "correct reasioning" some reasning that
    actually is correct.

    There is no counter-example that can possibly exist >>>>>>>>>>>>>>>>>>>>>>>>>> that can show there are any gaps in the body of human
    knowledge that can be expressed in language that begins
    with a consistent set of basic facts and only applies
    semantic logical entailment to these facts. >>>>>>>>>>>>>>>>>>>>>>>>>
    There is no language that begins with a consistent set of basic facts
    and only applies semantic logical entailment to those facts and can
    express all of human knowledge without any gaps. >>>>>>>>>>>>>>>>>>>>>>>>
    A subset of formalized English does do this. >>>>>>>>>>>>>>>>>>>>>>>
    Nobody has ever presented such subset. >>>>>>>>>>>>>>>>>>>>>>
    ChatGPT rewords my words into that subset. >>>>>>>>>>>>>>>>>>>>>
    Your words have much less material than all human knowledge without
    any gaps. Therefore it is impossible to verify that you have told
    every necessary word to it.

    Categorically exhaustive reasoning reverse-engineers >>>>>>>>>>>>>>>>>>>> the required architecture of the system. Wittgenstein >>>>>>>>>>>>>>>>>>>> did this on Gödel https://www.liarparadox.org/ Wittgenstein.pdf
    and he was so succinct eliminate the convoluted mess of Gödel
    numbers that people mistook his succinct analysis as simplistic
    not understanding what Gödel was really saying. >>>>>>>>>>>>>>>>>>>
    Yes, an expectable consequence of ignoring essential aspects is
    not understanding.

    Gödel numbers are merely the ridiculously convoluted >>>>>>>>>>>>>>>>>> way that Gödel added the functionality of this simple >>>>>>>>>>>>>>>>>> operator: ⊢ to a formal language woefully too inexpressive.

    Natural numbers are one of the best understood topics of mathematics.
    Therefore restricting the assumptions to natural numbers provdes the
    basis for the most interesting result.

    Of course one can ask whether one can prove a similar theorem about
    finite strings. It is much simpler to express claims and proofs as
    fimite strings as thats how they are usually expressed anyway. But
    that requires that one first constructs a theory of finite strings.

    But we can show a direct one-to-one mapping of finite strings in a
    finite alphabet to natural numbers (it just becomes the notational base
    for the numbers).

    That's true, and I would prefer that rather than Gödel's mapping. But
    the proof of Gödel's theorem is simpler if the number of symbols in
    the alphabet is prime even if that would mean that some of the symbols
    are unused.

    Godel's Theorem doesn't need the number of symbols to be prime, it uses
    prime numbers to number the symbols, and prime powers for the position.

    And consequently Gödel's example of an undecidable formula is more complex
    than needed. Which doesn't really matter as the complex details can be
    hidden behind definitions.


    ...We are therefore confronted with a proposition which asserts its own
    unprovability. 15 ...
    (Gödel 1931:40-41)

    Which is a statement in the meta-logic, not in the logic. >>>>>>>>>>>
    G asserts it isn't provable, but asserting that there can be no number
    which can encode a proof of itself.

    This statement MUST be either true of false.

    It's actually both.

    It is a lie that it is even a statement.
    I could equally say this statement is true or false: "What time is it?"

    You cant say that in the language of Peano arithmetic.

    PA is ridiculously inexpressive so that the key
    essence is hidden bu far too many purely extraneous
    details.

    PA can express everything we need to know about natural numbers.
    Complexities can be hidden behind definitions.

    MTT can express anything that we way to know about
    formal expressions of language.

     Since Incompleteness applies to PA OR ABOVE.
    I go with above.

    You may need to rewrite the proof for the language of the theory you >>>>>> want to use, especially if you don't want to use the ordinary logic. >>>>>
    All that I did was get rid of the purely extraneous
    complexity of Gödel's G

    All that complexity is in Gödel's proof. You need to rewrite the proof >>>> and verify its equivalence to the original if you want to ger rid of
    the complexity.

    But the complexity affects only the verification of the correctness of >>>> the proof. The meaning of the conclusion is simple.

    *Gödel already said that it is equivalent*

    Not about my comment.

    I am not going to do any useless busy work.

    That's a good idea. You have already done more than enough.
    --
    Mikko

    --- Synchronet 3.21a-Linux NewsLink 1.2
  • From Mikko@[email protected] to comp.theory on Tue Nov 4 11:56:17 2025
    From Newsgroup: comp.theory

    On 2025-11-03 23:45:57 +0000, olcott said:

    On 11/2/2025 6:45 AM, Mikko wrote:
    On 2025-11-01 13:54:09 +0000, olcott said:

    On 11/1/2025 4:18 AM, Mikko wrote:
    On 2025-10-31 12:20:13 +0000, olcott said:

    On 10/31/2025 6:15 AM, Mikko wrote:
    On 2025-10-30 13:03:23 +0000, olcott said:

    On 10/30/2025 5:50 AM, Mikko wrote:
    On 2025-10-29 16:25:00 +0000, olcott said:

    On 10/29/2025 5:45 AM, Mikko wrote:
    On 2025-10-28 15:12:29 +0000, olcott said:

    On 10/28/2025 4:58 AM, Mikko wrote:
    On 2025-10-28 01:22:21 +0000, Richard Damon said:

    On 10/27/25 5:45 AM, Mikko wrote:
    On 2025-10-26 17:57:16 +0000, Richard Damon said:

    On 10/26/25 7:44 AM, Mikko wrote:
    On 2025-10-25 19:57:19 +0000, olcott said:

    On 10/25/2025 6:59 AM, Mikko wrote:
    On 2025-10-24 17:37:43 +0000, olcott said: >>>>>>>>>>>>>>>>>>
    On 10/24/2025 2:46 AM, Mikko wrote:
    On 2025-10-23 15:39:13 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>
    On 10/23/2025 5:02 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>> On 2025-10-22 12:39:31 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>>>
    On 10/22/2025 4:23 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>>> On 2025-10-21 15:11:19 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>>>>>
    On 10/21/2025 4:31 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>>>>> On 2025-10-20 16:24:46 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>>>>>>>
    On 10/20/2025 3:55 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>>> On 2025-10-19 15:03:34 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>>>>>>>>>
    On 10/19/2025 3:44 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>> On 2025-10-18 10:58:15 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    On 10/18/2025 4:30 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    That is not a sense of "proof". >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    That is the correct way to do a proof. >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    A way to do is not a sense. >>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    The conventional way to do proofs concludes that >>>>>>>>>>>>>>>>>>>>>>>>>>>>> within its rules if the Moon is made from green >>>>>>>>>>>>>>>>>>>>>>>>>>>>> cheese and the Moon is not made from green cheese >>>>>>>>>>>>>>>>>>>>>>>>>>>>> this proves that Donald Trump is the Lord and savior Jesus Christ.

    Right, and the empirical falct that nobody has verified all of
    1. the Moon is made from green cheese >>>>>>>>>>>>>>>>>>>>>>>>>>>> 2. the Moon is not made from grenn cheese >>>>>>>>>>>>>>>>>>>>>>>>>>>> 3. Donald Trump is not the Lord and saviour Jesus Christ
    at the same time supports the idea that the conventiona wya to
    do proofs is correct and trustworthy. >>>>>>>>>>>>>>>>>>>>>>>>>>>
    When we require that correct reasoning is only semantic
    logical entailment from basic facts the Principle of
    Explosion ceases to exist. >>>>>>>>>>>>>>>>>>>>>>>>>>
    Only if you exclude from "correct reasioning" some reasning that
    actually is correct.

    There is no counter-example that can possibly exist >>>>>>>>>>>>>>>>>>>>>>>>> that can show there are any gaps in the body of human >>>>>>>>>>>>>>>>>>>>>>>>> knowledge that can be expressed in language that begins
    with a consistent set of basic facts and only applies >>>>>>>>>>>>>>>>>>>>>>>>> semantic logical entailment to these facts. >>>>>>>>>>>>>>>>>>>>>>>>
    There is no language that begins with a consistent set of basic facts
    and only applies semantic logical entailment to those facts and can
    express all of human knowledge without any gaps. >>>>>>>>>>>>>>>>>>>>>>>
    A subset of formalized English does do this. >>>>>>>>>>>>>>>>>>>>>>
    Nobody has ever presented such subset. >>>>>>>>>>>>>>>>>>>>>
    ChatGPT rewords my words into that subset. >>>>>>>>>>>>>>>>>>>>
    Your words have much less material than all human knowledge without
    any gaps. Therefore it is impossible to verify that you have told
    every necessary word to it.

    Categorically exhaustive reasoning reverse-engineers >>>>>>>>>>>>>>>>>>> the required architecture of the system. Wittgenstein >>>>>>>>>>>>>>>>>>> did this on Gödel https://www.liarparadox.org/ Wittgenstein.pdf
    and he was so succinct eliminate the convoluted mess of Gödel
    numbers that people mistook his succinct analysis as simplistic
    not understanding what Gödel was really saying. >>>>>>>>>>>>>>>>>>
    Yes, an expectable consequence of ignoring essential aspects is
    not understanding.

    Gödel numbers are merely the ridiculously convoluted >>>>>>>>>>>>>>>>> way that Gödel added the functionality of this simple >>>>>>>>>>>>>>>>> operator: ⊢ to a formal language woefully too inexpressive. >>>>>>>>>>>>>>>>
    Natural numbers are one of the best understood topics of mathematics.
    Therefore restricting the assumptions to natural numbers provdes the
    basis for the most interesting result.

    Of course one can ask whether one can prove a similar theorem about
    finite strings. It is much simpler to express claims and proofs as
    fimite strings as thats how they are usually expressed anyway. But
    that requires that one first constructs a theory of finite strings.

    But we can show a direct one-to-one mapping of finite strings in a
    finite alphabet to natural numbers (it just becomes the notational base
    for the numbers).

    That's true, and I would prefer that rather than Gödel's mapping. But
    the proof of Gödel's theorem is simpler if the number of symbols in
    the alphabet is prime even if that would mean that some of the symbols
    are unused.

    Godel's Theorem doesn't need the number of symbols to be prime, it uses
    prime numbers to number the symbols, and prime powers for the position.

    And consequently Gödel's example of an undecidable formula is more complex
    than needed. Which doesn't really matter as the complex details can be
    hidden behind definitions.


    ...We are therefore confronted with a proposition which asserts its own
    unprovability. 15 ...
    (Gödel 1931:40-41)

    G := (F ⊬ G) // Olcott's Minimal Type Theory
    https://philarchive.org/archive/PETMTT-4v2 // YACC BNF of MTT >>>>>>>>>>>
    ?- G = not(provable(F, G)).
    G = not(provable(F, G)).

    ?- unify_with_occurs_check(G, not(provable(F, G))).
    false.

    Gödel, Kurt 1931.
    On Formally Undecidable Propositions of Principia Mathematica And >>>>>>>>>>> Related Systems

    Nice to see that you don't disagree.

    In other words you agree that I proved 1931 Incompleteness is incorrect.
    Gödel's G when boiled down to its barest essence is simply semantically
    unsound the same way the Liar Paradox is unsound.

    As yousually your "in other words" is a lie. Existence of a simpler proof
    does not make the original one incorrect.

    My words are true within your words:
       "Nice to see that you don't disagree."
    If you didn't mean that then you should not have said that.

    I did not say nor mean "you did not disagree with anything". The usual >>>>>> meaning of what I said is that you don't disagree with what I said in >>>>>> my previous message about the complexity of Gödel's sentence.

    The complexity of Gödel's sentence is nuts.
    G := (F ⊬ G) Just detect the cycle in this
    and Gödel is refuted.

    Nice to see that you still don't disagree with my comment about the
    complexity of Gödel's sentence.

    Yet I absolutely do disagree.

    OK, you think Gödel's numbering scheme is simple.

    ...We are therefore confronted with a proposition which asserts its own unprovability. 15 ... (Gödel 1931:40-41)

    It totally hides the details that proof his theorem is unsound.

    You have never revealed any unsound detail of the proof, not even
    whether it uses a false premise or an invalid inference.
    --
    Mikko

    --- Synchronet 3.21a-Linux NewsLink 1.2
  • From olcott@[email protected] to comp.theory on Tue Nov 4 10:29:40 2025
    From Newsgroup: comp.theory

    On 11/4/2025 3:46 AM, Mikko wrote:
    On 2025-11-03 23:40:06 +0000, olcott said:

    On 11/2/2025 6:41 AM, Mikko wrote:
    On 2025-11-01 13:50:53 +0000, olcott said:

    On 11/1/2025 4:10 AM, Mikko wrote:
    On 2025-10-31 12:09:48 +0000, olcott said:

    On 10/31/2025 6:02 AM, Mikko wrote:
    On 2025-10-30 12:54:57 +0000, olcott said:

    On 10/30/2025 5:37 AM, Mikko wrote:
    On 2025-10-29 16:22:11 +0000, olcott said:

    On 10/29/2025 5:43 AM, Mikko wrote:
    On 2025-10-28 15:07:18 +0000, olcott said:

    On 10/28/2025 4:54 AM, Mikko wrote:
    On 2025-10-27 13:56:21 +0000, olcott said:

    On 10/27/2025 4:45 AM, Mikko wrote:
    On 2025-10-26 17:57:16 +0000, Richard Damon said: >>>>>>>>>>>>>>>
    On 10/26/25 7:44 AM, Mikko wrote:
    On 2025-10-25 19:57:19 +0000, olcott said:

    On 10/25/2025 6:59 AM, Mikko wrote:
    On 2025-10-24 17:37:43 +0000, olcott said: >>>>>>>>>>>>>>>>>>>
    On 10/24/2025 2:46 AM, Mikko wrote:
    On 2025-10-23 15:39:13 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>>
    On 10/23/2025 5:02 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>> On 2025-10-22 12:39:31 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>>>>
    On 10/22/2025 4:23 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>>>> On 2025-10-21 15:11:19 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>>>>>>
    On 10/21/2025 4:31 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>> On 2025-10-20 16:24:46 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>>>>>>>>
    On 10/20/2025 3:55 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>>>> On 2025-10-19 15:03:34 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    On 10/19/2025 3:44 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> On 2025-10-18 10:58:15 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    On 10/18/2025 4:30 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    That is not a sense of "proof". >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    That is the correct way to do a proof. >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    A way to do is not a sense. >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    The conventional way to do proofs >>>>>>>>>>>>>>>>>>>>>>>>>>>>>> concludes that
    within its rules if the Moon is made from >>>>>>>>>>>>>>>>>>>>>>>>>>>>>> green
    cheese and the Moon is not made from green >>>>>>>>>>>>>>>>>>>>>>>>>>>>>> cheese
    this proves that Donald Trump is the Lord >>>>>>>>>>>>>>>>>>>>>>>>>>>>>> and savior Jesus Christ. >>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    Right, and the empirical falct that nobody >>>>>>>>>>>>>>>>>>>>>>>>>>>>> has verified all of
    1. the Moon is made from green cheese >>>>>>>>>>>>>>>>>>>>>>>>>>>>> 2. the Moon is not made from grenn cheese >>>>>>>>>>>>>>>>>>>>>>>>>>>>> 3. Donald Trump is not the Lord and saviour >>>>>>>>>>>>>>>>>>>>>>>>>>>>> Jesus Christ
    at the same time supports the idea that the >>>>>>>>>>>>>>>>>>>>>>>>>>>>> conventiona wya to
    do proofs is correct and trustworthy. >>>>>>>>>>>>>>>>>>>>>>>>>>>>
    When we require that correct reasoning is >>>>>>>>>>>>>>>>>>>>>>>>>>>> only semantic
    logical entailment from basic facts the >>>>>>>>>>>>>>>>>>>>>>>>>>>> Principle of
    Explosion ceases to exist. >>>>>>>>>>>>>>>>>>>>>>>>>>>
    Only if you exclude from "correct reasioning" >>>>>>>>>>>>>>>>>>>>>>>>>>> some reasning that
    actually is correct.

    There is no counter-example that can possibly >>>>>>>>>>>>>>>>>>>>>>>>>> exist
    that can show there are any gaps in the body >>>>>>>>>>>>>>>>>>>>>>>>>> of human
    knowledge that can be expressed in language >>>>>>>>>>>>>>>>>>>>>>>>>> that begins
    with a consistent set of basic facts and only >>>>>>>>>>>>>>>>>>>>>>>>>> applies
    semantic logical entailment to these facts. >>>>>>>>>>>>>>>>>>>>>>>>>
    There is no language that begins with a >>>>>>>>>>>>>>>>>>>>>>>>> consistent set of basic facts >>>>>>>>>>>>>>>>>>>>>>>>> and only applies semantic logical entailment to >>>>>>>>>>>>>>>>>>>>>>>>> those facts and can
    express all of human knowledge without any gaps. >>>>>>>>>>>>>>>>>>>>>>>>
    A subset of formalized English does do this. >>>>>>>>>>>>>>>>>>>>>>>
    Nobody has ever presented such subset. >>>>>>>>>>>>>>>>>>>>>>
    ChatGPT rewords my words into that subset. >>>>>>>>>>>>>>>>>>>>>
    Your words have much less material than all human >>>>>>>>>>>>>>>>>>>>> knowledge without
    any gaps. Therefore it is impossible to verify that >>>>>>>>>>>>>>>>>>>>> you have told
    every necessary word to it.

    Categorically exhaustive reasoning reverse-engineers >>>>>>>>>>>>>>>>>>>> the required architecture of the system. Wittgenstein >>>>>>>>>>>>>>>>>>>> did this on Gödel https://www.liarparadox.org/ >>>>>>>>>>>>>>>>>>>> Wittgenstein.pdf
    and he was so succinct eliminate the convoluted mess >>>>>>>>>>>>>>>>>>>> of Gödel
    numbers that people mistook his succinct analysis as >>>>>>>>>>>>>>>>>>>> simplistic
    not understanding what Gödel was really saying. >>>>>>>>>>>>>>>>>>>
    Yes, an expectable consequence of ignoring essential >>>>>>>>>>>>>>>>>>> aspects is
    not understanding.

    Gödel numbers are merely the ridiculously convoluted >>>>>>>>>>>>>>>>>> way that Gödel added the functionality of this simple >>>>>>>>>>>>>>>>>> operator: ⊢ to a formal language woefully too >>>>>>>>>>>>>>>>>> inexpressive.

    Natural numbers are one of the best understood topics >>>>>>>>>>>>>>>>> of mathematics.
    Therefore restricting the assumptions to natural >>>>>>>>>>>>>>>>> numbers provdes the
    basis for the most interesting result.

    Of course one can ask whether one can prove a similar >>>>>>>>>>>>>>>>> theorem about
    finite strings. It is much simpler to express claims >>>>>>>>>>>>>>>>> and proofs as
    fimite strings as thats how they are usually expressed >>>>>>>>>>>>>>>>> anyway. But
    that requires that one first constructs a theory of >>>>>>>>>>>>>>>>> finite strings.

    But we can show a direct one-to-one mapping of finite >>>>>>>>>>>>>>>> strings in a finite alphabet to natural numbers (it just >>>>>>>>>>>>>>>> becomes the notational base for the numbers).

    That's true, and I would prefer that rather than Gödel's >>>>>>>>>>>>>>> mapping. But
    the proof of Gödel's theorem is simpler if the number of >>>>>>>>>>>>>>> symbols in
    the alphabet is prime even if that would mean that some >>>>>>>>>>>>>>> of the symbols
    are unused.

    Gödel numbers hide this simple essence behind a convoluted >>>>>>>>>>>>>> mess:
    G := (F ⊬ G)

    No, that is not the sentence. For Gödel's purposes it was >>>>>>>>>>>>> important to
    cover languages that have no symbol for ':=' or '⊬'. >>>>>>>>>>>>>
    But that is irrelevant to my preference for the numbering >>>>>>>>>>>>> method.

    His result is supposed to apply to any formal language >>>>>>>>>>>> as expressive as PA or above.

    Yes, includint PA itself. Therefore his proof could not >>>>>>>>>>> assume any
    symbols other than those of PA. A proof that requires other >>>>>>>>>>> symbols
    proves nothing about PA.

    If he started with Minimal Type Theory and the understanding >>>>>>>>>> that cycles in the evaluation sequence of expressions indicate >>>>>>>>>> that they are semantically unsound we would have never heard >>>>>>>>>> of Incompleteness.

    Sooner or later someone would have found incompleteness anyway. >>>>>>>>
    Incompleteness is a misconception nothing more.

    No, it is a part of analytic knowledge. You have not shown any error >>>>>>> in Gödel's and other proofs that every theory of natural numbers is >>>>>>> incomplete. All you have shown is that you don't like the fact and >>>>>>> some rationale for your dislike.

    His incompleteness applies to PA or above, thus
    applies to MTT.

    You have never shown the full theory of MTT so hard to tell. But if >>>>>>> MTT is consistent it should be provably incomplete.

    I showed the entire language specification you just
    didn't pay attention.

    Irrelevant to my comment that some parts of the theory are not yet
    shown.

    Its exactly the same thing a FOL with additional operators
    to make it much more expressive. For example it can directly
    expression any HOL logic expression.

    You mean it includes "tertium non datur" and "the principle of
    explosion"?

    I give an example.

    Thank's but the definition of the theory is still missing.

    The theory is entirely expressed by the conventional
    meaning of it operators and the syntax that I provided.

    They don't express any theory. Shall we conclude that there is no theory?



    In other words you are trying to get away with
    saying that you have no idea what this means: A ↔ B ???

    https://en.wikipedia.org/wiki/List_of_logic_symbols https://philarchive.org/archive/PETMTT-4v2

    What more is there to any math theory besides
    the meaning of its symbols combined with its syntax
    (both of which I just provided) ???
    --
    Copyright 2025 Olcott "Talent hits a target no one else can hit; Genius
    hits a target no one else can see." Arthur Schopenhauer
    --- Synchronet 3.21a-Linux NewsLink 1.2
  • From olcott@[email protected] to comp.theory on Tue Nov 4 11:45:04 2025
    From Newsgroup: comp.theory

    On 11/4/2025 3:51 AM, Mikko wrote:
    On 2025-11-04 00:32:51 +0000, olcott said:

    On 11/3/2025 6:29 PM, Tristan Wibberley wrote:
    On 03/11/2025 23:40, olcott wrote:

    [the snip of the century]

    G := (F ⊬ G)
    G is defined as unprovable from F.
    That is the ordinary "defined as" operator.

    That's "definitionally reduces to", I think. If "(F ⊬ G)" is not
    ultimately defined then G can still be not defined.

    "define" /is/ a funny word isn't it? Several fields have mixed it up in
    different ways.


    ?- G = not(provable(F, G)).
    G = not(provable(F, G)).

    ?- unify_with_occurs_check(G, not(provable(F, G))).
    false.

    The point is that Prolog determines it is semantically
    unsound because it has a cycle in the directed graph of
    its evaluation sequence.

    Prolog does not deremine it semantically unsound.

    In other words you think that when the evaluation
    of an expression gets stuck in an infinite loop
    because of the self-reference in this expression
    that this expression is semantically sound?

    The library predicate
    unify_with_occurs_check is required fail if the unification would produce
    a loop as a special feature of that feature. It is there for programmers
    that want to ensure that they don't create loops were they don't want
    loops. A loop in a data structure is a syntactic feature. There is no semantic considerations in unify_with_occurs_check.


    It is a cycle in the directed graph of the expression's
    evaluation sequence.

    In theorem proving, unification without the occurs
    check can lead to unsound inference. For example,
    the Prolog goal X = f(X) will succeed, binding X
    to a cyclic structure which has no counterpart in
    the Herbrand universe.

    https://en.wikipedia.org/wiki/Occurs_check
    --
    Copyright 2025 Olcott "Talent hits a target no one else can hit; Genius
    hits a target no one else can see." Arthur Schopenhauer
    --- Synchronet 3.21a-Linux NewsLink 1.2
  • From olcott@[email protected] to comp.theory on Tue Nov 4 12:05:34 2025
    From Newsgroup: comp.theory

    On 11/4/2025 3:56 AM, Mikko wrote:
    On 2025-11-03 23:45:57 +0000, olcott said:

    On 11/2/2025 6:45 AM, Mikko wrote:
    On 2025-11-01 13:54:09 +0000, olcott said:

    On 11/1/2025 4:18 AM, Mikko wrote:
    On 2025-10-31 12:20:13 +0000, olcott said:

    On 10/31/2025 6:15 AM, Mikko wrote:
    On 2025-10-30 13:03:23 +0000, olcott said:

    On 10/30/2025 5:50 AM, Mikko wrote:
    On 2025-10-29 16:25:00 +0000, olcott said:

    On 10/29/2025 5:45 AM, Mikko wrote:
    On 2025-10-28 15:12:29 +0000, olcott said:

    On 10/28/2025 4:58 AM, Mikko wrote:
    On 2025-10-28 01:22:21 +0000, Richard Damon said:

    On 10/27/25 5:45 AM, Mikko wrote:
    On 2025-10-26 17:57:16 +0000, Richard Damon said: >>>>>>>>>>>>>>>
    On 10/26/25 7:44 AM, Mikko wrote:
    On 2025-10-25 19:57:19 +0000, olcott said:

    On 10/25/2025 6:59 AM, Mikko wrote:
    On 2025-10-24 17:37:43 +0000, olcott said: >>>>>>>>>>>>>>>>>>>
    On 10/24/2025 2:46 AM, Mikko wrote:
    On 2025-10-23 15:39:13 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>>
    On 10/23/2025 5:02 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>> On 2025-10-22 12:39:31 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>>>>
    On 10/22/2025 4:23 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>>>> On 2025-10-21 15:11:19 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>>>>>>
    On 10/21/2025 4:31 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>> On 2025-10-20 16:24:46 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>>>>>>>>
    On 10/20/2025 3:55 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>>>> On 2025-10-19 15:03:34 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    On 10/19/2025 3:44 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> On 2025-10-18 10:58:15 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    On 10/18/2025 4:30 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    That is not a sense of "proof". >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    That is the correct way to do a proof. >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    A way to do is not a sense. >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    The conventional way to do proofs >>>>>>>>>>>>>>>>>>>>>>>>>>>>>> concludes that
    within its rules if the Moon is made from >>>>>>>>>>>>>>>>>>>>>>>>>>>>>> green
    cheese and the Moon is not made from green >>>>>>>>>>>>>>>>>>>>>>>>>>>>>> cheese
    this proves that Donald Trump is the Lord >>>>>>>>>>>>>>>>>>>>>>>>>>>>>> and savior Jesus Christ. >>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    Right, and the empirical falct that nobody >>>>>>>>>>>>>>>>>>>>>>>>>>>>> has verified all of
    1. the Moon is made from green cheese >>>>>>>>>>>>>>>>>>>>>>>>>>>>> 2. the Moon is not made from grenn cheese >>>>>>>>>>>>>>>>>>>>>>>>>>>>> 3. Donald Trump is not the Lord and saviour >>>>>>>>>>>>>>>>>>>>>>>>>>>>> Jesus Christ
    at the same time supports the idea that the >>>>>>>>>>>>>>>>>>>>>>>>>>>>> conventiona wya to
    do proofs is correct and trustworthy. >>>>>>>>>>>>>>>>>>>>>>>>>>>>
    When we require that correct reasoning is >>>>>>>>>>>>>>>>>>>>>>>>>>>> only semantic
    logical entailment from basic facts the >>>>>>>>>>>>>>>>>>>>>>>>>>>> Principle of
    Explosion ceases to exist. >>>>>>>>>>>>>>>>>>>>>>>>>>>
    Only if you exclude from "correct reasioning" >>>>>>>>>>>>>>>>>>>>>>>>>>> some reasning that
    actually is correct.

    There is no counter-example that can possibly >>>>>>>>>>>>>>>>>>>>>>>>>> exist
    that can show there are any gaps in the body >>>>>>>>>>>>>>>>>>>>>>>>>> of human
    knowledge that can be expressed in language >>>>>>>>>>>>>>>>>>>>>>>>>> that begins
    with a consistent set of basic facts and only >>>>>>>>>>>>>>>>>>>>>>>>>> applies
    semantic logical entailment to these facts. >>>>>>>>>>>>>>>>>>>>>>>>>
    There is no language that begins with a >>>>>>>>>>>>>>>>>>>>>>>>> consistent set of basic facts >>>>>>>>>>>>>>>>>>>>>>>>> and only applies semantic logical entailment to >>>>>>>>>>>>>>>>>>>>>>>>> those facts and can
    express all of human knowledge without any gaps. >>>>>>>>>>>>>>>>>>>>>>>>
    A subset of formalized English does do this. >>>>>>>>>>>>>>>>>>>>>>>
    Nobody has ever presented such subset. >>>>>>>>>>>>>>>>>>>>>>
    ChatGPT rewords my words into that subset. >>>>>>>>>>>>>>>>>>>>>
    Your words have much less material than all human >>>>>>>>>>>>>>>>>>>>> knowledge without
    any gaps. Therefore it is impossible to verify that >>>>>>>>>>>>>>>>>>>>> you have told
    every necessary word to it.

    Categorically exhaustive reasoning reverse-engineers >>>>>>>>>>>>>>>>>>>> the required architecture of the system. Wittgenstein >>>>>>>>>>>>>>>>>>>> did this on Gödel https://www.liarparadox.org/ >>>>>>>>>>>>>>>>>>>> Wittgenstein.pdf
    and he was so succinct eliminate the convoluted mess >>>>>>>>>>>>>>>>>>>> of Gödel
    numbers that people mistook his succinct analysis as >>>>>>>>>>>>>>>>>>>> simplistic
    not understanding what Gödel was really saying. >>>>>>>>>>>>>>>>>>>
    Yes, an expectable consequence of ignoring essential >>>>>>>>>>>>>>>>>>> aspects is
    not understanding.

    Gödel numbers are merely the ridiculously convoluted >>>>>>>>>>>>>>>>>> way that Gödel added the functionality of this simple >>>>>>>>>>>>>>>>>> operator: ⊢ to a formal language woefully too >>>>>>>>>>>>>>>>>> inexpressive.

    Natural numbers are one of the best understood topics >>>>>>>>>>>>>>>>> of mathematics.
    Therefore restricting the assumptions to natural >>>>>>>>>>>>>>>>> numbers provdes the
    basis for the most interesting result.

    Of course one can ask whether one can prove a similar >>>>>>>>>>>>>>>>> theorem about
    finite strings. It is much simpler to express claims >>>>>>>>>>>>>>>>> and proofs as
    fimite strings as thats how they are usually expressed >>>>>>>>>>>>>>>>> anyway. But
    that requires that one first constructs a theory of >>>>>>>>>>>>>>>>> finite strings.

    But we can show a direct one-to-one mapping of finite >>>>>>>>>>>>>>>> strings in a finite alphabet to natural numbers (it just >>>>>>>>>>>>>>>> becomes the notational base for the numbers).

    That's true, and I would prefer that rather than Gödel's >>>>>>>>>>>>>>> mapping. But
    the proof of Gödel's theorem is simpler if the number of >>>>>>>>>>>>>>> symbols in
    the alphabet is prime even if that would mean that some >>>>>>>>>>>>>>> of the symbols
    are unused.

    Godel's Theorem doesn't need the number of symbols to be >>>>>>>>>>>>>> prime, it uses prime numbers to number the symbols, and >>>>>>>>>>>>>> prime powers for the position.

    And consequently Gödel's example of an undecidable formula >>>>>>>>>>>>> is more complex
    than needed. Which doesn't really matter as the complex >>>>>>>>>>>>> details can be
    hidden behind definitions.


    ...We are therefore confronted with a proposition which >>>>>>>>>>>> asserts its own unprovability. 15 ...
    (Gödel 1931:40-41)

    G := (F ⊬ G) // Olcott's Minimal Type Theory
    https://philarchive.org/archive/PETMTT-4v2 // YACC BNF of MTT >>>>>>>>>>>>
    ?- G = not(provable(F, G)).
    G = not(provable(F, G)).

    ?- unify_with_occurs_check(G, not(provable(F, G))).
    false.

    Gödel, Kurt 1931.
    On Formally Undecidable Propositions of Principia
    Mathematica And Related Systems

    Nice to see that you don't disagree.

    In other words you agree that I proved 1931 Incompleteness is >>>>>>>>>> incorrect.
    Gödel's G when boiled down to its barest essence is simply >>>>>>>>>> semantically
    unsound the same way the Liar Paradox is unsound.

    As yousually your "in other words" is a lie. Existence of a >>>>>>>>> simpler proof
    does not make the original one incorrect.

    My words are true within your words:
       "Nice to see that you don't disagree."
    If you didn't mean that then you should not have said that.

    I did not say nor mean "you did not disagree with anything". The >>>>>>> usual
    meaning of what I said is that you don't disagree with what I
    said in
    my previous message about the complexity of Gödel's sentence.

    The complexity of Gödel's sentence is nuts.
    G := (F ⊬ G) Just detect the cycle in this
    and Gödel is refuted.

    Nice to see that you still don't disagree with my comment about the
    complexity of Gödel's sentence.

    Yet I absolutely do disagree.

    OK, you think Gödel's numbering scheme is simple.

    ...We are therefore confronted with a proposition which asserts its
    own unprovability. 15 ... (Gödel 1931:40-41)

    It totally hides the details that proof his theorem is unsound.

    You have never revealed any unsound detail of the proof, not even
    whether it uses a false premise or an invalid inference.


    The details of the proof that use Gödel numbers as their
    primary basis hide the underlying semantics about exactly
    what unprovable in F actually means.

    The first incompleteness theorem states that in any
    consistent formal system F within which a certain
    amount of arithmetic can be carried out, there are
    statements of the language of F which can neither
    be proved nor disproved in F.

    https://plato.stanford.edu/entries/goedel-incompleteness/
    Gödel 1936 proof applies to any formal system that is
    as expressive as arithmetic OR BETTER.
    --
    Copyright 2025 Olcott "Talent hits a target no one else can hit; Genius
    hits a target no one else can see." Arthur Schopenhauer
    --- Synchronet 3.21a-Linux NewsLink 1.2
  • From Mikko@[email protected] to comp.theory on Wed Nov 5 12:46:01 2025
    From Newsgroup: comp.theory

    On 2025-11-04 17:45:04 +0000, olcott said:

    On 11/4/2025 3:51 AM, Mikko wrote:
    On 2025-11-04 00:32:51 +0000, olcott said:

    On 11/3/2025 6:29 PM, Tristan Wibberley wrote:
    On 03/11/2025 23:40, olcott wrote:

    [the snip of the century]

    G := (F ⊬ G)
    G is defined as unprovable from F.
    That is the ordinary "defined as" operator.

    That's "definitionally reduces to", I think. If "(F ⊬ G)" is not
    ultimately defined then G can still be not defined.

    "define" /is/ a funny word isn't it? Several fields have mixed it up in >>>> different ways.


    ?- G = not(provable(F, G)).
    G = not(provable(F, G)).

    ?- unify_with_occurs_check(G, not(provable(F, G))).
    false.

    The point is that Prolog determines it is semantically
    unsound because it has a cycle in the directed graph of
    its evaluation sequence.

    Prolog does not deremine it semantically unsound.

    In other words you think that when the evaluation
    of an expression gets stuck in an infinite loop
    because of the self-reference in this expression
    that this expression is semantically sound?

    First of all, it does not stick in an infinite loop if you don't do
    with it anything that would stick in an infinte loop.

    Usually sticking in an infinite loop is not desired or even perimitted
    but there are exceptions. It all depends on the purpose of the program.
    If the prupose is to compute all digits of pi then an infinte loop is
    needed.
    --
    Mikko

    --- Synchronet 3.21a-Linux NewsLink 1.2
  • From Mikko@[email protected] to comp.theory on Wed Nov 5 12:47:25 2025
    From Newsgroup: comp.theory

    On 2025-11-04 16:29:40 +0000, olcott said:

    On 11/4/2025 3:46 AM, Mikko wrote:
    On 2025-11-03 23:40:06 +0000, olcott said:

    On 11/2/2025 6:41 AM, Mikko wrote:
    On 2025-11-01 13:50:53 +0000, olcott said:

    On 11/1/2025 4:10 AM, Mikko wrote:
    On 2025-10-31 12:09:48 +0000, olcott said:

    On 10/31/2025 6:02 AM, Mikko wrote:
    On 2025-10-30 12:54:57 +0000, olcott said:

    On 10/30/2025 5:37 AM, Mikko wrote:
    On 2025-10-29 16:22:11 +0000, olcott said:

    On 10/29/2025 5:43 AM, Mikko wrote:
    On 2025-10-28 15:07:18 +0000, olcott said:

    On 10/28/2025 4:54 AM, Mikko wrote:
    On 2025-10-27 13:56:21 +0000, olcott said:

    On 10/27/2025 4:45 AM, Mikko wrote:
    On 2025-10-26 17:57:16 +0000, Richard Damon said: >>>>>>>>>>>>>>>>
    On 10/26/25 7:44 AM, Mikko wrote:
    On 2025-10-25 19:57:19 +0000, olcott said: >>>>>>>>>>>>>>>>>>
    On 10/25/2025 6:59 AM, Mikko wrote:
    On 2025-10-24 17:37:43 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>
    On 10/24/2025 2:46 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>> On 2025-10-23 15:39:13 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>>>
    On 10/23/2025 5:02 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>>> On 2025-10-22 12:39:31 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>>>>>
    On 10/22/2025 4:23 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>>>>> On 2025-10-21 15:11:19 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>>>>>>>
    On 10/21/2025 4:31 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>>> On 2025-10-20 16:24:46 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>>>>>>>>>
    On 10/20/2025 3:55 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>> On 2025-10-19 15:03:34 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    On 10/19/2025 3:44 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> On 2025-10-18 10:58:15 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    On 10/18/2025 4:30 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    That is not a sense of "proof". >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    That is the correct way to do a proof. >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    A way to do is not a sense. >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    The conventional way to do proofs concludes that
    within its rules if the Moon is made from green >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> cheese and the Moon is not made from green cheese
    this proves that Donald Trump is the Lord and savior Jesus Christ.

    Right, and the empirical falct that nobody has verified all of
    1. the Moon is made from green cheese >>>>>>>>>>>>>>>>>>>>>>>>>>>>>> 2. the Moon is not made from grenn cheese >>>>>>>>>>>>>>>>>>>>>>>>>>>>>> 3. Donald Trump is not the Lord and saviour Jesus Christ
    at the same time supports the idea that the conventiona wya to
    do proofs is correct and trustworthy. >>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    When we require that correct reasoning is only semantic
    logical entailment from basic facts the Principle of
    Explosion ceases to exist. >>>>>>>>>>>>>>>>>>>>>>>>>>>>
    Only if you exclude from "correct reasioning" some reasning that
    actually is correct.

    There is no counter-example that can possibly exist >>>>>>>>>>>>>>>>>>>>>>>>>>> that can show there are any gaps in the body of human
    knowledge that can be expressed in language that begins
    with a consistent set of basic facts and only applies
    semantic logical entailment to these facts. >>>>>>>>>>>>>>>>>>>>>>>>>>
    There is no language that begins with a consistent set of basic facts
    and only applies semantic logical entailment to those facts and can
    express all of human knowledge without any gaps. >>>>>>>>>>>>>>>>>>>>>>>>>
    A subset of formalized English does do this. >>>>>>>>>>>>>>>>>>>>>>>>
    Nobody has ever presented such subset. >>>>>>>>>>>>>>>>>>>>>>>
    ChatGPT rewords my words into that subset. >>>>>>>>>>>>>>>>>>>>>>
    Your words have much less material than all human knowledge without
    any gaps. Therefore it is impossible to verify that you have told
    every necessary word to it.

    Categorically exhaustive reasoning reverse-engineers >>>>>>>>>>>>>>>>>>>>> the required architecture of the system. Wittgenstein >>>>>>>>>>>>>>>>>>>>> did this on Gödel https://www.liarparadox.org/ Wittgenstein.pdf
    and he was so succinct eliminate the convoluted mess of Gödel
    numbers that people mistook his succinct analysis as simplistic
    not understanding what Gödel was really saying. >>>>>>>>>>>>>>>>>>>>
    Yes, an expectable consequence of ignoring essential aspects is
    not understanding.

    Gödel numbers are merely the ridiculously convoluted >>>>>>>>>>>>>>>>>>> way that Gödel added the functionality of this simple >>>>>>>>>>>>>>>>>>> operator: ⊢ to a formal language woefully too inexpressive.

    Natural numbers are one of the best understood topics of mathematics.
    Therefore restricting the assumptions to natural numbers provdes the
    basis for the most interesting result.

    Of course one can ask whether one can prove a similar theorem about
    finite strings. It is much simpler to express claims and proofs as
    fimite strings as thats how they are usually expressed anyway. But
    that requires that one first constructs a theory of finite strings.

    But we can show a direct one-to-one mapping of finite strings in a
    finite alphabet to natural numbers (it just becomes the notational base
    for the numbers).

    That's true, and I would prefer that rather than Gödel's mapping. But
    the proof of Gödel's theorem is simpler if the number of symbols in
    the alphabet is prime even if that would mean that some of the symbols
    are unused.

    Gödel numbers hide this simple essence behind a convoluted mess:
    G := (F ⊬ G)

    No, that is not the sentence. For Gödel's purposes it was important to
    cover languages that have no symbol for ':=' or '⊬'. >>>>>>>>>>>>>>
    But that is irrelevant to my preference for the numbering method.

    His result is supposed to apply to any formal language >>>>>>>>>>>>> as expressive as PA or above.

    Yes, includint PA itself. Therefore his proof could not assume any >>>>>>>>>>>> symbols other than those of PA. A proof that requires other symbols
    proves nothing about PA.

    If he started with Minimal Type Theory and the understanding >>>>>>>>>>> that cycles in the evaluation sequence of expressions indicate >>>>>>>>>>> that they are semantically unsound we would have never heard >>>>>>>>>>> of Incompleteness.

    Sooner or later someone would have found incompleteness anyway. >>>>>>>>>
    Incompleteness is a misconception nothing more.

    No, it is a part of analytic knowledge. You have not shown any error >>>>>>>> in Gödel's and other proofs that every theory of natural numbers is >>>>>>>> incomplete. All you have shown is that you don't like the fact and >>>>>>>> some rationale for your dislike.

    His incompleteness applies to PA or above, thus
    applies to MTT.

    You have never shown the full theory of MTT so hard to tell. But if >>>>>>>> MTT is consistent it should be provably incomplete.

    I showed the entire language specification you just
    didn't pay attention.

    Irrelevant to my comment that some parts of the theory are not yet shown.

    Its exactly the same thing a FOL with additional operators
    to make it much more expressive. For example it can directly
    expression any HOL logic expression.

    You mean it includes "tertium non datur" and "the principle of explosion"? >>>>
    I give an example.

    Thank's but the definition of the theory is still missing.

    The theory is entirely expressed by the conventional
    meaning of it operators and the syntax that I provided.

    They don't express any theory. Shall we conclude that there is no theory?

    In other words you are trying to get away with
    saying that you have no idea what this means: A ↔ B ???

    In other words you are trying to get away with a straw man deception.
    --
    Mikko

    --- Synchronet 3.21a-Linux NewsLink 1.2
  • From Mikko@[email protected] to comp.theory on Wed Nov 5 12:49:11 2025
    From Newsgroup: comp.theory

    On 2025-11-04 18:05:34 +0000, olcott said:

    On 11/4/2025 3:56 AM, Mikko wrote:
    On 2025-11-03 23:45:57 +0000, olcott said:

    On 11/2/2025 6:45 AM, Mikko wrote:
    On 2025-11-01 13:54:09 +0000, olcott said:

    On 11/1/2025 4:18 AM, Mikko wrote:
    On 2025-10-31 12:20:13 +0000, olcott said:

    On 10/31/2025 6:15 AM, Mikko wrote:
    On 2025-10-30 13:03:23 +0000, olcott said:

    On 10/30/2025 5:50 AM, Mikko wrote:
    On 2025-10-29 16:25:00 +0000, olcott said:

    On 10/29/2025 5:45 AM, Mikko wrote:
    On 2025-10-28 15:12:29 +0000, olcott said:

    On 10/28/2025 4:58 AM, Mikko wrote:
    On 2025-10-28 01:22:21 +0000, Richard Damon said:

    On 10/27/25 5:45 AM, Mikko wrote:
    On 2025-10-26 17:57:16 +0000, Richard Damon said: >>>>>>>>>>>>>>>>
    On 10/26/25 7:44 AM, Mikko wrote:
    On 2025-10-25 19:57:19 +0000, olcott said: >>>>>>>>>>>>>>>>>>
    On 10/25/2025 6:59 AM, Mikko wrote:
    On 2025-10-24 17:37:43 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>
    On 10/24/2025 2:46 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>> On 2025-10-23 15:39:13 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>>>
    On 10/23/2025 5:02 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>>> On 2025-10-22 12:39:31 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>>>>>
    On 10/22/2025 4:23 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>>>>> On 2025-10-21 15:11:19 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>>>>>>>
    On 10/21/2025 4:31 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>>> On 2025-10-20 16:24:46 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>>>>>>>>>
    On 10/20/2025 3:55 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>> On 2025-10-19 15:03:34 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    On 10/19/2025 3:44 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> On 2025-10-18 10:58:15 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    On 10/18/2025 4:30 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    That is not a sense of "proof". >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    That is the correct way to do a proof. >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    A way to do is not a sense. >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    The conventional way to do proofs concludes that
    within its rules if the Moon is made from green >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> cheese and the Moon is not made from green cheese
    this proves that Donald Trump is the Lord and savior Jesus Christ.

    Right, and the empirical falct that nobody has verified all of
    1. the Moon is made from green cheese >>>>>>>>>>>>>>>>>>>>>>>>>>>>>> 2. the Moon is not made from grenn cheese >>>>>>>>>>>>>>>>>>>>>>>>>>>>>> 3. Donald Trump is not the Lord and saviour Jesus Christ
    at the same time supports the idea that the conventiona wya to
    do proofs is correct and trustworthy. >>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    When we require that correct reasoning is only semantic
    logical entailment from basic facts the Principle of
    Explosion ceases to exist. >>>>>>>>>>>>>>>>>>>>>>>>>>>>
    Only if you exclude from "correct reasioning" some reasning that
    actually is correct.

    There is no counter-example that can possibly exist >>>>>>>>>>>>>>>>>>>>>>>>>>> that can show there are any gaps in the body of human
    knowledge that can be expressed in language that begins
    with a consistent set of basic facts and only applies
    semantic logical entailment to these facts. >>>>>>>>>>>>>>>>>>>>>>>>>>
    There is no language that begins with a consistent set of basic facts
    and only applies semantic logical entailment to those facts and can
    express all of human knowledge without any gaps. >>>>>>>>>>>>>>>>>>>>>>>>>
    A subset of formalized English does do this. >>>>>>>>>>>>>>>>>>>>>>>>
    Nobody has ever presented such subset. >>>>>>>>>>>>>>>>>>>>>>>
    ChatGPT rewords my words into that subset. >>>>>>>>>>>>>>>>>>>>>>
    Your words have much less material than all human knowledge without
    any gaps. Therefore it is impossible to verify that you have told
    every necessary word to it.

    Categorically exhaustive reasoning reverse-engineers >>>>>>>>>>>>>>>>>>>>> the required architecture of the system. Wittgenstein >>>>>>>>>>>>>>>>>>>>> did this on Gödel https://www.liarparadox.org/ Wittgenstein.pdf
    and he was so succinct eliminate the convoluted mess of Gödel
    numbers that people mistook his succinct analysis as simplistic
    not understanding what Gödel was really saying. >>>>>>>>>>>>>>>>>>>>
    Yes, an expectable consequence of ignoring essential aspects is
    not understanding.

    Gödel numbers are merely the ridiculously convoluted >>>>>>>>>>>>>>>>>>> way that Gödel added the functionality of this simple >>>>>>>>>>>>>>>>>>> operator: ⊢ to a formal language woefully too inexpressive.

    Natural numbers are one of the best understood topics of mathematics.
    Therefore restricting the assumptions to natural numbers provdes the
    basis for the most interesting result.

    Of course one can ask whether one can prove a similar theorem about
    finite strings. It is much simpler to express claims and proofs as
    fimite strings as thats how they are usually expressed anyway. But
    that requires that one first constructs a theory of finite strings.

    But we can show a direct one-to-one mapping of finite strings in a
    finite alphabet to natural numbers (it just becomes the notational base
    for the numbers).

    That's true, and I would prefer that rather than Gödel's mapping. But
    the proof of Gödel's theorem is simpler if the number of symbols in
    the alphabet is prime even if that would mean that some of the symbols
    are unused.

    Godel's Theorem doesn't need the number of symbols to be prime, it uses
    prime numbers to number the symbols, and prime powers for the position.

    And consequently Gödel's example of an undecidable formula is more complex
    than needed. Which doesn't really matter as the complex details can be
    hidden behind definitions.


    ...We are therefore confronted with a proposition which asserts its own
    unprovability. 15 ...
    (Gödel 1931:40-41)

    G := (F ⊬ G) // Olcott's Minimal Type Theory
    https://philarchive.org/archive/PETMTT-4v2 // YACC BNF of MTT >>>>>>>>>>>>>
    ?- G = not(provable(F, G)).
    G = not(provable(F, G)).

    ?- unify_with_occurs_check(G, not(provable(F, G))).
    false.

    Gödel, Kurt 1931.
    On Formally Undecidable Propositions of Principia Mathematica And
    Related Systems

    Nice to see that you don't disagree.

    In other words you agree that I proved 1931 Incompleteness is incorrect.
    Gödel's G when boiled down to its barest essence is simply semantically
    unsound the same way the Liar Paradox is unsound.

    As yousually your "in other words" is a lie. Existence of a simpler proof
    does not make the original one incorrect.

    My words are true within your words:
       "Nice to see that you don't disagree."
    If you didn't mean that then you should not have said that.

    I did not say nor mean "you did not disagree with anything". The usual >>>>>>>> meaning of what I said is that you don't disagree with what I said in >>>>>>>> my previous message about the complexity of Gödel's sentence.

    The complexity of Gödel's sentence is nuts.
    G := (F ⊬ G) Just detect the cycle in this
    and Gödel is refuted.

    Nice to see that you still don't disagree with my comment about the >>>>>> complexity of Gödel's sentence.

    Yet I absolutely do disagree.

    OK, you think Gödel's numbering scheme is simple.

    ...We are therefore confronted with a proposition which asserts its own >>> unprovability. 15 ... (Gödel 1931:40-41)

    It totally hides the details that proof his theorem is unsound.

    You have never revealed any unsound detail of the proof, not even
    whether it uses a false premise or an invalid inference.

    The details of the proof that use Gödel numbers as their
    primary basis hide the underlying semantics about exactly
    what unprovable in F actually means.

    No, they don't. That is very clear ly expressed.
    --
    Mikko

    --- Synchronet 3.21a-Linux NewsLink 1.2
  • From olcott@[email protected] to comp.theory on Wed Nov 5 05:52:40 2025
    From Newsgroup: comp.theory

    On 11/5/2025 4:49 AM, Mikko wrote:
    On 2025-11-04 18:05:34 +0000, olcott said:

    On 11/4/2025 3:56 AM, Mikko wrote:
    On 2025-11-03 23:45:57 +0000, olcott said:

    On 11/2/2025 6:45 AM, Mikko wrote:
    On 2025-11-01 13:54:09 +0000, olcott said:

    On 11/1/2025 4:18 AM, Mikko wrote:
    On 2025-10-31 12:20:13 +0000, olcott said:

    On 10/31/2025 6:15 AM, Mikko wrote:
    On 2025-10-30 13:03:23 +0000, olcott said:

    On 10/30/2025 5:50 AM, Mikko wrote:
    On 2025-10-29 16:25:00 +0000, olcott said:

    On 10/29/2025 5:45 AM, Mikko wrote:
    On 2025-10-28 15:12:29 +0000, olcott said:

    On 10/28/2025 4:58 AM, Mikko wrote:
    On 2025-10-28 01:22:21 +0000, Richard Damon said: >>>>>>>>>>>>>>>
    On 10/27/25 5:45 AM, Mikko wrote:
    On 2025-10-26 17:57:16 +0000, Richard Damon said: >>>>>>>>>>>>>>>>>
    On 10/26/25 7:44 AM, Mikko wrote:
    On 2025-10-25 19:57:19 +0000, olcott said: >>>>>>>>>>>>>>>>>>>
    On 10/25/2025 6:59 AM, Mikko wrote:
    On 2025-10-24 17:37:43 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>>
    On 10/24/2025 2:46 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>> On 2025-10-23 15:39:13 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>>>>
    On 10/23/2025 5:02 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>>>> On 2025-10-22 12:39:31 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>>>>>>
    On 10/22/2025 4:23 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>> On 2025-10-21 15:11:19 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>>>>>>>>
    On 10/21/2025 4:31 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>>>> On 2025-10-20 16:24:46 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    On 10/20/2025 3:55 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> On 2025-10-19 15:03:34 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    On 10/19/2025 3:44 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> On 2025-10-18 10:58:15 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    On 10/18/2025 4:30 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    That is not a sense of "proof". >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    That is the correct way to do a proof. >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    A way to do is not a sense. >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    The conventional way to do proofs >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> concludes that >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> within its rules if the Moon is made >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> from green
    cheese and the Moon is not made from >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> green cheese
    this proves that Donald Trump is the >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> Lord and savior Jesus Christ. >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    Right, and the empirical falct that >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> nobody has verified all of >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> 1. the Moon is made from green cheese >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> 2. the Moon is not made from grenn cheese >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> 3. Donald Trump is not the Lord and >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> saviour Jesus Christ >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> at the same time supports the idea that >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> the conventiona wya to >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> do proofs is correct and trustworthy. >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    When we require that correct reasoning is >>>>>>>>>>>>>>>>>>>>>>>>>>>>>> only semantic
    logical entailment from basic facts the >>>>>>>>>>>>>>>>>>>>>>>>>>>>>> Principle of
    Explosion ceases to exist. >>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    Only if you exclude from "correct >>>>>>>>>>>>>>>>>>>>>>>>>>>>> reasioning" some reasning that >>>>>>>>>>>>>>>>>>>>>>>>>>>>> actually is correct.

    There is no counter-example that can >>>>>>>>>>>>>>>>>>>>>>>>>>>> possibly exist
    that can show there are any gaps in the body >>>>>>>>>>>>>>>>>>>>>>>>>>>> of human
    knowledge that can be expressed in language >>>>>>>>>>>>>>>>>>>>>>>>>>>> that begins
    with a consistent set of basic facts and >>>>>>>>>>>>>>>>>>>>>>>>>>>> only applies
    semantic logical entailment to these facts. >>>>>>>>>>>>>>>>>>>>>>>>>>>
    There is no language that begins with a >>>>>>>>>>>>>>>>>>>>>>>>>>> consistent set of basic facts >>>>>>>>>>>>>>>>>>>>>>>>>>> and only applies semantic logical entailment >>>>>>>>>>>>>>>>>>>>>>>>>>> to those facts and can
    express all of human knowledge without any gaps. >>>>>>>>>>>>>>>>>>>>>>>>>>
    A subset of formalized English does do this. >>>>>>>>>>>>>>>>>>>>>>>>>
    Nobody has ever presented such subset. >>>>>>>>>>>>>>>>>>>>>>>>
    ChatGPT rewords my words into that subset. >>>>>>>>>>>>>>>>>>>>>>>
    Your words have much less material than all human >>>>>>>>>>>>>>>>>>>>>>> knowledge without
    any gaps. Therefore it is impossible to verify >>>>>>>>>>>>>>>>>>>>>>> that you have told
    every necessary word to it.

    Categorically exhaustive reasoning reverse-engineers >>>>>>>>>>>>>>>>>>>>>> the required architecture of the system. Wittgenstein >>>>>>>>>>>>>>>>>>>>>> did this on Gödel https://www.liarparadox.org/ >>>>>>>>>>>>>>>>>>>>>> Wittgenstein.pdf
    and he was so succinct eliminate the convoluted >>>>>>>>>>>>>>>>>>>>>> mess of Gödel
    numbers that people mistook his succinct analysis >>>>>>>>>>>>>>>>>>>>>> as simplistic
    not understanding what Gödel was really saying. >>>>>>>>>>>>>>>>>>>>>
    Yes, an expectable consequence of ignoring >>>>>>>>>>>>>>>>>>>>> essential aspects is
    not understanding.

    Gödel numbers are merely the ridiculously convoluted >>>>>>>>>>>>>>>>>>>> way that Gödel added the functionality of this simple >>>>>>>>>>>>>>>>>>>> operator: ⊢ to a formal language woefully too >>>>>>>>>>>>>>>>>>>> inexpressive.

    Natural numbers are one of the best understood topics >>>>>>>>>>>>>>>>>>> of mathematics.
    Therefore restricting the assumptions to natural >>>>>>>>>>>>>>>>>>> numbers provdes the
    basis for the most interesting result.

    Of course one can ask whether one can prove a similar >>>>>>>>>>>>>>>>>>> theorem about
    finite strings. It is much simpler to express claims >>>>>>>>>>>>>>>>>>> and proofs as
    fimite strings as thats how they are usually >>>>>>>>>>>>>>>>>>> expressed anyway. But
    that requires that one first constructs a theory of >>>>>>>>>>>>>>>>>>> finite strings.

    But we can show a direct one-to-one mapping of finite >>>>>>>>>>>>>>>>>> strings in a finite alphabet to natural numbers (it >>>>>>>>>>>>>>>>>> just becomes the notational base for the numbers). >>>>>>>>>>>>>>>>>
    That's true, and I would prefer that rather than >>>>>>>>>>>>>>>>> Gödel's mapping. But
    the proof of Gödel's theorem is simpler if the number >>>>>>>>>>>>>>>>> of symbols in
    the alphabet is prime even if that would mean that some >>>>>>>>>>>>>>>>> of the symbols
    are unused.

    Godel's Theorem doesn't need the number of symbols to be >>>>>>>>>>>>>>>> prime, it uses prime numbers to number the symbols, and >>>>>>>>>>>>>>>> prime powers for the position.

    And consequently Gödel's example of an undecidable >>>>>>>>>>>>>>> formula is more complex
    than needed. Which doesn't really matter as the complex >>>>>>>>>>>>>>> details can be
    hidden behind definitions.


    ...We are therefore confronted with a proposition which >>>>>>>>>>>>>> asserts its own unprovability. 15 ...
    (Gödel 1931:40-41)

    G := (F ⊬ G) // Olcott's Minimal Type Theory
    https://philarchive.org/archive/PETMTT-4v2 // YACC BNF of MTT >>>>>>>>>>>>>>
    ?- G = not(provable(F, G)).
    G = not(provable(F, G)).

    ?- unify_with_occurs_check(G, not(provable(F, G))). >>>>>>>>>>>>>> false.

    Gödel, Kurt 1931.
    On Formally Undecidable Propositions of Principia >>>>>>>>>>>>>> Mathematica And Related Systems

    Nice to see that you don't disagree.

    In other words you agree that I proved 1931 Incompleteness >>>>>>>>>>>> is incorrect.
    Gödel's G when boiled down to its barest essence is simply >>>>>>>>>>>> semantically
    unsound the same way the Liar Paradox is unsound.

    As yousually your "in other words" is a lie. Existence of a >>>>>>>>>>> simpler proof
    does not make the original one incorrect.

    My words are true within your words:
       "Nice to see that you don't disagree."
    If you didn't mean that then you should not have said that. >>>>>>>>>
    I did not say nor mean "you did not disagree with anything". >>>>>>>>> The usual
    meaning of what I said is that you don't disagree with what I >>>>>>>>> said in
    my previous message about the complexity of Gödel's sentence. >>>>>>>>
    The complexity of Gödel's sentence is nuts.
    G := (F ⊬ G) Just detect the cycle in this
    and Gödel is refuted.

    Nice to see that you still don't disagree with my comment about the >>>>>>> complexity of Gödel's sentence.

    Yet I absolutely do disagree.

    OK, you think Gödel's numbering scheme is simple.

    ...We are therefore confronted with a proposition which asserts its
    own unprovability. 15 ... (Gödel 1931:40-41)

    It totally hides the details that proof his theorem is unsound.

    You have never revealed any unsound detail of the proof, not even
    whether it uses a false premise or an invalid inference.

    The details of the proof that use Gödel numbers as their
    primary basis hide the underlying semantics about exactly
    what unprovable in F actually means.

    No, they don't. That is very clearly expressed.


    They don't answer the question why and how is G unprovable in F
    their answer is that there is some number that some how says so.

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

    G := (F ⊬ G) is unprovable in F because it has a cycle in
    the directed graph of its evaluation sequence. This is the
    same thing as a infinite loop in a program that is supposed
    to produce a result.
    --
    Copyright 2025 Olcott "Talent hits a target no one else can hit; Genius
    hits a target no one else can see." Arthur Schopenhauer
    --- Synchronet 3.21a-Linux NewsLink 1.2
  • From olcott@[email protected] to comp.theory on Wed Nov 5 05:55:33 2025
    From Newsgroup: comp.theory

    On 11/5/2025 4:46 AM, Mikko wrote:
    On 2025-11-04 17:45:04 +0000, olcott said:

    On 11/4/2025 3:51 AM, Mikko wrote:
    On 2025-11-04 00:32:51 +0000, olcott said:

    On 11/3/2025 6:29 PM, Tristan Wibberley wrote:
    On 03/11/2025 23:40, olcott wrote:

    [the snip of the century]

    G := (F ⊬ G)
    G is defined as unprovable from F.
    That is the ordinary "defined as" operator.

    That's "definitionally reduces to", I think. If "(F ⊬ G)" is not
    ultimately defined then G can still be not defined.

    "define" /is/ a funny word isn't it? Several fields have mixed it
    up in
    different ways.


    ?- G = not(provable(F, G)).
    G = not(provable(F, G)).

    ?- unify_with_occurs_check(G, not(provable(F, G))).
    false.

    The point is that Prolog determines it is semantically
    unsound because it has a cycle in the directed graph of
    its evaluation sequence.

    Prolog does not deremine it semantically unsound.

    In other words you think that when the evaluation
    of an expression gets stuck in an infinite loop
    because of the self-reference in this expression
    that this expression is semantically sound?

    First of all, it does not stick in an infinite loop if you don't do
    with it anything that would stick in an infinte loop.


    That you do not know prolog very well is not a rebuttal.
    ?- unify_with_occurs_check(G, not(provable(F, G))).
    false.

    Usually sticking in an infinite loop is not desired or even perimitted
    but there are exceptions. It all depends on the purpose of the program.
    If the prupose is to compute all digits of pi then an infinte loop is
    needed.

    --
    Copyright 2025 Olcott "Talent hits a target no one else can hit; Genius
    hits a target no one else can see." Arthur Schopenhauer
    --- Synchronet 3.21a-Linux NewsLink 1.2
  • From Mikko@[email protected] to comp.theory on Thu Nov 6 10:35:03 2025
    From Newsgroup: comp.theory

    On 2025-11-05 11:55:33 +0000, olcott said:

    On 11/5/2025 4:46 AM, Mikko wrote:
    On 2025-11-04 17:45:04 +0000, olcott said:

    On 11/4/2025 3:51 AM, Mikko wrote:
    On 2025-11-04 00:32:51 +0000, olcott said:

    On 11/3/2025 6:29 PM, Tristan Wibberley wrote:
    On 03/11/2025 23:40, olcott wrote:

    [the snip of the century]

    G := (F ⊬ G)
    G is defined as unprovable from F.
    That is the ordinary "defined as" operator.

    That's "definitionally reduces to", I think. If "(F ⊬ G)" is not >>>>>> ultimately defined then G can still be not defined.

    "define" /is/ a funny word isn't it? Several fields have mixed it up in >>>>>> different ways.


    ?- G = not(provable(F, G)).
    G = not(provable(F, G)).

    ?- unify_with_occurs_check(G, not(provable(F, G))).
    false.

    The point is that Prolog determines it is semantically
    unsound because it has a cycle in the directed graph of
    its evaluation sequence.

    Prolog does not deremine it semantically unsound.

    In other words you think that when the evaluation
    of an expression gets stuck in an infinite loop
    because of the self-reference in this expression
    that this expression is semantically sound?

    First of all, it does not stick in an infinite loop if you don't do
    with it anything that would stick in an infinte loop.

    That you do not know prolog very well is not a rebuttal.

    That you can lie is not a rebuttal of my rebuttal.

    ?- unify_with_occurs_check(G, not(provable(F, G))).
    false.

    Usually sticking in an infinite loop is not desired or even perimitted
    but there are exceptions. It all depends on the purpose of the program.
    If the prupose is to compute all digits of pi then an infinte loop is
    needed.

    If you think there is something wrong in what I said then point out
    the wrong words and tell what should be said instead. Until that we
    may reagard my words as right and correct.
    --
    Mikko

    --- Synchronet 3.21a-Linux NewsLink 1.2
  • From Mikko@[email protected] to comp.theory on Thu Nov 6 10:39:58 2025
    From Newsgroup: comp.theory

    On 2025-11-05 11:52:40 +0000, olcott said:

    On 11/5/2025 4:49 AM, Mikko wrote:
    On 2025-11-04 18:05:34 +0000, olcott said:

    On 11/4/2025 3:56 AM, Mikko wrote:
    On 2025-11-03 23:45:57 +0000, olcott said:

    On 11/2/2025 6:45 AM, Mikko wrote:
    On 2025-11-01 13:54:09 +0000, olcott said:

    On 11/1/2025 4:18 AM, Mikko wrote:
    On 2025-10-31 12:20:13 +0000, olcott said:

    On 10/31/2025 6:15 AM, Mikko wrote:
    On 2025-10-30 13:03:23 +0000, olcott said:

    On 10/30/2025 5:50 AM, Mikko wrote:
    On 2025-10-29 16:25:00 +0000, olcott said:

    On 10/29/2025 5:45 AM, Mikko wrote:
    On 2025-10-28 15:12:29 +0000, olcott said:

    On 10/28/2025 4:58 AM, Mikko wrote:
    On 2025-10-28 01:22:21 +0000, Richard Damon said: >>>>>>>>>>>>>>>>
    On 10/27/25 5:45 AM, Mikko wrote:
    On 2025-10-26 17:57:16 +0000, Richard Damon said: >>>>>>>>>>>>>>>>>>
    On 10/26/25 7:44 AM, Mikko wrote:
    On 2025-10-25 19:57:19 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>
    On 10/25/2025 6:59 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>> On 2025-10-24 17:37:43 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>>>
    On 10/24/2025 2:46 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>>> On 2025-10-23 15:39:13 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>>>>>
    On 10/23/2025 5:02 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>>>>> On 2025-10-22 12:39:31 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>>>>>>>
    On 10/22/2025 4:23 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>>> On 2025-10-21 15:11:19 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>>>>>>>>>
    On 10/21/2025 4:31 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>> On 2025-10-20 16:24:46 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    On 10/20/2025 3:55 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> On 2025-10-19 15:03:34 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    On 10/19/2025 3:44 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> On 2025-10-18 10:58:15 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    On 10/18/2025 4:30 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    That is not a sense of "proof". >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    That is the correct way to do a proof. >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    A way to do is not a sense. >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    The conventional way to do proofs concludes that
    within its rules if the Moon is made from green
    cheese and the Moon is not made from green cheese
    this proves that Donald Trump is the Lord and savior Jesus Christ.

    Right, and the empirical falct that nobody has verified all of
    1. the Moon is made from green cheese >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> 2. the Moon is not made from grenn cheese >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> 3. Donald Trump is not the Lord and saviour Jesus Christ
    at the same time supports the idea that the conventiona wya to
    do proofs is correct and trustworthy. >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    When we require that correct reasoning is only semantic
    logical entailment from basic facts the Principle of
    Explosion ceases to exist. >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    Only if you exclude from "correct reasioning" some reasning that
    actually is correct. >>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    There is no counter-example that can possibly exist
    that can show there are any gaps in the body of human
    knowledge that can be expressed in language that begins
    with a consistent set of basic facts and only applies
    semantic logical entailment to these facts. >>>>>>>>>>>>>>>>>>>>>>>>>>>>
    There is no language that begins with a consistent set of basic facts
    and only applies semantic logical entailment to those facts and can
    express all of human knowledge without any gaps. >>>>>>>>>>>>>>>>>>>>>>>>>>>
    A subset of formalized English does do this. >>>>>>>>>>>>>>>>>>>>>>>>>>
    Nobody has ever presented such subset. >>>>>>>>>>>>>>>>>>>>>>>>>
    ChatGPT rewords my words into that subset. >>>>>>>>>>>>>>>>>>>>>>>>
    Your words have much less material than all human knowledge without
    any gaps. Therefore it is impossible to verify that you have told
    every necessary word to it.

    Categorically exhaustive reasoning reverse-engineers >>>>>>>>>>>>>>>>>>>>>>> the required architecture of the system. Wittgenstein >>>>>>>>>>>>>>>>>>>>>>> did this on Gödel https://www.liarparadox.org/ Wittgenstein.pdf
    and he was so succinct eliminate the convoluted mess of Gödel
    numbers that people mistook his succinct analysis as simplistic
    not understanding what Gödel was really saying. >>>>>>>>>>>>>>>>>>>>>>
    Yes, an expectable consequence of ignoring essential aspects is
    not understanding.

    Gödel numbers are merely the ridiculously convoluted >>>>>>>>>>>>>>>>>>>>> way that Gödel added the functionality of this simple >>>>>>>>>>>>>>>>>>>>> operator: ⊢ to a formal language woefully too inexpressive.

    Natural numbers are one of the best understood topics of mathematics.
    Therefore restricting the assumptions to natural numbers provdes the
    basis for the most interesting result. >>>>>>>>>>>>>>>>>>>>
    Of course one can ask whether one can prove a similar theorem about
    finite strings. It is much simpler to express claims and proofs as
    fimite strings as thats how they are usually expressed anyway. But
    that requires that one first constructs a theory of finite strings.

    But we can show a direct one-to-one mapping of finite strings in a
    finite alphabet to natural numbers (it just becomes the notational base
    for the numbers).

    That's true, and I would prefer that rather than Gödel's mapping. But
    the proof of Gödel's theorem is simpler if the number of symbols in
    the alphabet is prime even if that would mean that some of the symbols
    are unused.

    Godel's Theorem doesn't need the number of symbols to be prime, it uses
    prime numbers to number the symbols, and prime powers for the position.

    And consequently Gödel's example of an undecidable formula is more complex
    than needed. Which doesn't really matter as the complex details can be
    hidden behind definitions.


    ...We are therefore confronted with a proposition which asserts its own
    unprovability. 15 ...
    (Gödel 1931:40-41)

    G := (F ⊬ G) // Olcott's Minimal Type Theory
    https://philarchive.org/archive/PETMTT-4v2 // YACC BNF of MTT >>>>>>>>>>>>>>>
    ?- G = not(provable(F, G)).
    G = not(provable(F, G)).

    ?- unify_with_occurs_check(G, not(provable(F, G))). >>>>>>>>>>>>>>> false.

    Gödel, Kurt 1931.
    On Formally Undecidable Propositions of Principia Mathematica And
    Related Systems

    Nice to see that you don't disagree.

    In other words you agree that I proved 1931 Incompleteness is incorrect.
    Gödel's G when boiled down to its barest essence is simply semantically
    unsound the same way the Liar Paradox is unsound.

    As yousually your "in other words" is a lie. Existence of a simpler proof
    does not make the original one incorrect.

    My words are true within your words:
       "Nice to see that you don't disagree."
    If you didn't mean that then you should not have said that. >>>>>>>>>>
    I did not say nor mean "you did not disagree with anything". The usual
    meaning of what I said is that you don't disagree with what I said in
    my previous message about the complexity of Gödel's sentence. >>>>>>>>>
    The complexity of Gödel's sentence is nuts.
    G := (F ⊬ G) Just detect the cycle in this
    and Gödel is refuted.

    Nice to see that you still don't disagree with my comment about the >>>>>>>> complexity of Gödel's sentence.

    Yet I absolutely do disagree.

    OK, you think Gödel's numbering scheme is simple.

    ...We are therefore confronted with a proposition which asserts its own >>>>> unprovability. 15 ... (Gödel 1931:40-41)

    It totally hides the details that proof his theorem is unsound.

    You have never revealed any unsound detail of the proof, not even
    whether it uses a false premise or an invalid inference.

    The details of the proof that use Gödel numbers as their
    primary basis hide the underlying semantics about exactly
    what unprovable in F actually means.

    No, they don't. That is very clearly expressed.

    They don't answer the question why and how is G unprovable in F
    their answer is that there is some number that some how says so.

    That no proof proves G is sufficient to say that G is unprovable.
    --
    Mikko

    --- Synchronet 3.21a-Linux NewsLink 1.2
  • From olcott@[email protected] to comp.theory on Thu Nov 6 05:03:30 2025
    From Newsgroup: comp.theory

    On 11/6/2025 2:35 AM, Mikko wrote:
    On 2025-11-05 11:55:33 +0000, olcott said:

    On 11/5/2025 4:46 AM, Mikko wrote:
    On 2025-11-04 17:45:04 +0000, olcott said:

    On 11/4/2025 3:51 AM, Mikko wrote:
    On 2025-11-04 00:32:51 +0000, olcott said:

    On 11/3/2025 6:29 PM, Tristan Wibberley wrote:
    On 03/11/2025 23:40, olcott wrote:

    [the snip of the century]

    G := (F ⊬ G)
    G is defined as unprovable from F.
    That is the ordinary "defined as" operator.

    That's "definitionally reduces to", I think. If "(F ⊬ G)" is not >>>>>>> ultimately defined then G can still be not defined.

    "define" /is/ a funny word isn't it? Several fields have mixed it >>>>>>> up in
    different ways.


    ?- G = not(provable(F, G)).
    G = not(provable(F, G)).

    ?- unify_with_occurs_check(G, not(provable(F, G))).
    false.

    The point is that Prolog determines it is semantically
    unsound because it has a cycle in the directed graph of
    its evaluation sequence.

    Prolog does not deremine it semantically unsound.

    In other words you think that when the evaluation
    of an expression gets stuck in an infinite loop
    because of the self-reference in this expression
    that this expression is semantically sound?

    First of all, it does not stick in an infinite loop if you don't do
    with it anything that would stick in an infinte loop.


    The key idea is that the expression has a cycle in the
    directed graph of its evaluation sequence. This does
    make the expression semantically unsound.

    I understand this better than most people because I
    created Minimal Type Theory from scratch that does
    this same thing and it does this the same way. My
    whole purpose in creating Minimal Type Theory was to
    do this same thing in this same way.

    That you do not know prolog very well is not a rebuttal.

    That you can lie is not a rebuttal of my rebuttal.


    That you say these things is defamation of character.
    When you act like you don't know Prolog this *is*
    sufficient evidence that you don't know Prolog.

    If you don't totally understand unify_with_occurs_check()
    You don't know Prolog well enough to understand what
    I am saying even if you program in Prolog every day.

    ?- unify_with_occurs_check(G, not(provable(F, G))).
    false.

    Usually sticking in an infinite loop is not desired or even perimitted
    but there are exceptions. It all depends on the purpose of the program.
    If the prupose is to compute all digits of pi then an infinte loop is
    needed.

    If you think there is something wrong in what I said then point out
    the wrong words and tell what should be said instead. Until that we
    may reagard my words as right and correct.

    --
    Copyright 2025 Olcott "Talent hits a target no one else can hit; Genius
    hits a target no one else can see." Arthur Schopenhauer
    --- Synchronet 3.21a-Linux NewsLink 1.2
  • From olcott@[email protected] to comp.theory on Thu Nov 6 05:08:22 2025
    From Newsgroup: comp.theory

    On 11/6/2025 2:39 AM, Mikko wrote:
    On 2025-11-05 11:52:40 +0000, olcott said:

    On 11/5/2025 4:49 AM, Mikko wrote:
    On 2025-11-04 18:05:34 +0000, olcott said:

    On 11/4/2025 3:56 AM, Mikko wrote:
    On 2025-11-03 23:45:57 +0000, olcott said:

    On 11/2/2025 6:45 AM, Mikko wrote:
    On 2025-11-01 13:54:09 +0000, olcott said:

    On 11/1/2025 4:18 AM, Mikko wrote:
    On 2025-10-31 12:20:13 +0000, olcott said:

    On 10/31/2025 6:15 AM, Mikko wrote:
    On 2025-10-30 13:03:23 +0000, olcott said:

    On 10/30/2025 5:50 AM, Mikko wrote:
    On 2025-10-29 16:25:00 +0000, olcott said:

    On 10/29/2025 5:45 AM, Mikko wrote:
    On 2025-10-28 15:12:29 +0000, olcott said:

    On 10/28/2025 4:58 AM, Mikko wrote:
    On 2025-10-28 01:22:21 +0000, Richard Damon said: >>>>>>>>>>>>>>>>>
    On 10/27/25 5:45 AM, Mikko wrote:
    On 2025-10-26 17:57:16 +0000, Richard Damon said: >>>>>>>>>>>>>>>>>>>
    On 10/26/25 7:44 AM, Mikko wrote:
    On 2025-10-25 19:57:19 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>>
    On 10/25/2025 6:59 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>> On 2025-10-24 17:37:43 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>>>>
    On 10/24/2025 2:46 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>>>> On 2025-10-23 15:39:13 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>>>>>>
    On 10/23/2025 5:02 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>> On 2025-10-22 12:39:31 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>>>>>>>>
    On 10/22/2025 4:23 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>>>> On 2025-10-21 15:11:19 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    On 10/21/2025 4:31 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> On 2025-10-20 16:24:46 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    On 10/20/2025 3:55 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> On 2025-10-19 15:03:34 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    On 10/19/2025 3:44 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> On 2025-10-18 10:58:15 +0000, olcott >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> said:

    On 10/18/2025 4:30 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    That is not a sense of "proof". >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    That is the correct way to do a proof. >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    A way to do is not a sense. >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    The conventional way to do proofs >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> concludes that >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> within its rules if the Moon is made >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> from green >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> cheese and the Moon is not made from >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> green cheese >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> this proves that Donald Trump is the >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> Lord and savior Jesus Christ. >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    Right, and the empirical falct that >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> nobody has verified all of >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> 1. the Moon is made from green cheese >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> 2. the Moon is not made from grenn cheese >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> 3. Donald Trump is not the Lord and >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> saviour Jesus Christ >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> at the same time supports the idea that >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> the conventiona wya to >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> do proofs is correct and trustworthy. >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    When we require that correct reasoning >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> is only semantic >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> logical entailment from basic facts the >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> Principle of
    Explosion ceases to exist. >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    Only if you exclude from "correct >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> reasioning" some reasning that >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> actually is correct. >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    There is no counter-example that can >>>>>>>>>>>>>>>>>>>>>>>>>>>>>> possibly exist
    that can show there are any gaps in the >>>>>>>>>>>>>>>>>>>>>>>>>>>>>> body of human
    knowledge that can be expressed in >>>>>>>>>>>>>>>>>>>>>>>>>>>>>> language that begins >>>>>>>>>>>>>>>>>>>>>>>>>>>>>> with a consistent set of basic facts and >>>>>>>>>>>>>>>>>>>>>>>>>>>>>> only applies
    semantic logical entailment to these facts. >>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    There is no language that begins with a >>>>>>>>>>>>>>>>>>>>>>>>>>>>> consistent set of basic facts >>>>>>>>>>>>>>>>>>>>>>>>>>>>> and only applies semantic logical >>>>>>>>>>>>>>>>>>>>>>>>>>>>> entailment to those facts and can >>>>>>>>>>>>>>>>>>>>>>>>>>>>> express all of human knowledge without any >>>>>>>>>>>>>>>>>>>>>>>>>>>>> gaps.

    A subset of formalized English does do this. >>>>>>>>>>>>>>>>>>>>>>>>>>>
    Nobody has ever presented such subset. >>>>>>>>>>>>>>>>>>>>>>>>>>
    ChatGPT rewords my words into that subset. >>>>>>>>>>>>>>>>>>>>>>>>>
    Your words have much less material than all >>>>>>>>>>>>>>>>>>>>>>>>> human knowledge without
    any gaps. Therefore it is impossible to verify >>>>>>>>>>>>>>>>>>>>>>>>> that you have told
    every necessary word to it.

    Categorically exhaustive reasoning reverse- >>>>>>>>>>>>>>>>>>>>>>>> engineers
    the required architecture of the system. >>>>>>>>>>>>>>>>>>>>>>>> Wittgenstein
    did this on Gödel https://www.liarparadox.org/ >>>>>>>>>>>>>>>>>>>>>>>> Wittgenstein.pdf
    and he was so succinct eliminate the convoluted >>>>>>>>>>>>>>>>>>>>>>>> mess of Gödel
    numbers that people mistook his succinct >>>>>>>>>>>>>>>>>>>>>>>> analysis as simplistic
    not understanding what Gödel was really saying. >>>>>>>>>>>>>>>>>>>>>>>
    Yes, an expectable consequence of ignoring >>>>>>>>>>>>>>>>>>>>>>> essential aspects is
    not understanding.

    Gödel numbers are merely the ridiculously convoluted >>>>>>>>>>>>>>>>>>>>>> way that Gödel added the functionality of this simple >>>>>>>>>>>>>>>>>>>>>> operator: ⊢ to a formal language woefully too >>>>>>>>>>>>>>>>>>>>>> inexpressive.

    Natural numbers are one of the best understood >>>>>>>>>>>>>>>>>>>>> topics of mathematics.
    Therefore restricting the assumptions to natural >>>>>>>>>>>>>>>>>>>>> numbers provdes the
    basis for the most interesting result. >>>>>>>>>>>>>>>>>>>>>
    Of course one can ask whether one can prove a >>>>>>>>>>>>>>>>>>>>> similar theorem about
    finite strings. It is much simpler to express >>>>>>>>>>>>>>>>>>>>> claims and proofs as
    fimite strings as thats how they are usually >>>>>>>>>>>>>>>>>>>>> expressed anyway. But
    that requires that one first constructs a theory of >>>>>>>>>>>>>>>>>>>>> finite strings.

    But we can show a direct one-to-one mapping of >>>>>>>>>>>>>>>>>>>> finite strings in a finite alphabet to natural >>>>>>>>>>>>>>>>>>>> numbers (it just becomes the notational base for the >>>>>>>>>>>>>>>>>>>> numbers).

    That's true, and I would prefer that rather than >>>>>>>>>>>>>>>>>>> Gödel's mapping. But
    the proof of Gödel's theorem is simpler if the number >>>>>>>>>>>>>>>>>>> of symbols in
    the alphabet is prime even if that would mean that >>>>>>>>>>>>>>>>>>> some of the symbols
    are unused.

    Godel's Theorem doesn't need the number of symbols to >>>>>>>>>>>>>>>>>> be prime, it uses prime numbers to number the symbols, >>>>>>>>>>>>>>>>>> and prime powers for the position.

    And consequently Gödel's example of an undecidable >>>>>>>>>>>>>>>>> formula is more complex
    than needed. Which doesn't really matter as the complex >>>>>>>>>>>>>>>>> details can be
    hidden behind definitions.


    ...We are therefore confronted with a proposition which >>>>>>>>>>>>>>>> asserts its own unprovability. 15 ...
    (Gödel 1931:40-41)

    G := (F ⊬ G) // Olcott's Minimal Type Theory >>>>>>>>>>>>>>>> https://philarchive.org/archive/PETMTT-4v2 // YACC BNF >>>>>>>>>>>>>>>> of MTT

    ?- G = not(provable(F, G)).
    G = not(provable(F, G)).

    ?- unify_with_occurs_check(G, not(provable(F, G))). >>>>>>>>>>>>>>>> false.

    Gödel, Kurt 1931.
    On Formally Undecidable Propositions of Principia >>>>>>>>>>>>>>>> Mathematica And Related Systems

    Nice to see that you don't disagree.

    In other words you agree that I proved 1931 Incompleteness >>>>>>>>>>>>>> is incorrect.
    Gödel's G when boiled down to its barest essence is simply >>>>>>>>>>>>>> semantically
    unsound the same way the Liar Paradox is unsound.

    As yousually your "in other words" is a lie. Existence of a >>>>>>>>>>>>> simpler proof
    does not make the original one incorrect.

    My words are true within your words:
       "Nice to see that you don't disagree."
    If you didn't mean that then you should not have said that. >>>>>>>>>>>
    I did not say nor mean "you did not disagree with anything". >>>>>>>>>>> The usual
    meaning of what I said is that you don't disagree with what I >>>>>>>>>>> said in
    my previous message about the complexity of Gödel's sentence. >>>>>>>>>>
    The complexity of Gödel's sentence is nuts.
    G := (F ⊬ G) Just detect the cycle in this
    and Gödel is refuted.

    Nice to see that you still don't disagree with my comment about >>>>>>>>> the
    complexity of Gödel's sentence.

    Yet I absolutely do disagree.

    OK, you think Gödel's numbering scheme is simple.

    ...We are therefore confronted with a proposition which asserts
    its own unprovability. 15 ... (Gödel 1931:40-41)

    It totally hides the details that proof his theorem is unsound.

    You have never revealed any unsound detail of the proof, not even
    whether it uses a false premise or an invalid inference.

    The details of the proof that use Gödel numbers as their
    primary basis hide the underlying semantics about exactly
    what unprovable in F actually means.

    No, they don't. That is very clearly expressed.

    They don't answer the question why and how is G unprovable in F
    their answer is that there is some number that some how says so.

    That no proof proves G is sufficient to say that G is unprovable.


    If G is semantic gibberish then G would not be provable.
    These are the ways that G is semantic gibberish. They
    are all semantic gibberish.

    ...there is also a close relationship with the “liar” 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 ...
    (Gödel 1931:40-41)

    Gödel, Kurt 1931.
    On Formally Undecidable Propositions of Principia Mathematica And
    Related Systems
    --
    Copyright 2025 Olcott "Talent hits a target no one else can hit; Genius
    hits a target no one else can see." Arthur Schopenhauer
    --- Synchronet 3.21a-Linux NewsLink 1.2
  • From Mikko@[email protected] to comp.theory on Fri Nov 7 10:14:22 2025
    From Newsgroup: comp.theory

    On 2025-11-06 11:03:30 +0000, olcott said:

    On 11/6/2025 2:35 AM, Mikko wrote:
    On 2025-11-05 11:55:33 +0000, olcott said:

    On 11/5/2025 4:46 AM, Mikko wrote:
    On 2025-11-04 17:45:04 +0000, olcott said:

    On 11/4/2025 3:51 AM, Mikko wrote:
    On 2025-11-04 00:32:51 +0000, olcott said:

    On 11/3/2025 6:29 PM, Tristan Wibberley wrote:
    On 03/11/2025 23:40, olcott wrote:

    [the snip of the century]

    G := (F ⊬ G)
    G is defined as unprovable from F.
    That is the ordinary "defined as" operator.

    That's "definitionally reduces to", I think. If "(F ⊬ G)" is not >>>>>>>> ultimately defined then G can still be not defined.

    "define" /is/ a funny word isn't it? Several fields have mixed it up in
    different ways.


    ?- G = not(provable(F, G)).
    G = not(provable(F, G)).

    ?- unify_with_occurs_check(G, not(provable(F, G))).
    false.

    The point is that Prolog determines it is semantically
    unsound because it has a cycle in the directed graph of
    its evaluation sequence.

    Prolog does not deremine it semantically unsound.

    In other words you think that when the evaluation
    of an expression gets stuck in an infinite loop
    because of the self-reference in this expression
    that this expression is semantically sound?

    First of all, it does not stick in an infinite loop if you don't do
    with it anything that would stick in an infinte loop.

    The key idea is that the expression has a cycle in the
    directed graph of its evaluation sequence. This does
    make the expression semantically unsound.

    The expression "semanitcally unsound" does not mean anything if
    no semantics is applied. It is also meaningless if the aplied
    semantics does not assound any soundness to anything.
    --
    Mikko

    --- Synchronet 3.21a-Linux NewsLink 1.2
  • From Mikko@[email protected] to comp.theory on Fri Nov 7 10:21:24 2025
    From Newsgroup: comp.theory

    On 2025-11-06 11:08:22 +0000, olcott said:

    On 11/6/2025 2:39 AM, Mikko wrote:
    On 2025-11-05 11:52:40 +0000, olcott said:

    On 11/5/2025 4:49 AM, Mikko wrote:
    On 2025-11-04 18:05:34 +0000, olcott said:

    On 11/4/2025 3:56 AM, Mikko wrote:
    On 2025-11-03 23:45:57 +0000, olcott said:

    On 11/2/2025 6:45 AM, Mikko wrote:
    On 2025-11-01 13:54:09 +0000, olcott said:

    On 11/1/2025 4:18 AM, Mikko wrote:
    On 2025-10-31 12:20:13 +0000, olcott said:

    On 10/31/2025 6:15 AM, Mikko wrote:
    On 2025-10-30 13:03:23 +0000, olcott said:

    On 10/30/2025 5:50 AM, Mikko wrote:
    On 2025-10-29 16:25:00 +0000, olcott said:

    On 10/29/2025 5:45 AM, Mikko wrote:
    On 2025-10-28 15:12:29 +0000, olcott said:

    On 10/28/2025 4:58 AM, Mikko wrote:
    On 2025-10-28 01:22:21 +0000, Richard Damon said: >>>>>>>>>>>>>>>>>>
    On 10/27/25 5:45 AM, Mikko wrote:
    On 2025-10-26 17:57:16 +0000, Richard Damon said: >>>>>>>>>>>>>>>>>>>>
    On 10/26/25 7:44 AM, Mikko wrote:
    On 2025-10-25 19:57:19 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>>>
    On 10/25/2025 6:59 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>>> On 2025-10-24 17:37:43 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>>>>>
    On 10/24/2025 2:46 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>>>>> On 2025-10-23 15:39:13 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>>>>>>>
    On 10/23/2025 5:02 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>>> On 2025-10-22 12:39:31 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>>>>>>>>>
    On 10/22/2025 4:23 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>> On 2025-10-21 15:11:19 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    On 10/21/2025 4:31 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> On 2025-10-20 16:24:46 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    On 10/20/2025 3:55 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> On 2025-10-19 15:03:34 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    On 10/19/2025 3:44 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> On 2025-10-18 10:58:15 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    On 10/18/2025 4:30 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    That is not a sense of "proof". >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    That is the correct way to do a proof. >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    A way to do is not a sense. >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    The conventional way to do proofs concludes that
    within its rules if the Moon is made from green
    cheese and the Moon is not made from green cheese
    this proves that Donald Trump is the Lord and savior Jesus Christ.

    Right, and the empirical falct that nobody has verified all of
    1. the Moon is made from green cheese >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> 2. the Moon is not made from grenn cheese >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> 3. Donald Trump is not the Lord and saviour Jesus Christ
    at the same time supports the idea that the conventiona wya to
    do proofs is correct and trustworthy. >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    When we require that correct reasoning is only semantic
    logical entailment from basic facts the Principle of
    Explosion ceases to exist. >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    Only if you exclude from "correct reasioning" some reasning that
    actually is correct. >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    There is no counter-example that can possibly exist
    that can show there are any gaps in the body of human
    knowledge that can be expressed in language that begins
    with a consistent set of basic facts and only applies
    semantic logical entailment to these facts. >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    There is no language that begins with a consistent set of basic facts
    and only applies semantic logical entailment to those facts and can
    express all of human knowledge without any gaps. >>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    A subset of formalized English does do this. >>>>>>>>>>>>>>>>>>>>>>>>>>>>
    Nobody has ever presented such subset. >>>>>>>>>>>>>>>>>>>>>>>>>>>
    ChatGPT rewords my words into that subset. >>>>>>>>>>>>>>>>>>>>>>>>>>
    Your words have much less material than all human knowledge without
    any gaps. Therefore it is impossible to verify that you have told
    every necessary word to it. >>>>>>>>>>>>>>>>>>>>>>>>>
    Categorically exhaustive reasoning reverse- engineers >>>>>>>>>>>>>>>>>>>>>>>>> the required architecture of the system. Wittgenstein >>>>>>>>>>>>>>>>>>>>>>>>> did this on Gödel https://www.liarparadox.org/ Wittgenstein.pdf
    and he was so succinct eliminate the convoluted mess of Gödel
    numbers that people mistook his succinct analysis as simplistic
    not understanding what Gödel was really saying. >>>>>>>>>>>>>>>>>>>>>>>>
    Yes, an expectable consequence of ignoring essential aspects is
    not understanding.

    Gödel numbers are merely the ridiculously convoluted >>>>>>>>>>>>>>>>>>>>>>> way that Gödel added the functionality of this simple >>>>>>>>>>>>>>>>>>>>>>> operator: ⊢ to a formal language woefully too inexpressive.

    Natural numbers are one of the best understood topics of mathematics.
    Therefore restricting the assumptions to natural numbers provdes the
    basis for the most interesting result. >>>>>>>>>>>>>>>>>>>>>>
    Of course one can ask whether one can prove a similar theorem about
    finite strings. It is much simpler to express claims and proofs as
    fimite strings as thats how they are usually expressed anyway. But
    that requires that one first constructs a theory of finite strings.

    But we can show a direct one-to-one mapping of finite strings in a
    finite alphabet to natural numbers (it just becomes the notational base
    for the numbers).

    That's true, and I would prefer that rather than Gödel's mapping. But
    the proof of Gödel's theorem is simpler if the number of symbols in
    the alphabet is prime even if that would mean that some of the symbols
    are unused.

    Godel's Theorem doesn't need the number of symbols to be prime, it uses
    prime numbers to number the symbols, and prime powers for the position.

    And consequently Gödel's example of an undecidable formula is more complex
    than needed. Which doesn't really matter as the complex details can be
    hidden behind definitions.


    ...We are therefore confronted with a proposition which asserts its own
    unprovability. 15 ...
    (Gödel 1931:40-41)

    G := (F ⊬ G) // Olcott's Minimal Type Theory >>>>>>>>>>>>>>>>> https://philarchive.org/archive/PETMTT-4v2 // YACC BNF of MTT >>>>>>>>>>>>>>>>>
    ?- G = not(provable(F, G)).
    G = not(provable(F, G)).

    ?- unify_with_occurs_check(G, not(provable(F, G))). >>>>>>>>>>>>>>>>> false.

    Gödel, Kurt 1931.
    On Formally Undecidable Propositions of Principia Mathematica And
    Related Systems

    Nice to see that you don't disagree.

    In other words you agree that I proved 1931 Incompleteness is incorrect.
    Gödel's G when boiled down to its barest essence is simply semantically
    unsound the same way the Liar Paradox is unsound. >>>>>>>>>>>>>>
    As yousually your "in other words" is a lie. Existence of a simpler proof
    does not make the original one incorrect.

    My words are true within your words:
       "Nice to see that you don't disagree."
    If you didn't mean that then you should not have said that. >>>>>>>>>>>>
    I did not say nor mean "you did not disagree with anything". The usual
    meaning of what I said is that you don't disagree with what I said in
    my previous message about the complexity of Gödel's sentence. >>>>>>>>>>>
    The complexity of Gödel's sentence is nuts.
    G := (F ⊬ G) Just detect the cycle in this
    and Gödel is refuted.

    Nice to see that you still don't disagree with my comment about the >>>>>>>>>> complexity of Gödel's sentence.

    Yet I absolutely do disagree.

    OK, you think Gödel's numbering scheme is simple.

    ...We are therefore confronted with a proposition which asserts its own
    unprovability. 15 ... (Gödel 1931:40-41)

    It totally hides the details that proof his theorem is unsound.

    You have never revealed any unsound detail of the proof, not even
    whether it uses a false premise or an invalid inference.

    The details of the proof that use Gödel numbers as their
    primary basis hide the underlying semantics about exactly
    what unprovable in F actually means.

    No, they don't. That is very clearly expressed.

    They don't answer the question why and how is G unprovable in F
    their answer is that there is some number that some how says so.

    That no proof proves G is sufficient to say that G is unprovable.

    If G is semantic gibberish then G would not be provable.

    That does not follow. G if provable if there is a proof that is
    valid in the theory and ends with G. If there is not then G is
    unprovable. Consequently, if G is not in the language of the
    theory then it is unprovable.

    But Gödel's G is a sentence of the first order Peano arithmetic and
    therefore has an arithmetic meaning. Gödel also proved that in its
    arithmetic meaning G is true. In some non-arthmetic meaning it can
    be false.
    --
    Mikko

    --- Synchronet 3.21a-Linux NewsLink 1.2
  • From olcott@[email protected] to comp.theory on Fri Nov 7 07:00:44 2025
    From Newsgroup: comp.theory

    On 11/7/2025 2:14 AM, Mikko wrote:
    On 2025-11-06 11:03:30 +0000, olcott said:

    On 11/6/2025 2:35 AM, Mikko wrote:
    On 2025-11-05 11:55:33 +0000, olcott said:

    On 11/5/2025 4:46 AM, Mikko wrote:
    On 2025-11-04 17:45:04 +0000, olcott said:

    On 11/4/2025 3:51 AM, Mikko wrote:
    On 2025-11-04 00:32:51 +0000, olcott said:

    On 11/3/2025 6:29 PM, Tristan Wibberley wrote:
    On 03/11/2025 23:40, olcott wrote:

    [the snip of the century]

    G := (F ⊬ G)
    G is defined as unprovable from F.
    That is the ordinary "defined as" operator.

    That's "definitionally reduces to", I think. If "(F ⊬ G)" is not >>>>>>>>> ultimately defined then G can still be not defined.

    "define" /is/ a funny word isn't it? Several fields have mixed >>>>>>>>> it up in
    different ways.


    ?- G = not(provable(F, G)).
    G = not(provable(F, G)).

    ?- unify_with_occurs_check(G, not(provable(F, G))).
    false.

    The point is that Prolog determines it is semantically
    unsound because it has a cycle in the directed graph of
    its evaluation sequence.

    Prolog does not deremine it semantically unsound.

    In other words you think that when the evaluation
    of an expression gets stuck in an infinite loop
    because of the self-reference in this expression
    that this expression is semantically sound?

    First of all, it does not stick in an infinite loop if you don't do
    with it anything that would stick in an infinte loop.

    The key idea is that the expression has a cycle in the
    directed graph of its evaluation sequence. This does
    make the expression semantically unsound.

    The expression "semanitcally unsound" does not mean anything if
    no semantics is applied. It is also meaningless if the aplied
    semantics does not assound any soundness to anything.


    You are trying to be a s disagreeable as possible.

    G := (F ⊬ G)
    The above expression has a cycle in the directed
    graph of its evaluation sequence making it incorrect.
    --
    Copyright 2025 Olcott "Talent hits a target no one else can hit; Genius
    hits a target no one else can see." Arthur Schopenhauer
    --- Synchronet 3.21a-Linux NewsLink 1.2
  • From olcott@[email protected] to comp.theory on Fri Nov 7 07:31:46 2025
    From Newsgroup: comp.theory

    On 11/7/2025 2:21 AM, Mikko wrote:
    On 2025-11-06 11:08:22 +0000, olcott said:

    On 11/6/2025 2:39 AM, Mikko wrote:
    On 2025-11-05 11:52:40 +0000, olcott said:

    On 11/5/2025 4:49 AM, Mikko wrote:
    On 2025-11-04 18:05:34 +0000, olcott said:

    On 11/4/2025 3:56 AM, Mikko wrote:
    On 2025-11-03 23:45:57 +0000, olcott said:

    On 11/2/2025 6:45 AM, Mikko wrote:
    On 2025-11-01 13:54:09 +0000, olcott said:

    On 11/1/2025 4:18 AM, Mikko wrote:
    On 2025-10-31 12:20:13 +0000, olcott said:

    On 10/31/2025 6:15 AM, Mikko wrote:
    On 2025-10-30 13:03:23 +0000, olcott said:

    On 10/30/2025 5:50 AM, Mikko wrote:
    On 2025-10-29 16:25:00 +0000, olcott said:

    On 10/29/2025 5:45 AM, Mikko wrote:
    On 2025-10-28 15:12:29 +0000, olcott said:

    On 10/28/2025 4:58 AM, Mikko wrote:
    On 2025-10-28 01:22:21 +0000, Richard Damon said: >>>>>>>>>>>>>>>>>>>
    On 10/27/25 5:45 AM, Mikko wrote:
    On 2025-10-26 17:57:16 +0000, Richard Damon said: >>>>>>>>>>>>>>>>>>>>>
    On 10/26/25 7:44 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>> On 2025-10-25 19:57:19 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>>>>
    On 10/25/2025 6:59 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>>>> On 2025-10-24 17:37:43 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>>>>>>
    On 10/24/2025 2:46 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>> On 2025-10-23 15:39:13 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>>>>>>>>
    On 10/23/2025 5:02 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>>>> On 2025-10-22 12:39:31 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    On 10/22/2025 4:23 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> On 2025-10-21 15:11:19 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    On 10/21/2025 4:31 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> On 2025-10-20 16:24:46 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    On 10/20/2025 3:55 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> On 2025-10-19 15:03:34 +0000, olcott >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> said:

    On 10/19/2025 3:44 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> On 2025-10-18 10:58:15 +0000, >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> olcott said: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    On 10/18/2025 4:30 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    That is not a sense of "proof". >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    That is the correct way to do a >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> proof. >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    A way to do is not a sense. >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    The conventional way to do proofs >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> concludes that >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> within its rules if the Moon is made >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> from green >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> cheese and the Moon is not made from >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> green cheese >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> this proves that Donald Trump is the >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> Lord and savior Jesus Christ. >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    Right, and the empirical falct that >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> nobody has verified all of >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> 1. the Moon is made from green cheese >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> 2. the Moon is not made from grenn >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> cheese
    3. Donald Trump is not the Lord and >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> saviour Jesus Christ >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> at the same time supports the idea >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> that the conventiona wya to >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> do proofs is correct and trustworthy. >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    When we require that correct reasoning >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> is only semantic >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> logical entailment from basic facts >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> the Principle of >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> Explosion ceases to exist. >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    Only if you exclude from "correct >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> reasioning" some reasning that >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> actually is correct. >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    There is no counter-example that can >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> possibly exist >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> that can show there are any gaps in the >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> body of human
    knowledge that can be expressed in >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> language that begins >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> with a consistent set of basic facts and >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> only applies
    semantic logical entailment to these facts. >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    There is no language that begins with a >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> consistent set of basic facts >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> and only applies semantic logical >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> entailment to those facts and can >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> express all of human knowledge without >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> any gaps.

    A subset of formalized English does do this. >>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    Nobody has ever presented such subset. >>>>>>>>>>>>>>>>>>>>>>>>>>>>
    ChatGPT rewords my words into that subset. >>>>>>>>>>>>>>>>>>>>>>>>>>>
    Your words have much less material than all >>>>>>>>>>>>>>>>>>>>>>>>>>> human knowledge without
    any gaps. Therefore it is impossible to >>>>>>>>>>>>>>>>>>>>>>>>>>> verify that you have told >>>>>>>>>>>>>>>>>>>>>>>>>>> every necessary word to it. >>>>>>>>>>>>>>>>>>>>>>>>>>
    Categorically exhaustive reasoning reverse- >>>>>>>>>>>>>>>>>>>>>>>>>> engineers
    the required architecture of the system. >>>>>>>>>>>>>>>>>>>>>>>>>> Wittgenstein
    did this on Gödel https://www.liarparadox.org/ >>>>>>>>>>>>>>>>>>>>>>>>>> Wittgenstein.pdf
    and he was so succinct eliminate the >>>>>>>>>>>>>>>>>>>>>>>>>> convoluted mess of Gödel
    numbers that people mistook his succinct >>>>>>>>>>>>>>>>>>>>>>>>>> analysis as simplistic
    not understanding what Gödel was really saying. >>>>>>>>>>>>>>>>>>>>>>>>>
    Yes, an expectable consequence of ignoring >>>>>>>>>>>>>>>>>>>>>>>>> essential aspects is
    not understanding.

    Gödel numbers are merely the ridiculously >>>>>>>>>>>>>>>>>>>>>>>> convoluted
    way that Gödel added the functionality of this >>>>>>>>>>>>>>>>>>>>>>>> simple
    operator: ⊢ to a formal language woefully too >>>>>>>>>>>>>>>>>>>>>>>> inexpressive.

    Natural numbers are one of the best understood >>>>>>>>>>>>>>>>>>>>>>> topics of mathematics.
    Therefore restricting the assumptions to natural >>>>>>>>>>>>>>>>>>>>>>> numbers provdes the
    basis for the most interesting result. >>>>>>>>>>>>>>>>>>>>>>>
    Of course one can ask whether one can prove a >>>>>>>>>>>>>>>>>>>>>>> similar theorem about
    finite strings. It is much simpler to express >>>>>>>>>>>>>>>>>>>>>>> claims and proofs as
    fimite strings as thats how they are usually >>>>>>>>>>>>>>>>>>>>>>> expressed anyway. But
    that requires that one first constructs a theory >>>>>>>>>>>>>>>>>>>>>>> of finite strings.

    But we can show a direct one-to-one mapping of >>>>>>>>>>>>>>>>>>>>>> finite strings in a finite alphabet to natural >>>>>>>>>>>>>>>>>>>>>> numbers (it just becomes the notational base for >>>>>>>>>>>>>>>>>>>>>> the numbers).

    That's true, and I would prefer that rather than >>>>>>>>>>>>>>>>>>>>> Gödel's mapping. But
    the proof of Gödel's theorem is simpler if the >>>>>>>>>>>>>>>>>>>>> number of symbols in
    the alphabet is prime even if that would mean that >>>>>>>>>>>>>>>>>>>>> some of the symbols
    are unused.

    Godel's Theorem doesn't need the number of symbols >>>>>>>>>>>>>>>>>>>> to be prime, it uses prime numbers to number the >>>>>>>>>>>>>>>>>>>> symbols, and prime powers for the position. >>>>>>>>>>>>>>>>>>>
    And consequently Gödel's example of an undecidable >>>>>>>>>>>>>>>>>>> formula is more complex
    than needed. Which doesn't really matter as the >>>>>>>>>>>>>>>>>>> complex details can be
    hidden behind definitions.


    ...We are therefore confronted with a proposition >>>>>>>>>>>>>>>>>> which asserts its own unprovability. 15 ... >>>>>>>>>>>>>>>>>> (Gödel 1931:40-41)

    G := (F ⊬ G) // Olcott's Minimal Type Theory >>>>>>>>>>>>>>>>>> https://philarchive.org/archive/PETMTT-4v2 // YACC BNF >>>>>>>>>>>>>>>>>> of MTT

    ?- G = not(provable(F, G)).
    G = not(provable(F, G)).

    ?- unify_with_occurs_check(G, not(provable(F, G))). >>>>>>>>>>>>>>>>>> false.

    Gödel, Kurt 1931.
    On Formally Undecidable Propositions of Principia >>>>>>>>>>>>>>>>>> Mathematica And Related Systems

    Nice to see that you don't disagree.

    In other words you agree that I proved 1931
    Incompleteness is incorrect.
    Gödel's G when boiled down to its barest essence is >>>>>>>>>>>>>>>> simply semantically
    unsound the same way the Liar Paradox is unsound. >>>>>>>>>>>>>>>
    As yousually your "in other words" is a lie. Existence of >>>>>>>>>>>>>>> a simpler proof
    does not make the original one incorrect.

    My words are true within your words:
       "Nice to see that you don't disagree."
    If you didn't mean that then you should not have said that. >>>>>>>>>>>>>
    I did not say nor mean "you did not disagree with
    anything". The usual
    meaning of what I said is that you don't disagree with what >>>>>>>>>>>>> I said in
    my previous message about the complexity of Gödel's sentence. >>>>>>>>>>>>
    The complexity of Gödel's sentence is nuts.
    G := (F ⊬ G) Just detect the cycle in this
    and Gödel is refuted.

    Nice to see that you still don't disagree with my comment >>>>>>>>>>> about the
    complexity of Gödel's sentence.

    Yet I absolutely do disagree.

    OK, you think Gödel's numbering scheme is simple.

    ...We are therefore confronted with a proposition which asserts >>>>>>>> its own unprovability. 15 ... (Gödel 1931:40-41)

    It totally hides the details that proof his theorem is unsound. >>>>>>>
    You have never revealed any unsound detail of the proof, not even >>>>>>> whether it uses a false premise or an invalid inference.

    The details of the proof that use Gödel numbers as their
    primary basis hide the underlying semantics about exactly
    what unprovable in F actually means.

    No, they don't. That is very clearly expressed.

    They don't answer the question why and how is G unprovable in F
    their answer is that there is some number that some how says so.

    That no proof proves G is sufficient to say that G is unprovable.

    If G is semantic gibberish then G would not be provable.

    That does not follow.


    G := "lksef 34t987n m nk6f9-823t5jkn mhgtr,edgsbm"
    try and prove that.

    G if provable if there is a proof that is
    valid in the theory and ends with G. If there is not then G is
    unprovable. Consequently, if G is not in the language of the
    theory then it is unprovable.


    G := "this sentence is not true"
    That is semantic gibberish because it has a cycle
    in its directed graph.

    This is what a cycle in the directed graph of
    its evaluation sequence looks like:

    "this sentence is not true"
    What is it not true about?
    It is not true about being not true.
    What is it is not true about being not true about.
    It is it is not true about being not true about being not true.

    This sentence is not true: "This sentence is not true"
    is true because the inner sentence is gibberish.

    But Gödel's G is a

    convoluted mess that can be succinctly expressed
    as this: G := (F ⊬ G)

    A the screwy tricks that Gödel used were because
    he chose a language with insufficient expressiveness.
    If you want to talk about provability then use a
    language with a provability operator: ⊢

    You want to talk about self-reference then use a language
    having a way to directly express self-reference with this
    operator :=

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

    https://monoskop.org/images/9/93/Kurt_G%C3%B6del_On_Formally_Undecidable_Propositions_of_Principia_Mathematica_and_Related_Systems_1992.pdf


    When you try to do this in a language lacking these
    basic building blocks you are going to have lots of
    purely extraneous complexity.

    sentence of the first order Peano arithmetic and
    therefore has an arithmetic meaning. Gödel also proved that in its arithmetic meaning G is true. In some non-arthmetic meaning it can
    be false.


    G := (F ⊬ G) // Is is true that this G is not provable
    because it has a cycle in its evaluation sequence preventing
    if from even being evaluated.

    Page 254 of Clocksin & Mellish explain this in depth. https://athena.ecs.csus.edu/~mei/logicp/Programming_in_Prolog.pdf
    --
    Copyright 2025 Olcott "Talent hits a target no one else can hit; Genius
    hits a target no one else can see." Arthur Schopenhauer
    --- Synchronet 3.21a-Linux NewsLink 1.2
  • From Mikko@[email protected] to comp.theory on Sat Nov 8 10:34:22 2025
    From Newsgroup: comp.theory

    On 2025-11-07 13:00:44 +0000, olcott said:

    On 11/7/2025 2:14 AM, Mikko wrote:
    On 2025-11-06 11:03:30 +0000, olcott said:

    On 11/6/2025 2:35 AM, Mikko wrote:
    On 2025-11-05 11:55:33 +0000, olcott said:

    On 11/5/2025 4:46 AM, Mikko wrote:
    On 2025-11-04 17:45:04 +0000, olcott said:

    On 11/4/2025 3:51 AM, Mikko wrote:
    On 2025-11-04 00:32:51 +0000, olcott said:

    On 11/3/2025 6:29 PM, Tristan Wibberley wrote:
    On 03/11/2025 23:40, olcott wrote:

    [the snip of the century]

    G := (F ⊬ G)
    G is defined as unprovable from F.
    That is the ordinary "defined as" operator.

    That's "definitionally reduces to", I think. If "(F ⊬ G)" is not >>>>>>>>>> ultimately defined then G can still be not defined.

    "define" /is/ a funny word isn't it? Several fields have mixed it up in
    different ways.


    ?- G = not(provable(F, G)).
    G = not(provable(F, G)).

    ?- unify_with_occurs_check(G, not(provable(F, G))).
    false.

    The point is that Prolog determines it is semantically
    unsound because it has a cycle in the directed graph of
    its evaluation sequence.

    Prolog does not deremine it semantically unsound.

    In other words you think that when the evaluation
    of an expression gets stuck in an infinite loop
    because of the self-reference in this expression
    that this expression is semantically sound?

    First of all, it does not stick in an infinite loop if you don't do >>>>>> with it anything that would stick in an infinte loop.

    The key idea is that the expression has a cycle in the
    directed graph of its evaluation sequence. This does
    make the expression semantically unsound.

    The expression "semanitcally unsound" does not mean anything if
    no semantics is applied. It is also meaningless if the aplied
    semantics does not assound any soundness to anything.

    You are trying to be a s disagreeable as possible.

    A truth is a truth even when you disagree.

    G := (F ⊬ G)
    The above expression has a cycle in the directed
    graph of its evaluation sequence making it incorrect.

    By the usual rules it is syntactiaclly incorrect because he symbol on
    the left side of := is used on the right side.

    But that is irrelevant to Gödel's proof where G is not used before
    nor in the definition of G.
    --
    Mikko

    --- Synchronet 3.21a-Linux NewsLink 1.2
  • From Mikko@[email protected] to comp.theory on Sat Nov 8 10:37:19 2025
    From Newsgroup: comp.theory

    On 2025-11-07 13:31:46 +0000, olcott said:

    On 11/7/2025 2:21 AM, Mikko wrote:
    On 2025-11-06 11:08:22 +0000, olcott said:

    On 11/6/2025 2:39 AM, Mikko wrote:
    On 2025-11-05 11:52:40 +0000, olcott said:

    On 11/5/2025 4:49 AM, Mikko wrote:
    On 2025-11-04 18:05:34 +0000, olcott said:

    On 11/4/2025 3:56 AM, Mikko wrote:
    On 2025-11-03 23:45:57 +0000, olcott said:

    On 11/2/2025 6:45 AM, Mikko wrote:
    On 2025-11-01 13:54:09 +0000, olcott said:

    On 11/1/2025 4:18 AM, Mikko wrote:
    On 2025-10-31 12:20:13 +0000, olcott said:

    On 10/31/2025 6:15 AM, Mikko wrote:
    On 2025-10-30 13:03:23 +0000, olcott said:

    On 10/30/2025 5:50 AM, Mikko wrote:
    On 2025-10-29 16:25:00 +0000, olcott said:

    On 10/29/2025 5:45 AM, Mikko wrote:
    On 2025-10-28 15:12:29 +0000, olcott said: >>>>>>>>>>>>>>>>>>
    On 10/28/2025 4:58 AM, Mikko wrote:
    On 2025-10-28 01:22:21 +0000, Richard Damon said: >>>>>>>>>>>>>>>>>>>>
    On 10/27/25 5:45 AM, Mikko wrote:
    On 2025-10-26 17:57:16 +0000, Richard Damon said: >>>>>>>>>>>>>>>>>>>>>>
    On 10/26/25 7:44 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>>> On 2025-10-25 19:57:19 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>>>>>
    On 10/25/2025 6:59 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>>>>> On 2025-10-24 17:37:43 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>>>>>>>
    On 10/24/2025 2:46 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>>> On 2025-10-23 15:39:13 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>>>>>>>>>
    On 10/23/2025 5:02 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>> On 2025-10-22 12:39:31 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    On 10/22/2025 4:23 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> On 2025-10-21 15:11:19 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    On 10/21/2025 4:31 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> On 2025-10-20 16:24:46 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    On 10/20/2025 3:55 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> On 2025-10-19 15:03:34 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    On 10/19/2025 3:44 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> On 2025-10-18 10:58:15 +0000, olcott said:

    On 10/18/2025 4:30 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> That is not a sense of "proof". >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> That is the correct way to do a proof. >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    A way to do is not a sense. >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    The conventional way to do proofs concludes that
    within its rules if the Moon is made from green
    cheese and the Moon is not made from green cheese
    this proves that Donald Trump is the Lord and savior Jesus Christ.

    Right, and the empirical falct that nobody has verified all of
    1. the Moon is made from green cheese >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> 2. the Moon is not made from grenn cheese >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> 3. Donald Trump is not the Lord and saviour Jesus Christ
    at the same time supports the idea that the conventiona wya to
    do proofs is correct and trustworthy. >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    When we require that correct reasoning is only semantic
    logical entailment from basic facts the Principle of
    Explosion ceases to exist. >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    Only if you exclude from "correct reasioning" some reasning that
    actually is correct. >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    There is no counter-example that can possibly exist
    that can show there are any gaps in the body of human
    knowledge that can be expressed in language that begins
    with a consistent set of basic facts and only applies
    semantic logical entailment to these facts. >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    There is no language that begins with a consistent set of basic facts
    and only applies semantic logical entailment to those facts and can
    express all of human knowledge without any gaps.

    A subset of formalized English does do this. >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    Nobody has ever presented such subset. >>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    ChatGPT rewords my words into that subset. >>>>>>>>>>>>>>>>>>>>>>>>>>>>
    Your words have much less material than all human knowledge without
    any gaps. Therefore it is impossible to verify that you have told
    every necessary word to it. >>>>>>>>>>>>>>>>>>>>>>>>>>>
    Categorically exhaustive reasoning reverse- engineers
    the required architecture of the system. Wittgenstein
    did this on Gödel https://www.liarparadox.org/ Wittgenstein.pdf
    and he was so succinct eliminate the convoluted mess of Gödel
    numbers that people mistook his succinct analysis as simplistic
    not understanding what Gödel was really saying. >>>>>>>>>>>>>>>>>>>>>>>>>>
    Yes, an expectable consequence of ignoring essential aspects is
    not understanding.

    Gödel numbers are merely the ridiculously convoluted >>>>>>>>>>>>>>>>>>>>>>>>> way that Gödel added the functionality of this simple
    operator: ⊢ to a formal language woefully too inexpressive.

    Natural numbers are one of the best understood topics of mathematics.
    Therefore restricting the assumptions to natural numbers provdes the
    basis for the most interesting result. >>>>>>>>>>>>>>>>>>>>>>>>
    Of course one can ask whether one can prove a similar theorem about
    finite strings. It is much simpler to express claims and proofs as
    fimite strings as thats how they are usually expressed anyway. But
    that requires that one first constructs a theory of finite strings.

    But we can show a direct one-to-one mapping of finite strings in a
    finite alphabet to natural numbers (it just becomes the notational base
    for the numbers).

    That's true, and I would prefer that rather than Gödel's mapping. But
    the proof of Gödel's theorem is simpler if the number of symbols in
    the alphabet is prime even if that would mean that some of the symbols
    are unused.

    Godel's Theorem doesn't need the number of symbols to be prime, it uses
    prime numbers to number the symbols, and prime powers for the position.

    And consequently Gödel's example of an undecidable formula is more complex
    than needed. Which doesn't really matter as the complex details can be
    hidden behind definitions.


    ...We are therefore confronted with a proposition which asserts its own
    unprovability. 15 ...
    (Gödel 1931:40-41)

    G := (F ⊬ G) // Olcott's Minimal Type Theory >>>>>>>>>>>>>>>>>>> https://philarchive.org/archive/PETMTT-4v2 // YACC BNF of MTT

    ?- G = not(provable(F, G)).
    G = not(provable(F, G)).

    ?- unify_with_occurs_check(G, not(provable(F, G))). >>>>>>>>>>>>>>>>>>> false.

    Gödel, Kurt 1931.
    On Formally Undecidable Propositions of Principia Mathematica And
    Related Systems

    Nice to see that you don't disagree.

    In other words you agree that I proved 1931 Incompleteness is incorrect.
    Gödel's G when boiled down to its barest essence is simply semantically
    unsound the same way the Liar Paradox is unsound. >>>>>>>>>>>>>>>>
    As yousually your "in other words" is a lie. Existence of a simpler proof
    does not make the original one incorrect.

    My words are true within your words:
       "Nice to see that you don't disagree."
    If you didn't mean that then you should not have said that. >>>>>>>>>>>>>>
    I did not say nor mean "you did not disagree with anything". The usual
    meaning of what I said is that you don't disagree with what I said in
    my previous message about the complexity of Gödel's sentence. >>>>>>>>>>>>>
    The complexity of Gödel's sentence is nuts.
    G := (F ⊬ G) Just detect the cycle in this
    and Gödel is refuted.

    Nice to see that you still don't disagree with my comment about the
    complexity of Gödel's sentence.

    Yet I absolutely do disagree.

    OK, you think Gödel's numbering scheme is simple.

    ...We are therefore confronted with a proposition which asserts its own
    unprovability. 15 ... (Gödel 1931:40-41)

    It totally hides the details that proof his theorem is unsound. >>>>>>>>
    You have never revealed any unsound detail of the proof, not even >>>>>>>> whether it uses a false premise or an invalid inference.

    The details of the proof that use Gödel numbers as their
    primary basis hide the underlying semantics about exactly
    what unprovable in F actually means.

    No, they don't. That is very clearly expressed.

    They don't answer the question why and how is G unprovable in F
    their answer is that there is some number that some how says so.

    That no proof proves G is sufficient to say that G is unprovable.

    If G is semantic gibberish then G would not be provable.

    That does not follow.

    G := "lksef 34t987n m nk6f9-823t5jkn mhgtr,edgsbm"
    try and prove that.

    The expression is not in the language of Peano arithmeitc so G
    is not provable in Peano arithmetic. Perhaps it is provable
    in some other theory that I don't know.
    --
    Mikko

    --- Synchronet 3.21a-Linux NewsLink 1.2
  • From olcott@[email protected] to comp.theory on Sat Nov 8 07:47:15 2025
    From Newsgroup: comp.theory

    On 11/8/2025 2:34 AM, Mikko wrote:
    On 2025-11-07 13:00:44 +0000, olcott said:

    On 11/7/2025 2:14 AM, Mikko wrote:
    On 2025-11-06 11:03:30 +0000, olcott said:

    On 11/6/2025 2:35 AM, Mikko wrote:
    On 2025-11-05 11:55:33 +0000, olcott said:

    On 11/5/2025 4:46 AM, Mikko wrote:
    On 2025-11-04 17:45:04 +0000, olcott said:

    On 11/4/2025 3:51 AM, Mikko wrote:
    On 2025-11-04 00:32:51 +0000, olcott said:

    On 11/3/2025 6:29 PM, Tristan Wibberley wrote:
    On 03/11/2025 23:40, olcott wrote:

    [the snip of the century]

    G := (F ⊬ G)
    G is defined as unprovable from F.
    That is the ordinary "defined as" operator.

    That's "definitionally reduces to", I think. If "(F ⊬ G)" is not >>>>>>>>>>> ultimately defined then G can still be not defined.

    "define" /is/ a funny word isn't it? Several fields have >>>>>>>>>>> mixed it up in
    different ways.


    ?- G = not(provable(F, G)).
    G = not(provable(F, G)).

    ?- unify_with_occurs_check(G, not(provable(F, G))).
    false.

    The point is that Prolog determines it is semantically
    unsound because it has a cycle in the directed graph of
    its evaluation sequence.

    Prolog does not deremine it semantically unsound.

    In other words you think that when the evaluation
    of an expression gets stuck in an infinite loop
    because of the self-reference in this expression
    that this expression is semantically sound?

    First of all, it does not stick in an infinite loop if you don't do >>>>>>> with it anything that would stick in an infinte loop.

    The key idea is that the expression has a cycle in the
    directed graph of its evaluation sequence. This does
    make the expression semantically unsound.

    The expression "semanitcally unsound" does not mean anything if
    no semantics is applied. It is also meaningless if the aplied
    semantics does not assound any soundness to anything.

    You are trying to be a s disagreeable as possible.

    A truth is a truth even when you disagree.


    You are making no effort to understand the truth.
    This is causing you to get wrong answers.

    You do not understand what a cycle in the directed
    graph of an evaluation sequence is and on the basis
    of your lack of understanding to conclude that it
    is nonsense.

      G := (F ⊬ G)
    The above expression has a cycle in the directed
    graph of its evaluation sequence making it incorrect.

    By the usual rules it is syntactiaclly incorrect because he symbol on
    the left side of := is used on the right side.


    Yes. Prolog detects the semantic error syntactically.

    But that is irrelevant to Gödel's proof where G is not used before
    nor in the definition of G.


    G := (F ⊬ G) // encodes G asserts its own unprovability in F
    ...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
    --
    Copyright 2025 Olcott "Talent hits a target no one else can hit; Genius
    hits a target no one else can see." Arthur Schopenhauer
    --- Synchronet 3.21a-Linux NewsLink 1.2