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

[Alex Shkotin <alex.shkotin@xxxxxxxxx>]

Pat and John,

Briefly: Let's look at FOL group theory with 0,+ as in J. Barwise book.

Proposal 2.1. states that in this theory there is no a finite number of formulas equivalent to

∀n≥1∀x∃y ny=x.             (6)

And this is a good reason for many-sorted language to be introduced, where we can write (6) as

∀n:N∀x:G∃y:G n≥1 → n*y=x.

And we need to define function for "*" like this:

Declaration Mult N G:G. Add infix "*" to Mult.

Definition Mult(n y)   if(n=1 return(y)) ; return(Mult(n-1 y)+y).

I wrote more words in Russian (ZF mentioned).

Thank you,

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    (01)