views:

55

answers:

2

Hi!

I do not really know if this is scientifically proven, but I've read in a book (It was a relatively modern AI book by Peter Norvig) that second-order logical programming could be more expressive than existing first-order languages.

The question is: Is it statistically/symbolically proven that higher-order predicate logics exceed first-order predicates in their expressive power? Or they just bring the modularity/convenience/maintainability to your knowledge bases?

Additionally: If there is some kind of firm direction in which I could go seeking more expressive power than I have (I mean exactly the descriptive potential of the symbols I write in given semantics/syntax) - then I would be glad to hear just almost everything :)

Thank you.

+7  A: 

Second order logic is more powerful and expressive than first order logic. Second order logic allows one to quantify over relations in addition to variables; thus it is possible, using a single sentence of second order logic, to express something that would require an infinite number of first order logic sentences. The relationship is similar to that between FOL and propositional logic.

As an example, consider the SOL statement:

\forall R \exists x \exists y (x R y)

This states that for any relation R there are x and y such that x R y holds. In order to express this in FOL, one would need a statement for each relation R in the language, which clearly could be infinite.

For a more interesting example, one could look at the proof that the transitive closure of a relation is not expressible in FOL. I can post it if you want to see it; but for the sake of succinctness I will omit it unless someone wants it.

Edit: You may also be interested in Descriptive Complexity -- essentially, it ties together the notions of complexity and expressibility -- if you can fully state a problem in a certain fragment of logic, then you know it is contained within the corresponding complexity class. For example, if a problem can be stated in Existential Second Order Logic, then it's in NP; if it can be stated in First Order Logic + a Least Fixed Point operator, then it's in P. If you can show that every statement of existential second order logic can be translated to FOL(LFP), then you've proven P=NP. (well, you've proven NP\subset P, but since the other containment is already known, you've proven equality...)

TJ Ellis
Thanks, I know the basics of second-order logics; but still have a question - In normal man's understanding, a facility to express relations over relations etc. is an increase of expressive power? Maybe I just don't get that concept? (By 'that concept' I mean the expressiveness)
Bubba88
BTW, you could post a link to that proof you mentioned if it's convenient for you:)
Bubba88
I realize that I did not address all of your questions; I do not know the results of any attempts at using SOL in logic programming, however, theoretically speaking, yes, SOL is more expressive.
TJ Ellis
Thanks, it's much more clear for me now.
Bubba88
Yes, it is an increase in expressive power -- there are statements in SOL that cannot be captured in FOL.
TJ Ellis
*raises hand* I would like to see the transitive closure proof, if you have it handy.
harms
aaaand here's the proof; sorry, it's pretty wordy and not nearly as succinct as it could have been; it's from an old homework set from a math logic class. http://uc.edu/~ellisto/tc.pdf
TJ Ellis
+1  A: 

You may want to look into dependent type theories.

Alexey Romanov