[ontoiop-forum] DOL finalisation

[John F Sowa]

On 1/2/2018 3:58 PM, rick wrote:
> You're trolling again. I thought we had an agreement.

Our agreement was to be civil.

My recent notes in this thread were factual and civil:

  1. For classical FOL, the model theory is sufficient to specify
     the semantics.  All sound and complete FOL proof theories are
     equivalent.  Therefore, the choice of proof procedure is a
     matter of convenience and efficiency.  The implementers should
     be free to choose whatever version they prefer.

  2. As Pat has said, the only way anybody has ever used sequence
     markers in CL is to state the equivalent of axiom schemata.
     During the development of the ISO standard, I argued for that
     option as the only way that should be approved in the standard.
     But Pat and Chris wanted to leave the more general option open.

  3. For proofs that depend heavily on a type hierarchy, proofs with
     a sorted version of FOL can be far more efficient than proofs
     with unsorted FOL.  I argued for a sorted option in CL, but
     the committee did not approve.  However, it is possible for
     implementers to use CL notation with a sorted theorem prover
     and gain that improvement in performance -- but only for
     those texts that abide by the sort restrictions.

  4. A type hierarchy, by itself, can only specify a small part
     of what is necessary for ontology or software specifications.
     If you want to combine your type systems with a logic that
     has the full expressive power of FOL, how can you preserve
     the intuitionistic restrictions without using an intuitionistic
     theorem prover?  Are there any practical applications that
     take advantage of a full intuitionistic system?

  5. I do not know of any comparisons of the efficiency of sorted
     proof procedures vs. the intuitionistic methods that you have
     recommended.  If you know of any such studies, I would very
     much like to see them.

John