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 (项)... Formula (公式)...
Sentential variable or propositional variable... Sentential formula, propositional formula, or formula... Well-formed formula... Proposition (命题)... Conjecture or hypothesis is a proposition someone believes to be true but has not been verified or falsified.
Sentence... bound variable... free variable...
Axiom (or postulate): a proposition regarded as self-evidently true without proof. Axiom scheme... Axiomatic system: a logical system of axioms or axiom schemes stated in a formal language. Theorem: a proposition proved to be true by accepted mathematical operations and arguments. Model...
Derivation rule...
Proof: A rigorous mathematical argument which unequivocally demonstrates the truth of a proposition.
First-order logic (一阶逻辑) or predicate logic (谓词逻辑) has exactly one type... Propositional logic (命题逻辑)
consistent... completeness theorem... incompleteness theorem...