$\vDash$ is used for semantic ideas, while $\vdash$ is used for syntactical ideas.
Prerequisite Definitions
Definition. Model
$\Sigma$ is a set of $\lan$ sentences. $\mA$ is said to be a model (interpretation) of $\Sigma$ if for every $\lan$-sentence $\varphi\in\Sigma$, $\varphi$ is true in $\mA$ (denoted by $\mA\vDash\varphi$). In this way, we write $\mA\vDash\Sigma$.
Definition. Satisfiability
A $\lan$-sentence $\varphi$ is said to be satisfiable if $\varphi$ has at least one model.
Definition. Theorem ( $\vdash \varphi$ )
There are many ways to define a theorem in a language $\lan$. In the context of Model Theory, we usually define a theorem using the following (syntactic entailment) way.
A $\lan$-sentence $\varphi$ is said to be a theorem (denoted by $\vdash\varphi$) if $\varphi$ is derivable using the axioms and inference rules of $\lan$
Definition. Validity ( $\vDash\varphi$ )
A $\lan$-sentence $\varphi$ is said to be valid (denoted by $\vDash\varphi$) if $\varphi$ holds in every model of $\lan$.
Definition. Rule of Inference (aka. Modus Ponens aka. Rule of Detachment)
A $\lan$-sentence $\varphi$ is said to be inferred from $\psi$ and $\theta$ by detachment iff $\theta$ is $\psi\to\varphi$ .
Definition. Deduction $(\Sigma\vdash\varphi)$
A $\lan$-sentence $\varphi$ is said to be deducible from a set $\Sigma$ of $\lan$-sentences (denoted by $\Sigma\vdash\varphi$) if there exists a finite sequence $\{\psi_k\}_{k=0}^n$ of $\lan$-sentences such that
- $\varphi=\psi_n$
- for every possible $k$, $\psi_k$ is either a tautology, or $\psi_k\in\Sigma$, or can be inferred from $\psi_i$ and $\psi_j$ with $0\leq i,j< k$.
Definition. Consequence ( $\Sigma\vDash\varphi$ )
A $\lan$-sentence $\varphi$ is said to be the consequence of a set $\Sigma$ of $\lan$-sentences if every model of $\Sigma$ is a model of $\{\varphi\}$. Specially if $\Sigma$ is a singleton $\{\psi\}$, we can write $\psi\vDash\varphi$ ($\varphi$ is a consequnce of $\psi$).
Definition. Elementary Equivalence ( $\mA\equiv\mB$ )
Two $\lan$-models $\mA$ and $\mB$ are said to be elementarily equivalent iff for every $\lan$-sentence $\varphi$, $\varphi$ is true in $\mA$ iff. $\varphi$ is true in $\mB$.
Definition. Theory
- A set $\Gamma$ of $\lan$-sentences is said to be a theory.
- If $\Gamma$ is a theory, $\Gamma$ is called closed if every consequence of $\Gamma$ belongs to $\Gamma$ ( $\Gamma\vDash\varphi\implies\varphi\in\Gamma$ )
Definition. Axiom of Theory
- A set $\Delta$ of $\lan$-sentences is said to be a set of axioms of a theory $\Gamma$ iff $\Gamma$ and $\Delta$ have the same consequences.
- A theory $\Gamma$ is called finitely axiomatizable if it has a finite set $\Delta$ of axioms.
- Since we can form a conjunction of a set of sentences, $\Delta$ is finites is equivalent to $|\Delta|=1$.
Definition. Logical System
A logical system $\sys$ is formally defined to be $\sys=(\lan, \Axiom, \IR, \vdash)$ where
- $\lan$ is called language (a set of symbols) of the system.
- $\Axiom$ is a set of axioms of the system.
- $\IR$ is a set of inferrence rules of the system
In the logical system, any $\lan$-sentence that could be proved using $\Axiom$ and $\IR$ is called a theorem of the system (same as the definition above).
Definition. Recursively enumerable sets.
A set $S\subset\mathbb N$ is said to be recursively enumerable (RE), or semidecidable, if there is an algorithm (or Turing Machine) such that the set of input numbers for which the algorithm halts is exactly $S$.
Of course if $S$ is not a subset of $\mathbb N$, but has the same cardinal as a subset of $\mathbb N$, then we can also define $S$ to be an extended recursively enumerable sets easily.
Definition. Recursively axiomatized system
A logical system $\sys=(\lan, \Axiom, \IR, \vdash)$ is said to be recursively axiomatized if $\Axiom$ is recursively enumerable.
Definition. Consistence (of a set of $\lan$-sentences)
$\Sigma$ is a set of $\lan$-sentences, we say $\Sigma$ is consistent if $\Sigma$ is not inconsistent, and $\Sigma$ is said to be inconsistent if for all sentence $\varphi$ in $\lan$, $\Sigma\vdash\varphi$ .
Another intuitive way to define inconsistency is that there exists a $\lan$-sentence $\varphi$ such that $\Sigma\vdash\varphi$ and $\Sigma\vdash\neg\varphi$. This post shows that both definitions are equivalent.
Definition. Maximal Consistent (of a set of $\lan$-sentences)
A set of $\lan$-sentences $\Sigma$ is said to be maximal consistent iff $\Sigma$ is consistent and for each $\lan$-sentence $\psi\notin\Sigma$, $\Sigma\cup\psi$ is inconsistent.
Definition. Cardinal (基数) of a language
Cardinal (or power) of a language $\lan$ is defined as $\omega \cup |\lan|$, denoted by $\|\lan\|$
- Power 表示势是一种比较老派的说法, 在现代的数学教材中已经不再使用.
- 这里的表述比较奇怪, 似乎是混淆了基数和序数的概念. 比较好的定义应当是这样的 $\|\mathcal L\|:=\max\{ℵ₀, |\mathcal L|\}$
- $|\mathcal L|$表示基本符号集合的基数, $\|\mathcal L\|$ 表示语言的"全部能力"，必须考虑到所有可能的公式构造
Definition. Soundness
Given a formal system $\sys=(\lan, \Gamma, \IR, \vdash)$, if any $\mathcal L$-sentence $\varphi$ that a theorem of $\sys$ (i.e. $\varphi$ can be deduced from $\Gamma$ using $\IR$), $\varphi$ is valid (i.e. $\varphi$ is a consequence of $\Gamma$), i.e.
then we say this system $\sys$ is sound.
Note that soundness is a quite basic requirement for logic system, because we usually don’t want it happen that what we can prove is true. But there are in fact some applications of unsound logical systems in CS, trading off for performance:
we usually DO NOT allow a logical system to be unsound in mathematical research, which is highly likely to destroy the generality of our conclusion.
Definition. Completeness
Given a formal system $\sys=(\lan, \Gamma, \IR, \vdash)$, if any $\mathcal L$-sentence $\varphi$ that is valid (i.e. $\varphi$ is a consequence of $\Gamma$), $\varphi$ is a theorem of $\sys$ (i.e. $\varphi$ can be deduced from $\Gamma$ using $\IR$), i.e.
then we say this system $\sys$ is complete. Otherwise we say this system is incomplete.
Theorem. First order logic is complete. (Gödel, 1929)
Unlike soundness as a basic guarantee of a logical system, completeness is what mathematicians are chasing for, although it cannot always be achieved, as stated in the following theorem.
Theorem. Gödel’s first incompleteness theorem.
Any recursively axiomatized and consistent logical system $\sys$ with its axioms containing Peano’s Axioms is incomplete.
Note that completeness holds in sentential logic and first order logic, but fails in second order logic because it has too much expressive power. Compeleteness theorem is likely to fail in infinitary logic systems. Generally, if a logic is more complicated (more expressive power), it’s more likely that completeness theorem fails in that logic.
Models Constructed from Constants
1. Completeness and Compactness
Definition. Witness
$T$ is a set of sentences in $\mathcal L$, $C$ is a set of constant symbols in $\mathcal L$, $C$ is said to be a witness of $T$ in $\mathcal L$ iff for every $\lan$-formula in this language with at most a free variable (denoted by $x$), $\exists c\in C$ s.t.
We say that $T$ has witness in $\mathcal L$ iff $T$ has some set $C$ of witnesses in $\mathcal L$ .
Lemma. A consistent theory in $\lan$ can be extended in $\bar\lan$ to include new constants as witnesses. That is,
Let $T$ be a consistent set of $\lan$-sentences. Let $C$ be a set of new constant symbols of power $|C|=\|\lan\|$. Let $\bar\lan=\lan\cup C$ be a simple expansion of $\lan$ formed by adding $C$ . Then $T$ can be extended to a consistent set of sentences $\bar T$ in which has $C$ as a set of witnesses in $\bar \lan$.
Pf. We firstly define New Constants. Let $\alpha = \|\lan\|$. For each $ \beta < \alpha$, define a new constant $c_\beta$, ensuring $c_\beta$ does not occur in $\lan$, and that $c_\beta \neq c_\gamma$ for $\beta \neq \gamma$. The set $C = \{ c_\beta : \beta < \alpha \}$ is added to the language, forming the expanded language $\bar\lan = \lan \cup C$. Construct an increasing sequence of sentence sets $T = T_0 \subset T_1 \subset \dots \subset T_\xi \subset \dots$, and define a sequence of constants $\{d_\xi\}_{\xi\in\Xi}$ such that:
- Each $T_\xi$ is consistent in $\bar \lan$;
- If $\xi = \zeta + 1$ is a successor ordinal, then $T_{\xi} = T_\zeta \cup \{(\exists x_\zeta) \varphi_\zeta \rightarrow \varphi_\zeta(d_\zeta)\}$, where $x_\zeta$ is the free variable in $\varphi_\zeta$ (if it has one), and $\varphi_{\zeta}$ is an arbitrary formula in $\bar\lan$ that contains at most one free variable. Otherwise, set $x_\zeta = v_0$ (which is a default placeholder variable to handle some special cases like this).
- If $\xi$ is a nonzero limit ordinal, then $T_{\xi} = \bigcup_{\zeta < \xi} T_\zeta$.
Note that the number of sentences in $T_{\zeta}$, which are not sentences of $\lan$ is smaller than $\alpha$. Furthermore, each such sentence contains at most a finite number of constants from $C$. So one can always find a constant from $C$ that has never appeared in $T_{\zeta}$ for each $\zeta$. Therefore let $d_{\zeta}$ be the first element of $C$ which has not yet occurred in $T_{\zeta}$.
In the recursive step, assuming $T_\zeta$ is defined and consistent, I’ll show that $T_{\xi}$ is also consistent. Otherwise
i.e.
but since $d_{\zeta}$ has never appeared in $T_{\zeta}$, we have a tricky transformation as follows
i.e.
which indicates that $T_\zeta$ is inconsistent.
This implies the consistency of the entire sequence $\{T_\xi\}_{\xi\in\Xi}$, and thus $T = \bigcup_{\xi < \alpha} T_\xi$ is consistent. Define $T = \bigcup_{\xi < \alpha} T_\xi$. It is evident that $T$ is a consistent extension of $T$, and $T$ includes witnesses for each formula, completing the proof.
Lemma.
Theorem. Downward Lowenheim-Skolem-Tarski Theorem
Every consistent theory $T$ in $\lan$ has a model of power at most $\|\lan\|$.
Theorem. Upward Lowenheim-Skolem-Tarski Theorem
Theorem. Compactness
A set $\Sigma$ of $\lan$-sentences has a model if and only if every finite subset of $\Sigma$ has a model.