Re: [ontolog-forum] Types of Formal (logical) Definitions inontology

["henson" <henson.graves@xxxxxxxxxxx>]

Alex,

I am familiar Dumontier’s work. Where they have problems is in constructing OWL axiom sets for a molecule such as H2O which constrains the models to only consist of molecules with exactly three atoms. There are a lot of papers by Horrocks and Motik and students on this topic. This has led them to try graph extensions of DL and logic programming extensions.

Let me know if you need more pointers.

Henson

 

From: Alex Shkotin

Sent: Wednesday, July 09, 2014 8:54 AM

To: henson

Cc: [ontolog-forum] ; andrei rodin

Subject: Re: [ontolog-forum] Types of Formal (logical) Definitions inontology

 

Henson,

 

just about OWL. If we google "owl ontology chemistry" we got some. What about http://dumontierlab.com/?page=ontologies?
I don't think they have problems with chemistry, atom, molecule...

From other side if you have sentences of some knowledge in English not expressible in OWL give us and we can make formal languages competition.
I bet FOL.

Alex

2014-07-08 20:31 GMT+04:00 henson <henson.graves@xxxxxxxxxxx>:

Alex,

The observation about digraphs is on target. The axioms for a category in a 2-sorted logic start with the digraph signature and add axioms for composition and identity. Note that the composition axioms are precisely path composition in a graph. However, in a graph one writes f.g rather than g (f ). A digraph uniquely determines a category. All of the application work that I do builds on the fact that the applications generally start with a directed graph. Note that the axioms for a category use the three place predicate f:X –>Y which is defined as dom(f ) = X and codomain( f ) = Y. So the axioms for a category use equality. Note also that one can use the notation f:Y for  the relation codomain( f) = Y. This is not epsilon. In a topos if f:X –> Y, p:Y –> Omega, p (f ) = true, then f \in Y. Using p:Y –> Omega to construct the type Y{p} then in a topos you have a subtype algebra, as you probably know. my impression is this is the correct interpretation of epsilon. I agree with Andrei.

 

The ability to start with digraphs makes category theory much better than DL (OWL) for dealing with structure such as molecular or product structure.

 

 

Henson

 

 

 

From: Alex Shkotin

Sent: Tuesday, July 08, 2014 9:39 AM

To: henson

Cc: [ontolog-forum] ; andrei rodin

Subject: Re: [ontolog-forum] Types of Formal (logical) Definitions inontology

 

Henson,

just a few summer words about categories and Set theory.

1) Consider a very subtle category, may be a topos. Let's forget about composition for a moment - we get digraph.

Formal theory of digraphs itself is very interesting as it does not have an axioms at all.

We just need signature <Sorts ob, ar; Functions dom ar:ob, cod ar:ob>.

Well, we keep in mind that dom, cod are a full functions, but it's usual in math.

Unfortunately this important theory does not mentioned in great list

http://en.wikipedia.org/wiki/List_of_first-order_theories

2) Goldblatt has mentioned somewhere in his book that we may look at ∈ as an arrow from element to set.

What Set theory does study then? Huge digraph:-)

It's more or less simple:

- there is no loops and cycles,

- there is no parallel arrows,

- there are sources (∅, pra-elements);

- there are sinks - classes;

...

But how many outcome arrows does have not a class? It's greater than any cardinal number.

 

Alex

 

2014-07-07 19:27 GMT+04:00 henson <henson.graves@xxxxxxxxxxx>:

Alex,

What you say is exactly what I mean regarding partial functions. General logics which admit partial functions are very unsatisfactory and messy in my opinion. But with the decidability conditions for partial functions then one can can construct or recognize a model when the interpretation of the definedness precondition is met. So the model theory works well for this limited kind of partialness.

 

Patrick Suppes has made a strong argument that standard FOL theories will always be inadequate for axiomatizing applications; he suggests using set theory as the alternative.

 

Many years ago I worked for Pat to engineer his version of set theory to be used in a first order theorem prover/proof checker. The reduction of everything to epsilon was just not really practical. This made me look for other alternatives with the same expressive power. Topos theory was a natural candidate as it simply gives algebraic axioms for the constructions of cartesian product, disjoint union, etc. This approach turned out to work quite well for implementation. I implemented a system based on the topos approach in the 1980s. Topos theory also needs some engineering to get rid of existential statements in subobject classification.

 

My experience confirms that Pat is correct that standard FOL will not work for application axiom system development, one needs multiple sorts, and decidable preconditions for operations. However, there are these alternatives to set theory such as topos theory. Type theory is another alternative, but I prefer topos theory for physical applications. Type theory works well software for software applications.

 

