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...