[ontoiop-forum] DOL finalisation

[John F Sowa]

On 1/2/2018 1:25 PM, Pat Hayes wrote:
> the intended purpose for ISO 24707 did not require a specification
> of any kind of proof theory for the CL language specified; the authors
> of that standard did not contemplate giving such a proof theory in any
> future revision to ISO 24707

I agree.  But there is a difference between classical FOL and
intuitionistic FOL.  In classical FOL, validity (determined by
the model theory) is equivalent to provability (determined by
the proof theory).  The only reasons for preferring one proof
theory to another are convenience and efficiency.

Therefore, it would be a mistake for the ISO standard to state
any preference for one proof theory or another.  The model
theory is compatible with any or all classical proof theories.

But some kinds of logics -- for example, intuitionistic or
relevance -- place restrictions on the rules of inference.

Since Rick is advocating an intuitionistic type theory, I
believe that is why he keeps asking about the proof theory.

But Rick has not stated any reason why an intuitionistic
logic is necessary or even desirable as a foundation for
specifying ontology, software, programming languages, or
any version of science or engineering.

John