XPost: comp.theory, sci.math   
   From: news.dead.person.stones@darjeeling.plus.com   
      
   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.   
      
   --- SoupGate-DOS v1.05   
    * Origin: you cannot sedate... all the things you hate (1:229/2)