First-Order Predicate Calculus

While propositional logic serves as the foundation for logical reasoning, it is insufficient for describing the internal structure of mathematical statements. Propositional logic treats sentences as atomic units, whereas First-Order Logic (FOL), or Predicate Calculus, allows us to analyze the relationships between objects, their properties, and the scope of those assertions. FOL is the standard language of modern mathematics and set theory.

The Formal Alphabet of First-Order Logic

A first-order language is defined by its signature, which consists of:

1. Variables: Symbols like $x,y,z$ that range over a domain.
2. Constants: Specific names for objects in the domain, e.g., $0$ or $1$.
3. Functions: Symbols that map objects to other objects, e.g., $f(x)$ or $+(x,y)$.
4. Predicates (Relations): Symbols that represent properties or relationships, e.g., $P(x)$ or $<(x,y)$.
5. Logical Connectives: $\neg ,\wedge ,\vee ,⟹,⟺$.
6. Quantifiers: $\forall$ (Universal) and $\exists$ (Existential).

Well-Formed Formulas (WFFs)

The syntax of FOL is defined by recursive rules.

• Terms are variables, constants, or functions applied to terms.
• Atomic Formulas are predicates applied to terms, e.g., $R(t_1,t_2,\dots ,t_n)$.
• Formulas are built from atomic formulas using connectives and quantifiers.

A Sentence is a formula with no free variables. For example, $\forall x\exists y(x<y)$ is a sentence in the language of arithmetic, whereas $x<y$ is a formula with two free variables.

Semantics: Interpretations and Structures

The “truth” of a first-order formula depends on its Interpretation (or Model). An interpretation $\mathcal{I}$ consists of:

1. A Domain (Universe) $D$: A non-empty set of objects.
2. Mapping Functions: Each constant $c$ is assigned an element $c^{\mathcal{I}}\in D$. Each $n$-ary function $f$ is assigned a mapping $f^{\mathcal{I}}:D^n\to D$.
3. Mapping Relations: Each $n$-ary predicate $P$ is assigned a subset $P^{\mathcal{I}}\subseteq D^n$.

A formula $\varphi$ is satisfied by an interpretation if it evaluates to true under that specific mapping. If a sentence $\varphi$ is true in every possible interpretation, it is called Valid (the FOL analogue of a tautology).

Quantificational Inference Rules

Deduction in FOL requires specific rules for handling quantifiers:

1. Universal Instantiation (UI): If $\forall xP(x)$ is true, then $P(c)$ is true for any constant $c$ in the domain.
2. Universal Generalization (UG): If $P(x)$ is proven for an arbitrary $x$ (with no assumptions on $x$), then $\forall xP(x)$ is true.
3. Existential Generalization (EG): If $P(c)$ is true for some constant $c$, then $\exists xP(x)$ is true.
4. Existential Instantiation (EI): If $\exists xP(x)$ is true, we can “name” that element $k$, provided $k$ is a new constant not appearing elsewhere in the proof.

The Power of Identity

Most mathematical systems include the Identity Predicate ($=$). The axioms for identity are:

• Reflexivity: $\forall x(x=x)$.
• Substitution: $\forall x\forall y(x=y⟹(P(x)⟺P(y)))$.

These axioms allow us to define the “Uniqueness Quantifier” ($\exists !$): $\exists !xP(x)⟺\exists x(P(x)\wedge \forall y(P(y)⟹y=x))$

Limitations and Higher-Order Logic

First-order logic is powerful because of the Completeness Theorem (proven by Kurt Gödel): any formula that is logically valid (true in all models) is provable in the formal system. However, it has limitations, such as the Löwenheim-Skolem Theorem, which states that if a first-order theory has an infinite model, it has models of every infinite cardinality. This means FOL cannot uniquely “pin down” the structure of the real numbers $\mathbb{R}$. To describe properties like “every non-empty set of reals bounded above has a least upper bound,” we would need Second-Order Logic, where we can quantify over sets of elements.

Modeling Predicate Logic in Code

In computational logic, we often use Unification and Resolution to handle predicates. We can represent a simple knowledge base and query it.

type Entity = string;
type Predicate = (e: Entity) => boolean;

const Domain: Entity[] = ["Socrates", "Plato", "Aristotle", "Man"];

const isMan: Predicate = (e) => ["Socrates", "Plato", "Aristotle"].includes(e);
const isMortal: Predicate = (e) => isMan(e); // Axiom: ∀x (Man(x) ⇒ Mortal(x))

// Universal Check: ∀x (Man(x) ⇒ Mortal(x))
const checkUniversal = () => {
    return Domain.every(x => !isMan(x) || isMortal(x));
};

// Existential Check: ∃x (Man(x) ∧ Mortal(x))
const checkExistential = () => {
    return Domain.some(x => isMan(x) && isMortal(x));
};

console.log(`Universal validity: ${checkUniversal()}`);
console.log(`Existential validity: ${checkExistential()}`);

Exercise

While this code snippet is a trivial discrete simulation, it illustrates how predicates function as boolean-valued functions over a domain of discourse. In pure mathematics, the domains are often uncountable, requiring symbolic proof rather than exhaustive checking.