* Higher order predicates. Prolog has them.

Prolog is not first-order. That's how it's described but it lacks the fundamental distinction between predicate and function symbols that makes First-Order Logic, first-order.

To clarify. A FOL language begins with an "alphabet" (sometimes called a "signature") of predicate symbols, function symbols (including constants), variables, the five logical connectives (¬, ∧, ∨, →, and ↔) and punctuation (left and right parens, comma, dot, colon). The sets of predicate, function and variable symbols are disjoint.

Function symbols are used to define terms, inductively, as follows. A variable is a term; a constant is a term; if f is a function symbol and t_1, ..., t_n are terms, then f(t_1, ..., t_n) is a term.

Terms are used to define formulae as follows: If P is a predicate symbol and t_1, ..., t_n are terms, then P(t_1, ..., t_n) is an atomic formula, or atom. If φ is a formula, then ¬φ is a formula. If φ, ψ are formulae, then φ ∧ ψ, φ ∨ ψ, φ → ψ, and φ ↔ ψ are formulae.

Literals and clauses are defined as follows: if A is an atom, then A is a positive literal and ¬A is a negative literal. A clause is a disjunction of literals. A clause with a single positive literal is definite. A definite clause with no function symbols other than constants is datalog.

Now, if you squint a bit at all of the above and then at a Prolog program you will see a serious violation of the rules of FOL syntax. Observe:

This is Prolog:

  p(x, y):- q(r(x),z), r(p(x,z)).

See? r/1 and p/2 are used both as the symbols of terms and as the symbols of atomic formulae. That is a violation of FOL syntax. What's more, it's a violation of the "first-order" nature of FOL, where functions are "at a lower order" than predicates. That is, in FOL, terms map to entities in the domain of discourse, whereas formulae map to relations over entities in the domain of discourse.

But Prolog doesn't care. Prolog doesn't care if an object is a predicate, or a function, if it's a mapping, or a relation. For Prolog there's no distinction, and because there's no distinction it can treat everything as an argument to everything else: an atomic formula can be "passed" to an atomic formula, and taken apart, and put back together again. For example, you can do this sort of thing:

  ?- T_ =.. [p,X,Y,Z], T =.. [r,T_].
  T_ = p(X, Y, Z),
  T = r(p(X, Y, Z)).

That is no first-order functionality! In fact, in Prolog you can write this sort of thing:

  prove(L):- true.
  prove(L,Ls):- prove(L), prove(Ls).
  prove(L):- L \= (_,_), clause(L,Bs), prove(Bs).

And that is a Prolog interpreter written in Prolog. A program that evaluates programs? Toto, I don't think we're in FOL anymore.

I don't disagree with what you say here, but ... I'm coming at it from a formal semantics point of view. (I find Prolog and indeed "logic programming" in a larger sense to be all promise and little delivery on this front.) Perhaps you can check if your `prove` example is expressible in HiLog ... if so, it's more-or-less first order (in a semantically clean way). I believe the hard working XSB have an implementation.

I don't know that Prolog, or logic programming, makes any promises about formal semantics. I have to say I don't think of Prolog or logic programming in that context. Except for the more general point that Prolog programs are theories, and when a query is executied, that's a theorem being proven.

Btw, I'm not at all complaining about Prolog's higher-order. That may be a "hidden" feature, but it's a really, really useful one. FOL is actually very restrictive in many ways. As far as I understand it, the distinction between first and higher-order logics was not made by Peirce and Frege, who tended to fudge the orders a lot, just like Prolog.

In any case, for me, logic programming begins and ends with Robinson's paper on Resolution. That was not about formal semantics, and only about a sound and complete inference rule. And that (soundness and completeness) is all I really need to know. The rest (including definite clauses, SLD-Resolution and Prolog) is all implementation details.