Re: William T. Parry gets rid of Disjunction introduction

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.

> André
> 
>> I am going with this in terms of
>>
>> The Definitional View of Atomic Systems in Proof-Theoretic
>> Semantics Thomas Piecha and Peter Schroeder-Heister
>>
>> When you actually look at the meaning of the English
>> words of the sentences then it becomes obvious that
>> the principle of explosion can only occur when you
>> ignore this underlying semantics.
>>
> 


-- 
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).