ontolog-forum
[Top] [All Lists]

## Re: [ontolog-forum] type free logic and higher order quantification

 To: ontolog-forum@xxxxxxxxxxxxxxxx "John F. Sowa" Fri, 19 Aug 2011 10:31:54 -0400 <4E4E73DA.6070602@xxxxxxxxxxx>
 ```Rick,    (01) As Pat emphasized, there is a huge semantic difference between quantifying over relations (which can be done in Common Logic with a first-order style of semantics) and the kind of higher-order logic that logicians have been kicking around.    (02) In fact, many logicians have now come to believe that the infinite hierarchy of relations, relations of relations, etc., which are assumed for higher-order logic, should *not* be considered part of logic. They should be considered a version of set theory.    (03) The computational system called HOL does not assume the hierarchies that logicians talk about. In fact, HOL uses a semantics that is very similar to CL. (It's probably a subset of CL semantics, but it would be necessary to check that claim.)    (04) PH >> Ask yourself whether [axioms (R a) and (Q b)] entail the following: >> >> (exists (p)(and (p a)(p b) ) >> >> i.e. that there is a property that applies both to a and to b. >> >> If you intuitively answer "no", then you are thinking first-order, >> and would likely find CL congenial. If it seems obviously "yes", >> then you are thinking in a genuinely higher-order way. >> >> It really does matter which way you choose, as you will be >> interested in very different logics.    (05) RM > Understood. I've been heads down on functional programming lately, so > I'm getting more comfy with higher order thinking.    (06) But the usual versions of functional programming are not higher-order in the way logicians use the term.    (07) For Pat's example, the axioms (R a) and (Q b) can be satisfied in a CL domain that has only four entities: {R, Q, a, b}.    (08) In that model, there is no p such that (p a) and (p b) are both true. Therefore the statement (exists (p) (and (p a)(p b)) is false.    (09) But in the logicians' version of higher order logic, for any domain of individuals such as {a,b}, there is an infinite hierarchy of domains of all possible relations over the domain {a,b}, relations of relations over that domain, ...    (010) Since all possible relations are included, there would have to be some relation p such that (p a) and (p b).    (011) If you're using functional programming, I doubt that you would naturally think of that infinite hierarchy while you're writing a program. I suspect that you're more likely to think about CL kinds of models.    (012) RM > to establish a hierarchy of types to avoid paradox.    (013) You don't need a hierarchy of types to avoid paradox. In CL, the statement equivalent to Russell's paradox has a stable truth value: false. No paradox.    (014) As far as types are concerned, I'd like to emphasize that you can, if you wish, partition the domain of a CL model in disjoint sets that you can call types.    (015) CL does not prevent you from using types. In fact, it encourages you to do so by using quantifier restrictions. For example,    (016) (forall ((x Employee)) (exists ((y SSN)) ... ))    (017) This says that for all x of type Employee, there exists a y of type SSN, where Employee and SSN are monadic relations that restrict the domain of quantification of the variables x and y.    (018) This gives you weak typing. A logic with strong typing, such as Z, can be mapped to a system with weak typing such as CL. Furthermore, if you use quantifier restrictions, you can map the CL statements that came from Z back to Z statements.    (019) What you get with Z is the option of using syntactic checks that prevent any possible type mismatch. If you really, really want strong type checking, you could also parse any set of CL statements that were derived from Z to ensure that they obey the Z constraints.    (020) On the other hand, there are many legitimate sentences that you can express in CL, which cannot be expressed in Z:    (021) "The number 23 is not an elephant."    (022) That is a true statement, which could be written (not (Elephant 23)).    (023) But you can't say that in Z because 'Elephant(23)' is a syntax error.    (024) In summary, you can map strongly typed logics to CL, if you want them. If you really want to enforce the rules for strong typing, you can even write a CL parser that would enforce those typing rules.    (025) But CL also permits you to use weak typing or no typing at all.    (026) John    (027) _________________________________________________________________ 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    (028) ```
 Current Thread [ontolog-forum] type free logic and higher order quantification, Rick Murphy Re: [ontolog-forum] type free logic and higher order quantification, Pat Hayes Re: [ontolog-forum] type free logic and higher order quantification, Christopher Menzel Re: [ontolog-forum] type free logic and higher order quantification, Rick Murphy Re: [ontolog-forum] type free logic and higher order quantification, John F. Sowa <= Re: [ontolog-forum] type free logic and higher order quantification, Pat Hayes Re: [ontolog-forum] type free logic and higher order quantification, John F. Sowa Re: [ontolog-forum] type free logic and higher order quantification, Christopher Menzel Re: [ontolog-forum] type free logic and higher order quantification, Pat Hayes Re: [ontolog-forum] type free logic and higher order quantification, Christopher Menzel Re: [ontolog-forum] type free logic and higher order quantification, Rick Murphy Re: [ontolog-forum] type free logic and higher order quantification, k Goodier Re: [ontolog-forum] type free logic and higher order quantification, Christopher Menzel Re: [ontolog-forum] type free logic and higher order quantification, Rick Murphy Re: [ontolog-forum] type free logic and higher order quantification, John F. Sowa