XPost: comp.theory, sci.math   
   From: news.dead.person.stones@darjeeling.plus.com   
      
   On 02/01/2026 15:25, Richard Damon wrote:   
   > On 1/2/26 1:14 AM, Tristan Wibberley wrote:   
   >> On 02/01/2026 04:45, Richard Damon wrote:   
   >>   
   >>>   
   >>>> Truth in the base system has always   
   >>>> actually been theorems of the base system.   
   >>>   
   >>> But only if "Theorem" includes things proven to be true in the system   
   >>> even if the proof is in another.   
   >>   
   >> If the statement is derived in another then it is a theorem of the other.   
   >   
   > I will disagree with you here. Maybe it iw what you are trying to define   
   "derived" as.   
   >   
   > I can certainly use one system to guide me in building a statement in   
   another. Or do you think that   
   > is a task too hard?   
   >   
   > I can certainly use one system that knows about another to show that a   
   statement must be true in   
   > that other.   
   >   
   > If you want to reserve the lable "Theorem" for only things provable in taht   
   system, I will let you,   
   > but point out I think you are in the minority, and ask for your reference   
   that specifies that.   
      
   No, I'd say Tristan is spot on with how that's normally done.   
      
   While speaking informally, "theorem" can mean "a mathematical statement that   
   has a convincing   
   argument for its truth" (e.g. Pythagoras' theorem), in formal logic "Theorem"   
   and "Theory" have a   
   technical meaning:  "Theory" being the deductive closure of a set of axioms,   
   and a Theorem being a   
   sentence of the Theory.  So every Theorem in the Theory has a "derivation"   
   from the theories axioms.   
     It is not directly to do with "truth" in the formal system.  [Of course, we   
   want our system   
   (including axioms) to be sound, so all Theorems will be true.]   
      
         
      
   Of course, you could be learning from an author taking a different approach,   
   but I haven't   
   personally come across one who would say that the sentence represented by G   
   was a "Theorem" of the   
   underlying logical system!  (That would (IMO) be grossly misleading...)   
      
   Similarly, the word "proof" can be informal (simply an argument that convinces   
   people of the truth   
   of a statement), or refer to the "proof calculus" of the formal system being   
   discussed.  Most   
   authors I've come across seem to use "proof" more or less informally and for   
   clarity choose another   
   word for whatever sequence of syntactic "proof steps" the formal system   
   specifies.  Often   
   "derivation" is used, and that seems intuitive to me, so I try to always use   
   that term here, and   
   using "proof" for more general mathematial arguments, e.g. proving that the G   
   statement is "true"   
   using some meta-theory.   
      
   Also just as an aside, I don't recall that Godel ever talked about "truth" of   
   his G statement.  His   
   proof was concerned with provability.  (Neither the G sentence nor its   
   negation is provable.)   
      
      
   Mike.   
      
   --- SoupGate-DOS v1.05   
    * Origin: you cannot sedate... all the things you hate (1:229/2)