The question of the expressive power of logical reasoning with a higher order

Question

I really don't know if this is scientifically proven, but I read in a book (it was a relatively modern AI book by Peter Norwig) that second-order logic programming can be more expressive than existing first-order languages.

The question arises: is it statistically / symbolically proven that higher order logics exceed first-order predicates in their expressive power? Or do they just bring modularity / convenience / support to your knowledge base?

Additionally: If there is any solid direction in which I could look for a more expressive power than I do (I mean the descriptive potential of the characters that I write in this semantics / syntax), then I would be glad to hear almost all:)

Thanks.

Answer 1

Second-order logic is more powerful and expressive than first-order logic. Second-order logic allows you to quantify relationships in addition to variables; thus, using one sentence of second-order logic, one can express what will require an infinite number of logical sentences of the first order. The relationship is similar to the relationship between FOL and sentence logic.

As an example, consider the SOL statement:

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

This means that for any relation R there are x and y such that x R y holds. To express this in FOL, we would need a statement for each R relation in the language, which obviously could be infinite.

For a more interesting example, one might look at the proof that the transitive closure of a relation is not expressed in FOL. I can publish it if you want to see it; but for the sake of brevity, I omit it if someone does not want it.

Edit: You may also be interested in Descriptive Complexity - essentially, it connects the concepts of complexity and expressiveness - if you can fully state the problem in a specific piece of logic, then you know that it is contained in the corresponding complexity class. For example, if the problem can be indicated in the logic of existential second order, then it is in NP; if it can be specified in first-order logic + the smallest fixed point, then it is in P. If you can show that each statement of existential second-order logic can be translated into FOL (LFP), then you proved that P = NP, ( well, you proved NP \ subset P, but since the other shell is already known, you proved the equality ...)

Answer 2

You can look at dependent types of theories .