\documentclass[12pt]{article}
\usepackage{mymacros}

\begin{document}
\title{5.7-5.8}
\author{Andrew Lounsbury}
\date{April 1, 2020}
\maketitle

\section{5.7, p.142}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{enumerate}
\item
	\begin{enumerate}
		\item
		\begin{align*}
			\ulcorner (\fa v_3)(v_3+0 = v_4) \urcorner &= \left<5,\ulcorner v_3\urcorner, \ulcorner v_3+0 = 4 \urcorner\right> \\
			&= \left<5,\left<6\right>,\left<7, \ulcorner v_3+0\urcorner,\ulcorner v_4\urcorner\right>\right> \\
			&= \left<5, 2^7, \left<7, \left<13, \ulcorner v_3 \urcorner, \ulcorner 0 \urcorner\right>, \left<8\right>\right>\right> \\
			&= \left<5, 2^7, \left<7, \left<13, \left<6\right>, \left<9\right>\right>, 2^9\right>\right> \\
			&= \left<5, 2^7, \left<7, \left<13, 2^7, 2^{10}\right>, 2^9\right>\right> \\
			&= 2^5 3^{2^7} 5^{\left[2^7 3^{\left(2^{13} 3^{2^7} 5^{2^{10}}\right)} 5^{2^9}\right]}
		\end{align*}
		
		\item
		\begin{align*}
			\ulcorner SSSS0 \urcorner &= \left<11, \ulcorner SSS0 \urcorner\right> \\
			&= \left<11, \left<11, \ulcorner SS0 \urcorner\right>\right> \\
			&= \left<11, \left<11, \left<11, \ulcorner S0 \urcorner\right>\right>\right> \\
			&= \left<11, \left<11, \left<11, \left<11, \left<9\right>\right>\right>\right>\right> \\
			&= \left<11, \left<11, \left<11, \left<11, 2^9\right>\right>\right>\right> \\
			&= 2^{11} 3^{
						\left[
						2^{11} 3^{
								\left[2^{11} 3^{
												\left[
													2^{11} 3^{2^9}
												\right]
											}
								\right]
								}
						\right]
						}
		\end{align*}
	\end{enumerate}
	
	\item
		\begin{enumerate}
		\item
		\[
			\begin{array}{l}
			2^8 
			3^{[2^{14} 3^{\left(2^{18} 3^9 5^{1025}+1\right)} 5^{\left(2^{18} 3^{33} 5^{1025}+1\right)}+1]}
			5^{[2^{18} 3^{129} 5^{1025}+1]} \\
			\left<7, 2^{14} 3^{\left(2^{18} 3^9 5^{1025}+1\right)}5^{\left(2^{18} 3^{33} 5^{1025}+1\right)}, 2^{18} 3^{129} 5^{1025}\right> \\
			\left<7,\left<13, 2^{18} 3^9 5^{1025}, 2^{18} 3^{33} 5^{1025}\right>, \left<17, 128, 1024\right>\right> \\
			\left<7,\left<13, \left<17, 8, 1024\right>, \left<17, 32, 1024\right>\right>, \left<17, 128, 1024\right>\right> \\
			\left<7,\left<13, \left<17, 2^3, 2^{10}\right>, \left<17, 2^5, 2^{10}\right>\right>, \left<17, 2^7, 2^{10}\right>\right> \\
			\left<7,\left<13, \left<17, \left<2\right>, \left<9\right>\right>, \left<17, \left<4\right>, \left<9\right>\right>\right>, \left<17, \left<6\right>, \left<9\right>\right>\right> \\
			\left<7,\left<13, \left<17, \ulcorner v_1 \urcorner, \ulcorner 0 \urcorner\right>, \left<17, \ulcorner v_2 \urcorner, \ulcorner 0 \urcorner\right>\right>, \left<17, \ulcorner v_3 \urcorner, \ulcorner 0 \urcorner\right>\right> \\
			\left<7, \left<13, \ulcorner Ev_1 0 \urcorner, \ulcorner Ev_2 0 \urcorner\right>, \ulcorner Ev_3 0 \urcorner\right> \\
			\left<7, \ulcorner+ Ev_1 0 Ev_2 0 \urcorner, \ulcorner Ev_3 0 \urcorner\right> \\
			=+ Ev_1 0   Ev_2 0   Ev_3 0 \\
			\end{array}
		\]
		
		\item
		\[
			\begin{array}{l}
				2^2 3^{[2^{20} 3^{1025} 5^{\left(2^{12} 3^{1025}+1\right)}+1]} \\
				\left<1, 2^{20} 3^{1025} 5^{(2^{12} 3^{1025}+1)}\right> \\
				\left<1, \left<19, 1024, 2^{12} 3^{1025}\right>\right> \\
				\left<1, \left<19, 1024, \left<11, 1024\right>\right>\right> \\
				\left<1, \left<19, 1024, \ulcorner Sv_5 \urcorner\right>\right> \\
				\left<1, \ulcorner v_5Sv_5 \urcorner\right> \\
				\neg<v_5Sv_5
			\end{array}
		\]
		
		\item
		\[
			\begin{array}{l}
				2^6 3^9 5^{\left(2^8 3^9 5^9+1\right)} \\
				\left<5, 8, 2^8 3^9 5^9\right> \\
				\left<5, 8, \left<7, 8, 8\right>\right> \\
				\left<5, 8, \left<7, \left<2\right>, \left<2\right>\right>\right> \\
				\left<5, 8, \ulcorner = v_1v_1 \urcorner\right> \\
				(\fa v_1)(= v_1v_1)
			\end{array}
		\]
		
		\end{enumerate}

\end{enumerate}

\newpage

\section{5.8, p.147}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{enumerate}
	\item
	\begin{enumerate}
		\item
		\underline{$Term(\phi)$}: not a formula, the argument for $Term$ must be a (G\"odel) number%of an $\Ell_{NT}$-term
		, not an $\Ell_{NT}$-formula $\phi$
		
		\item
		\underline{$Term(\ulcorner \phi \urcorner)$}: this is a formula
		
		\item
		\underline{$Term(\ol{\ulcorner \phi \urcorner})$}: not a formula, the argument for $Term$ must be a (G\"odel) number%of an $\Ell_{NT}$-term
		, not an $\Ell_{NT}$-formula $\phi$
		\[
			\ol{\ulcorner \phi \urcorner} :\equiv \underbrace{S \cdots S}_{\ulcorner \phi \urcorner \text{ times}}0
		\]
		
	\end{enumerate}

	\item[5.]
	If $a$ is a natural number greater than or equal to 1, then $p_a \le 2^{a^a}$, where $p_a$ is the $a$-th prime number. 
	\begin{proof}
		\underline{Base case}: If $a = 1$, then, $p_a = p_1 = 2 \le 2 = 2^{1^1} = 2^{a^a}$. \\
		\underline{Induction}: Suppose $p_k \le 2^{k^k}$ for some arbitrary natural number $k$. Note that $p_{k+1} \le p_{\min}$, where $p_{\min}$ is the smallest prime factor of $p_1 \cdots p_k-1$. Also, note that $p_1 \cdots p_k = 2p_2 \cdots p_k$ is even, so $p_1 \cdots p_k-1$ is odd. Hence, $p_{k+1} < 3 \le p_{\min}$. We know $p_{k+1} < 3$ because we would otherwise have $3 \le p_{k+1} < p_{\min}$, contradicting $p_{k+1} \le p_{\min}$. Then, $p_{k+1} < 3 < 2^{2^2} \le 2^{(k+1)^{(k+1)}}$, 
		as desired. 
	\end{proof}
\end{enumerate}
\end{document}