Re: The simple essence of Proof Theoretic Semantics

On 09/07/2026 06:16, olcott wrote:
> On 7/8/2026 2:42 AM, Mikko wrote:
>> On 06/07/2026 17:36, olcott wrote:
>>> On 7/6/2026 2:59 AM, Mikko wrote:
>>>> On 04/07/2026 20:13, olcott wrote:
>>>>> On 7/4/2026 3:49 AM, Mikko wrote:
>>>>>> On 03/07/2026 21:38, olcott wrote:
>>>>>>> On 7/3/2026 1:21 PM, André G. Isaak wrote:
>>>>>>>> On 2026-07-03 12:12, olcott wrote:
>>>>>>>>> On 7/3/2026 12:17 PM, André G. Isaak wrote:
>>>>>>>>>> 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, 
>>>>>>>>> Model theory has been expressly off-topic for
>>>>>>>>> many weeks in every thread. Whenever you ignore
>>>>>>>>> this the rest of your reply will be ignored.
>>>>>>>>
>>>>>>>> The rest of my post which you snipped and (presumably) ignored 
>>>>>>>> explained *why* you are wrong about this. PTS does not reject 
>>>>>>>> models or model theory. It simply doesn't rely on model- 
>>>>>>>> theoretic semantics. Q *requires* a model.
>>>>>>>
>>>>>>> It replaces Model theory With PTS.
>>>>>>> That you do not understand this is your mistake.
>>>>>>>
>>>>>>> "Is x true" is replaced with something like "Is x provable".
>>>>>>
>>>>>> "Is x provable" is there already. Why would one want to lose
>>>>>> "Is x true"? If one dosn't need "Is x true" one needn't use
>>>>>> it.
>>>>>
>>>>> The whole focus of most PTS "Is x provable".
>>>>> Model theory looks at true in a model and ignores
>>>>> the connection between true and provable.
>>>>
>>>> People rarely care about PTS or model theory. More often they 
>>>> careabout what is or is not true about someting they consider 
>>>> important.
>>>>
>>>
>>> Hence we must correct the divergence of logic
>>> from correct reasoning if we are to automate
>>> correct reasoning.
>>
>> Most people would accept as correct any reasoning that produce true
>> conclusions from true premises. 
> 
> I need a system that is good enough to make disinformation
> systems funded by many billions per year look like ridiculous
> fools even to themselves.

Sorry, I can't give you one, and I don't kwno anyone who could.

-- 
Mikko