XPost: comp.theory, sci.math   
   From: mikko.levanto@iki.fi   
      
   On 16/02/2026 15:47, olcott wrote:   
   > On 2/16/2026 5:25 AM, Mikko wrote:   
   >> On 15/02/2026 15:02, polcott wrote:   
   >>> On 2/15/2026 3:18 AM, Mikko wrote:   
   >>>> On 14/02/2026 17:31, polcott wrote:   
   >>>>> On 2/14/2026 3:14 AM, Mikko wrote:   
   >>>>>> On 13/02/2026 15:32, olcott wrote:   
   >>>>>>> On 2/13/2026 2:30 AM, Mikko wrote:   
   >>>>>>>> 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.   
   >>>>>>>   
   >>>>>>> Its all in a finite directed acyclic graph of knowledge.   
   >>>>>>   
   >>>>>> No, it is not. The set of provable statements of the first order   
   >>>>>> Peano   
   >>>>>> arithmetic is infinite so it cannot be in a finite graph.   
   >>>>>   
   >>>>> The specialized nature of my work has exceeded the technical   
   >>>>> knowledge of people here and most everywhere else.   
   >>>>   
   >>>> That an inifinite sent cannot be in a finite graph may exceed your   
   >>>> technical knowledge but certainly doesn't everyone else's.   
   >>   
   >>> ∀x((x > 10) ⇒ (x > 0))   
   >>> Does not mean to test every x.   
   >>   
   >> Irrelevant. That is only one sentence, not infinitely many.   
   >>   
   >>> ∀x ∈ PA (True(PA, x) ↔ PA ⊢ x)   
   >>> Does not mean to test every x in PA   
   >>   
   >> No, it merely declares that there are two symbols for one predicate   
   >> (which, if interpreted accordint to the usual meaning of either symbol,   
   >> is uncomputable).   
   >   
   > What do you think that this means: PA ⊢ x ?   
      
   The exact meaning depends on the context and the meanings of the types   
   of the left and right side expressions. The usual metalogical meaning   
   is that x is a theorem of some variant of PA. If something else is   
   meant that should be specified in the opus where the expression is used.   
      
   --   
   Mikko   
      
   --- SoupGate-Win32 v1.05   
    * Origin: you cannot sedate... all the things you hate (1:229/2)