XPost: comp.theory, sci.math   
   From: polcott333@gmail.com   
      
   On 1/3/2026 10:32 AM, Mike Terry wrote:   
   > On 03/01/2026 03:30, Richard Damon wrote:   
   >> On 1/2/26 9:43 PM, André G. Isaak wrote:   
   >>> On 2026-01-01 20:09, Richard Damon wrote:   
   >>>> On 1/1/26 9:45 PM, André G. Isaak wrote:   
   >>>>> On 2026-01-01 16:48, Richard Damon wrote:   
   >>>>>> On 1/1/26 6:13 PM, Tristan Wibberley wrote:   
   >>>>>>> On 01/01/2026 22:40, Richard Damon wrote:   
   >>>>>>>   
   >>>>>>>> But it IS a theorem of the base system, as it uses ONLY the   
   >>>>>>>> mathematical   
   >>>>>>>> operations definable in the base system. What makes you think it   
   >>>>>>>> isn't a   
   >>>>>>>> Theorem in the base system.   
   >>>>>>>   
   >>>>>>> It has no derivation in the base system, if it had you wouldn't   
   >>>>>>> think   
   >>>>>>> the base system were incomplete.   
   >>>>>>>   
   >>>>>>   
   >>>>>> It has no PROOF in the base system.   
   >>>>>   
   >>>>> Which means it is not a theorem of the base system. A theorem is a   
   >>>>> statement which can be proven in a particular system.   
   >>>>   
   >>>> I guess it depends on your definition of a "Theorem".   
   >>>>   
   >>>> I am using the one that goes:   
   >>>>   
   >>>> "A Theorem is a statement that has been proven."   
   >>>  >   
   >>>> note, no restriction that the proof was in the system the Theorem is   
   >>>> stated in, as long as the proof shows that it is actually True in   
   >>>> that system.   
   >>>   
   >>> A theorem is a statement that can be derived from the axioms of a   
   >>> particular system. It may be true in other systems, but it is only a   
   >>> theorem in systems in which it can be derived.   
   >>   
   >> Right, And the statement og Godel's G can be fully derived in the base   
   >> system, as it is purely a mathematical relationship using the   
   >> operations derivable in the system.   
   >   
   > Neither G nor ¬G has a derivation (in your terms, a "formal prooof")   
   > within the base system.  That is what Godel proves, showing that the   
   > base system is incomplete.   
   >   
   > Mike.   
   >   
   >>   
   >> The implications of this statement can't be understood in the system,   
   >> but that isn't a requirment to be a Theorem.   
   >>   
   >>>   
   >>> An obvious example to illustrate this would be the fact that there   
   >>> are many theorems which can be derived in Euclidean geometry, but   
   >>> which are not theorems of various non-Euclidean geometries. That is   
   >>> to say, not only can they not be derived in those non-Euclidean   
   >>> geometries, but they can be shown to be *false* in those non-   
   >>> Euclidean geometries.   
   >>   
   >> Right, but G isn't like this.   
   >>   
   >>>   
   >>> Theoremhood is always tied to a particular formal system.   
   >>   
   >> Right, and the statement G needs nothing outside of the base system to   
   >> be created.   
   >>   
   >   
   > Sure.  Just creating a statement doesn't mean the statement is a   
   > Theorem.  Theorems need a "formal proof" (aka, a derivation) in that   
   > formal system.  You have a basic misunderstanding somewhere!   
   >   
   > Mike.   
   >   
   >   
   >> What the meta-system provides is a "hidden" meaning to it.   
   >>   
   >>>   
   >>> André   
   >>>   
   >>   
   >>   
   >> It is sort of like given a binary of a program. The base computer   
   >> still considers it a program, even if the only way to figure out what   
   >> this program does is to run it with all sorts of input. So, even   
   >> without a C compiler, that binary is a program.   
   >>   
   >> WIth the C compiler and the C source code, we can understand much   
   >> better what the program does, and might not need to run it for a bunch   
   >> of inputs.   
   >>   
   >> The fact that program came out of the C compiler. doesn't make it not   
   >> a program for that processor.   
   >>   
   >> In the same way, G is a statement about using a specific set of   
   >> operations defined in the base system and whether any number given   
   >> will statisfy it. WIth just the assembly code, that may be impossible   
   >> to determine, as there are an infinite number of possible inputs, so   
   >> we can't test them all.   
   >>   
   >> But, that sequence of operations that G uses, came out of a "compiler"   
   >> in the meta-system, from which we can see that this set of   
   >> instructions are just a proof tester, to see if the number is a   
   >> representation of a give proof of the statement G in the base system,   
   >> where every proof in the base system produces a unique number, and   
   >> every number produces a possible proof in the base system (though many   
   >> are just non-sense)   
   >>   
   >> The fact we used a "compiler" to generate the statement doesn't make   
   >> it not a program in the base system, but does let us understand what   
   >> it does.   
   >   
   > You have used lots of words to explain, in effect, that the G statement   
   > is a statement of the base system.  Well, most everybody here   
   > understands that perfectly well.  (Not PO though...)  Your analogy with   
   > programs has nothing more than   
   >   
   >    program  <---> statement in the language of the formal system   
   >                   (or what is often called a "sentence" in   
   that language)   
   >   
   > so program does not correlate with "Theorem" of the formal system.  All   
   > the stuff about compilers helping us to understand the purpose of   
   > program is ok, but has nothing to do with whether the program   
   > corresponds to a Theorem.   
   >   
   > You seem to understand that Godel proves that the G statement does NOT   
   > have a "derivation" (aka "formal proof using the specified proof rules   
   > of the base system") in the base system.  I.e. it is specifically NOT a   
   > "Theorem" of the base system, in the sense that people use that word /in   
   > the realm of formal logic/.   
   >   
   >   
   > Mike.   
   >   
      
   ...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   
      
   A proposition which asserts its own unprovability   
   literally means: G asserts its own unprovability.   
      
   This semantically entails that:   
   A proof of G requires a sequence of inference   
   steps that prove that they themselves do not exist.   
      
   ...14 Every epistemological antinomy can likewise   
   be used for a similar undecidability proof...   
   (Gödel 1931:40-41)   
      
   This literally means that the Liar Paradox can   
   likewise be used for a similar undecidability proof.   
      
   This semantically entails that:   
   ?- LP = not(true(LP)).   
   LP = not(true(LP)).   
   ?- unify_with_occurs_check(LP, not(true(LP))).   
   false.   
      
   Expands to not(true(not(true(not(true(not(true(...))))))))   
   Proves that the Liar Paradox is ungrounded, thus   
   neither G nor LP are truth bearers or propositions.   
      
   *Key difference between math and the philosophy of math*   
   The philosophy of math says maybe we have   
   been thinking about this stuff all wrong.   
      
   Math says of course we haven't been thinking   
   about this stuff all wrong everyone knows   
   that math is infallible.   
      
      
   [continued in next message]   
      
   --- SoupGate-DOS v1.05   
    * Origin: you cannot sedate... all the things you hate (1:229/2)