XPost: comp.theory, sci.math   
   From: polcott333@gmail.com   
      
   On 1/3/2026 1:18 PM, Richard Damon wrote:   
   > On 1/3/26 11:47 AM, olcott wrote:   
   >> 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)   
   >   
   > WHich you don't seem to understand is the INTERPREATION of the statement   
   > made in the meta system about the statement.   
   >   
      
   That is not what the sentence literally says.   
      
   >>   
   >> 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.   
   >   
   > Nope. Just that it uses language too complicated for you to understand.   
   >   
   > G, itself, asserts no such thing.   
   >   
   >>   
   >> This semantically entails that:   
   >> A proof of G requires a sequence of inference   
   >> steps that prove that they themselves do not exist.   
   >   
   > Right, so no such prove IN THE BASE SYSTEM can exist.   
   >   
   >>   
      
   [continued in next message]   
      
   --- SoupGate-DOS v1.05   
    * Origin: you cannot sedate... all the things you hate (1:229/2)