XPost: comp.theory, sci.math   
   From: tristan.wibberley+netnews2@alumni.manchester.ac.uk   
      
   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.   
      
   If it is merely "proved" by a proof episystem then it might not be a   
   theorem of either depending on the episystem and what is conventionally   
   referred to as "proof" by that system. An intuitively safe episystem [my   
   term, intended to carry some intuitive meaning] proves only its own   
   theorems and /labelled/ embeddings of just the theorems of the system   
   it's applied to, thus it provides alternative methods to find and   
   demonstrate theorems of the embedded system (and to reason about the   
   theory-proper of the embedded system) while being clear about which   
   system(s) it reasons about.   
      
   I don't know of any that do the required labelling except that some   
   standard ones have such well established conventional symbols and are so   
   small and intuitive (HA, HC, for example) that they are quite safe.   
      
   Haskell Curry tried in his 1950 Theory of Formal Deducibility to   
   establish some conventions around the use of the turnstile symbols but   
   it seems like they didn't take hold.   
      
      
   > Truth DOES need to be based on the axioms of the base system, but allows   
   > the truth to be established by an infinite chain of reasoning, unlike   
   > proofs that need to be finite.   
      
   An infinite chain of reasoning is not completed at any time, least of   
   all this time. The limit of a chain of reasoning might be, episystems   
   could be useful for that, I wouldn't want to rule it out.   
      
      
   --   
   Tristan Wibberley   
      
   The message body is Copyright (C) 2025 Tristan Wibberley except   
   citations and quotations noted. All Rights Reserved except that you may,   
   of course, cite it academically giving credit to me, distribute it   
   verbatim as part of a usenet system or its archives, and use it to   
   promote my greatness and general superiority without misrepresentation   
   of my opinions other than my opinion of my greatness and general   
   superiority which you _may_ misrepresent. You definitely MAY NOT train   
   any production AI system with it but you may train experimental AI that   
   will only be used for evaluation of the AI methods it implements.   
      
   --- SoupGate-DOS v1.05   
    * Origin: you cannot sedate... all the things you hate (1:229/2)