XPost: comp.theory, sci.math   
   From: news.dead.person.stones@darjeeling.plus.com   
      
   On 02/01/2026 17:54, Richard Damon wrote:   
   > On 1/2/26 12:24 PM, Mike Terry wrote:   
   >> 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.]   
   >>   
   >>       
   >   
   > Note, the addition of the adjective DEDUCTIVE.   
      
   That's the type of theory most often encountered, I'd say.  GIT is concerned   
   with such a theory,   
   where axioms are given etc. and we are looking at what sentences can be proved   
   from those axioms.   
   Wikipedia always tries to be as general as it can possibly be, making it an   
   awful place for someone   
   trying to /learn/ a maths topic.  It's great if you're already a maths   
   professor, then you can read   
   some article and nod wisely, and suggest edits to make it /even more/ general!   
   :)   
      
   >   
   >>   
   >> 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...)   
   >   
   > I will somewhat agree here, because generally the term is reserved for   
   statements about a more   
   > general truth, as opposed to a statement about a specific fact. But the most   
   generic definition is   
   > just a statment that has been proven.   
      
   Yes, but we are talking about formal systems, and "Theorem" in such a context   
   implies a proof   
   /within the proof calculus of that formal system/.  That is what GIT is   
   concerned with.  (I give an   
   example of what I mean by "proof calculus" below, but I'm sure you understand   
   the idea, just   
   possibly not the wording.)   
      
   >   
   >>   
   >> 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.   
   >   
   > The issue is that "derivation" doesn't actually imply a finiteness, which is   
   a necessity of "proof".   
      
   Where do you get that idea?  Are you thinking "derivation" is just an informal   
   word?  I'm using it   
   in the technical sense previously explained.   
      
   Within a formal system there will be a set of rules which define what a valid   
   "derivation" looks   
   like.  These would ensure that such derivations are finite.  (I'm sure someone   
   at some time has made   
   a special study of "infinite proofs", but that is off the beaten track.)  As   
   explained in my   
   previous post, I'm using "derivation" as the technical term for whatever   
   passes as a "formal proof   
   conforming to the requirements of the proof calculus of the system".  This is   
   so that the idea does   
   not get muddled with your more general kind of proof = "convincing argument in   
   some meta-theory".   
      
   Derivations have Gödel numbers.  "Convincing arguments in the meta-theory" do   
   not.  The idea of a   
   Gödel number for an infinite derivation does not make sense.   
      
   >   
   > The point is that the standard statement of "Incompleteness" talks about the   
   provability of   
   > statements in the system. Provability is inherently about the ability to   
   create a proof in the system.   
      
   "(FORMAL) Proof in the system" = "derivation".  You want to use the word   
   "proof" more generally,   
   namely to cover arguments in a meta-theory which establish some meta-truth   
   concerning the base   
   system.  That's ok [and the reason I use "derivation" to distinguish from   
   "informal proof"], but not   
   the type of "proof" that incompleteness refers to.   
      
   >   
   > Yes, often an other will use a more confined word to establish the method of   
   a proof.   
      
   Right.  The logical system will have some kind of "proof calculus" which says   
   EXACTLY what   
   constitutes a valid derivation for that system.  E.g. perhaps something like:   
      
      A derivation is a finite sequence of sentences in the language of the   
   formal system, such that   
      each sentence is either:   
      -   an axiom of the system,   
      -   or can be constructed from previous sentences by applying one of the   
          following "deduction rules":   
          -   [probably something equivalent to Modus Ponens]   
          -   [maybe other listed rules]   
      The last sentence of the derivation is the "result" of the derivation.   
      
   When Gödel talks of provability in a system, he always means such a   
   derivation, not some informal   
   convincing argument.   
      
    From here on I'm just going to use the word derivation without explaining it   
   every time!   
      
   >   
   >>   
   >> Also just as an aside, I don't recall that Godel ever talked about "truth"   
   of his G statement.   
      
   [continued in next message]   
      
   --- SoupGate-DOS v1.05   
    * Origin: you cannot sedate... all the things you hate (1:229/2)