home bbs files messages ]

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

   sci.logic      Logic -- math, philosophy & computationa      262,936 messages   

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

   Message 262,722 of 262,936   
   Mikko to olcott   
   Re: The Halting Problem asks for too muc   
   25 Jan 26 13:19:19   
   
   XPost: sci.math, comp.theory   
   From: mikko.levanto@iki.fi   
      
   On 24/01/2026 16:01, olcott wrote:   
   > On 1/24/2026 2:20 AM, Mikko wrote:   
   >> On 23/01/2026 12:22, olcott wrote:   
   >>> On 1/23/2026 3:13 AM, Mikko wrote:   
   >>>> On 22/01/2026 18:40, olcott wrote:   
   >>>>> 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.   
   >>>>   
   >>>> There is no concept of "truth-bearer" in an uninterpreted theory   
   >>>> because   
   >>>> there is not concept of "truth". The relevant concept is "sell-formed-   
   >>>> formula" and Gödels sentence is one. It may be true or false in an   
   >>>> interpretation.   
   >>   
   >>> There is a   
   >>> "true on the basis of meaning expressed in language"   
   >>> and I figured out how to make it computable over the   
   >>> body of knowledge.   
   >>   
   >> Except that "true on the basis of meaning expressed in language" is   
   >> nmt computable and does not cover all of the body of knowldge.   
   >   
   > When the basis of "true" is proof theoretic semantics   
   > internal to the formal system relative to its own axioms   
   > and not truth conditional in a separate model outside   
   > of the system undecidability ceases to exist.   
      
   No, it does not. It does not matter what you call it, a sentence   
   that cannot be neither proven nor disproven is undecidable because   
   that is what the word means. An example is Gödel's sentence in   
   Peano arithmetics.   
      
   --   
   Mikko   
      
   --- 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