One way to look at using set theory or topos theory represented within some slightly extended version of set theory, is that one is separating the inference mechanism (logic) from the expressiveness (the ontology). While they overlap, one can use relatively simple logics with very expressive ontological languages. That is higher order logic is not needed for applications as these systems can represent higher order logic in their term calculus. One also sees this kind of thing in systems like Hilog.

 

Henson

 

From: Alex Shkotin

Sent: Monday, July 07, 2014 4:22 AM

To: [ontolog-forum]

Cc: andrei rodin

Subject: Re: [ontolog-forum] Types of Formal (logical) Definitions inontology

 

Henson,

 

I just have 2-sorted Goldblatt's description in TOPOI. The categorial analysis of logic. 1979.

 

I like idea that set theory is may be over reduced to one prime predicate symbol ∈. Maybe it's like a Scheffer stroke for propositional calculus:-)

In this case category should replace algebraic system as a model for theory?

 

When we work with a partial function it is necessary to supply a predicate for an area where it's defined. For ex. for x/y it's y<>0. This is just a pre-condition to calculate term "x/y" value without abort. And if we have an arbitrary term with partial functions we should derive pre-condition for it.

Is this what you keep as "decidable well-formedness conditions for operations"?

 

Alex

2014-07-06 20:05 GMT+04:00 henson <henson.graves@xxxxxxxxxxx>:

As Alex notes the axioms for a category can be expressed in FOL. This was first done by W. Lawvere and about 1965. He represented comp as a relation. This is very messy. The most direct way to represent composition is, as Alex notes, is to represent composition as a partial operation in FOL. This operation is not an arbitrary partial operation. The well-formedness condition is decidable. Lawvere calls this Tarski’s hygiene condition for formal systems. If anybody knows a reference for this please let me know. In a FOL system which admits decidable conditions for well-formedness natural deduction conditions work perfectly well.

 

John S. may recall I have suggested that (a replacement for) CL should be a multi-sorted and allow decidable well-formedness conditions for operations. I encounter this situation frequently in both mathematics and applications to engineering and molecular science.

 

Lawvere in the late 60s gave FOL axioms for a topos, which can be viewed as an algebraic form of set theory, but provides a very useful generalization that enables dynamic systems to be represented in the extended FOL, which I will call for the moment conditional FOL. Also by using conditional FOL the concept of functorial semantics in category theory can be made copasetic with FOL model theory.

 

Lawvere’s  Topos axioms, with one exception, can be expressed in a restriction of the conditional FOL to rules. One can  find this in Lambek and Scott’s book. With great care the exception can be eliminated giving a very constructive version of the topos axioms, which yields an implementable, very tractable reasoning system.

 

These topos axioms serve as a formal ontology for a lot of classical mathematical applications. When one goes to non-classical applications such as quantum theory, one needs generalizations to monoidal categories to provide a suitable ontology, see Abransky.

 

Category theory is definable in FOL and is, in my opinion, a better universal foundation than set theory, as the interpretation of category primitives in terms of recognition procedures works better in many applications than set theory primitives in terms of collectives. It is much easier to talk about a recognition procedure for an iPad than the collection of iPads.

 

The conditional FOL provides the logic, the category axioms provide a formal ontology within the logic.

 

There is more to the story, as Andrei is aware. One generally needs to talk about not just one theory, but multiple theories and their relationships. The enclosed paper was given at PhML-2014.

 

Henson Graves

 

From: Alex Shkotin

Sent: Sunday, July 06, 2014 9:16 AM

To: Pat Hayes

Cc: andrei rodin ; [ontolog-forum]

Subject: Re: [ontolog-forum] Types of Formal (logical) Definitions inontology

 

Pat,

category theory is just 2-sorts theory like this

Sorts: ob {- objects-}, ar {- arrows-}.

Functions: dom ar:ob, cod ar:ob, one ob:ar, comp ar ar:ar infix "∘".

And axioms:

dom(g∘f)=dom(f). cod(g∘f)=cod(g).

h∘(g∘f)=(h∘g)∘f.

dom(one(b))=b. cod(one(b))=b.

one(b)∘f=f. g∘one(b)=g.

And we should keep in mind that comp is partial with predicate of definability - Defined(x∘y) =def dom(x)=cod(y).

Alex

2014-07-03 9:29 GMT+04:00 Pat Hayes <phayes@xxxxxxx>:

On Jun 26, 2014, at 3:56 AM, Alex Shkotin <alex.shkotin@xxxxxxxxx> wrote:

