Re: William T. Parry gets rid of Disjunction introduction

On 7/7/2026 2:29 PM, André G. Isaak wrote:
> On 2026-07-07 13:19, olcott wrote:
>> On 7/7/2026 1:46 PM, André G. Isaak wrote:
>>> On 2026-07-07 10:04, olcott wrote:
>>>> On 7/7/2026 10:31 AM, André G. Isaak wrote:
>>>>> On 2026-07-06 21:40, olcott wrote:
>>>>>> On 7/6/2026 10:28 PM, André G. Isaak wrote:
>>>>>>> On 2026-07-06 21:12, olcott wrote:
>>>>>>>> On 7/6/2026 10:03 PM, André G. Isaak wrote:
>>>>>>>>> On 2026-07-06 20:44, olcott wrote:
>>>>>>>>>> On 7/6/2026 9:41 PM, André G. Isaak wrote:
>>>>>>>>>>> On 2026-07-06 20:24, olcott wrote:
>>>>>>>>>>>
>>>>>>>>>>>> ∀x(φ(x) ∧ ¬φ(x)) ⊢ ⊥
>>>>>>>>>>>> and
>>>>>>>>>>>>         Γ ⊢ ⊥
>>>>>>>>>>>> --------------------
>>>>>>>>>>>> derivation terminated
>>>>>>>>>>>
>>>>>>>>>>> That's simply gibberish.
>>>>>>>>>>>
>>>>>>>>>>> André
>>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>> How do you think that:
>>>>>>>>>>  From a contradiction nothing follows
>>>>>>>>>> should be encoded?
>>>>>>>>>
>>>>>>>>> Since you don't understand the formalism you're trying to use, 
>>>>>>>>> why bother trying to formalize it? 
>>>>>>>>
>>>>>>>> Both LLMs agree that I am already correct.
>>>>>>>
>>>>>>> LLMs carry no weight in my opinion. 
>>>>>>
>>>>>> This is also your own error.
>>>>>>
>>>>>>> And since you can't clearly express yourself, it wouldn't be 
>>>>>>> clear exactly what they were agreeing with anyways.
>>>>>>>
>>>>>>
>>>>>> How do we formalize: "from a contradiction nothing follows?"
>>>>>
>>>>> You really ought to take an introductory course in formal logic, or 
>>>>> simply give up on trying to formalize things. If you really wanted 
>>>>> to you could write something like
>>>>>
>>>>> ∀Φ ¬∃Ψ (Φ ∧ ¬Φ) → Ψ
>>>>>
>>>>> But simply looking at the truth table for → would reveal that this 
>>>>> statement is false.
>>>>>
>>>>
>>>> P ⊢ Q means syntactic derivation implements semantic
>>>> entailment encoded in syntactically the language.
>>>> This is the only inference steps allowed. The entailment
>>>> rules depend on the represented domain.
>>>
>>> That really doesn't seem to say anything. Why don't you illustrate 
>>> this with a simple mathematical proof which shows exactly what you 
>>> mean by 'semantic entailments encoded syntactically in the language'
>>>
>>
>> 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.


-- 
Copyright 2026 Olcott

My 28 year goal has been to make
"true on the basis of meaning expressed in language"
reliably computable for the entire body of knowledge.
The complete structure of this system is now defined.

The entire body of knowledge expressed in language is
comprised of two types of relations between finite strings:
(a) *Axioms* Expressions of language that are stipulated to be true.

My system bridges the analytic/synthetic distinction by
expressly encoding all empirical "atomic facts" in a formal
language such as CycL of the Cyc project.

(b) *Inference Rules* Expressions of language that are semantically
entailed syntactically from (a) and/or (b).