First-order Logic

A formal system for describing and reasoning about objects, their properties, and their relations. This system is described typically by talking about individual objects and applying predicates and relationships to them. It allows operations like $\forall$ and $\exists$. You cannot quantify the predicates themselves, just the objects.

Model

The model revolves solely around objects, forbidding reasoning about predicates themselves. For example, you could say the following:

$$forallx:("Human"(x)->"Mortal"(x))$$

Which is saying that all humans are mortal. The objects are being reasoned on.

Conversely, you could not say this:

$$forallP:(P("Socrates")->P("Plato"))$$

Which is saying that for all properties that apply to Socrates, they also apply to Plato. This moves us into higher order logic as we are now reasoning about the properties themselves rather than the objects that are Socrates and Plato.

What’s the point?

First order logic is useful because it is very powerful on the objects themselves. By limiting what you can talk about, the reasoning becomes manageable. This makes it so everything becomes provable.

Things like ACL2, thus, are first-order logics, as they care more about being complete proof systems.

On the other hand, higher order logics are typically better for proving incredibly hard problems, as you lose tractability (the ability to solve problems that are, in general, outside of polynomial time).