First-order logic

Where propositional logic treats an entire statement as a unit, first-order logic can represent a property of an object as P(a) or a relation between objects as R(a,b). The argument positions matter: R(a,b) need not say the same thing as R(b,a). Constants designate objects, while variables provide positions used in general statements.

Formation rules build formulas from atomic formulas through connectives and quantifiers. An occurrence of a variable may be free or bound by a quantifier; a formula with no free variables is a sentence. Thus P(x) leaves a position open, whereas ∀xP(x) binds x. Being well formed is a syntactic achievement, not a guarantee of truth.

The qualification “first-order” concerns what variables range over: objects in the domain, rather than properties or relations of those objects as in higher-order logic.

References: [1]

An interpretation specifies a domain and the meanings of the nonlogical symbols. Under standard first-order semantics the domain is nonempty, constants designate its members, and predicates specify properties or relations. Evaluating an open formula also requires assigning objects to its free variables. Satisfaction expresses whether the formula's condition holds under those choices.

For a concrete example, let the domain contain just the numbers 1 and 2, interpret P as being even, and let a designate 2. Then P(a) and ∃xP(x) are true, but ∀xP(x) is false. Universal quantification requires satisfaction by every domain member; existential quantification requires at least one. Quantifiers range over objects, including any objects that have not been given individual names.

References: [2] [1]

The formulas ∀x∃yR(x,y) and ∃y∀xR(x,y) impose different conditions. The first permits the choice of y to depend on x. The second requires a single choice of y that works for every x. Interchanging these quantifiers is therefore not an innocent rearrangement.

Take the domain {1,2} and interpret R(x,y) as equality. Every element equals itself, so ∀x∃yR(x,y) holds. No single element equals both 1 and 2, so ∃y∀xR(x,y) fails. This small model isolates the difference without relying on an ambiguous everyday sentence or assumptions about the behavior of real people.

References: [3]

A sentence may be true in one interpretation and false in another. Logical validity demands truth in every admissible interpretation. Likewise, premises entail a conclusion when no interpretation makes all those premises true and the conclusion false. Finding one model that supports the conclusion cannot establish this universal relationship.

From ∀xP(x), the inference to P(a) is valid: a designates an object in the domain. From ∃xP(x), however, P(a) does not generally follow, because the object satisfying P need not be the object designated by a. Satisfiability asks only for some interpretation in which a sentence holds. Keeping these notions separate prevents facts about one selected model from being mistaken for consequences guaranteed by logical form.

Semantic validity can be connected to formal proof: first-order completeness says an appropriate calculus captures validity in all interpretations. It does not supply a procedure that halts on every formula and answers valid or invalid; general first-order validity is undecidable. Having rules sufficient to prove every valid formula and having an automated decision procedure that always finishes are different requirements. Completeness of the proof system does not establish the latter.

References: [4] [5]