[ontoiop-forum] DOL finalisation

Tue Jan 2 21:32:25 CET 2018

Pat,

Do you disagree with the following?

TM> "due to the infinitary nature, there won't be any theorem provers,
even with your restriction to axioms."

It seems greater care is needed to confirm your understanding.

See below for more fun.

--
Rick

On 01/02/2018 01:25 PM, Pat Hayes wrote:
> 
> 
>> On Jan 2, 2018, at 7:00 AM, rick <rick at rickmurphy.org> wrote:
>>
>> Till & Fabian, consider the following under DOL public comment, open
>> through March 2018 and relevant to the required Business Committee
>> Questionnaire.
>>
>> I have cc'd Larry Johnson OMG's Technical Director.
>>
>> The recent email exchange confirmed that the authors of ISO 24707
>> determined the need for revisions to incorporate an unspecified
>> "induction principle" after its publication.
> 
> As one of the two main authors of the technical parts of ISO 24707, I do not agree with the previous sentence. The authors of ISO 24707 did /not/ determine a need for an unspecified induction principle, and my recent email exchanges with Rick Murphy (copied below) do /not/ confirm any such interpretation. 

You had not rejected Till's recommendation regarding induction.

Am I correct the record should reflect that you reject such an approach?

You had previously said:

PH> "I understand (and respect) your preference for 2OL over infinitary
for prover-relevant reasons"

> As I pointed out to Rick in one of the emails, 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; and if they had done, the simple reduction of sequence marker syntax to the weak infinitary logic Lw1w would have sufficed, without mentioning induction. 

As you said Lw-1,w was discovered by the authors after publication of
24707. Revisionism is only good in the next revision of the standard.

--
Rick

