Zeroth-order logic

Zeroth-order logic is a term for a quantifier-free fragment of first-order logic.

A finitely axiomatizable zeroth-order logic is isomorphic to a propositional logic. Zeroth-order logic can transcend the power of propositional logic if axiom schemata are allowed. An example is given by the system Primitive recursive arithmetic, or PRA.

Example

The well-known syllogism

* All men are mortal
* Socrates is a man
* Therefore, Socrates is mortal

cannot be formalized in propositional logic, because of the use of predicates like "is a man" and "is mortal". The obvious formalization in first-order logic uses universal quantification to model the use of "All".

The following weak version of the syllogism can be formalized in propositional logic:

* If Socrates is a man, then Socrates is mortal
* Socrates is a man
* Therefore, Socrates is mortal

This can be done by introducing propositional constants "SMN" (for "Socrates is a man") and "SML" (for "Socrates is mortal"), and the two axioms
* "SMN" → "SML", and
* "SMN".Together with the usual rule of modus ponens the conclusion follows.

In this weak version most of the essence of the original syllogism has been lost. In predicate logic one can instead introduce predicates "Man" (for "is a man'), "Mortal" (for "is mortal"), constants "A" (for "Aristotle"), "S" (for "Socrates"), "Z" (for "Zeus"), and so on, and use a multitude of axioms, one for each individual:
* "Man"("A") → "Mortal"("A")
* "Man"("S") → "Mortal"("S")
* "Man"("Z") → "Mortal"("Z")
* ...
* "Man"("S")
* ¬"Mortal"("Z")Again, modus ponens allows to conclude "Mortal"("S"). If the axioms for contraposition are added, also ¬"Man"("Z") becomes a theorem.

By using an axiom schema, the above can be collapsed into:
* "Man"("x") → "Mortal"("x")
* "Man"("S")
* ¬"Mortal"("Z")The first line uses the variable "x", which can be instantiated by any constant for an individual, such as "S". The axioms are then the substitution instances of the schema.

An equivalent approach is to declare the schema to be a plain axiom and to make variable substitution a special inference rule of the logic.

Relation to general first-order logic

At first glance it might appear that by using axiom schemata as in the example any first-order logic can be made zeroth-order. However, in general only universal quantifiers at the outermost level can be eliminated this way.