Re: The simple essence of Proof Theoretic Semantics

On 2026-07-03 10:48, olcott wrote:
> On 7/3/2026 9:45 AM, André G. Isaak wrote:
>> On 2026-07-02 23:02, olcott wrote:
>>> On 7/1/2026 9:03 PM, olcott wrote:
>>>> Q cannot do the ∀x without an infinite sequence of steps.
>>>
>>> So your phrasing is good: Q would need something like an infinite 
>>> sequence of steps (or a single principle that summarizes them) to get 
>>> the ∀x. Since formal proofs must be finite, and Q lacks the tool 
>>> (induction) that would allow a finite proof of the infinite claim, 
>>> the universal statement remains unprovable.
>>
>> I'm not sure why you are responding to yourself nor who 'your 
>> phrasing' refers to since you don't quote anyone. But, assuming we're 
>> still talking about ∀ x, S(x) ≠ x in Q, your reasoning is simply off.
>>
>> You *can* prove universally quantified claims in Q, just not that 
>> particular claim.
>>
> 
> What is the reason that (∀x, S(x) ≠ x) cannot be proved in Q?

Because it isn't true in all models of Q, so there would be a serious 
problem with Q if it could prove this.

> Are the universally quantified claims that can be proven like
> this one (∀x, x = x) ?

That and many others. I have no idea what you mean by 'like this one'. 
It can prove many things involving universal quantifiers.

>> And there isn't an infinite sequence of steps that will get you from 
>> the axioms of Q to ∀ x, S(x) ≠ x. There's *no* sequence of steps, 
>> finite or infinite.
>>
> 
> So trying every element of the set of natural numbers
> would not derive the truth value after am infinite
> number of steps (that never complete)?

Trying every element of the set of natural numbers would depend on a 
model of Q which instantiates the natural numbers. There are models of Q 
which do not.

>> The issue here is that there are models of Q 
> 
> Which do not exist in PTS thus are off topic in this thread.
> All of the rest is off-topic in this thread.

Q *requires* a model. It isn't meaningful without one. You are terribly 
confused about PTS. PTS does not reject models. It just doesn't rely on 
model-theoretic semantics since it is only concerned with proof and not 
truth. Models will often define what is and isn't true but won't define 
which propositions are derivable purely from from the axioms of the 
system which is what PTS is concerned with

When we say that (∀x, S(x) ≠ x) is not provable in Q, we are effectively 
saying that it cannot be shown to hold for all possible models of Q 
solely from the axioms of Q.

But crucially (∀x, S(x) ≠ x) is *always* a truth bearer for every model 
of Q.

>> in which ∀ x, S(x) ≠ x is true, but there are also models of Q in 
>> which it is false.
>>
>> For any given model of Q, it will either be true or false, so your 
>> claim that ∀ x, S(x) ≠ x is somehow 'not a truth bearer' is simply 
>> ludicrous. It's simply the case that this particular statement cannot 
>> be derived as a theorem of Q nor can its negation. Thus Q is incomplete.
>>
>> André
>>
> 
> 

-- 
To email remove 'invalid' & replace 'gm' with well known Google mail 
service.