> Pat Hayes
> 
>>
>> The DOL authors claim to "handle" sequence markers in HETS using "second
>> order logic" which by conformance with MOF and fUML is outside the scope
>> of DOL.
>>
>> Pat, thanks for taking the time to answer my questions. I am heads down
>> this year on dependent types and univalence.
>>
>> --
>> Rick
>>
>> On 12/27/2017 02:44 PM, Pat Hayes wrote:
>>>
>>>
>>>> On Dec 27, 2017, at 6:17 AM, rick <rick at rickmurphy.org> wrote:
>>>>
>>>> On 12/21/2017 07:50 PM, Pat Hayes wrote:
>>>>>
>>>>>
>>>>>> On Dec 21, 2017, at 9:54 AM, rick <rick at rickmurphy.org> wrote:
>>>>>>
>>>>>> How about it, Pat?
>>>>>>
>>>>>> No derivations for "Common Logic"?
>>>>>>
>>>>>> ISO 24707 actually has no inference rules or proof theory at all,
>>>>>> correct? How can they be "out of scope" for a logic?
>>>>>
>>>>> Did anyone suggest they are? 
>>>>
>>>> You excluded them in 24707, 1 Scope which reads in part as follows:
>>>>
>>>> "The following are outside the scope of this International Standard:
>>>> * the specification of proof theory or inference rules; “
>>>
>>> Right. The standard does not include those. The intended purpose of CL was to be a ‘standard format’ for the variety of notations and syntactic conventions all in use for FOL. One gets to define this exactly by providing one (abstract) syntax with a rigorously described model theory. It is then up to users of other notations to define their mappings to this syntax and check that their semantics are preserved under that mapping. None of this requires the notation to have a proof theory: in fact, such a proof theory might well be an impediment to such use, as it would impose an extra burden on translation which would not be relevant to the intended use of 24707.
>>>
>>>>
>>>> It's not logic without them.
>>>
>>> That is a matter of opinion. FOL is widely considered to be a (note singular) logic, yet there are probably 50 or more different proof theories and syntaxes for it. But only one model theory.
>>>
>>>>>> Shouldn't the ISO 24707 authors have released a Common LISP library by
>>>>>> now? It's been 10 years.
>>>>>
>>>>> The CL effort was done pro bono, and AFAIK none of the authors have funding to work on it further. I certainly have not. Anyone who is interested is welcome to develop CL inference engines or other software, of course. 
>>>>
>>>> Ten years gone and there's no reference implementation, right?
>>>
>>> Right. AFAIK, nobody is working on it. Feel free to pick up the reins if you want to: it’s not in any way proprietary. I myself have retired from academic work, and Chris Menzel is a full-time philosopher.
>>>
>>>>
>>>> We are told that HETS parses CLIF syntax, but "handles" sequence markers
>>>> in second order logic, likely as polymorphic list types.
>>>>
>>>> A consumer of 24707 and standards which depend on it assume significant
>>>> risk.
>>>
>>> Not for the original intended use. 
>>>
>>>>
>>>>>> Fabian, Annex D is only informative, but the following sentence may be
>>>>>> naively interpreted to mean that second order logic is required, or
>>>>>> somehow provided.
>>>>>>
>>>>>> "Note that sequences are essentially a non-first-order feature that
>>>>>>
>>>>>> can be expressed in second-order logic.”
>>>>>
>>>>> Well, that sentence is of course true.
>>>>
>>>> Really? Where would I find sequence markers in the literature on
>>>> second-order logic? Reference please.
>>>
>>> Sequence markers get you (a subset of) Lw1-w, which is strictly weaker than second-order. This is kind of obvious since you can define lists in second-order and quantify over them, and define integers to count how long they are, etc.. 
>>>
>>>>
>>>> Assuming a reference, the sentence would be equally true in let's say
>>>> the calculus of constructions, right?
>>>
>>> I have no idea. We did not even look at CoC as being relevant to 24707. CoC is not easily relatable to FOL, is it? Curry-Howard gets you *intuitionist propositional* logic, which is a very small and idiosyncratic subset of FOL. 
>>>
>>>> Everything that has lists, right?
>>>
>>> Not everything, surely. LISP has lists. but it doesn't have a logical model theory. I am not aware of any other extension of FOL that ‘has lists’ in the same sense. 
>>>
>>>>> The mapping to Lw1w was not noticed until after that was written. We had a strong intuition that second-order was too strong, which is why this says 'can be expressed’ rather than ‘requires’. 
>>>>
>>>> There's no mapping and there's no claim of induction related to sequence
>>>> markers in 24707. 24707 has a vague reference to fix points.
>>>
>>> It would not have been appropriate to include such details in 24707 even if we had had them worked out. Standards documents are not academic papers: there are strict rules about what should be included and what not, and distinguishing normative from informative text, and being rather exact about requirements and so forth. 24707 gives a model theory for sequence markers. 
>>>
>>> Perhaps it would have been better to have left them out, in retrospect, as they are not strictly FO; but they were part of KIF which was the origin of CL, and we had worked out a precise semantics for them (which KIF did not), and they are only a tiny step up from strict FO, so we decided to keep them. And they are very useful in defining embeddings, as we found when translating OWL into CL.
>>>
>>>> And all we've read is a post-hoc claim of an unspecified "induction
>>>> principle."
>>>>
>>>> There's no proof, or inference rules, and there's no reference
>>>> implementation. Given the related "handle" claim, it sounds like
>>>> "requires" rather than "can be expressed" to me.
>>>>
>>>>> If someone reads that sentence in the way you imply, above, then I would suggest they are not competent to read a formal specification. 
>>>>
>>>> That seems pervasive around standards organizations.
>>>
>>> Well, there are rules about how standards documents use language. Its a bit like being at a court: you have to be extra careful about how things are phrased, as these have consequences that you can ignore in less formal settings. 
>>>
>>>>>> This is an example of how misinformation is being circulated about
>>>>>> "Common Logic." I have discussed this before at OMG.
>>>>>>
>>>>>> How do you respond to the fact that Java and C# provide parametric
>>>>>> polymorphism, but CL and DOL do not?
>>>>>
>>>>> With a puzzled frown, not understanding what possible relevance Java or C++ have to anything in this entire discussion (or in ISO 24707)
>>>>
>>>> They have lists similar to those in second order logic which seem to be
>>>> required to implement sequence markers in 24707.
>>>
>>> They have lists, but thay aren’t logics. So they don’t have, for example, quantifiers or connectives or logical sentences or a model theory. They are about as relevant to 24707 as shopping lists.
>>>
>>> Pat
>>>
>>>>
>>>> Turn that frown upside down.
>>>>
>>>> --
>>>> Rick
>>>>
>>>>> Pat
>>>>>
>>>>>>
>>>>>> Good to see folks promoting Goguen's work though.
>>>>>>
>>>>>> --
>>>>>> Rick
>>>>>>
>>>>>> On 12/20/2017 07:00 PM, rick wrote:
>>>>>>> Maybe Pat can show the derivations to avoid further misunderstanding.
>>>>>>>
>>>>>>> --
>>>>>>> Rick
>>>>>>>
>>>>>>> On 12/20/2017 05:32 PM, Pat Hayes wrote:
>>>>>>>> I hadn’t seen that diagram before. I believe that it is inaccurate to describe CL as having ‘some second-order constructs’. Sequence markers take CL outside FO expressivity, but not to second-order. CL with sequence markers is in fact a subset of the infinitary logic Lw1-w which allows countably infinite conjunctions. This is a long way short of full second-order logic. If one restricts CL (Lw1-w) so that sequence markers (infinite conjunctions) occur only on the LHS of sequents, it is first order. So sequence makers can be used in ontologies (ie as ‘axioms’) without going beyond FO expressivity. 
>>>>>>>>
>>>>>>>> Pat
>>>>>>>>
>>>>>>>>> On Dec 20, 2017, at 7:01 AM, John F Sowa <sowa at bestweb.net> wrote:
>>>>>>>>>
>>>>>>>>> Congratulations to everyone working on the DOL project.
>>>>>>>>>
>>>>>>>>> From Fabian via ontoiop-forum,
>>>>>>>>>> Good news concerning the standardisation of DOL! During the last
>>>>>>>>>> OMG Technical Meeting the Architecture Board approved the changes
>>>>>>>>>> that we made to DOL during the “Finalisation Phase” (which in our
>>>>>>>>>> case lasted 2 years). Hence, we cleared the last major hurdle on
>>>>>>>>>> our way to the release of DOL 1.0. I expect that this will happen
>>>>>>>>>> in February 2018.
>>>>>>>>>
>>>>>>>>> And Fabian, I'm sending a copy of this note to Ontolog Forum, and
>>>>>>>>> I also attached a copy of an earlier diagram (dol.jpg).
>>>>>>>>>
>>>>>>>>> Does this diagram reflect the current version?  If so (or not),
>>>>>>>>> could you please send the URL of the latest documentation to
>>>>>>>>> Ontolog Forum?
>>>>>>>>>
>>>>>>>>> And is software available for the various mappings in that diagram?
>>>>>>>>>
>>>>>>>>> John
>>>>>>>>> <dol.jpg>
>>>>>>>>> _________________________________________________________________
>>>>>>>>> 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
>>>>>>>>
>>>>>>>>
>>>>>>>>
>>>>>>>> _________________________________________________________________
>>>>>>>> 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
>>>>>>>>
>>>>>>
>>>>>>
>>>>>
>>>>>
>>>>>
>>>>>
>>>>
>>>>
>>>
>>>
>>>
>>>
>>
>> _________________________________________________________________
>> 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
> 
> 
> 
> 