$\vDash$ is used for semantic ideas, while $\vdash$ is used for syntactical ideas.
1. 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 $\phi\in\Sigma$, $\phi$ is true in $\mA$ (denoted by $\mA\vDash\phi$). In this way, we write $\mA\vDash\Sigma$.
Definition. Satisfiability
A $\lan$-sentence $\phi$ is said to be satisfiable if $\phi$ has at least one model.
Definition. Theorem ( $\vdash \phi$ )
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 $\phi$ is said to be a theorem (denoted by $\vdash\phi$) if $\phi$ is derivable using the axioms and inference rules of $\lan$
Definition. Validity ( $\vDash\phi$ )
A $\lan$-sentence $\phi$ is said to be valid (denoted by $\vDash\phi$) if $\phi$ holds in every model of $\lan$.
Definition. Rule of Inference (aka. Modus Ponens aka. Rule of Detachment)
A $\lan$-sentence $\phi$ is said to be inferred from $\psi$ and $\theta$ by detachment iff $\theta$ is $\psi\to\phi$ .
Definition. Deduction $(\Sigma\vdash\phi)$
A $\lan$-sentence $\phi$ is said to be deducible from a set $\Sigma$ of $\lan$-sentences (denoted by $\Sigma\vdash\phi$) if there exists a finite sequence $\{\psi_k\}_{k=0}^n$ of $\lan$-sentences such that
- $\phi=\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\phi$ )
A $\lan$-sentence $\phi$ is said to be the consequence of a set $\Sigma$ of $\lan$-sentences if every model of $\Sigma$ is a model of $\{\phi\}$. Specially if $\Sigma$ is a singleton $\{\psi\}$, we can write $\psi\vDash\phi$ ($\phi$ is a consequence 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 $\phi$, $\phi$ is true in $\mA$ iff. $\phi$ is true in $\mB$, i.e.
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\phi\implies\phi\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 inference 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 semi-decidable, 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. Compare the concept of recursively enumerable and recursive
Definition. Recursively sets
A set $S\subset \N$ is said to be recursive if there’s an algorithm such that given any input $x\in \N$, it will produce the answer “yes” if $x\in\N$ and answer “no” otherwise
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 $\phi$ in $\lan$, $\Sigma\vdash\phi$ .
Another intuitive way to define inconsistency is that there exists a $\lan$-sentence $\phi$ such that $\Sigma\vdash\phi$ and $\Sigma\vdash\neg\phi$. 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 of logic system
Given a formal system $\sys=(\lan, \Gamma, \IR, \vdash)$, if any $\mathcal L$-sentence $\phi$ that a theorem of $\sys$ (i.e. $\phi$ can be deduced from $\Gamma$ using $\IR$), $\phi$ is valid (i.e. $\phi$ 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 of logic system
Given a formal system $\sys=(\lan, \Gamma, \IR, \vdash)$, if any $\mathcal L$-sentence $\phi$ that is valid (i.e. $\phi$ is a consequence of $\Gamma$), $\phi$ is a theorem of $\sys$ (i.e. $\phi$ can be deduced from $\Gamma$ using $\IR$), i.e.
then we say this system $\sys$ is complete. Otherwise we say this system is incomplete.
Definition. Completeness of theory
A theory $T$ of $\lan$-sentences is called complete (in $\lan$) iff its set of consequences is maximal consistent. i.e. for each $\lan$-sentence $\phi$,
Note that definition of completeness of a theory aligns with the definition of the completeness of a formal system. This is like, restrict the formal system to its sub-system (there’s no such a word), and the $\IR$ can often be reasoned from the context. In our notes, we only consider the first order logic, so the $\IR$ would be just the $\IR$ of first order logic system.
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. Completeness 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.
2. Models
2.1. Properties in FO logic
Definition. Isomorphism of first order models
Two $\lan$-models $\mA$ and $\mB$ are said to be isomorphic, denoted by $\mA\Iso\mB$ iff there exists a bijection
such that
- for each $n$-ary relation $R$ of $\mA$ and the corresponding $R'$ of $B$
- for each $n$-ary function $G$ of $\mA$ and the corresponding function $G'$ of $B$,
- for each constant $c$ of $\mA$ and the corresponding $c'$ of $B$,
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) \phi_\zeta \rightarrow \phi_\zeta(d_\zeta)\}$, where $x_\zeta$ is the free variable in $\phi_\zeta$ (if it has one), and $\phi_{\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.
Theorem. Extended Completeness Theorem
Theorem. Downward Lowenheim-Skolem-Tarski Theorem
Every consistent theory $T$ in $\lan$ has a model of cardinal at most $\|\lan\|$.
Theorem. Upward Lowenheim-Skolem-Tarski Theorem
If a theory $T$ has infinitely many models, then it has infinite models of any given cardinal $\alpha\geq \|\lan\|$
Theorem. Compactness
A set $\Sigma$ of $\lan$-sentences has a model if and only if every finite subset of $\Sigma$ has a model.
Corollary. It is impossible to characterize finiteness or countability, respectively, in first-order logic.
This could be proved using Upward LST Theorem and Compactness Theorem.
Definition. Standardness of Number Theory
The standard model of number theory is $\lll \omega, +,\cdot, S, 0,\rrr$ where
- $S$ is the successor function
- the rest symbols have their normal meanings
All other non-isomorphic models are called nonstandard
Corollary. There exist nonstandard models of complete number theory.
Theorem.
Let $\mA$ and $\mB$ be two $\lan$-models and $f:A\to B$, then TTFE
- $f$ is a isomorphic embedding of $\mA$ into $\mB$
- There exists an extension $\mC\supset\mB$ and an isomorphism $g:\mC\Iso\mB$ such that $f\subset g$
- $(\mB, fa)_{a\in\mA}$ is a model of the diagram of $\mA$
2.2. Omitting Types and Interpolation Theorems
****Definition**. Realize and Omit
Let $\Sigma$ be a set of $\lan$-formulas using variables no more than $x_1, x_2, \ldots, x_n$. Let $\mA$ be a model for $\lan$. We say that
- $\mA$ realizes $\Sigma$ iff some $n$-tuple of $A^n$ satisfies $\Sigma$
- $\mA$ omits $\Sigma$ if $\mA$ does not realize $\Sigma$
- $\Sigma$ is satisfiable in $\mA$ if $\mA$ realizes $\Sigma$
By definition it’s easy to observe that a set $\Sigma$ of $\lan$-formula is consistent if there exists a $\lan$-model that realizes $\Sigma$.
Definition. Type
A type $\Gamma(x_1, x_2, \ldots, x_n)$ in the variables $x_1, x_2, \ldots, x_n$ is defined to be the maximal consistent set of $\lan$-formulas in these variables.
e.g. Given any model $\mA$ and $n$-tuple $\clo a=(a_i)_{i=1}^n\in A^n$, the set
is a type, and in fact a unique type realized by $a_1, a_2, \ldots, a_n$. In this case, we call $\Gamma$ the type of $a_1, a_2, \ldots,a_n$ in $\mA$.
Definition. Locally realize
Let $\Sigma=\Sigma(\xn)$ be a set of $\lan$-formulas. A $\lan$-theory $T$ is said to locally realize $\Sigma$ iff there’s a $\lan$-formula $\phi(\xn)$ such that
- $\phi$ is consistent with $T$
- $\forall\sigma\in\Sigma.T\vDash \phi\to\sigma$
That is, every $n$-tuple in a model of $T$ which satisfies $\phi$ realizes $\Sigma$
The concept of locally realize is just restrict the subject from “model” to “theory”. There’s no more differences.
Definition. Locally omit
Let $\Sigma=\Sigma(\xn)$ be a set of $\lan$-formulas. A $\lan$-theory $T$ is said to locally omit $\Sigma$ iff $T$ does not locally realize $\Sigma$.
Thus, $T$ locally omits $\Sigma$ iff for every formula $\phi(\xn)$ which is consistent with $T$, there exists $\sigma\in\Sigma$ such that $\phi\land \neg\sigma$ is consistent with $T$
Lemma.
Let $T$ be a complete theory in $\lan$, and let $\Sigma=\Sigma(x_1,x_2,\ldots,x_n)$ be a set of $\lan$-formulas. If $T$ has a model which omits $\Sigma$, then $T$ locally omits $\Sigma$.
Theorem. Omitting Types Theorem.
Let $T$ be a consistent theory in a countable language $\lan$,and let $\Sigma(x_1, \ldots x_n)$ be a set of formulas. If $T$ locally omits $\Sigma$, then $T$ has a countable model which omits $\Sigma$.
Corollary. Let $\lan$ be a countable language. A theory $T$ has a (countable) model omitting $\Sigma(\xn)$ iff some complete extension of $T$ locally omits $\Sigma(\xn)$
Definition. $\omega$-model
Consider the language $\{+, \cdot, \Succ, 0\}$.
- An $\omega$-model is a model $\mA$ with the underlying set $A=\omega$. That is, $\mA$ omits $\{x\neq 1,x\neq 2,\ldots\}$
- A $\lan$-theory $T$ is said to be $\omega$-complete iff for every $\lan$-formula $\phi(x)$ we have the following $\omega$-rule holds
Corollary. Let $T$ be a consistent theory in $\lan$,
- If $T$ is $\omega$-consistent, then $T$ has a $\omega$-model
- If $T$ has a $\omega$-model, then $T$ is $\omega$-consistent
Definition. $\omega$-logic system
The $\omega$-logic system is exactly the same as first order logic system with two differences.
- the $\omega$-rule is added as a inference rule to $\omega$-logic
- infinitely long proof is allowed in $\omega$-logic
Theorem. $\omega$-completeness theorem
A $\lan$-theory $T$ is consistent in $\omega$-logic iff $T$ has an $\omega$-model.
Theorem. Craig interpolation theorem
Let $\phi,\psi$ be $\lan$-sentences such that $\phi\vDash\psi$. There exists a $\lan$-sentence $\theta$ such that
- $\phi\vDash\theta\land \theta\vDash\psi$
- Every relation, function or constant symbol (excluding $=$) which occurs in $\theta$ also occurs in both $\phi$ and $\psi$
Theorem. Robinson’s consistency theorem
Let $\lan_1$ and $\lan_2$ be two languages and let $\lan=\lan_1\cap\lan_2$. Suppose $T$ is a consistent $\lan$-theory, and $T_1\supset T, T_2\supset T$ are two consistent theories in $\lan_1$ and $\lan_2$ respectively, then $T_1\cup T_2$ is consistent in the language $\lan_1\cup\lan_2$
Theorem. Lyndon interpolation theorem
Let $\phi,\psi$ be $\lan$-sentences such that $\phi\vDash\psi$. There exists a $\lan$-sentence $\theta$ such that
- $\phi\vDash\theta\land \theta\vDash\psi$
- Every relation symbol (excluding $=$) which occurs positively in $\theta$ occurs positively in both $\phi$ and $\psi$
- Every relation symbol (excluding $=$) which occurs negatively in $\theta$ occurs negatively in both $\phi$ and $\psi$
Definition. implicit / explicit definition of predicate from sentences
Let $P$ and $P'$ be two $n$-ary relations not in language $\lan$. Let
- $\Sigma(P)$ be the set of sentences of the language $\lan\cup\{P\}$,
- $\Sigma(P')$ be the set of sentences of the language $\lan\cup\{P'\}$,
then we say $\Sigma(P)$ implicitly defines $P$ iff
Equivalently if $(\mA, R)$ and $(\mA, R')$ are two models of $\Sigma(P)$, then $R=R'$. We say $\Sigma(P)$ explicitly defines $P$ iff there exists a $\lan$-formula $\phi(\xn)$ such that
Theorem. Beth’s theorem
$\Sigma(P)$ defines $P$ explicitly iff $\Sigma(P)$ defines $P$ implicitly.
2.3. Countable Models of Complete Theories
In this section, all the languages mentioned are countable. We mainly talk about two kinds of models in this section.
- atomic models (small)
- saturated models (large)
Definition. relative completeness of formula in theory
Let $T$ be a complete $\lan$-theory. A formula $\phi(\xn)$ is said to be complete in $T$ if for every formula $\psi(\xn)$, exactly one of the followings holds
Definition. completable
A formula $\theta(\xn)$ is said to be completable in $T$ if there’s a complete formula $\phi(\xn)$ such that
$\theta$ is said to be incompletable if $\theta$ is not completable.
Definition. atomic theories / models
A theory $T$ is said to be atomic if every $\lan$-formula which is consistent with $T$ is completable in $T$. A model $\mA$ is said to be an atomic model if every $n$-tuple $a_1,a_2\ldots,a_n\in A$ satisfies a complete formula in $\Th(\mA)$
Theorem. existence of atomic models
Let $T$ be a complete $\lan$-theory. $T$ has a countable atomic model iff $T$ is atomic.
Theorem. uniqueness theorem for atomic models
If $\mA$ and $\mB$ are countable atomic models and $\mA\equiv\mB$, then $\mA\Iso\mB$
Definition. saturated models (饱和模型)
A model $\mA$ is said to be $\omega$-saturated if for every finite set $Y\subset A$, every set of formulas $\Gamma(x)$
2.4. Recursively Saturated Models
Definition. recursively enumerable sets
Definition. $\Delta_0$ formula
A $\Delta_0$ formula, or bounded quantifier formula, is a formula in the language $\lan$ using only $\in$ symbol and equality which is built from atomic formulas using only logic connectives and relativized quantifiers $(\forall x\in y)$ and $(\exists x\in y)$
Definition. $\Sigma_1$ formula
A $\Sigma_1$ formula is a formula built from $\Delta_0$ formula using
- positive connectives $\land$, $\lor$; and
- bounded quantifiers $\forall x\in y,\exists x\in y$; and
- existential quantifiers $\exists x$
Definition. recursive language
A language $\lan$ is said to be recursive if the set of symbols of $\lan$ and functions giving the number of arities (places) of symbols of $\lan$ are recursive subsets of $R(\omega)$, that is
2.5. Lindström’s Characterization of FOL
In this section we shall prove a result of Lindstrom which shows that first order logic is the only logic for which the Compactness Theorem and Downward Lowenheim-Skolem Theorem hold.
Definition. abstract logic
An abstract logic is a pair of classes $(l,\vDash_l)$ with the following properties, where $l$ is called the class of sentences and $\vDash_l$ is called the satisfaction relation of the logic, satisfying
- Occurrence Property.
- Expansion Property
- Isomorphism Property
- Renaming Property
- Closure Property
- Quantifier Property
Definition. model (of sentences) in abstract logic
A model of a set $T$ of sentences in an abstract logic $l$ is