First-order logic编辑历史

**First-order logic** (FOL), also known as predicate logic, is a formal system in mathematical logic that extends propositional logic by incorporating quantifiers (∀ "for all," ∃ "there exists") and predicates that express properties of objects or relations among them. It provides a precise language for representing statements about individual objects and their relationships, forming the foundation for much of modern mathematics, computer science (especially automated reasoning and database theory), and analytic philosophy.

## 1 Syntax

The syntax of first-order logic defines the well‑formed expressions (formulas) of the language. It consists of an alphabet and a set of formation rules.

### 1.1 Alphabet of first‑order logic

The alphabet is divided into logical symbols and non‑logical symbols.

#### 1.1.1 Logical symbols

The logical symbols are fixed and have a constant meaning across all first‑order languages. They include:
- **Connectives**: ¬ (negation), ∧ (conjunction), ∨ (disjunction), → (implication), ↔ (biconditional).
- **Quantifiers**: ∀ (universal quantifier, “for all”), ∃ (existential quantifier, “there exists”).
- **Variables**: typically denoted by letters such as x, y, z, possibly with subscripts.
- **Equality**: the binary predicate symbol = (although sometimes treated as a logical symbol, in some treatments it is included in the non‑logical part).
- **Punctuation**: parentheses and commas.

#### 1.1.2 Non‑logical symbols

The non‑logical symbols form the signature of a particular first‑order language. They include:
- **Constant symbols**: names for specific individuals (e.g., a, b, c).
- **Function symbols**: symbols that denote functions from individuals to individuals, each with a fixed arity (e.g., f, g).
- **Predicate symbols**: symbols that denote properties or relations among individuals, each with a fixed arity (e.g., P, Q, R). The equality symbol is often considered a distinguished binary predicate.