\documentclass[12pt]{article}
 \usepackage[margin=1in]{geometry} 
\usepackage{amsmath,amsthm,amssymb,amsfonts}
 
 \newtheorem*{lt}{\L o\'{s} Test}
  \newtheorem*{theorem}{Theorem}

 

\newcommand{\bN}{\mathbb{N}}
\newcommand{\bQ}{\mathbb{Q}}
\newcommand{\bR}{\mathbb{R}}
\newcommand{\bZ}{\mathbb{Z}}

\newcommand{\cC}{\mathcal{C}}
\newcommand{\cP}{\mathcal{P}}

\newcommand{\bx}{\bold{x}}
\newcommand{\by}{\bold{y}}
\newcommand{\bz}{\bold{z}}

\newcommand{\id}{\text{I}}
 
\newenvironment{problem}[2][Problem]{\begin{trivlist}
\item[\hskip \labelsep {\bfseries #1}\hskip \labelsep {\bfseries #2.}]}{\end{trivlist}}
%If you want to title your bold things something different just make another thing exactly like this but replace "problem" with the name of the thing you want, like theorem or lemma or whatever
 \date{}
\begin{document}
 
%\renewcommand{\qedsymbol}{\filledbox}
%Good resources for looking up how to do stuff:
%Binary operators: http://www.access2science.com/latex/Binary.html
%General help: http://en.wikibooks.org/wiki/LaTeX/Mathematics
%Or just google stuff
 
\title{Math 141b Problem Set 5}
\author{Due March 5, 2019}

\maketitle
 
Choose four of the following to do.  
 
\begin{enumerate}
	\item We typically use the phrase `G\"{o}del sentence' to refer to a sentence as constructed in the proof of first incompleteness theorem, that is, a fixed point of the negation of the provability predicates for some nice coding.  They are unprovable, but are they true? (True means `true in $\bN$,' assuming the consistency of $PA$ and that $\bN$ satisfies it.)
	\item I mentioned this in class, but you prove it.  Using the second incompleteness theorem, find a consistent but $\omega$-inconsistent theory (assuming the consistency of $PA$).
	\item In developing primitive recursive functions, we wanted there to be a function that was big enough to witness $*$ and many other functions as bounded leastness.  Let's make that precise here.  Find a primitive recursive function $big$ such that we always have $m*n \leq big(m+n)$.
	\item In Goldfarb's notes (under Course Information, Textbook on my website), he proves the fixed point lemma in \S 3.1.  He then informally discusses how to generate inequivalent fixed points for the same predicate.  Formalize this to show: for any formula $\phi(x)$ in the language of arithmetic, there are inequivalent $\psi, \psi'$ that are both fixed points of $\phi$.
	\item Let $\phi$ be a sentence and $Prv$ be a standard provability predicate.  Define $\psi_n$ by $\psi_0 = \phi$ and $\psi_{n+1} = Prv(\lceil \psi_n \rceil)$.  Show that if there are $n<k$ such that $PA \vdash` \psi_k \to \psi_n'$, then $PA \vdash \phi$.
	\item In much of the development of the primitive recursive predicates, we assumed that we were plugging in certain types of numbers (sequence numbers) without explicitly requiring it.  For instance, we know what $m*n$ is if both $m$ and $n$ are sequence numbers.  What does the $*$ operation do if one or both of the inputs are not sequence numbers?
	\item Show* that a Rosser provability predicate is not a standard provability predicate.\\
	
	* This is something that Goldfarb's notes mention.  However, I wasn't able to prove it in my playing around with it.  So I give this on a problem set where you can choose which problems to do as a statement I'm pretty sure is true, but that I might have misread.
\end{enumerate}

\end{document}

