[ontoiop-forum] DOL finalisation

[rick]

John,

You're trolling again. I thought we had an agreement.

--
Rick

On 01/02/2018 02:42 PM, John F Sowa wrote:
> 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
> 
> _________________________________________________________________
> To Post: mailto:ontoiop-forum at ovgu.de
> Message Archives: https://listserv.ovgu.de//pipermail/ontoiop-forum
> Config/Unsubscribe: https://listserv.ovgu.de/mailman/listinfo/ontoiop-forum
> Community Files (open): http://interop.cim3.net/file/pub/OntoIOp/
> Community Wiki: http://ontoiop.org
> 
>