Groups | Search | Server Info | Login | Register

Groups > comp.software-eng > #3977

Re: Making the body of knowledge computable

Cross-posted to 6 groups.

Show all headers | View raw

On 2/12/2026 6:29 AM, Richard Damon wrote:
> On 2/11/26 8:08 AM, olcott wrote:
>> On 2/11/2026 6:56 AM, Richard Damon wrote:
>>> On 2/10/26 11:59 PM, olcott wrote:
>>>> We completely replace the foundation of truth conditional
>>>> semantics with proof theoretic semantics. Then expressions
>>>> are "true on the basis of meaning expressed in language"
>>>> only to the extent that all their meaning comes from
>>>> inferential relations to other expressions of that language.
>>>> This is a purely linguistic PTS notion of truth with no
>>>> connections outside the inferential system.
>>>>
>>>> Well-founded proof-theoretic semantics reject expressions
>>>> lacking a "well-founded justification tree" as meaningless.
>>>> ∀x (~Provable(T, x) ⇔ Meaningless(T, x))
>>>>
>>>
>>> The problem is that you new system can't handle mathematics.
>>>
>>> The problem, as has been pointed out, is that mathematics, by the 
>>> axiom of induction, accepts as true statements that can be 
>>> established by an infinite number of steps as true, and shows a 
>>> method to solve SOME of them.
>>>
>>> Also, "Halting" is a well-founded property of ALL machines, as they 
>>> MUST either Halt or not, and HALTING is always provable, so those 
>>> machines that do not halt, must be non-halting.
>>>
>>> Your "logic" essentially denies the property of the excluded middle 
>>> for systems that have infinite members, but some statements are 
>>> inherently of the class of the excluded middle.
>>>
>>> As I have said, TRY to show how your PTS can establish the 
>>> mathematics of the Natural Numbers.
>>>
>>> Try to even fully define ADDITION without the need for allowing 
>>> unbounded steps.
>>>
>>
>> ∀x ∈ PA (  True(PA, x) ≡ PA ⊢  x )
>> ∀x ∈ PA ( False(PA, x) ≡ PA ⊢ ¬x )
>> ∀x ∈ PA ( ¬WellFounded(PA, x) ≡ (¬True(PA, x) ∧ (¬False(PA, x)))
> 
> So, where is "Addition" in that?
> 
> How do you determine ~True(PA, x)? in your proof-Theoretic semantics?
> 

0=1
equal(successor(0), successor(successor(0))==FALSE

>>
>>    "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..." https://doi.org/10.1007/s11245-011-9107-6
> 
> A question in General Philosophy, not Formal Logic.
> 
>>
>> Spend 20 hours carefully studying this and get back to me.
>> https://plato.stanford.edu/entries/proof-theoretic-semantics/
> 
> Which is a paper on PHILOSOPHY, not Formal Logic.
> 

Logic and math choose a notion of truth from philosophy and
the choose the wrong one.

∀x (Provable(T, x) ⇔ Meaningful(T, x)) --- (Schroeder-Heister 2024)
∀x (Provable(x) ⇒ True(x)) --- Anchored in (Prawitz, 2012)

> Note, Formal Logic BEGINS with its definiton of Truth, which is based on 
> the, possibly infinite, application of its logical rules.
> 

As you yourself kept harping on some times true(x)
exists outside of the domain of knowledge.

> To change that to a Proof-Theoretical Semantics basis changes the 
> results of the system. In particular, any system that generates an 
> infinite domain (like mathemtics) becomes problematic.
> 

Only in cases where a truth value requires infinite
inference steps.

>>
>> It makes "true on the basis of meaning expressed in language"
>> reliably computable for the entire body of knowledge.
>>
> 
> Nope.
> 
> IT makes your definition of "true" just a lie.
> 

∀x (Provable(T, x) ⇔ Meaningful(T, x)) --- (Schroeder-Heister 2024)
∀x (Provable(x) ⇒ True(x)) --- Anchored in (Prawitz, 2012)

That you are woefully ignorant of PTS does not entail
that I am incorrect. What you call an intentional falsehood
has always been your own ignorance.

> How can you "compute" if a number exist that satisfies the relationship 
> that Godel developes in his proof?
> 

PTS has no notion of satisfies.

> Why does that relationship, which is just built from the fundamental 
> operation of mathematics in PA not have "meaning"?
> 

When any expression of language lacks a semantic connection
to the expressions that define it this expression remains
undefined.

> Where is the line between that relationship, and the statement that we 
> can assert that 1 + 1 = 2?
> 

successor(0) + successor(0) = successor(successor(0))

> Proof-Thoeretic Semantics in sets with infinite members just severly 
> limits what you can do in that field.
> 
> And that is why real Proof-Theoretic Semantics doesn't assert that what 
> we haven't proven is meaningless, just that we don't yet know the 
> meaning, because it knows that all we can know is that we haven't yet 
> proven something, and not that it can't be proven, unless we can 
> actually find a proof of that (like proving its opposite).
> 

It could be meaningless or it could be unknown either
way is is outside of the domain of knowledge.

> Your system becomes a lie, because while you assert you are using just 
> Proof-Theoretical Semantics, you need to actully have Truth-Conditional 
> logic to determine those semantics, as there ARE things not provablable 
> unprovable, and thus your tri-valued system (true, false, non-well- 
> founded) can't have values exstablished by proof-thoeretic logic.
> 

Like I already said carefully study the article written by
the guy that coined the term: Proof-Theoretic Semantics
https://plato.stanford.edu/entries/proof-theoretic-semantics/

-- 
Copyright 2026 Olcott<br><br>

My 28 year goal has been to make <br>
"true on the basis of meaning expressed in language"<br>
reliably computable for the entire body of knowledge.<br><br>

This required establishing a new foundation<br>

Back to comp.software-eng | Previous | Next — Previous in thread | Next in thread | Find similar

Thread

Making the body of knowledge computable olcott <polcott333@gmail.com> - 2026-02-10 22:59 -0600
  Re: Making the body of knowledge computable Richard Damon <Richard@Damon-Family.org> - 2026-02-11 07:56 -0500
    Re: Making the body of knowledge computable olcott <polcott333@gmail.com> - 2026-02-11 07:08 -0600
      Re: Making the body of knowledge computable Richard Damon <Richard@Damon-Family.org> - 2026-02-12 07:29 -0500
        Re: Making the body of knowledge computable olcott <polcott333@gmail.com> - 2026-02-12 10:06 -0600
          Re: Making the body of knowledge computable Richard Damon <Richard@Damon-Family.org> - 2026-02-12 23:11 -0500

csiph-web