\documentclass[12pt]{amsart}
\usepackage{amsmath, amsthm, amssymb, amsfonts}
\usepackage{enumerate}
\usepackage{hyperref}
\usepackage{verbatim}
%\numberwithin{equation}{section}

%%%Document Configuration
\pagestyle{headings}
%\addtolength{\topmargin}{-.5in}
\textwidth = 6in 
\oddsidemargin = .25in
\evensidemargin = .25in
\voffset = -1in
\textheight = 9.5 in
%\textwidth = 6in
%\parindent = 0in
%\headsep = 0in
\relpenalty = 9999
\binoppenalty = 9999
%linespacing
\renewcommand{\baselinestretch}{1.25}
\reversemarginpar     
%%%

%%%Theorem Configuration
\theoremstyle{plain}
\newtheorem*{main}{Main~Theorem}
\newtheorem{thm}{Theorem}[section]
\newtheorem*{thm*}{Theorem}
\newtheorem*{claim*}{Claim}
\newtheorem{cor}[thm]{Corollary}
\newtheorem*{cor*}{Corollary}
\newtheorem*{conj*}{Conjecture}
\newtheorem{exer}[thm]{Exercise}
\newtheorem{fact}[thm]{Fact}
\newtheorem{lem}[thm]{Lemma}
\newtheorem*{lem*}{Lemma}
\newtheorem{prop}[thm]{Proposition}
\newtheorem*{prob*}{Problem}
\newtheorem{remark}[thm]{Remark}
\newtheorem*{remark*}{Remark}
\newtheorem{hw}[section]{}
%\newtheorem{hw}[section]{HW}
\newtheorem{dfn}{Definition}[section]
\newtheorem*{dfn*}{Definition}
\newtheorem*{eg*}{Example}
%%%

