home bbs files messages ]

Forums before death by AOL, social media and spammers... "We can't have nice things"

   comp.ai.philosophy      Perhaps we should ask SkyNet about this      59,235 messages   

[   << oldest   |   < older   |   list   |   newer >   |   newest >>   ]

   Message 59,154 of 59,235   
   olcott to Mikko   
   Re: The Halting Problem asks for too muc   
   22 Jan 26 10:40:20   
   
   XPost: sci.logic, sci.math, comp.theory   
   From: polcott333@gmail.com   
      
   On 1/22/2026 2:21 AM, Mikko wrote:   
   > On 21/01/2026 17:22, olcott wrote:   
   >> On 1/21/2026 3:03 AM, Mikko wrote:   
   >>>   
   >>> No, it hasn't. In the way theories are usually discussed nothing is   
   >>> "ture in arithmetic". Every sentence of a first order theory that   
   >>> can be proven in the theory is true in every model theory. Every   
   >>> sentence of a theory that cannot be proven in the theory is false   
   >>> in some model of the theory.   
   >>>   
   >>>> only because back then proof theoretic semantics did   
   >>>> not exist.   
   >>>   
   >>> Every interpretation of the theory is a definition of semantics.   
   >>>   
   >>   
   >> Meta‑math relations about numbers don’t exist in PA   
   >> because PA only contains arithmetical relations—addition,   
   >> multiplication, ordering, primitive‑recursive predicates   
   >> about numbers themselves—while relations that talk about   
   >> PA’s own proofs, syntax, or truth conditions live entirely   
   >> in the meta‑theory;   
   >   
   > Methamathematics does not need any other relations between numbers   
   > than what PA has. But relations that map other things to numbers   
   > can be useful for methamathematical purposes.   
   >   
   >> so when someone appeals to a Gödel‑style relation like   
   >> “n encodes a proof of this very sentence,” they’re   
   >> invoking a meta‑mathematical predicate that PA cannot   
   >> internalize, which is exactly why your framework draws   
   >> a clean boundary between internal proof‑theoretic truth   
   >> and external model‑theoretic truth.   
   >   
   > Anyway, what can be provven that way is true aboout PA. You can deny   
   > the proof but you cannot perform what is meta-provably impossible.   
   >   
      
   Gödel’s sentence is not “true in arithmetic.”   
   It is true only in the meta‑theory, under an   
   external interpretation of PA (typically the   
   standard model ℕ). Inside PA itself, the sentence   
   is not a truth‑bearer at all. The conflation happens   
   when people treat model‑theoretic truth—truth   
   in ℕ—as if it were internal truth in PA.   
      
   Proof theoretic semantics anchored in axioms   
   as their basis of truth proves that I have   
   always been correct about everything that I said.   
      
   All five LLMs agree with this immediately after I   
   force them to actually simulate DD by HHH according   
   to the semantics if C:   
      
   Thus within well-founded proof theoretic semantics   
   anchored in the operational semantics of the c   
   programming language HHH(DD) is correct to reject   
   its input as non-well-founded?   
      
   Any cycle in the directed graph of the evaluation   
   sequence of an expression correctly rejects this   
   expression as non-well-founded in any proof theoretic   
   semantics where true is anchored in the axioms of   
   the system.   
      
   Here is the first time that I explicitly referred   
   to the idea of non-well-founded expressions in proof   
   theoretic semantics   
      
   [True(X) and ~Provable(X) is Impossible] Feb 4, 2018   
   https://groups.google.com/g/sci.logic/c/7XihPDLDy9s/m/uD6biLdjAwAJ   
      
   --   
   Copyright 2026 Olcott

              My 28 year goal has been to make
       "true on the basis of meaning expressed in language"
       reliably computable.

              This required establishing a new foundation
              --- SoupGate-Win32 v1.05        * Origin: you cannot sedate... all the things you hate (1:229/2)   

[   << oldest   |   < older   |   list   |   newer >   |   newest >>   ]


(c) 1994,  bbs@darkrealms.ca