First-order logic

First-order logic is a formal system whose variables range over individual objects and whose predicates express properties and relations among them. It uses quantifiers such as “for all” and “there exists,” but does not quantify directly over properties or relations.

Predicate: A predicate is an expression that represents a property of objects or a relation among them. Predicates supply the properties and relations that first-order formulas assert.
First-order language: A first-order language is a specified collection of symbols and formation rules for expressing formulas about objects. Its vocabulary and grammar define the formulas used in a particular first-order theory.
Gödel's completeness theorem: Gödel's completeness theorem states that every sentence true in all models of a first-order theory is provable from that theory. It shows that semantic consequence in first-order logic has a matching proof system.
Propositional logic: Propositional logic studies formulas built from whole propositions using connectives, without quantifying over objects. It lacks the object variables and quantifiers that let first-order logic express general claims.
Quantifier: A quantifier specifies how many objects in a domain satisfy a condition. Universal and existential quantifiers let formulas range over individual objects.
Tarski's definition of truth: Tarski's definition of truth gives a recursive account of when a formal sentence is true in an interpretation. It explains truth in a structure by evaluating terms, predicates, connectives, and quantifiers.
Compactness theorem: The compactness theorem states that a set of first-order sentences has a model if every finite subset has a model. Compactness yields existence results that cannot be obtained by checking only one finite fragment.
Second-order logic: Second-order logic allows quantification over properties, relations, or sets as well as individual objects. It expresses some structural claims unavailable to first-order quantification over objects alone.
Domain of discourse: A domain of discourse is the collection of objects over which variables range in a formal interpretation. The domain fixes which objects first-order variables can refer to.
Natural deduction: Natural deduction is a proof system that derives conclusions from premises using introduction and elimination rules. Its quantifier rules provide a direct way to prove first-order arguments.

Linked from 75 pages