- From: pat hayes <phayes@ai.uwf.edu>
- Date: Thu, 26 Apr 2001 19:43:25 -0500
- To: "Seth Russell" <seth@robustai.net>
- Cc: <www-rdf-interest@w3.org>

>From: "pat hayes" <phayes@ai.uwf.edu> > > > I wonder, could I make a plea that y'all change your terminology here > > slightly? The term 'higher-order' already has an accepted usage now > > for about80 years, and it isn't this, so this is likely to cause all > > kinds of confusion and wasted time. What you are talking about is > > meta-language statements (statements about other statements), not > > higher-order statements. > >Sorry, that was my foo pa Not just yours, lots of people get this wrong, even those who ought to know better. >.. i have these concepts all smushed together in >my mind ... and am playing catch up with my education. But I still don't >get what makes logic higher order. I have tried to depict my understanding >of your description in the graph at >http://robustai.net/mentography/higherOrder.gif which I have also put on >the Public CMap server under the SemanticWeb Project. If you do find the >time to answer me, maybe you could show where I have gone wrong by mutating >my graph. Hmm, not sure I follow the graph , I'm afraid. Sorry, I tend to work with words better. The higher-order/firstorder distinction is rather a subtle one to get exactly right. Let me sketch it first and then correct the sketch later, OK? Sketch First-order logic asserts relations between things, so you can say things like (IsBiggerThan Bill Fred) ie relation IsBiggerThan holds between things Bill and Fred, and it quantifies over the things, so you can say (forall (?x) (exists (?y)(IsBiggerThan ?y ?x))) ie for any thing x there is something y which is bigger than it, ie everything has something bigger than it. (I didnt say it was true, only that you can say it.) OK. In second-order logic, you can also quantify over the (first-order) relations and have (second-order) relations on relations, so for example you could say that IsBiggerThan is transitive: (Transitive IsBiggerThan) and define Transitive: (forall (?R) (iff (Transitive ?R) (forall (?x ?y ?z)(implies (and (?R ?x ?y)(?R ?y ?z)) (?r ?x ?z))) )) Notice that the ?R ranges over (first-order) relations, not just things. In third-order, you can have relations on second-order relations, and so on... Higher-order means you can go as high up the ladder of relations of relations of... as you want. In practice nobody much wants to go beyond second-order, most of the time, but you never know. Real Story What *really* makes a logic higher-order is that when you quantify over 'all relations', that really does mean ALL relations, not just the ones you happen to mention. There are a hell of a lot of relations; more than you probably ever want to think about. For example, consider the property (unary relation, ie relation with one argument) of being further north than the oldest plumber born in Philadelphia. Hey, its a perfectly good property; but when you said (forall (?p)...) did you really have that in mind as a possibility? Answer: if you are a mathematical logician, yes, you did. The moral of which is that real higher-order logic is probably more use to mathematicians than anyone else. For another example, suppose you wanted to say that two people had something in common, and thought of using a second-order sentence like (exists (?P) (and (?P Bill)(?P Joe))) to say it (ie there is some property true of Bill and of Joe), and you were thinking of ?P's like 'eye-color' or 'watches baseball'. It wouldnt do the job for you, since in real higher-order logic, this is trivially true of any two things, since the property of 'being either Bill or Joe' satisfies it. Written using lambda this would be (lambda (?x) (or (= ?x Bill)(= ?x Joe))). Obviously this is true of Bill (who is equal to Bill) and also of Joe, so it works for ?P. No good saying "that's not a real property": in real second-order logic it is, tough luck. The connection with lambda-calculus is that any lambda-expression with a sentence body defines a relation. ANY lambda-expression. So higher-order logic has an inference rule (called 'comprehension', sometimes its phrased as an axiom) which allows you to make any sentence into a lambda-expression. If you can say it, its can be used to define a relation, is the idea. ------ As you can see, none of this has got anything to do with sentences about sentences: its all to do with sentences about relations. Hope this helps. Pat Hayes --------------------------------------------------------------------- IHMC (850)434 8903 home 40 South Alcaniz St. (850)202 4416 office Pensacola, FL 32501 (850)202 4440 fax phayes@ai.uwf.edu http://www.coginst.uwf.edu/~phayes

Received on Thursday, 26 April 2001 20:43:32 UTC