> Pat,
>
> You: "All of modern mathematics, for example, can be written in FOL."
> But
> Let me cite from Handbook of Mathematical Logic, J. Barwise (Ed.) N-H PC, 1977,
> V.I,
> p.15 "Last concept (f) [periodic group] is not a FOL concept. Let's see why..."

This is talking about FO *definability*. That is a delicate topic that needs to be understood carefully. But all of modern mathematics can be expressed in set theory, and ZFC is a first-order theory (see http://en.wikipedia.org/wiki/Zermelo-Fraenkel_set_theory).
(To be fair, some philosophers insist that category theory is not definable in set theory and is a better universal foundation. I have no idea of category theory can be expressed in FOL.)

> p.19 "2.6. There is no set of FOL axioms to describe R [real numbers] isomorphically."

Isomorphically, of course. There is no set of FO axioms to describe the natural numbers isomorphically, never mind the reals. (Goedel's theorem.) But that does not mean that reasoning about these structures cannot be done in FOL. It can. In fact, if any reasoning can be done in a finite time, with finite proofs, then it can be done in FOL. This has been given exact force as Lindstrom's theorem (http://en.wikipedia.org/wiki/Lindstr%C3%B6m's_theorem), which says that ANY logical system which is compact (= proofs are finite) and satisfies the Lowenheim/Skolem property (trickier to characterize, but what it boils down to is that the semantic and syntactic ideas of truth coincide properly) must be representable as a FO theory.

But in any case, FOL is clearly of central importance in modern foundations of mathematics, in a sharp contrast to Aristotelian syllogistic logic.

Pat

>
> Sorry my translation back to English from Russian edition of 1982.
> What do you think?
>
> Alex
>
>
>
> 2014-06-25 21:01 GMT+04:00 Pat Hayes <phayes@xxxxxxx>:
>
> On Jun 23, 2014, at 10:25 PM, rrovetto@xxxxxxxxxxx wrote:
>
> > Thank you all for the feedback thus far. A couple of quick follows-ups:
> > ...
> > To add context to my original question: I'd basically like to know what non-FOL/non-syllogism logical formalisms are there for ontologies?
> > This question assumes that FOL is based on Aristotelean syllogistic logic. Based on my studies in philosophy FOL is essentially presented as a modern form or translation of it.
>
> No. FOL is indeed more modern, and it 'contains' syllogistic logic, but it is far more powerful (expressive) than anything known to Aristotle. All of modern mathematics, for example, can be written in FOL. One can make out a good case that anything that can be formalized in *any* language that has a reasonable notion of 'proof', can be expressed in FOL. See http://tinyurl.com/o9a9hyc (for example) for more on this.
>
> So the premis of your question, below, is mistaken.
>
> > Now, my concern with this is that since syllogistic logic is not how the mind reasons
>
> Nobody knows how the mind reasons. THe mind is certainly capable of following syllogisms, however.
>
> > , and is also very limited (in terms of producing truthful results/consequences, and expressivity, if not other things), why isn't a non-syllogistic-based logic used for ontologies? Why is FOL used?
>
> Actually, for the bulk of actual uses, weaker logics than FOL are used, because they are decideable. OWL-DL for example is based on description logics.
>
> Pat Hayes
>
> >
> > If anyone can answer, or address this, I eagerly await your thoughts. Thanks.
> >
> > Aside from that, please continue mentioning any other logics that are used.
> >
> > On Tue, Jun 24, 2014 at 4:06 AM, Rich Cooper <rich@xxxxxxxxxxxxxxxxxxxxxx> wrote:
> > By the same logic, a concept can be the product of
> > 'subordinate components', or more linguistically
> > aimed, 'a product of properties and behaviors'.
> > The choice of alternative interpretations, or the
> > choice of a component list, is the distinction
> > between Mereology and other forms of logical
> > representation.
> >
> > So unions of alternatives and products of
> > component parts seem to be equivalent castings.
> >
> > -Rich
> >
> > Sincerely,
> > Rich Cooper
> > EnglishLogicKernel.com
> > Rich AT EnglishLogicKernel DOT com
> > 9 4 9 \ 5 2 5 - 5 7 1 2
> >
> > -----Original Message-----
> > From: ontolog-forum-bounces@xxxxxxxxxxxxxxxx
> > [mailto:ontolog-forum-bounces@xxxxxxxxxxxxxxxx] On
> > Behalf Of Barkmeyer, Edward J
> > Sent: Monday, June 23, 2014 2:17 PM
> > To: [ontolog-forum]
> > Subject: Re: [ontolog-forum] Types of Formal
> > (logical) Definitions in ontology
> >
> > John makes an important addition to my list.  In
> > addition to defining a concept as the union of a
> > set of 'subordinate' concepts', it is also
> > possible to define a 'class' or a 'term' (less
> > clearly a 'concept') as a specific set of named
> > things.  This latter is also referred to as an
> > "extensional definition".  One can define 'primary
> > color' as "one of red, orange, yellow, green,
> > blue, indigo, violet," without being at all clear
> > about what the distinguishing properties are.
> >
> > (I tend to think that a 'concept' should have a
> > definition that involves specifying properties,
> > but then "being the color red" and "being John
> > Malkovich" can be considered properties.)
> >
> > -Ed
> >
> > > -----Original Message-----
> > > From: ontolog-forum-bounces@xxxxxxxxxxxxxxxx
> > [mailto:ontolog-forum-
> > > bounces@xxxxxxxxxxxxxxxx] On Behalf Of John F
> > Sowa
> > > Sent: Monday, June 23, 2014 4:47 PM
> > > To: ontolog-forum@xxxxxxxxxxxxxxxx
> > > Subject: Re: [ontolog-forum] Types of Formal
> > (logical) Definitions in ontology
> > >
> > > Ed and Pat,
> > >
> > > Pat raises an important point:
> > >
> > > PJH
> > > > If all classes are defined in terms of other
> > classes, where does the
> > > > whole process get started?
> > >
> > > All three of those methods assume you have some
> > classes to start:
> > >
> > > EJB
> > > > 1) identify a more general concept and the
> > delimiting characteristics
> > > >    of the subordinate concept being defined
> > > >    This is exactly:  An A is a B that C.
> > > > 2) identify a list of subordinate concepts
> > that together cover the
> > > >    more general concept being defined - the
> > union of other defined classes:
> > > >    An A is a B or a C or a D.
> > > > 3) One can also define a Class as the
> > intersection of two or more classes,
> > > >    but that is just a special case of (1):  An
> > A is a B that is also a C.
> > >
> > > Those are all set forming operations.  Set
> > theory has a starting method:
> > >     {x | P(x)} -- the set of all x for which
> > some property P is true.
> > >
> > > That property P can also be specified by
> > enumeration:
> > >     {x | x=a or x=b or x=c}
> > >
> > > What distinguishes a class from a set are the
> > identity criteria:
> > >
> > >   1. Two sets S1 and S2 are identical if they
> > have the same elements.
> > >
> > >   2. Two classes or concepts C1 and C2 are
> > identical if they have the
> > >      same or logically equivalent defining
> > property or predicate P.
> > >
> > > The set of all cows, for example, changes with
> > every birth or death.
> > > But the concept cow is determined by an
> > unchanging predicate P.
> > >
> > > John
> > >
> > >
> > __________________________________________________
> > ________
> > > _______
> > > Message Archives:
> > http://ontolog.cim3.net/forum/ontolog-forum/
> > > Config Subscr:
> > http://ontolog.cim3.net/mailman/listinfo/ontolog-f
> > orum/
> > > Unsubscribe:
> > mailto:ontolog-forum-leave@xxxxxxxxxxxxxxxx
> > > Shared Files: http://ontolog.cim3.net/file/
> > Community Wiki:
> > > http://ontolog.cim3.net/wiki/ To join:
> > http://ontolog.cim3.net/cgi-
> > > bin/wiki.pl?WikiHomePage#nid1J
> > >
> >
> > __________________________________________________
> > _______________
> > Message Archives:
> > http://ontolog.cim3.net/forum/ontolog-forum/
> > Config Subscr:
> > http://ontolog.cim3.net/mailman/listinfo/ontolog-f
> > orum/
> > Unsubscribe:
> > mailto:ontolog-forum-leave@xxxxxxxxxxxxxxxx
> > Shared Files: http://ontolog.cim3.net/file/
> > Community Wiki: http://ontolog.cim3.net/wiki/
> > To join:
> > http://ontolog.cim3.net/cgi-bin/wiki.pl?WikiHomePa
> > ge#nid1J
> >
> >
> >
> > _________________________________________________________________
> > Message Archives: http://ontolog.cim3.net/forum/ontolog-forum/
> > Config Subscr: http://ontolog.cim3.net/mailman/listinfo/ontolog-forum/
> > Unsubscribe: mailto:ontolog-forum-leave@xxxxxxxxxxxxxxxx
> > Shared Files: http://ontolog.cim3.net/file/
> > Community Wiki: http://ontolog.cim3.net/wiki/
> > To join: http://ontolog.cim3.net/cgi-bin/wiki.pl?WikiHomePage#nid1J
> >
> >
> >
> > _________________________________________________________________
> > Message Archives: http://ontolog.cim3.net/forum/ontolog-forum/
> > Config Subscr: http://ontolog.cim3.net/mailman/listinfo/ontolog-forum/
> > Unsubscribe: mailto:ontolog-forum-leave@xxxxxxxxxxxxxxxx
> > Shared Files: http://ontolog.cim3.net/file/
> > Community Wiki: http://ontolog.cim3.net/wiki/
> > To join: http://ontolog.cim3.net/cgi-bin/wiki.pl?WikiHomePage#nid1J
>
> ------------------------------------------------------------
> IHMC                                     (850)434 8903 home
> 40 South Alcaniz St.            (850)202 4416   office
> Pensacola                            (850)202 4440   fax
> FL 32502                              (850)291 0667   mobile (preferred)
> phayes@xxxxxxx       http://www.ihmc.us/users/phayes
>
>
>
>
>
>
>
> _________________________________________________________________
> Message Archives: http://ontolog.cim3.net/forum/ontolog-forum/
> Config Subscr: http://ontolog.cim3.net/mailman/listinfo/ontolog-forum/
> Unsubscribe: mailto:ontolog-forum-leave@xxxxxxxxxxxxxxxx
> Shared Files: http://ontolog.cim3.net/file/
> Community Wiki: http://ontolog.cim3.net/wiki/
> To join: http://ontolog.cim3.net/cgi-bin/wiki.pl?WikiHomePage#nid1J
>
>
>
> _________________________________________________________________
> Message Archives: http://ontolog.cim3.net/forum/ontolog-forum/
> Config Subscr: http://ontolog.cim3.net/mailman/listinfo/ontolog-forum/
> Unsubscribe: mailto:ontolog-forum-leave@xxxxxxxxxxxxxxxx
> Shared Files: http://ontolog.cim3.net/file/
> Community Wiki: http://ontolog.cim3.net/wiki/
> To join: http://ontolog.cim3.net/cgi-bin/wiki.pl?WikiHomePage#nid1J

------------------------------------------------------------
IHMC                                     (850)434 8903 home
40 South Alcaniz St.            (850)202 4416   office
Pensacola                            (850)202 4440   fax
FL 32502                              (850)291 0667   mobile (preferred)
phayes@xxxxxxx       http://www.ihmc.us/users/phayes

 

---

_________________________________________________________________
Message Archives: http://ontolog.cim3.net/forum/ontolog-forum/ 
Config Subscr: http://ontolog.cim3.net/mailman/listinfo/ontolog-forum/ 
Unsubscribe: mailto:ontolog-forum-leave@xxxxxxxxxxxxxxxx
Shared Files: http://ontolog.cim3.net/file/
Community Wiki: http://ontolog.cim3.net/wiki/
To join: http://ontolog.cim3.net/cgi-bin/wiki.pl?WikiHomePage#nid1J

_________________________________________________________________
Message Archives: http://ontolog.cim3.net/forum/ontolog-forum/
Config Subscr: http://ontolog.cim3.net/mailman/listinfo/ontolog-forum/
Unsubscribe: mailto:ontolog-forum-leave@xxxxxxxxxxxxxxxx
Shared Files: http://ontolog.cim3.net/file/
Community Wiki: http://ontolog.cim3.net/wiki/
To join: http://ontolog.cim3.net/cgi-bin/wiki.pl?WikiHomePage#nid1J
 

 

---

_________________________________________________________________
Message Archives: http://ontolog.cim3.net/forum/ontolog-forum/ 
Config Subscr: http://ontolog.cim3.net/mailman/listinfo/ontolog-forum/ 
Unsubscribe: mailto:ontolog-forum-leave@xxxxxxxxxxxxxxxx
Shared Files: http://ontolog.cim3.net/file/
Community Wiki: http://ontolog.cim3.net/wiki/
To join: http://ontolog.cim3.net/cgi-bin/wiki.pl?WikiHomePage#nid1J

 

 

_________________________________________________________________
Message Archives: http://ontolog.cim3.net/forum/ontolog-forum/  
Config Subscr: http://ontolog.cim3.net/mailman/listinfo/ontolog-forum/  
Unsubscribe: mailto:ontolog-forum-leave@xxxxxxxxxxxxxxxx
Shared Files: http://ontolog.cim3.net/file/
Community Wiki: http://ontolog.cim3.net/wiki/ 
To join: http://ontolog.cim3.net/cgi-bin/wiki.pl?WikiHomePage#nid1J    (01)