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 in the universe of discourse. 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ə/) ("the object such that")...
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) | $℩$ |
| 4 | quantifier (o x A ↦ b) | $\forall$, $\exists$ |
| 5 | boolean connective (b ↦ b; b o b ↦ b) | $\lnot$; $\land$; $\lor$ |
| 6 | propositional connective (A o B ↦ b) | $\rightarrow$, $\leftrightarrow$ |
Provable $\vdash$, entails $\models$ ($\vDash$);
Table: Comparison of Terminology in Different Fields
| logical operator | boolean algebra | propositional calculus |
|---|---|---|
| logical equality | equality | logical biconditional |
Derivation/Logical rules. Axioms of equality: reflexivity, $x = x$; substitution, $x = y \rightarrow (A(x) \rightarrow A(y))$, where $A(y)$ is $A(x)$ with certain free entries of $x$ replaced with $y$ which remain free. Axiom of the definite description operator: $\exists! x A(x) \rightarrow A(℩ x A(x))$.
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...