First-Order Logic

First-order logic is a formal system of logic for expressing statements about objects, their properties, and their relations. It extends propositional logic by introducing variables, predicates, and quantifiers. “First-order” means that quantified variables range over individual objects in a domain, rather than directly over properties or relations. Its formal language, interpretations, and inference rules provide a framework for analyzing deductive reasoning. Unless otherwise specified, the term usually refers to classical first-order logic, commonly with equality. (builds.openlogicproject.org)

Language and syntax

A first-order language distinguishes logical symbols from a chosen nonlogical vocabulary, often called its signature. Logical symbols include variables, connectives such as negation and conjunction, and the quantifiers ∀ (“for every”) and ∃ (“there exists”). Nonlogical symbols include constants, function symbols, and predicate symbols, each function or predicate having a specified number of arguments. (people.math.wisc.edu)

The syntax defines expressions recursively. Terms designate objects: a variable or constant is a term, and applying a function symbol to suitable terms produces another term. Atomic formulas apply predicates to terms or equate two terms. Compound formulas are constructed using connectives and quantifiers. A two-place predicate can express a binary relation, such as “is less than.” An occurrence of a variable is bound when governed by a quantifier; otherwise it is free. A formula with no free variables is a sentence. (people.math.wisc.edu)

For example,

can express “Every human is mortal.” This states a conditional property of every object in the domain; it does not itself assert that humans exist. Existence requires a further statement such as $\exists x\,H(x)$. (cs.cmu.edu)

Interpretation and truth

The semantics assigns meanings through a structure. In the standard formulation, a structure has a nonempty domain and an interpretation of each nonlogical symbol. Constants denote domain elements, function symbols denote total functions on the domain, and predicates denote relations of the appropriate arity. Equality, when included as a logical symbol, denotes identity. A variable assignment supplies values for free variables. (cs.cmu.edu)

Truth is defined recursively. A universally quantified formula holds when its enclosed formula is true for every possible value of the quantified variable. An existentially quantified formula holds when at least one value makes it true. Thus quantifier order matters:

The first allows a different $y$ for each $x$; the second requires one $y$ that works for every $x$. (cs.cmu.edu)

A structure satisfying every sentence of a theory is a model of that theory. A sentence has logical validity when it is true in every structure for its language. Semantic consequence, written $\Gamma\models\varphi$, means that every model of the premises $\Gamma$ satisfies $\varphi$. These distinctions underpin model theory. (cs.cornell.edu)

Deduction and completeness

A deductive calculus specifies how to construct a formal proof from premises and logical rules. Common presentations include natural deduction, axiomatic calculi, and sequent calculus. Rules governing quantifiers include universal instantiation: from $\forall x\,P(x)$, one may infer $P(t)$, provided substitution avoids unintended variable binding. Proof theory studies such calculi and their derivations. (builds.openlogicproject.org)

Soundness means that derivability implies semantic consequence. The completeness theorem establishes the converse for suitable classical first-order calculi:

Consequently, every semantic consequence has a finite formal derivation, even when the premise set is infinite. (builds.openlogicproject.org)

This must be distinguished from Gödel’s incompleteness theorems. Logical completeness concerns consequences across all models. Incompleteness concerns limitations of consistent, effectively axiomatized theories sufficiently strong to represent arithmetic: such a theory need not decide every sentence in its language. An undecided sentence is not thereby a failure of the underlying logic’s completeness. (builds.openlogicproject.org)

Compactness and expressive limits

The compactness theorem states that a set of first-order sentences has a model if every finite subset has a model. Equivalently, inconsistency is already witnessed by finitely many premises. (cs.cornell.edu)

The Löwenheim–Skolem theorems impose further constraints. For a countable language, any theory with an infinite model has a countably infinite model and models of every infinite cardinality. First-order axioms therefore cannot characterize an infinite structure uniquely up to isomorphism among all structures. (cs.cornell.edu)

Compactness also prevents a first-order theory from having exactly all finite structures as its models. Adding sentences demanding at least $n$ distinct objects for every positive integer $n$ would make every finite subset satisfiable, forcing an infinite model. Particular finite sizes remain expressible using equality. (builds.openlogicproject.org)

In second-order logic, variables may instead range over properties or relations. First-order logic can nevertheless discuss sets when sets themselves are domain objects, as in set theory; the distinction concerns how quantification is interpreted, not whether sets are mentioned. (builds.openlogicproject.org)

Computability

Unrestricted first-order validity is undecidable: no algorithm always terminates with the correct answer for every input sentence. Validity is nevertheless semidecidable for an effectively presented language. Systematically enumerating proofs eventually finds a proof of any valid sentence, but may continue indefinitely for an invalid one. This difference between completeness and decidability establishes a fundamental limit on mechanical proof search. (builds.openlogicproject.org)