XPost: sci.math, comp.theory   
   From: mikko.levanto@iki.fi   
      
   On 12/02/2026 17:48, olcott wrote:   
   > On 2/12/2026 2:11 AM, Mikko wrote:   
   >> On 11/02/2026 14:38, olcott wrote:   
   >>> On 2/11/2026 4:51 AM, Mikko wrote:   
   >>>> On 10/02/2026 15:37, olcott wrote:   
   >>>>> On 2/10/2026 3:06 AM, Mikko wrote:   
   >>>>>> On 09/02/2026 17:36, olcott wrote:   
   >>>>>>> On 2/9/2026 8:57 AM, Mikko wrote:   
   >>>>>>>> On 07/02/2026 18:43, olcott wrote:   
   >>>>>>>>>   
   >>>>>>>>> Conventional logic and math have been paralyzed for   
   >>>>>>>>> many decades by trying to force-fit semantically   
   >>>>>>>>> ill-formed expressions into the box of True or False.   
   >>>>>>>>   
   >>>>>>>> Logic is not paralyzed. Separating semantics from inference rules   
   >>>>>>>> ensures that semantic problems don't affect the study of proofs   
   >>>>>>>> and provability.   
   >>>>>>>   
   >>>>>>> Then you end up with screwy stuff such as the psychotic   
   >>>>>>> https://en.wikipedia.org/wiki/Principle_of_explosion   
   >>>>>>   
   >>>>>> That you call it psychotic does not make it less useful. Often an   
   >>>>>> indirect proof is simpler than a direct one, and therefore more   
   >>>>>> convincing. But without the principle of explosion it might be   
   >>>>>> harder or even impossible to find one, depending on what there is   
   >>>>>> instead.   
   >>>>>   
   >>>>> Completely replacing the foundation of truth conditional   
   >>>>> semantics with proof theoretic semantics then an expression   
   >>>>> is "true on the basis of meaning expressed in language"   
   >>>>> only to the extent that its meaning is entirely comprised   
   >>>>> of its inferential relations to other expressions of that   
   >>>>> language. AKA linguistic truth determined by semantic   
   >>>>> entailment specified syntactically.   
   >>>>>   
   >>>>> Well-founded proof-theoretic semantics reject expressions   
   >>>>> lacking a "well-founded justification tree" as meaningless.   
   >>>>> ∀x (~Provable(T, x) ⇔ Meaningless(T, x))   
   >>>>   
   >>>> Usually it is thought that an expression can be determined to be   
   >>>> meaningful even when it is not known whether it is provable. For   
   >>>> example, the program fragment   
   >>>>   
   >>>>    if (x < 5) {   
   >>>>      show(x);   
   >>>>    }   
   >>>>   
   >>>> is quite meaningful even when one cannot prove or even know whether   
   >>>> x at the time of execution is less than 5.   
   >>>>   
   >>>   
   >>> Only Proof-Theoretic Semantics   
   >>> https://plato.stanford.edu/entries/proof-theoretic-semantics/   
   >>>   
   >>> Can make   
   >>> "true on the basis of meaning expressed in language"   
   >>> reliably computable for the entire body of knowledge.   
   >>   
   >> In order to achieve that all arithmetic must be excluded from   
   >> "true on the basis of meaning expressed in language". There   
   >> is no way to compute wheter a sentence of the first order   
   >> Peano arithmetic is provable.   
   >   
   > ∀x (Provable(T, x) ⇔ Meaningful(T, x)) --- (Schroeder-Heister 2024)   
   > ∀x (Provable(x) ⇒ True(x)) --- Anchored in (Prawitz, 2012)   
   >   
   > What is the appropriate notion of truth for sentences whose meanings are   
   > understood in epistemic terms such as proof or ground for an assertion?   
   > It seems that the truth of such sentences has to be identified with the   
   > existence of proofs or grounds...   
      
   Which means that if it is not determined whether there is a proof of   
   a sentence and no way to find out the truth of that sentence is not   
   known and cannot be computed.   
      
   --   
   Mikko   
      
   --- SoupGate-Win32 v1.05   
    * Origin: you cannot sedate... all the things you hate (1:229/2)