Re: Olcott's big correction to symbolic logic

On 08/07/2026 23:26, olcott wrote:
> On 7/8/2026 2:24 AM, Mikko wrote:
>> On 06/07/2026 18:15, olcott wrote:
>>
>>> P ⊢ Q where the rules of inference are only
>>> semantic entailment specified syntactically.
>>>
>>> Validity and Soundness
>>> A deductive argument is said to be valid if and only
>>> if it takes a form that makes it impossible for the
>>> premises to be true and the conclusion nevertheless
>>> to be false. https://iep.utm.edu/val-snd/
>>>
>>> Is corrected to mean
>>> A deductive argument is said to be valid if and only
>>> if it takes a form that the conclusion is semantically
>>> entailed by its premises.
>>>
>>> We do not use model theory to do this we use proof
>>> theoretic semantics.
> 
>> What does "semantic entailment" mean when model theory
>> is not used?
> 
> P ⊢ Q means syntactic derivation implements semantic
> entailment encoded in syntactically the language.
> This is the only inference steps allowed.

That does not answer the question. It does not specify
what "semantic entailment" means nor what inference
steps are allowed.

> "I drove my car to Walmart"
> entails that my motor vehicle consumed energy.

Not without additional premises that relate driving and car
to consumption and energy.

> It turns out that all HOL and type theory can be
> encoded in Prolog even though it cannot be processed
> in Prolog.
Or C or any language that supports long character strings.

-- 
Mikko