From f7048f1ec32c1426ccc65d8f0393cb74bf0a5771 Mon Sep 17 00:00:00 2001 From: zeramorphic Date: Fri, 10 May 2024 18:59:58 +0100 Subject: [PATCH] Some updates Signed-off-by: zeramorphic --- ii/lst/05_set_theory.tex | 2 +- iii/forcing/01_set_theory.tex | 28 ++++++------ iii/forcing/02_constructibility.tex | 30 +++++++------ iii/forcing/03_forcing.tex | 48 ++++++++++----------- iii/forcing/04_forcing_and_independence.tex | 2 +- iii/mtncl/05_indiscernibles.tex | 2 +- iii/mtncl/06_intuitionistic_logic.tex | 14 +++--- iii/mtncl/07_intuitionistic_semantics.tex | 2 +- 8 files changed, 65 insertions(+), 63 deletions(-) diff --git a/ii/lst/05_set_theory.tex b/ii/lst/05_set_theory.tex index c367dee..7210f17 100644 --- a/ii/lst/05_set_theory.tex +++ b/ii/lst/05_set_theory.tex @@ -50,7 +50,7 @@ \subsection{Axioms of \texorpdfstring{\(\symsfup{ZF}\)}{ZF}} where \( z \subseteq x \) means \( (\forall t)(t \in z \Rightarrow t \in x) \). We write \( \mathcal P(x) \) for the power set of \( x \). We can form the Cartesian product \( x \times y \) as a suitable subset of \( \mathcal P(\mathcal P(x \cup y)) \), as if \( z \in x, t \in y \), we have \( (z, t) = \qty{\qty{z}, \qty{z, t}} \in \mathcal P(\mathcal P(x \cup y)) \). - The set of all functions \( x \to y \) can be defined as a subset of \( \mathbb P(x \times y) \). + The set of all functions \( x \to y \) can be defined as a subset of \( \mathcal P(x \times y) \). \item \emph{Axiom of infinity}. Using our currently defined axioms, any model \( V \) must be infinite. For example, writing \( x^+ \) for the \emph{successor} of \( x \) defined as \( x \cup \qty{x} \), the sets \( \varnothing, \varnothing^+, \varnothing^{++}, \dots \) are distinct. diff --git a/iii/forcing/01_set_theory.tex b/iii/forcing/01_set_theory.tex index d1c92dc..4d908b8 100644 --- a/iii/forcing/01_set_theory.tex +++ b/iii/forcing/01_set_theory.tex @@ -18,7 +18,7 @@ \subsection{Introduction to independence results} \end{theorem} The continuum hypothesis is that there are no sets of cardinality strictly between \( \abs{\mathbb N} \) and \( \abs{\mathcal P(N)} = \abs{\mathbb R} \). \begin{definition} - The \emph{continuum hypothesis} \( \mathsf{CH} \) states that if \( X \subseteq \mathbb P(\mathbb N) \) is infinite, then either \( \abs{X} = \abs{\mathbb N} \) or \( \abs{X} = \abs{\mathcal P(\mathbb N)} \), or equivalently, + The \emph{continuum hypothesis} \( \mathsf{CH} \) states that if \( X \subseteq \mathcal P(\mathbb N) \) is infinite, then either \( \abs{X} = \abs{\mathbb N} \) or \( \abs{X} = \abs{\mathcal P(\mathbb N)} \), or equivalently, \[ 2^{\aleph_0} = \aleph_1 \] \end{definition} Progress was made on the continuum hypothesis in the 19th and 20th centuries. @@ -42,7 +42,7 @@ \subsection{Systems of set theory} We write \( \mathrm{FV}(\varphi) \) for the set of free variables of \( \varphi \). We will write \( \varphi(u_1, \dots, u_n) \) to emphasise the dependence of \( \varphi \) on its free variables \( u_1, \dots, u_n \). By doing so, we will allow ourselves to freely change the names of the free variables, and assume that substituted variables are free. -The syntax \( \varphi(u_0, \dots, u_n) \) does not imply that \( u_i \) occurs freely, or even at all. +The syntax \( \varphi(u_1, \dots, u_n) \) does not imply that \( u_i \) occurs freely, or even at all. Some of the most common axioms of set theory are as follows. \begin{enumerate} @@ -96,7 +96,7 @@ \subsection{Systems of set theory} We can then use formulas of the form \[ \exists C.\, (C \text{ is a class} \wedge \forall x \in C.\, \varphi) \] by defining it to mean that there is a formula \( \theta \) giving a class \( C \) satisfying \( \forall x \in C.\, \varphi \). -For example, the universe class \( \mathrm{V} = \qty{x \mid x = x} \), the Russell class \( R = \qty{x \mid x \notin x} \), and the class of ordinals are all definable. +For example, the universe class \( \mathrm{V} = \qty{x \mid x = x} \), the Russell class \( R = \qty{x \mid x \notin x} \), and the class of ordinals \( \mathrm{Ord} \) are all definable. Any set is a definable class. Classes are heavily dependent on the underlying model: if \( M = 2 \) then \( \mathrm{Ord} = 2 = M \), and if \( M = 3 \cup \qty{1} \) then \( \mathrm{Ord} = 3 \neq M \). @@ -128,10 +128,10 @@ \subsection{Adding defined functions} \begin{example} The intersection \( a \cap b \) can be defined as the unique set \( c \) such that \[ \forall x.\, (x \in c \iff x \in a \wedge x \in b) \] - This definition makes sense only if there is a unique \( c \) satisfying this formula \( \varphi(c) \). + This definition makes sense only if there is a unique \( c \) satisfying this formula \( \varphi(a, b, c) \). If \[ M = \qty{a, c, d, \qty{a}, \qty{a, b}, \qty{a, b, c}, \qty{a, b, d}} \] - then it is easy to check that both \( \qty{a} \) and \( \qty{a, d} \) satisfy \( \varphi \), so intersection cannot be defined. + then it is easy to check that both \( \qty{a} \) and \( \qty{a, b} \) satisfy \( \varphi(\{ a, b, c \}, \{ a, b, d \}, -) \), so intersection cannot be defined. \end{example} \subsection{Absoluteness} @@ -140,8 +140,8 @@ \subsection{Absoluteness} Other definitions need not, for example \( \mathcal P(\mathbb N) \), which need not be the true power set in a given transitive model. To quantify this behaviour, we need to define what it means for \( \varphi \) to hold in an arbitrary structure; this concept is called \emph{relativisation}. \begin{definition} - The quantifier \( \forall x \in a.\, \varphi \) is an abbreviation of \( \forall x.\, x \in a \Rightarrow \varphi \). - We use the analogous abbreviation for the existential quantifier. + The quantifier \( \forall x \in a.\, \varphi \) is an abbreviation of \( \forall x.\, (x \in a) \to \varphi \). + Similarly, \( \exists x \in a.\, \varphi \) is an abbreviation of \( \exists x.\, (x \in a) \wedge \varphi \). Let \( W \) be a class; we define by recursion the \emph{relativisation} \( \varphi^W \) of \( \varphi \) as follows. \begin{align*} (x \in y)^W &\equiv x \in y \\ @@ -168,7 +168,7 @@ \subsection{Absoluteness} We proceed by induction on the length of formulae. For example, \[ N \vDash (x \in y)^M \text{ iff } N \vDash x \in y \text{ and } x, y \in M \text{ iff } \theta(x), \theta(y), M \vDash x \in y \] - The cases for equality is similar, and disjunction and negation are simple. + The case for equality is similar, and disjunction and negation are simple. Finally, \[ N \vDash (\exists x.\, \varphi(x))^M \text{ iff } N \vDash \exists x.\, x \in M \wedge \varphi^M(x) \] which holds precisely when there is some \( x \in N \) such that \( N \vDash x \in M \) and \( N \vDash \varphi^M(x) \), but \( N \vDash x \in M \) if and only if \( \theta(x) \), giving the result as required. @@ -198,7 +198,7 @@ \subsection{Absoluteness} \( \varphi \leftrightarrow \psi \) does not imply \( \varphi^M \leftrightarrow \psi^M \). Let \( \varphi(v) \) be the statement \( \forall x.\, (x \notin v) \); in \( \mathsf{ZF} \) this defines \( \varnothing \). Now, the following are two ways to express \( 0 \in z \). - \[ \psi(z) \equiv \exists y.\, (\varphi(y) \wedge y \in z);\quad \theta(z) \equiv \forall y.\, (\varphi(y) \Rightarrow y \in z) \] + \[ \psi(z) \equiv \exists y.\, (\varphi(y) \wedge y \in z);\quad \theta(z) \equiv \forall y.\, (\varphi(y) \to y \in z) \] Note that if there exists a unique \( y \) such that \( \varphi(y) \), then these are equivalent. However, this is often not the case, for example if \[ a = 0;\quad b = \qty{0};\quad c = \qty{\qty{\qty{0}}};\quad M = \qty{a, b, c} \] @@ -207,7 +207,7 @@ \subsection{Absoluteness} The main obstacle to absoluteness for basic statements turns out to be transitivity of the model. \begin{definition} Given classes \( M \subseteq N \), we say that \( M \) is \emph{transitive} in \( N \) if - \[ \forall x, y \in N.\, (x \in M \wedge y \in x \Rightarrow y \in M) \] + \[ \forall x, y \in N.\, (x \in M \wedge y \in x \to y \in M) \] \end{definition} \subsection{The L\'evy hierarchy} @@ -324,7 +324,7 @@ \subsection{The L\'evy hierarchy} \[ \forall x \in a.\, \langle x, x \rangle \notin r \] \end{proof} \begin{corollary} - The statement that \( x \) is a transitive set totally ordered by \( \in \) is \( \Delta_0 \), and thus ordinals are in fact \( \Delta_0 \). + The statement that \( x \) is a transitive set totally ordered by \( \in \) is \( \Delta_0 \), and thus being an ordinal is \( \Delta_0 \). \end{corollary} \begin{lemma} (\( \mathsf{ZF} \)) @@ -522,7 +522,7 @@ \subsection{The reflection theorem} \eta & \text{where } \eta \text{ is the least ordinal such that } \exists x \in W_\eta.\, \varphi_j^W(x, \vb y) \end{cases} \] We set - \[ G_i(\delta) = \sup\qty{F_i(\vb y) \mid y \in W_\delta^{k_i}} \] + \[ G_i(\delta) = \sup\qty{F_i(\vb y) \mid \vb y \in W_\delta^{k_i}} \] If \( \varphi_i \) is not of this form, we set \( G_i(\delta) = 0 \) for all \( \delta \). Finally, we let \[ K(\delta) = \max\qty{\delta + 1, G_1(\delta), \dots, G_n(\delta)} \] @@ -572,7 +572,7 @@ \subsection{The reflection theorem} Then \( T \) is not finitely axiomatisable. That is, for any finite set of sentences \( \Gamma \) in \( \mathcal L_\in \) such that \( T \vdash \Gamma \), there exists a sentence \( \varphi \) such that \( T \vdash \varphi \) but \( \Gamma \nvdash \varphi \). \end{corollary} -This only holds for first-order theories; for example, G\"odel--Bernays set theory is finitely axiomatisable. +This only holds for first-order theories without classes; for example, G\"odel--Bernays set theory is finitely axiomatisable. \begin{proof} Let \( \varphi_1, \dots, \varphi_n \) be a set of sentences such that \( T \vdash \bigwedge_{i=1}^n \varphi_i \). Suppose that \( \bigwedge_{i=1}^n \varphi_i \) proves every axiom of \( T \). @@ -599,7 +599,7 @@ \subsection{Cardinal arithmetic} The cardinal arithmetic operations are defined as follows. Let \( \kappa, \lambda \) be cardinals. \begin{enumerate} - \item \( \kappa + \lambda = \abs{0 \times \kappa \cup 1 \times \lambda} \); + \item \( \kappa + \lambda = \abs{\qty{0} \times \kappa \cup \qty{1} \times \lambda} \); \item \( \kappa \cdot \lambda = \abs{\kappa \times \lambda} \); \item \( \kappa^\lambda = \abs{\kappa^\lambda} \), the cardinality of the set of functions \( \lambda \to \kappa \); \item \( \kappa^{<\lambda} = \sup\qty{\kappa^\alpha \mid \alpha < \lambda, \alpha \text{ a cardinal}} \). diff --git a/iii/forcing/02_constructibility.tex b/iii/forcing/02_constructibility.tex index b5f30f0..67fc276 100644 --- a/iii/forcing/02_constructibility.tex +++ b/iii/forcing/02_constructibility.tex @@ -18,9 +18,9 @@ \subsection{Definable sets} \end{remark} This definition involves a quantification over infinitely many formulas, so is not yet fully formalised. One method to do this is to code formulas as elements of \( \mathrm{V}_\omega \), called \emph{G\"odel codes}. -We can then use Tarski's satisfaction relation to define a formula \( \mathsf{Sat} \), and can then prove +We can then use Tarski's \emph{satisfaction relation} to define a formula \( \mathsf{Sat} \), and can then prove \[ \mathsf{Sat}(M, E, \ulcorner \varphi \urcorner, x_1, \dots, x_n) \leftrightarrow (M, \in) \vDash \varphi(x_1, \dots, x_n) \] -where \( \ulcorner \varphi \urcorner \in V_\omega \) is the G\"odel code for \( \varphi \). +where \( \ulcorner \varphi \urcorner \in \mathrm{V}_\omega \) is the G\"odel code for \( \varphi \). We will later use a different method to formalise it, but for now we will assume that this is well-defined. \subsection{Defining the constructible universe} @@ -63,7 +63,7 @@ \subsection{Defining the constructible universe} Then \[ \bigcup a = \qty{x \in \mathrm{L}_\alpha \mid (\mathrm{L}_\alpha, \in) \vDash \exists z.\, (z \in a \wedge x \in z)} \in \operatorname{Def}(\mathrm{L}_\alpha) \] \item For infinity, note that - \[ \omega = \qty{n \in \mathrm{L}_\omega \mid (\mathrm{L}_\omega, \in) \vDash n \in \mathrm{Ord}} \in \operatorname{Def}(\mathrm{L}_\alpha) \] + \[ \omega = \qty{n \in \mathrm{L}_\omega \mid (\mathrm{L}_\omega, \in) \vDash n \in \mathrm{Ord}} \in \operatorname{Def}(\mathrm{L}_\omega) \] \item Consider separation. Let \( \varphi \) be a formula, and let \( a, \vb u \in \mathrm{L}_\alpha \). We claim that @@ -123,8 +123,7 @@ \subsection{G\"odel functions} \item The reversed order of the free variables is done purely for technical reasons. \item \( \mathcal F_2 \) will correspond to disjunction for \( \Delta_0 \) formulas, intersection will correspond to intersection, \( \mathcal F_3 \) will give negation, and \( \mathcal F_9 \) and \( \mathcal F_{10} \) will give atomic formulas. \item \( \mathcal F_7 \) and \( \mathcal F_8 \) will deal with ordered \( n \)-tuples. - The triple \( \langle x_1, x_2, x_3 \rangle \), this is formed using \( x_1 \) and \( \langle x_2, x_3 \rangle \). - However, it cannot be formed using \( \langle x_1, x_2 \rangle \) and \( x_3 \). + For example, the triple \( \langle x_1, x_2, x_3 \rangle \) is formed using \( x_1 \) and \( \langle x_2, x_3 \rangle \), but it cannot be formed using \( \langle x_1, x_2 \rangle \) and \( x_3 \) without \( \mathcal F_7 \) or \( \mathcal F_8 \). \end{enumerate} \end{remark} \begin{proof} @@ -241,7 +240,8 @@ \subsection{G\"odel functions} The equalities are termed formulas as above, so \( \psi \) is a termed formula. Then \begin{align*} - \mathcal F_\varphi(a_1, \dots, a_n) &= \ran\ran\{\langle x_{n+2}, \dots, x_1\rangle \times a_j \times a_i \times a_n \times \dots \times a_1 \\&\quad\quad\quad\mid x_i = x_{n+1} \wedge x_j = x_{n+2} \wedge x_{n+1} \in x_{n+2}\} \\ + \mathcal F_\varphi(a_1, \dots, a_n) &= + \ran\ran\{\langle x_{n+2}, \dots, x_1\rangle \times a_j \times a_i \times a_n \times \dots \times a_1 \mid \\&\quad\quad\quad x_i = x_{n+1} \wedge x_j = x_{n+2} \wedge x_{n+1} \in x_{n+2}\} \\ &= \mathcal F_6(\mathcal F_6(\mathcal F_\psi(a_1, \dots, a_n), a_1), a_1) \end{align*} \end{itemize} @@ -257,19 +257,23 @@ \subsection{G\"odel functions} Now \begin{align*} \mathcal F_{\theta \wedge \psi}(a_1, \dots, a_n, \mathcal F_2(a_j, a_j)) &= \mathcal F_{\theta \wedge \psi}\qty(a_1, \dots, a_n, \bigcup a_j) \\ - &= \qty{\langle x_{n+1}, \dots, x_1 \rangle \in \qty(\bigcup a_j) \times a_n \times \dots \times a_1 \mid x_{n+1} \in x_j \wedge \forall k \leq n.\, x_k \in a_k \wedge \psi(x_1, \dots, x_{n+1})} + &= \Big\{\langle x_{n+1}, \dots, x_1 \rangle \in \qty(\bigcup a_j) \times a_n \times \dots \times a_1 \mid \\ + &\quad\quad\quad x_{n+1} \in x_j \wedge \forall k \leq n.\, x_k \in a_k \wedge \psi(x_1, \dots, x_{n+1})\Big\} \end{align*} So \begin{align*} - \ran(\mathcal F_{\theta \wedge \psi}\qty(a_1, \dots, a_n, \bigcup a_j)) &= \qty{\langle x_n, \dots, x_1 \rangle \in a_n \times \dots \times a_1 \mid \exists u.\, \langle u, x_n, \dots, x_1 \rangle \in \mathcal F_{\theta \wedge \psi}\qty(a_1, \dots, a_n, \bigcup a_j)} \\ - &= \qty{\langle x_n, \dots, x_1 \rangle \in a_n \times \dots \times a_1 \mid \exists x_{n+1} \in x_j.\, \psi(x_1, \dots, x_{n+1})} + \ran(\mathcal F_{\theta \wedge \psi}\qty(a_1, \dots, a_n, \bigcup a_j)) + &= \Big\{\langle x_n, \dots, x_1 \rangle \in a_n \times \dots \times a_1 \mid \\ + &\quad\quad\quad \exists u.\, \langle u, x_n, \dots, x_1 \rangle \in \mathcal F_{\theta \wedge \psi}\qty(a_1, \dots, a_n, \bigcup a_j)\Big\} \\ + &= \Big\{\langle x_n, \dots, x_1 \rangle \in a_n \times \dots \times a_1 \mid \\ + &\quad\quad\quad \exists x_{n+1} \in x_j.\, \psi(x_1, \dots, x_{n+1})\Big\} \end{align*} \end{proof} \begin{definition} A class \( C \) is \emph{closed under G\"odel functions} if whenever \( x, y \in C \), we have \( \mathcal F_i(x, y) \in C \) for \( i \in \qty{1, \dots, 10} \). Given a set \( b \), we let \( \mathrm{cl}(b) \) be the smallest set \( C \) containing \( b \) as a subset that is closed under G\"odel functions. \end{definition} -For example, \( \mathrm{cl}(\varnothing) = \varnothing \), \( \qty{a, b} \in \mathrm{cl}(\qty{a, b}) \), and \( \mathrm{cl}(b) = \mathrm{cl}(\mathrm{cl}(b)) \). +For example, \( \mathrm{cl}(\varnothing) = \varnothing \), \( a, b \in \mathrm{cl}(\qty{a, b}) \), and \( \mathrm{cl}(b) = \mathrm{cl}(\mathrm{cl}(b)) \). \begin{definition} Let \( b \) be a set. Define \( \mathcal D^n(b) \) inductively by @@ -331,7 +335,7 @@ \subsection{The axiom of constructibility} The \emph{axiom of constructibility} is the statement \( \mathrm{V} = \mathrm{L} \). Equivalently, \( \forall x.\, \exists \alpha \in \mathrm{Ord}.\, (x \in \mathrm{L}_\alpha) \). \end{definition} -We will show that if \( \mathsf{ZF} \) is consistent, then so is \( \mathsf{ZF} + (\mathrm{V} = \mathrm{L}) \), because \( \mathrm{L} \) is a model of \( \mathsf{ZF} + (\mathrm{V} = \mathrm{L}) \). +We will show that if \( \mathsf{ZF} \) is consistent, then so is \( \mathsf{ZF} + (\mathrm{V} = \mathrm{L}) \), by demonstrating that \( \mathrm{L} \) is a model of \( \mathsf{ZF} + (\mathrm{V} = \mathrm{L}) \). To do this, we will show that being constructible is absolute. \begin{lemma} \( Z = \mathrm{cl}(M) \) is \( \Delta_1^{\mathsf{ZF}} \). @@ -513,7 +517,7 @@ \subsection{The generalised continuum hypothesis in \texorpdfstring{\( \mathrm{L Then fix \( \varphi \) such that \[ \mathsf{ZFC} + \mathrm{V} = \mathrm{L} + \mathsf{GCH} \vdash \varphi \wedge \neg\varphi \] Then - \[ \mathsf{ZF} \vDash (\varphi \wedge \neg\varphi)^L \] + \[ \mathsf{ZF} \vdash (\varphi \wedge \neg\varphi)^L \] By relativisation, \( \varphi^L \wedge \neg(\varphi^L) \). Hence \( \mathsf{ZF} \) is inconsistent. \end{proof} @@ -549,7 +553,7 @@ \subsection{Combinatorial properties} \end{lemma} \begin{proof} If \( (A_\alpha)_{\alpha < \omega_1} \) is a \( \diamondsuit \)-sequence, then for all \( X \subseteq \omega \), there is \( \alpha > \omega \) such that \( X = A_\alpha \). - Thus \( \qty{A_\alpha \mid \alpha \in \omega_1 \mid A_\alpha \subseteq \omega} = \mathcal P(\omega) \). + Thus \( \qty{A_\alpha \mid \alpha \in \omega_1 \wedge A_\alpha \subseteq \omega} = \mathcal P(\omega) \). \end{proof} \begin{theorem} If \( \mathrm{V} = \mathrm{L} \), then \( \diamondsuit \) holds. diff --git a/iii/forcing/03_forcing.tex b/iii/forcing/03_forcing.tex index 96a2456..77831d7 100644 --- a/iii/forcing/03_forcing.tex +++ b/iii/forcing/03_forcing.tex @@ -6,7 +6,7 @@ \subsection{Introduction} We will then use the reflection theorem to obtain this result. If \( M \) is such a countable transitive model, we want to add \( \omega_2^M \)-many reals to \( M \). -We will try to do this a `minimal way'; for example, we do not want to add any ordinals. +We will try to do this in a `minimal way'; for example, we do not want to add any ordinals. This gives us much more control over the model that we build. Recall the argument that the sentence \( \varphi(x) \equiv \exists x.\, x^2 = 2 \) is independent of the axioms of fields: we began with a field in which the sentence failed, namely \( \mathbb Q \), and then extended it in a minimal way to \( \mathbb Q\qty[\sqrt{2}] \). @@ -22,7 +22,7 @@ \subsection{Introduction} Suppose we enumerate all formulas as \( \qty{\varphi_n \mid n \in \omega} \). Let \( r = \qty{n \mid M \vDash \varphi_n} \). If we added \( r \) to \( M \), we could then build a truth predicate for \( M \). -This would cause problems due to Tarski. +This would cause self-referential problems discussed by Tarski. The main issues we must overcome are the following. \begin{enumerate} @@ -38,7 +38,7 @@ \subsection{Introduction} To be generic, we will not specify any particular digits, but its decimal expansion will contain every finite sequence. We will call a specification \emph{dense} if any finite approximation can be extended to one satisfying the specification. For example, `beginning with a \( 7 \)' is not dense, but `containing the subsequence \( 746 \)' is dense. -It turns out that a real is generic precisely when it meets every dense specification. +We will define that a real is generic precisely when it meets every dense specification. Note that there are explicit, absolute bijections \( f : \mathcal P(\omega) \to \omega^\omega \), \( g : \omega^\omega \to 2^\omega \), \( h : 2^\omega \to \mathbb R \) and so on. So if \( M \vDash \mathsf{ZFC} \), knowledge of \( \mathcal P^M(\omega) \) gives us \( (\omega^\omega)^M, (2^\omega)^M, \mathbb R^M \). @@ -163,7 +163,7 @@ \subsection{Chains and \texorpdfstring{\( \Delta \)}{Δ}-systems} has size less than \( \kappa \). Therefore, there exists some \( X \in \mathcal C \) such that \( X \cap S = \varnothing \). We recursively choose \( X_\alpha \in \mathcal C \) for each \( \alpha < \kappa \) such that \( X_\alpha \cap \bigcup_{\beta < \alpha} X_\beta = \varnothing \). - Then \( {X_\alpha \mid \alpha < \kappa} \in [\mathcal C]^\kappa \) is a \( \Delta \)-system with empty root. + Then \( \qty{X_\alpha \mid \alpha < \kappa} \in [\mathcal C]^\kappa \) is a \( \Delta \)-system with empty root. \end{proof} We can show that assumptions in the above lemma were required. \begin{proposition} @@ -300,23 +300,21 @@ \subsection{Names} \[ M[G] = \qty{\dot x^G \mid \dot x \in M^{\mathbb P}} \] \end{definition} \begin{example} - \begin{enumerate} - \item If \( \varnothing \in M \), then \( \varnothing^G = \varnothing \). - \item Let - \[ \dot x = \qty{\langle p, \varnothing \rangle, \langle r, \qty{\langle q, \varnothing \rangle} \rangle} \] - If \( p, q, r \in G \), then - \begin{align*} - \dot x^G &= \qty{(\langle p, \varnothing \rangle)^G, \qty(\langle r, \qty{\langle q, \varnothing \rangle} \rangle)^G} \\ - &= \qty{\varnothing, \qty{(\langle q, \varnothing \rangle)^G}} \\ - &= \qty{\varnothing, \qty{\varnothing}} - \end{align*} - If \( p, r \notin G \), then - \[ \dot x^G = \varnothing \] - If \( r \in G \) but \( p, q \notin G \), then - \[ \dot x^G = \qty{(\langle q, \varnothing \rangle)^G} = \qty{\varnothing} \] - Finally, if \( p \in G \) but \( r \notin G \), then - \[ \dot x^G = \qty{\varnothing} \] - \end{enumerate} + If \( \varnothing \in M \), then \( \varnothing^G = \varnothing \). + Let + \[ \dot x = \qty{\langle p, \varnothing \rangle, \langle r, \qty{\langle q, \varnothing \rangle} \rangle} \] + If \( p, q, r \in G \), then + \begin{align*} + \dot x^G &= \qty{(\langle p, \varnothing \rangle)^G, \qty(\langle r, \qty{\langle q, \varnothing \rangle} \rangle)^G} \\ + &= \qty{\varnothing, \qty{(\langle q, \varnothing \rangle)^G}} \\ + &= \qty{\varnothing, \qty{\varnothing}} + \end{align*} + If \( p, r \notin G \), then + \[ \dot x^G = \varnothing \] + If \( r \in G \) but \( p, q \notin G \), then + \[ \dot x^G = \qty{(\langle q, \varnothing \rangle)^G} = \qty{\varnothing} \] + Finally, if \( p \in G \) but \( r \notin G \), then + \[ \dot x^G = \qty{\varnothing} \] \end{example} We aim to show the following major theorem. \begin{theorem}[generic model theorem] @@ -373,7 +371,7 @@ \subsection{Canonical names} \[ \dot G^G = \qty{\check p^G \mid p \in G} = \qty{p \mid p \in G} = G \] \end{proof} -\subsection{???} +\subsection{Verifying the axioms: part one} We can define unordered and ordered pairs of names, with sensible interpretations. \begin{definition} Given \( \mathbb P \)-names \( \dot x, \dot y \), let @@ -488,7 +486,7 @@ \subsection{???} If \( M[G] \) models any reasonable theory, we should have \( \mathbb P \setminus G \in M[G] \). We will try to build a name for \( \mathbb P \setminus G \). A natural name to consider is - \[ \dot c = \qty{\langle q, \dot p \rangle \mid p, q \in \mathbb P, p \perp q} \] + \[ \dot c = \qty{\langle q, \check p \rangle \mid p, q \in \mathbb P, p \perp q} \] Then \[ \dot c^G = \qty{p \mid \exists q \in G.\, p \perp q} \] If \( G \) is a filter, its elements are pairwise compatible, so \( G \cap \dot c^G = \varnothing \). @@ -508,7 +506,7 @@ \subsection{???} \subsection{The forcing relation} To show separation, we need to show that if \( \varphi(x, y) \) is a formula and \( \dot a, \dot b \) are \( \mathbb P \)-names, then -\[ C = \qty{\dot z \in \dot a^G \mid (\varphi(\dot z^G, \dot b^G))^{M[G]}} \in M[G] \] +\[ C = \qty{\dot z^G \in \dot a^G \mid (\varphi(\dot z^G, \dot b^G))^{M[G]}} \in M[G] \] This is unclear, even for simple formulas such as \( \varphi(x, y) \equiv x \notin y \). We will build a way to formally reason about \( M[G] \) from within \( M \), without having to rely on \( G \). To do this, we will define a relation \( p \Vdash \varphi \) between conditions \( p \in \mathbb P \) and names in \( \mathrm{V}^{\mathbb P} \). @@ -795,7 +793,7 @@ \subsection{The forcing theorem} Hence \( p \Vdash \dot x \in \dot y \), as required. \end{proof} -\subsection{\texorpdfstring{\( \mathsf{ZF} \)}{ZF} in forcing extensions} +\subsection{Verifying the axioms: part two} \begin{lemma} Suppose that \( M \) is a countable transitive model of \( \mathsf{ZF} \), \( \mathbb P \in M \) is a forcing poset, and \( G \subseteq \mathbb P \) is a generic filter. Then \( M[G] \) models separation. diff --git a/iii/forcing/04_forcing_and_independence.tex b/iii/forcing/04_forcing_and_independence.tex index 4aecc61..380503c 100644 --- a/iii/forcing/04_forcing_and_independence.tex +++ b/iii/forcing/04_forcing_and_independence.tex @@ -345,7 +345,7 @@ \subsection{Possible sizes of the continuum} \subsection{Larger chain conditions} We now discuss generalised Cohen forcing. Suppose that we want a model of \( \mathsf{ZFC} + \mathsf{CH} + (2^{\aleph_1} = \aleph_3) \). -Na\"ively, we might consider the forcing poset \( \Fn(\omega_3 \times \omega_1, 2) \), but we can show that \( \mathsf{CH} \) fails in this model. +Naively, we might consider the forcing poset \( \Fn(\omega_3 \times \omega_1, 2) \), but we can show that \( \mathsf{CH} \) fails in this model. \begin{proposition} Let \( M \) be a countable transitive model of \( \mathsf{ZFC} + \mathsf{GCH} \), and let \( (\kappa = \aleph_\alpha \wedge \kappa^\omega = \kappa)^M \). Let \( \mathbb P = \Fn(\kappa \times \omega, 2) \). diff --git a/iii/mtncl/05_indiscernibles.tex b/iii/mtncl/05_indiscernibles.tex index 6f6bd24..45e52ed 100644 --- a/iii/mtncl/05_indiscernibles.tex +++ b/iii/mtncl/05_indiscernibles.tex @@ -54,7 +54,7 @@ \subsection{Introduction} As \( \varepsilon \) generates \( F(\varepsilon) \), there is a finite suborder \( \varepsilon_0 \) such that \( \vb a \in F(\varepsilon_0) \). But \( \eta \) is infinite, so there is an embedding \( f : \varepsilon_0 \rightarrowtail \eta \). By assumption, \( F(f)(\vb a) \) satisfies \( \psi \) in \( F(\eta) \), so \( F(\varepsilon_0) \vDash \psi(\vb a) \), as \( \psi \) is quantifier-free so is preserved under substructures. - Similarly, \( F(\varepsilon) \vdash \psi(\vb a) \), as required. + Similarly, \( F(\varepsilon) \vDash \psi(\vb a) \), as required. \end{proof} \subsection{Existence of Ehrenfeucht--Mostowski functors} diff --git a/iii/mtncl/06_intuitionistic_logic.tex b/iii/mtncl/06_intuitionistic_logic.tex index 39e7b36..d873243 100644 --- a/iii/mtncl/06_intuitionistic_logic.tex +++ b/iii/mtncl/06_intuitionistic_logic.tex @@ -213,6 +213,13 @@ \subsection{The simply typed lambda calculus} \subsection{Basic properties} The following technical lemmas can be proven by induction. +\begin{lemma}[generation lemma] + \begin{enumerate} + \item For every variable \( x \), context \( \Gamma \), and type \( \sigma \), if \( \Gamma \Vdash x : \sigma \), then \( x : \sigma \in \Gamma \). + \item If \( \Gamma \Vdash (\lambda x: \tau.\, N) : \sigma \), then there is a type \( \rho \) such that \( \Gamma, x : \tau \Vdash N : \rho \), and \( \sigma = (\tau \to \rho) \). + \item If \( \Gamma \Vdash (M\, N) : \sigma \), then there is a type \( \tau \) such that \( \Gamma \Vdash M : \tau \to \sigma \) and \( \Gamma \Vdash N : \tau \). + \end{enumerate} +\end{lemma} \begin{lemma}[free variables lemma] Suppose that \( \Gamma \Vdash M : \sigma \). Then @@ -222,13 +229,6 @@ \subsection{Basic properties} \item \( \Delta \Vdash M : \sigma \) for some \( \Delta \subseteq \Gamma \) containing only the free variables of \( M \) in its domain. \end{enumerate} \end{lemma} -\begin{lemma}[generation lemma] - \begin{enumerate} - \item For every variable \( x \), context \( \Gamma \), and type \( \sigma \), if \( \Gamma \Vdash x : \sigma \), then \( x : \sigma \in \Gamma \). - \item If \( \Gamma \Vdash (\lambda x: \tau.\, N) : \sigma \), then there is a type \( \rho \) such that \( \Gamma, x : \tau \Vdash N : \rho \), and \( \sigma = (\tau \to \rho) \). - \item If \( \Gamma \Vdash (M\, N) : \sigma \), then there is a type \( \tau \) such that \( \Gamma \Vdash M : \tau \to \sigma \) and \( \Gamma \Vdash N : \tau \). - \end{enumerate} -\end{lemma} \begin{lemma}[substitution lemma] The typability relation respects substitution. \end{lemma} diff --git a/iii/mtncl/07_intuitionistic_semantics.tex b/iii/mtncl/07_intuitionistic_semantics.tex index 5563084..1d55e28 100644 --- a/iii/mtncl/07_intuitionistic_semantics.tex +++ b/iii/mtncl/07_intuitionistic_semantics.tex @@ -94,7 +94,7 @@ \subsection{Full simply typed lambda calculus} \and \inferrule{\ }{\Gamma \Vdash \star : 1} \and - \inferrule{\Gamma \Vdash M : 0}{\Gamma \Vdash !_\varphi\, M : \varphi} + \inferrule{\Gamma \Vdash M : 0}{\Gamma \Vdash {!_\varphi}\, M : \varphi} \end{mathpar} This typing relation captures the Brouwer--Heyting--Kolmogorov interpretation when paired with new reduction rules. \begin{mathpar}