Re: William T. Parry gets rid of Disjunction introduction

On 2026-07-07 15:13, olcott wrote:
> On 7/7/2026 3:08 PM, André G. Isaak wrote:
>> On 2026-07-07 13:53, olcott wrote:
>>> On 7/7/2026 2:29 PM, André G. Isaak wrote:
>>>> On 2026-07-07 13:19, olcott wrote:
>>
>>>>> To do with with minimal simplicity the axioms of
>>>>> PA are construed as semantic entailment thus when
>>>>> there is no sequence of inference steps between G
>>>>> and PA then G is Kripke undefined in PA.
>>>>
>>>> So why don't you illustrate this with an actual proof?
>>>>
>>>> André
>>>>
>>>
>>> The principle is simply whenever X cannot be proven
>>> in F then X is ungrounded in the atomic base F. Even
>>> diagonalization makes to attempt at actual proof.
>>
>> I can't make heads or tails of that.
>>
> 
> The actual proof in meta-math that G cannot be
> proved in PA is itself not any sequence of inference
> steps. It simply uses a version of the proof that
> Cantor use to show that reals are not countable.

???

Cantor's proof absolutely contained inference steps, as did Gödels. I 
don't think you actually know what you're talking about.

>> If you can't illustrate your alleged system with a simple proof, then 
>> I have no choice but to conclude that it is as ill-defined to you as 
>> it is to me.
>>
>> André
>>
> 
> 2 + 3 = 4 in PA cannot be proven because
> s(s(0)) + s(s(s(0))) != s(s(s(s(0))))

I asked you to provide an example of a proof which illustrates what you 
mean by "semantic entailments encoded syntactically in the language". I 
didn't ask for an example of something which cannot be proven.

André

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