Roman V for ZF universe

Signed-off-by: zeramorphic <[email protected]>

ii/lst/07_incompleteness.tex

@@ -31,7 +31,7 @@ \subsection{Coding}
 The analogous statement for generalisation is also definable in a similar way.
 The axioms of \( \symsfup{PA} \) are clearly definable, and `\( n \) codes a logical axiom or axiom of \( \symsfup{PA} \)' is definable.
 Given formulae \( p_1, \dots, p_n \), we code the sequence as
-\[ s(p_1, \dots, p_n) = 2^{c(p_1)} 3^{c(p_2)}\dots \text{\( n \) prime}^{c(p_n)} \]
+\[ s(p_1, \dots, p_n) = 2^{c(p_1)} 3^{c(p_2)}\dots \text{\( n \)th prime}^{c(p_n)} \]
 Thus, `\( n \) codes a proof' is definable, and `\( n \) codes a proof of \( S_m \)' is definable.
 Let \( \theta(m,n) \) be a formula defining `\( n \) codes a proof of \( S_m \)'.
 Let \( \phi(m) = \text{`\( S_m \) is provable'} \) is definable, as \( \phi(m) = (\exists n)(\theta(m,n)) \).
@@ -62,7 +62,7 @@ \subsection{G\"odel's incompleteness theorem}
 We cannot use the above proof to show that \( T \) is incomplete, since this would immediately derive a contradiction.
 Almost all of the above proof is still valid, so the only invalid part must lead to this contradiction; there must be no algorithm to decide truth of sentences in \( \symsfup{PA} \).
 \begin{theorem}
-    \( T \) is not definable.
+    \( T \) is not decidable.
 \end{theorem}
 Note that \( \symsfup{ZFC} \vdash \mathrm{Con}(\symsfup{PA}) \), where \( \mathrm{Con}(\symsfup{PA}) \) represents the sentence
 \[ (\forall x \in \omega)(x \text{ does not code a proof of } \bot) \]

iii/forcing/01.tex

@@ -39,7 +39,7 @@ \subsection{Systems of set theory}
 
 We say that an occurrence of a variable \( x \) is \emph{bound} in a formula \( \varphi \) if is in a quantifier \( \exists x \) or lies in the scope of such a quantifier.
 An occurrence is called \emph{free} if it is not bound.
-We write \( FV(\varphi) \) for the set of free variables of \( \varphi \).
+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.
@@ -96,13 +96,13 @@ \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 \( 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 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 \).
 
 Suppose that \( M \) is a set model of \( \mathsf{ZF} \); that is, \( M \) is a set.
 Let \( \mathcal D \) be the collection of definable classes over \( M \).
-Then one can show that \( \mathcal D \) is a set in our metatheoretic universe \( V \), and \( (M, \mathcal D) \) is a model of a second-order version of \( \mathsf{ZF} \), known as \emph{G\"odel--Bernays set theory}.
+Then one can show that \( \mathcal D \) is a set in our metatheoretic universe \( \mathrm{V} \), and \( (M, \mathcal D) \) is a model of a second-order version of \( \mathsf{ZF} \), known as \emph{G\"odel--Bernays set theory}.
 
 \subsection{Adding defined functions}
 Often in set theory, we use symbols such as \( 0, 1, \subseteq, \cap, \wedge, \forall \); they do not exist in our language.
@@ -186,13 +186,13 @@ \subsection{Absoluteness}
         \[ \forall x_1, \dots, x_n \in M.\, (\varphi^M(x_1, \dots, x_n) \leftrightarrow \varphi^N(x_1, \dots, x_n)) \]
     \end{enumerate}
 \end{definition}
-If \( N = V \), we simply say that \( \varphi \) is (upwards or downwards) absolute for \( M \).
+If \( N = \mathrm{V} \), we simply say that \( \varphi \) is (upwards or downwards) absolute for \( M \).
 If \( \Gamma \) is a set of formulas, we say that \( \Gamma \) is (upwards or downwards) absolute for \( M, N \) if and only if \( \varphi \) is (upwards or downwards) absolute for \( M, N \) for each \( \varphi \in \Gamma \).
 Suppose \( T \) is a set of sentences and \( f \) is a defined function by \( \varphi \).
 Then for \( M \subseteq N \) models of \( T \), we say that \( f \) is absolute for \( M, N \) precisely when \( \varphi \) is absolute for \( M, N \).
 \begin{example}
     If \( M \subseteq N \) both satisfy extensionality, then the empty set is absolute for \( M, N \) by the formula \( \forall x \in a.\, (x \neq x) \).
-    The power set of \( 2 \) is not absolute between \( 4 \) and \( V \), because in \( 4 \), it has only two elements.
+    The power set of \( 2 \) is not absolute between \( 4 \) and \( \mathrm{V} \), because in \( 4 \), it has only two elements.
 \end{example}
 \begin{example}
     \( \varphi \leftrightarrow \psi \) does not imply \( \varphi^M \leftrightarrow \psi^M \).
@@ -410,27 +410,27 @@ \subsection{Transfinite recursion}
     A relation \( R \) is \emph{set-like} on a class \( A \) if for all \( x \in A \), the collection of \( R \)-predecessors of \( x \) is a set.
 \end{definition}
 \begin{example}
-    \( \in \) is set-like on \( V \), but \( \ni \) is not set-like on \( V \).
+    \( \in \) is set-like on \( \mathrm{V} \), but \( \ni \) is not set-like on \( \mathrm{V} \).
 \end{example}
 Let \( A \) be a class, and let \( \varphi \) be such that \( A = \qty{x \mid \varphi(x)} \).
 Then \( A^W = \qty{x \mid \varphi^W(x)} \).
 We say that \( A \) is absolute for \( W \) if \( A^W = A \cap W \).
-Viewing a class relation \( R \subseteq V \times V \) as a collection of ordered pairs \( \qty{\langle x, y \rangle \mid \psi(x, y)} \), we have \( R^W = \qty{\langle x, y \rangle \mid \psi^W(x, y)} \), and say that \( R \) is absolute for \( W \) if \( R^W = R \cap W^2 \).
+Viewing a class relation \( R \subseteq \mathrm{V} \times \mathrm{V} \) as a collection of ordered pairs \( \qty{\langle x, y \rangle \mid \psi(x, y)} \), we have \( R^W = \qty{\langle x, y \rangle \mid \psi^W(x, y)} \), and say that \( R \) is absolute for \( W \) if \( R^W = R \cap W^2 \).
 Observe that if \( R \) is a class function, we can only refer to the \emph{function} \( R^W \) if we first check that \( (\forall x.\, \exists! y.\, \varphi(x, y))^W \).
 In this case, we have \( R^W : W \to W \), and we say that \( R \) is an absolute function for \( W \) iff \( R^W = \eval{R}_W \).
 
 We briefly recall the transfinite recursion theorem.
 \begin{theorem}
     Let \( R \) be a relation which is well-founded and set-like on a class \( A \).
-    Let \( F : A \times V \to V \) be a class function.
+    Let \( F : A \times \mathrm{V} \to \mathrm{V} \) be a class function.
     Given \( x \in A \), let \( \operatorname{pred}(A, x, R) = \qty{y \in A \mid y\mathrel{R}x} \) be the set of \( R \)-predecessors of \( x \) in \( A \).
-    Then there is a unique function \( G : A \to V \) such that for all \( x \in A \),
+    Then there is a unique function \( G : A \to \mathrm{V} \) such that for all \( x \in A \),
     \[ G(x) = F\qty(x, \eval{G}_{\operatorname{pred}(A, x, R)}) \]
 \end{theorem}
 We now prove the absoluteness of transfinite recursion.
 \begin{theorem}
     Let \( R \) be a relation which is well-founded and set-like on a class \( A \).
-    Let \( F : A \times V \to V \) be a class function, and let \( G : A \to V \) be the unique function given by applying transfinite recursion to \( F \).
+    Let \( F : A \times \mathrm{V} \to \mathrm{V} \) be a class function, and let \( G : A \to \mathrm{V} \) be the unique function given by applying transfinite recursion to \( F \).
     Suppose that \( W \) is a transitive model of \( \mathsf{ZF} \), and suppose that the following hold.
     \begin{enumerate}
         \item \( A \) and \( F \) are absolute for \( W \);