Formal language...
Domain of discourse, universe of discourse, or universe is the entirety of objects that can be considered in a formal theory.
calculus... predicate calculus, the propositional calculus and the λ-calculus...
alphabet...
Individual constant is a symbol for a fixed object. Boolean values are the two individual constants: true and false. Tautology $\top$, contradiction $\bot$...
Variable is a symbol for an object that takes values from a domain of variation. Individual variable is a symbol for an arbitrary object. Every formal language contains one or several types of individual variables, each type with an infinite set of variables. Predicate variable (or second-order variable) is a variable whose values can be predicates.
Predicate (谓词) $P: \prod_{i=1}^n D_i \mapsto 2$ is a function whose values are booleans: zero-place predicates are propositions; one-place predicates are properties; multi-place predicates are relations.
Logical operation...
Definite description operator (or definite descriptor) $℩$ (rotated greek letter "ι" /aɪˈoʊtə/) ...
Quantifier: universal quantification $\forall$ (rotated letter "A"), existential quantification $\exists$ (rotated letter "E"); uniqueness quantification $\exists!$;
Connective: (boolean connective) negation $\lnot$ ($\neg$), conjunction $\land$ or $&$, disjuction $\lor$ or $\parallel$; exclusive disjunction ** $\oplus$ or $\veebar$; (propositional connective) **material implication $\rightarrow$ ($\to$) or $\implies$, material conditional $\leftarrow$, material equivalence $\leftrightarrow$ or $\iff$ or $\equiv$;
Definition $:=$ or $\Leftrightarrow$ ("is a notation for");
Precedence grouping $()$
Table: Primitive Symbols and Their Reduction Orders for Term Rewriting. (b, boolean; x, term; A, B, formula)
| # | Operator Type | Operators |
|---|---|---|
| 1 | precedence grouping | $()$ |
| 2 | predicate (x o y ↦ b) | |
| 3 | definite descriptor (o x A ↦ x) | $℩$ ("the object such that") |
| 4 | quantifier (o x A ↦ b) | $\forall$ (for all), $\exists$ (there exists) |
| 5 | boolean connective (b ↦ b; b o b ↦ b) | $\lnot$ (not); $\land$ (and); $\lor$ (or) |
| 6 | propositional connective (A o B ↦ b) | $\rightarrow$ (implies), $\leftrightarrow$ (equivalent) |
Provable $\vdash$, entails $\models$ ($\vDash$);
Table: Comparison of Terminology in Different Fields
| logical operator | boolean algebra | propositional calculus |
|---|---|---|
| logical equality | equality | logical biconditional |
term...
Sentential variable or propositional variable... Sentential formula, propositional formula, or formula... Well-formed formula... Proposition (命题)...
Sentence... bound variable... free variable...
axiom... axiom scheme... axiomatic system... theorem... model...
Derivation rule...
First-order logic (一阶逻辑) or predicate logic (谓词逻辑) has exactly one type... Propositional logic (命题逻辑)
consistent... completeness theorem... incompleteness theorem...