ontolog-forum
[Top] [All Lists]

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

 To: "[ontolog-forum]" Pat Hayes Fri, 19 Aug 2011 14:52:20 -0500 <45BA1037-EA9E-4332-A7F3-BB8990EB746F@xxxxxxx>
 ``` On Aug 19, 2011, at 9:31 AM, John F. Sowa wrote:    (01) > Rick, > > 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. > > 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. > > 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.) > > 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. > > RM >> Understood. I've been heads down on functional programming lately, so >> I'm getting more comfy with higher order thinking. > > But the usual versions of functional programming are not higher-order > in the way logicians use the term. > > 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}. > > 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. > > 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, ... > > Since all possible relations are included, there would have to be > some relation p such that (p a) and (p b).    (02) In particular, it would be    (03) (lambda (x)(or (R x)(Q x)))    (04) which shows that even if one restricts oneself to lambda-definable relations (of which there are only countably many, instead of the uncountably many mathematically possible relations that would exist over any ground universe that contained, for example, any model of arithmetic) you would still get a divergence of intuition. As I am sure Chris will want to point out, the Henkin construction provides a(n arguably) first-order semantics for this lambda-definable fragment of true HO logic, so the higher/first-order wetlands get even boggier around here.    (05) > > 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.    (06) That is my suspicion also, but one never knows :-)    (07) > > RM >> to establish a hierarchy of types to avoid paradox. > > 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.    (08) It is    (09) (exists (Russel)(forall (x) (iff (Russel x)(not (x x)))))    (010) which yields a contradiction by instantiating x with Russell. What saves this from being a paradox is that it does not claim to *define* Russell, only to give exact conditions for its true application. In this case, those very conditions are contradictory, so the 'definition' fails to define. The usual formulation of defining conditions does not permit a definition to be false, which forces the paradox into existence.    (011) > 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. > > CL does not prevent you from using types. In fact, it encourages > you to do so by using quantifier restrictions. For example, > > (forall ((x Employee)) (exists ((y SSN)) ... )) > > 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. > > 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. > > 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. > > On the other hand, there are many legitimate sentences that you > can express in CL, which cannot be expressed in Z: > > "The number 23 is not an elephant." > > That is a true statement, which could be written (not (Elephant 23)). > > But you can't say that in Z because 'Elephant(23)' is a syntax error. > > 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. > > But CL also permits you to use weak typing or no typing at all.    (012) Put another way, strong typing is weak typing where some type-checking inferences are done by the parser rather than a post-parsing inference engine, and are considered to be mandatory.    (013) Pat    (014) > > John > > _________________________________________________________________ > 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 > >    (015) ------------------------------------------------------------ IHMC (850)434 8903 or (650)494 3973 40 South Alcaniz St. (850)202 4416 office Pensacola (850)202 4440 fax FL 32502 (850)291 0667 mobile phayesAT-SIGNihmc.us http://www.ihmc.us/users/phayes    (016) _________________________________________________________________ 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    (017) ```
 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