%%%semantic definitions
\DeclareMathOperator*{\Aut}{Aut}
\DeclareMathOperator*{\Con}{Con}
\DeclareMathOperator*{\Dom}{Dom}
%\DeclareMathOperator*{\Layer}{Layer}
\DeclareMathOperator{\im}{Im}
\DeclareMathOperator*{\Mod}{Mod}
\DeclareMathOperator*{\str}{str}
\DeclareMathOperator*{\Th}{Th}
\DeclareMathOperator*{\tp}{tp}
\DeclareMathOperator*{\ZFC}{ZFC}
\renewcommand{\div}{\mid}
\renewcommand{\emptyset}{\varnothing}
\renewcommand{\implies}{\Rightarrow}
\renewcommand{\natural}{\mathbb{N}}
\newcommand{\Acl}[1]{\obar{#1}}
\newcommand{\assign}{\leftarrow}
\newcommand{\Exists}{\Huge \exists}
\newcommand{\caseif}{\Rightarrow}
\newcommand{\caseonlyif}{\Leftarrow}
\newcommand{\cantprove}{\nvdash}
\newcommand{\ceil}[1]{\left\lceil{#1}\right\rceil}
\newcommand{\complex}{\mathbb{C}}
\newcommand{\field}{\mathbb{F}}
\newcommand{\floor}[1]{\left\lfloor{#1}\right\rfloor}
\newcommand{\minus}{\setminus}
\newcommand{\Layer}{\text{Layer}}
\newcommand{\power}[1]{{\mathcal{P}}({#1})}
\newcommand{\nonnegative}{\mathbb{N}}
%\newcommand{\index}[3]{_{#1 = #2}^{#3}} %old style, general
%\newcommand{\index}[3]{_{#1}^{#3}} %ordinal style from 0
%\newcommand{\indexz}[2]{_{#1 = 0}^{#2 - 1}} %old style, 0 to #2-1
%\newcommand{\indexz}[2]{For #1 from 0 to #2-1}} %pseudocode, 0 to #2-1
\newcommand{\indexz}[2]{_{#1 \in #2}} %ordinal style, 0 to #2-1
\newcommand{\integer}{\mathbb{Z}}
\newcommand{\intersect}{\cap}
\newcommand{\isomorphic}{\simeq}
\newcommand{\obar}[1]{\overline{#1}}
\newcommand{\proves}{\vdash}
\newcommand{\rational}{\mathbb{Q}}
\newcommand{\real}{\mathbb{R}}
\newcommand{\sst}{{\big|}} %not semantic, but used for \set, \setBig
\newcommand{\sstBig}{{\Big|}}
\newcommand{\set}[2]{\left\{#1 \sst #2 \right\}}
\newcommand{\setl}[2]{\left.\left\{#1 \right| #2 \right\}}
\newcommand{\setr}[2]{\left\{#1 \left| #2 \right\}\right.}
\newcommand{\setBig}[2]{\left\{#1 \sstBig #2 \right\}}
\newcommand{\union}{\cup}
\newcommand{\Union}{\bigcup}
\newcommand{\units}[1]{{\left(#1\right)}^{\times}}
%%%

%%%local definitions
\newcommand{\degin}{d^-}
\newcommand{\degout}{d^+}
\newcommand{\eleq}{\equiv}
\newcommand{\elleq}{\preccurlyeq}
\newcommand{\eqand}{\hspace{1pc}\text{and}\hspace{1pc}}
\newcommand{\gtlex}{\displaystyle \mathop{>}_{lex}}
\newcommand{\ltlex}{\displaystyle \mathop{<}_{lex}}
\newcommand{\Hy}{\eta}
\newcommand{\srj}{\hat{\rho}}
\newcommand{\srl}{\check{\rho}}
\newcommand{\lang}[1]{{\mathcal{#1}}}
\newcommand{\Los}{{\L o\'s}}
\newcommand{\LS}{{L\"{o}wenheim-Skolem }}
\newcommand{\lsh}{\texttt{<<}}
\newcommand{\rsh}{\texttt{>>}}
\newcommand{\mathscr}[1]{{\mathcal{#1}}}
\newcommand{\monster}{{\mathbb{M}}}
\newcommand{\ndiv}{\nmid}
\newcommand{\pam}{p_{A,M}(n)}
\newcommand{\pve}{pve}
\newcommand{\pvp}{pvp}
\newcommand{\pvr}{pvr}
\newcommand{\pvrf}{pvrf}
\newcommand{\st}[1]{{\mathcal{#1}}}
\newcommand{\structure}[1]{{\mathcal{#1}}}
\newcommand{\struct}[1]{\left\langle#1\right\rangle}
\newcommand{\subst}{\prec}
\newcommand{\symAnd}{\mathop{\bigwedge}}
\newcommand{\symand}{\wedge}
\newcommand{\symimply}{\rightarrow}
\newcommand{\symiff}{\leftrightarrow}
\newcommand{\symnot}{\neg}
\newcommand{\symor}{\vee}
\newcommand{\tuple}[1]{\obar{#1}}
\newcommand{\Tfcp}{T_E^{\text{fcp}}}
\newcommand{\WFF}{well-formed formula}
\newcommand{\zonein}[1]{Z^-_{#1}}
\newcommand{\zoneout}[1]{Z^+_{#1}}
\newcommand{\0}{\textbf{0}}
\newcommand{\suc}{\textbf{S}}
\newcommand{\A}{\mathfrak{A}}
\newcommand{\B}{\mathfrak{B}}
\newcommand{\D}{\mathcal{D}}
\newcommand{\F}{\mathcal{F}}
\newcommand{\NNN}{\mathfrak{N}}
\newcommand{\E}{\textbf{E}}
\newcommand{\Cn}{\textrm{Cn}}
\newcommand{\res}{\upharpoonright}
\renewcommand{\P}{{Pl\"{u}nnecke }}
%%%

%%%marginpars
\setlength{\marginparwidth}{1 in}
\let\oldmarginpar\marginpar
\renewcommand\marginpar[1]{\-\oldmarginpar[\raggedleft\footnotesize #1]%
{\raggedright\footnotesize #1}}

\begin{document}

\title{Josiah's Exercise on shallow models of ZFC}
\author{Dakota Blair}
\begin{abstract}
\end{abstract}
\maketitle

\section*{Notation}

\section*{Main}
\begin{exer}
Show that in models of
$T = \ZFC \symand \Con \ZFC \symand \symnot\Con(\ZFC \symand \Con \ZFC)$
existence proofs are contradictory.
\end{exer}

\begin{proof}
Consider a model of $T$.
By the completeness theorem, for any $\varphi$
\[
T \proves \varphi \iff T \models \varphi
\]

\end{proof}

\end{document}

\begin{dfn*}[]
\end{dfn*}

\begin{eg*}
\end{eg*}

\begin{thm*}
\end{thm*}

\begin{proof}
\end{proof}
