
% MAGNIFICATION
\magnification=\magstep4
\font\bigrm=cmr7 scaled \magstep4

%PDF
% http://insti.physics.sunysb.edu/~siegel/tex.shmtl

\def\rgboo#1{\pdfliteral{#1 rg #1 RG}}
\def\rgbo#1#2{\rgboo{#1}#2\rgboo{0 0 0}}
%\def\rgb#1#2{\mark{#1}\rgbo{#1}{#2}\mark{0 0 0}}

\def\yy{\catcode`/=12\catcode`~=12\catcode`\#=12\relax}
\def\zz{\catcode`/=\active\catcode`~=13\catcode`\#=6\relax}
\def\pdfklink#1#2{%
	\noindent\pdfstartlink user
		{/Subtype /Link
		/Border [ 0 0 0 ]
		/A << /S /URI /URI (#2) >>}{\rgbo{0 0 1}{#1}}%
	\pdfendlink
	}

\def\pdflink#1{\pdfklink{#1}{\eighttt #1}}

\def\image#1{\immediate\pdfximage{#1}
	\centerline{\hbox{\pdfrefximage \pdflastximage}}}

% QEA MACROS
\def\ul{\hbox{\tenmsa\char"70}}
\def\ur{\hbox{\tenmsa\char"71}}
\def\umlaut#1{\accent "7F #1}
\let\doublequote="
\catcode`"=13
\def"{}
\let\slash=/
\catcode`/=13
\def/{}
\def\a #1 #2"{\medbreak\par\noindent#1 {\it Ax.}\quad$#2$}
\def\t #1 #2"{\medbreak\par\noindent#1 {\it Th.}\quad$#2$}
\def\d #1 #2"{\medbreak\par\noindent#1 {\it Df.}\quad$#2$}
\def\fo #1 #2"{\medbreak\par\noindent#1 {\it Df.}\quad$#2$}
\def\fe #1 #2"{\medbreak\par\noindent#1 {\it Df.}\quad$#2$}
\def\pd #1 #2"{\medbreak\par\noindent#1 {\it Df.}\quad$#2$}
\def\p #1 #2"{\medskip\par{\ninepoint{\quad$#2$}}}
\def\XXX #1"{}
%\def\G{}
%\def\H{}
%\def\I{}
\def\n #1 #2 NEW #3"{$#2$}
\newif\ifproof
%\def\p #1 #2"{\ifdim\lastskip<\medskipamount\removelastskip\penalty3000\smallskip\fi\begingroup\prooftrue\binoppenalty=1000\baselineskip=11pt\scriptfont0=\ninerm\scriptfont1=\ninei\scriptfont2=\ninesy\scriptscriptfont0=\sixrm\scriptscriptfont1=\sixi\scriptscriptfont2=\sixsy\ninerm\par$\scriptstyle #2\!\!\!.$\par\endgroup\prooffalse}
\def\pf#1.#2"{\ifdim\lastskip<\bigskipamount\removelastskip\penalty3000\smallskip\fi\begingroup\prooftrue\binoppenalty=1000\baselineskip=11pt\scriptfont0=\ninerm\scriptfont1=\ninei\scriptfont2=\ninesy\scriptscriptfont0=\sixrm\scriptscriptfont1=\sixi\scriptscriptfont2=\sixsy\ninerm\par$\scriptstyle #2$\par\endgroup\prooffalse}
\def\\{\allowbreak\mskip 8mu plus 16mu minus 4mu}
\let\semicolon=;
\catcode`;=\active
%\def;{\ifmmode\semicolon\penalty1000\mskip.1mu\penalty1000\relax\else\semicolon\fi}
\def;{\ifmmode{\semicolon}\else\semicolon\fi}
\let\colon=:
\catcode`:=\active
\def:{{\colon}}
\let\comma=,
\catcode`,=\active
\def,{\ifmmode\comma\penalty8000\relax\else\comma\fi}
\def\sslash{$\scriptstyle\slash$}
\def\tild{$\scriptstyle\sim$}
\let\acute=\'
\def\'#1'{{}$#1${}}
\def\thm{\hbox{\it thm}}
\def\(#1,{_{#1}(}
%\let\dollar=\$
%\def\$#1:{}
\let\lowbar=\_
%\def\_{\lowbar\hskip1pt\discretionary{}{}{}}
\def\_{\allowbreak\ }
\def\iff{\allowbreak\hskip8pt plus2pt minus3pt\mathrel{\hbox{$\leftrightarrow$}}\hskip8pt plus2pt minus3pt}
\def\iffF{\allowbreak\leftrightarrow}
\def\imp{\allowbreak\hskip8pt plus2pt minus3pt\mathrel{\hbox{$\rightarrow$}}\hskip8pt plus2pt minus3pt}
\def\impP{\allowbreak\rightarrow}
\def\andD{\allowbreak\mathrel{\hskip1pt\&\hskip1pt}}
\def\and{\allowbreak\hskip7pt plus2pt minus3pt\mathrel{\&}\hskip7pt plus2pt minus3pt}
\def\AND{\allowbreak\hskip7pt plus2pt minus3pt\&\break}
%\def\and{\allowbreak\mskip7mu plus2mu minus3mu\mathrel{\&}\mskip7mu plus2mu minus3mu}
\def\orR{\allowbreak\kern1pt\lor\kern1.25pt}
\def\or{\allowbreak\hskip7pt plus2pt minus3pt\mathrel{\hbox{$\vee$}}\hskip7pt plus2pt minus3pt}
\def\OR{\allowbreak\hskip7pt plus2pt minus3pt{\hbox{$\vee$}}\break}
\def\leE{{\scriptstyle\le}}
\def\\{{\scriptstyle\le}}
\def\ltT{{\scriptstyle<}}
\def\inN{{\scriptstyle\in}}
\def\EC{{\rm EC}}
\def\UC{{\rm UC}}
\let\graveaccent=\`
\def\`#1{(.#1)}
\let\dotaccent=\.
\def\.{\cdot}
\def\:#1:#2:#3:#4:#5:#6:#7:{#1\{\,#4#5#6\allowbreak\,\colon\allowbreak\,#7\,\}}
\def\?#1;#2;#3;#4;#5;#6;#7;{\{\,\langle#3,#4\rangle\,\colon\,#3\in#5\and#6\and#7\,\}}
\def\@#1;#2;#3;#4;#5;{\{\,\langle#3,#4\rangle\allowbreak\,\colon\,#3\in#5\,\}}

% FONTS
%\font\bigrm=cmr7 scaled \magstep4
\font\tenmsa=msam10 
\font\eightmsa=msam8 
\font\bbbold=msbm10
\def\bbb#1{\hbox{\bbbold#1}}
\font\ninerm=cmr9
\font\ninebf=cmbx9
\font\nineit=cmti9
\font\ninei=cmmi9
\font\eighti=cmmi8
\font\eightrm=cmr8
\font\eightbf=cmbx8
\font\eightit=cmti8
\font\eightsl=cmsl8
\font\eighttt=cmtt8
\font\eightsy=cmsy8
\font\tenss=cmss10
\font\ninesy=cmsy9
\font\eightsy=cmsy8
\font\nineit=cmti9
\font\eightit=cmti8
\font\sixrm=cmr6
\font\sixbf=cmbx6
\font\sixi=cmmi6
\font\sixsy=cmsy6
\font\sans=cmss10
\font\ninesans=cmss9
\font\eightsans=cmss8
\font\sansit=cmssi10
\def\ninepoint{\def\rm{\fam0\ninerm}%
   \textfont0=\ninerm \scriptfont0=\sixrm \scriptscriptfont0=\fiverm
   \textfont1=\ninei \scriptfont1=\sixi \scriptscriptfont1=\fivei
   \textfont2=\ninesy \scriptfont2=\sixsy \scriptscriptfont2=\fivesy
   \textfont3=\tenex \scriptfont3=\tenex \scriptscriptfont3=\tenex
   \textfont\itfam=\nineit \def\it{\fam\itfam\nineit}%
   \textfont\bffam=\ninebf \scriptfont\bffam=\sixbf
    \scriptscriptfont\bffam=\fivebf \def\bf{\fam\bffam\ninebf}%
   \normalbaselineskip=11pt
   \setbox\strutbox=\hbox{\vrule height8pt depth 3pt width0pt}%
   \let\big=\ninebig \normalbaselines\rm}
\def\eightpoint{\def\rm{\fam0\eightrm}%
   \textfont0=\eightrm \scriptfont0=\sixrm \scriptscriptfont0=\fiverm
   \textfont1=\eighti \scriptfont1=\sixi \scriptscriptfont1=\fivei
   \textfont2=\eightsy \scriptfont2=\sixsy \scriptscriptfont2=\fivesy
   \textfont3=\tenex \scriptfont3=\tenex \scriptscriptfont3=\tenex
   \textfont\itfam=\eightit \def\it{\fam\itfam\eightit}%
   \textfont\bffam=\eightbf \scriptfont\bffam=\sixbf
    \scriptscriptfont\bffam=\fivebf \def\bf{\fam\bffam\eightbf}%
   \normalbaselineskip=11pt
   \setbox\strutbox=\hbox{\vrule height8pt depth 3pt width0pt}%
   \let\big=\eightbig \normalbaselines\rm}
\catcode`@=11
\def\ninebig#1{{\hbox{$\textfont0=\tenrm\textfont2=\tensy
  \left#1\vbox to7.25pt{}\right.\n@space$}}}
\catcode`@=12
\let\Smallskip=\smallskip
\def\SMALL{\ninepoint\def\medskip{}\def\Bigbreak{\Smallskip}\def\smallskip{}}

% MAGNIFICATION
%\magnification=\magstep1

% REGISTERS
\newcount\firstpage
\newcount\footno
\newcount\secno
\newtoks\chaptername
\newtoks\sectionname
\newwrite\raw
\newwrite\tabcon
\newif\ifindexmode

% FORMATING
\predisplaypenalty=0
\def\foot#1{\global\advance\footno by 1
  {\baselineskip=9pt 
	\frenchspacing
    \setbox\strutbox=\hbox{\vrule height7pt depth2pt width0pt}%
	\def\textindent##1{\indent\llap{##1}}%
	\def\sl{\eightsl}\def\bf{\eightbf}\def\rm{\eightrm}%
	\def\it{\eightit}\def\tt{\eighttt}%
	\eightrm\footnote{$^{\hbox{{\eightrm\the\footno}}}$}{#1}}}
\def\footnoterule{\kern-3pt \hrule width 2truein height 0pt}
%\hsize=11cm
%\vsize=17.5cm 
%\voffset=2\baselineskip
%\hoffset=1.7truecm
%\headline={\Headline}
%\footline={\Footline}
%\def\Headline{\ifnum\firstpage=\pageno \hfil \else\ifodd\pageno%
   %\righthead\else\lefthead\fi\fi}
%\def\Footline{\ifnum\firstpage=\pageno \hss\tenrm\folio\hss \else{}\fi}
%\newif\ifrighthead
%\def\lefthead{\tenrm\folio\hfil{\eightrm CHAPTER \chapno.\ \ \uppercase\expandafter{\the\chaptername}}\hfil}
%\def\righthead{\ifrighthead\hfil{\eightrm{\chapno.\botmark}}%
   %\hfil\tenrm\folio\else\lefthead\fi}
%\let\chapno=0
%\def\chap#1.#2{\chaptername={#2} \firstpage=\pageno 
    %\footno=0 \def\chapno{#1}
	%\secno=0
   %\hrule width0pt depth1.5cm
   %\centerline{\tenrm CHAPTER\ #1}\vskip .45cm
   %\centerline{\bigrm #2}\vskip 1cm \ifindexmode\write\tabcon%
   %{#1\  #2 \the\count0}\fi}
%\def\section#1{\rightheadtrue\def\sectionname{\eightrm\uppercase{#1}}\global\advance\secno by 1\bigbreak\noindent{\bf\the\secno.\  #1}\mark{\the\secno\ \ \sectionname}\medskip%
   %\ifindexmode\write\tabcon{#1 \the\count0}\fi\nobreak}
%\def\footnoterule{}
%\skip\footins=\medskipamount
%\def\poetry{\smallbreak\parindent=40pt \baselineskip=11pt
  %\setbox\strutbox=\hbox{\vrule height8pt depth3pt width 0pt}%
   %%\obeylines\ninerm}% LEAVE BLANK LINE AND TYPE {\poetry <poem>
%                                                                 }
%\def\endchap{\ifodd\pageno\vfill\supereject\headline={\hfil}\eject\line{}\vfil\eject\else\vfill\supereject\fi\headline={\Headline}\rightheadfalse\secno=0\footno=0}
%\def\endchap{\vfill\eject\secno=0}

% INDEXING
\def\ind#1{\ifindexmode\write\raw{#1, \the\count0 }#1\else#1\fi}
\def\sind#1{\ifindexmode\write\raw{#1, \the\count0 }\fi}
\def\ii#1.{\ifindexmode\write\raw{#1, \the\count0 }{\it#1}%
   \else{\it#1}\fi}
\def\b[#1]{\sind{#1]}[#1]}

% TEXT MACROS
\def\Lseq#1.#2{$\rm#1_1$,~\dots,~$\rm#1_#2$}
\def\secsign{\mathhexbox 278}
\def\pmb#1{\setbox0=\hbox{#1}\kern-.025em\copy0\kern-\wd0 \kern.05em\copy0\kern-\wd0 \kern-.025em\raise.0433em\box0 }
\def\SMASH{{\pmb{$\;\Smash$}}}
\def\smasH{{$\scriptstyle\Smash$}}
\long\def\Omit#1{}

% TEXT OR MATH MACROS
\def\ss{\hbox{{\rm S}}}
\def\sb{$\hbox{\sans S}^{\hbox{\eightsans b}}$}
\def\su{$\hbox{\sans S}^{\hbox{\eightsans u}}$}
\def\smallss{\hbox{{\eightsans S}}}
\def\smalltt{\hbox{{\eightsans T}}}
\def\smallssz{\hbox{{\eightsans S}}^0}
\def\vdss{\vdash_{\rm SS}}
\def\vdsb{\vdash_{{\smallss}^{\hbox{\eightsans b}}}}
\def\vT{\vdash_{\ro T}}
%\def\vS{\vdash_{\ro S}}
%\def\vSS{\vdash_{\rm SS}}
%\def\vSp{\vdash_{\ro S}'}
\def\vTp{\vdash_{\ro T'}}
\def\vdsss{\vdash_{\smallss^*}}
\def\vdssz{\vdash_{\smallss^0}}
\def\ssb{\hbox{$\overline{\ss}$}}
\def\ssbz{\hbox{$\overline{\ss}\,^0$}}
\def\sss{\hbox{$\ss^*$}}
\def\ssz{\hbox{$\ss^0$}}
\def\ssl{\hbox{$\ss^l$}}
\def\SS{\hbox{$\cal S$}}
\def\EE{\hbox{$\cal E$}}
\def\sso{\hbox{$\ss^\omega$}}
\def\qo{$\hbox{\sans Q}_0$}
\def\qob{$\overline{\hbox{\sans Q}}_0$}
\def\so{$\hbox{\sans S}_0$}
\def\sh#1{[Sh,~\S#1]}
\def\phiI{\phi^{\phantom\prime}_{\ro I}}
\def\down{^{\phantom\prime}}
\def\phip{\phi^+}
\def\cite#1{[{\ninerm PA~Ch.~#1}]}
\let\phi=\varphi
\def\N{\hbox{\bbb N}}
\def\Z{\hbox{\bbb Z}}
\def\bbS{\hbox{\bbb S}}
\let\hyphen=\-
\def\-{\relax\hyphen}
\def\cseq#1#2#3{#1_1#2\cdots#2#1_#3}
\def\lseq#1#2#3{#1_1#2\ldots#2#1_#3}
\def\ro#1{{\rm #1}}
\def\T{\hbox{\sans T}}
\def\F{\hbox{\sans F}}
\def\UU{\hbox{$\rm U_I$}}
\def\I{{\rm I}}
\def\PP{{\tenss P}}
\def\EBA{{\tenss EBA}}

\def\ti{\hbox{$\rm T\hskip1pt^\omega$}}
\def\len#1{|#1|}
\def\vti{\vdash_{\ro T^\omega}}
\def\bul{\hfill\hbox{\tenmsa\char3}}
\def\bull{\hfill\hbox{$\circ$}}
\def\endproof{\hbox{\tenmsa\char3}}
\def\tl{\hbox{$\rm T^\lambda$}}
\def\tlm{\hbox{$\rm T^{\lambda-1}$}}
\def\vtl{\vdash_{\ro T^\lambda}}
\def\vtz{\vdash_{\ro T^0}}
\def\vsz{\vdash_{\smallss^0}}
\def\vtlp{\vdash_{\ro T^{\lambda+1}}}
\def\Th{\medskip\par T{\eightrm HEOREM}}
\def\TH{Theorem}
\def\ds{\displaystyle}
\def\ax{{\it Ax. \quad }}
\def\df#1 {\medskip\par\noindent #1 {\it Def.\quad}}
\def\th#1 {\medskip\par\noindent #1 {\it Thm.\quad}}
\def\ax#1 {\medskip\par\noindent #1 {\it Ax.\quad}}
\def\med#1.#2\par{\smallskip\par\noindent #1.\quad$#2$\par}
\def\pz{\phantom0}
\def\dff{{\it Def}.\ }
\def\pf{\par\medskip\leavevmode\hbox{\it Proof. }}
\def\pff{\par\medskip\leavevmode\hbox{\it Pf. }}
\def\noin{\medskip\par\noindent}
%\def\noi#1.{\medskip\par\noindent$(#1)$\qquad}
\def\nn#1.{$(#1)$}
\def\noj{\medskip\par\quad}
\def\nok// #1.{\par\medskip\par\noindent(#1)\quad}
\def\NOK/ #1.{\par\medskip\par\noindent(#1)\quad}
\def\qd{\medskip\par\qquad}
%\def\opP{\oplus}
%\def\op{}
\def\op{{.}}
%\def\op{\oplus}
\def\ep{\epsilon}
\def\vep{\varepsilon}
\def\vepz{\varepsilon_0}
\def\vepl{\varepsilon_\lambda}
\def\veplo{\varepsilon_{\lambda+1}}
\def\veple{\varepsilon_\lambda^\od}
\def\od{\odot}
\def\pr{\preceq}
\def\heq{\mathrel{\hat=}}
\def\hpp{{\hat{\scriptstyle\preceq}}}
\def\hpr{\mathrel{\hat\preceq}}
\def\hP{\hbox{\rm\^P}}
\def\hop{\mathbin{\hat\oplus}}
\def\hod{\mathbin{\hat\odot}}
\def\hep{\hat\ep}
\def\hz{\hat{\0}}
\def\ho{\hat{\1}}
\def\hor{\hat\vee}
\def\hneg{\hat\neg}
%\def\phic{\ro C}
\def\phiz{{\phi^0}}
\def\phio{{\phi^1}}
\def\phit{{\phi^2}}
\def\phie{{\phi^3}}
\def\phif{{\phi^4}}
%\def\zphi{{^0\phi}}
%\def\ophi{{^1\phi}}
%\def\tphi{{^2\phi}}
\def\zphi{\phi^{(0)}}
\def\ophi{\phi^{(1)}}
\def\tphi{\phi^{(2)}}
\def\tvep{^2\vep}
%\def\phio{\phi^{\scriptscriptstyle\pr}}
%\def\phiw{\phi^{\textstyle\op}}
%\def\phie{{\phi^{\scriptscriptstyle\od}}}
%\def\pp{{\scriptstyle\preceq}}
%\def\arith#1.{\ul{\rm#1}\ur}
\def\vdashh{\vdash^\star}
\def\uu{^\#}
\def\true{\hbox{true}}

\def\evft{encodes a variable-free term}
\def\ecf{encodes a closed formula}
\def\eti{encodes a true inequality}
\def\ete{encodes a true equality}
\def\etaf{encodes a true atomic formula}
\def\etvff{encodes a true variable-free formula}
\def\easo{encodes an atomic subformula of }
\def\evff{encodes a variable-free formula}
\def\etof{encodes a true open formula}
\def\evff{encodes a variable-free formula}

\def\tg{$\Theta_\gamma$}
\def\tgo{$\Theta_{\gamma+1}$}
\def\tgobb{$\Theta_{\gamma+1}(b)$}
\def\tgb{$\rm\Theta_\gamma(b)$}
\def\tgbb{$\Theta_\gamma(b)$}
\def\sg{$\Sigma_\gamma$}
\def\sgo{$\Sigma_{\gamma+1}$}
\def\sgobb{$\Sigma_{\gamma+1}(b)$}
\def\sgb{$\rm\Sigma_\gamma(b)$}
\def\sgbb{$\Sigma_\gamma(b)$}

\def\si{\hbox{\it string-ind }}
\def\ffor{\hbox{\quad for \quad}}
%\def\GG{$\rm\ul G\ur$}
\long\def\omit#1{}

%REFERENCING

\def\R#1.{\medskip\par\noindent(#1)\qquad}
\def\r#1.{(#1)}

%NEW

\def\stars{\centerline{$*$\qquad$*$\qquad$*$}}
\def\truel{\hbox{true}_\lambda}
\def\pfz{\hbox{proof}_0}
\let\Norm=\|
\def\norm#1{\Norm#1\Norm}
\def\|{{\scriptstyle\pr}}
\def\for{\quad\hbox{for}\quad}
\def\un{^{\hbox{\eightsl u}}}
\def\qdd{\par\qquad}
\def\Ref/#1.{#1}
\def\0{\hbox{\eighttt0}}
\def\1{\hbox{\eighttt1}}
\def\l{\hbox{\eighttt<}}
\def\r{\hbox{\eighttt>}}
\def\sep{\hbox{\eighttt;}}
\def\fff{\hbox{\eighttt f}}
\def\ppp{\hbox{\eighttt p}}
\def\ccc{\hbox{\eighttt c}}
%\def\ssep{\hbox{\eighttt|}}
%\def\blank{\hbox{$\scriptscriptstyle\sqcup$}}
\def\ll{\hbox{$\scriptstyle\triangleleft$}}
\def\rr{\hbox{$\scriptstyle\triangleright$}}
\def\valids#1{\leavevmode$\vdash_{\rm SS}\!\[#1\]$}
\def\oth{,\allowbreak\ {\rm otherwise}\allowbreak\ }
%\def\t/#1.#2\par{\medbreak\par\noindent#1.\hbox{\it\ Th.}\quad$#2 $.\smallskip\par}
\def\Name{{\star}}
\def\QQ#1{\langle#1\hskip.1pt\rangle}
\def\valid#1{\leavevmode\hbox{\tenmsa\char15$\big\{$}#1\hbox{$\big\}$}}
\def\rlab#1{}
\let\eqnu=\eqno
\def\omegab{\bar\omega}
\def\db{{\bar\downarrow}}
%\def\ari#1{\ul{\hskip.2pt\rm#1\hskip.2pt}\ur}
\def\ari#1{\ul{\hskip.2pt#1\hskip.2pt}\ur}
\def\aari#1{\vphantom|^{\scriptscriptstyle\lbrace}{\hskip.2pt\rm#1\hskip.2pt}\vphantom|^{\scriptscriptstyle\rbrace}}
\def\bari#1{\vphantom{.}^{\scriptscriptstyle\{}{\hskip.2pt\hbox{$#1$}\hskip.2pt}\vphantom{.}^{\scriptscriptstyle\}}}
%\def\Ari#1{\sigma'\big(\ul{\hskip.4pt\rm#1\hskip.4pt}\ur\big)}
\def\da{{\downarrow}}
\def\opt{\mathbin{\tilde\op}}
\def\odt{\mathbin{\tilde\od}}
\def\Pt{\tilde{\ro P}}
\def\prt{\mathrel{\tilde\pr}}
\def\eqt{\mathrel{\tilde=}}
\def\negt{\tilde{\neg}}
\def\ort{\mathrel{\tilde\vee}}
\def\impt{\mathrel{\tilde\rightarrow}}
\def\ifft{\mathrel{\tilde\leftrightarrow}}
\def\andt{\mathrel{\hskip1pt\tilde\&\hskip1pt}}
\def\existst{\tilde{\exists}}
\def\forallt{\tilde{\forall}}
\def\Pb{\bar{\ro P}}
\def\ze{\mathbin{\uparrow}}
\def\name{\star}
\def\bd{^{\hbox{\eightsl bd}}}
\def\btr{^{\hbox{\eightsl btr}}}
\def\tr{^{\hbox{\eightsl tr}}}
\def\TR{{\hbox{\eightsl tr}}}
\def\bsi{^{\hbox{\eightsl bsi}}}
\def\model{\hbox{$\cal A$}}
\def\DD{\hbox{$\cal D$}}
\def\G{\hbox{$\cal G$}}
\def\AA{\hbox{$\cal A$}}
\def\ssc{$\ss^\circ$}
\def\vdtt{\vdash_{\smalltt}}
\def\be{\hbox{\quad be\quad}}
\def\Let{\hbox{\quad let\quad}}
\def\dt{\hbox{$\rm\Delta(T)$}}
\def\dtt{\hbox{$\rm\tilde\Delta(T)$}}
\def\tc{\hbox{$\rm T_c$}}
\def\tcp{\hbox{$\rm T_c'$}}

%\let\negg=\neg
%\def\neg{\negg\;}
\let\lbracket=[
\catcode`[=\active
\def[{\ifmmode\allowbreak\,\lbracket\,\else\lbracket\fi}
\let\rbracket=]
\catcode`]=\active
\def]{\ifmmode\,\rbracket\else\rbracket\fi}
\def\[{\allowbreak\,\big\lbracket\,}
\def\]{\big\rbracket}
\def\[{\,\big\lbracket\,}
\let\lbrace=\{
\let\rbrace=\}
\def\{{\allowbreak\,\lbrace\,} %}
\def\lBrace{\allowbreak\,\big\lbrace\,}
\def\rBrace{\big\rbrace}
\def\by{\quad\hbox{by }}
\def\aa{^{\scriptscriptstyle-\!\!\!>}}
\def\bb{^{\scriptscriptstyle<\!\!\!-}}
\def\z{\hbox{\it 0\/}}
\def\o{\hbox{\it 1\/}}
\def\noef{\hbox{$\negg{\vee}\exists$}-formula}
\def\L{$\cal L$}
\def\bk{\hfill\break\phantom.\quad}
\def\Q{\hbox{\sans Q}}
\def\Qz{\hbox{$\hbox{\sans Q}_0$}}
\def\Qo{\hbox{$\hbox{\sans Q}_1$}}
%\def\Qo{\hbox{\sans Q}$_1$}
\def\Qs{\hbox{$\hbox{\sans Q}^*$}}
\def\Qds{\hbox{$\hbox{\sans Q}^{**}$}}
%\def\bQo{\hbox{$\rm\widebar{Q}_1$}}
\yy\def\pa{www.math.princeton.edu/~nelson/books/pa.pdf}\zz
\def\PA{\hbox{\ninesans P}}
\def\ZFC{\hbox{\ninesans ZFC}}
\def\SSp{\hbox{$\SS_{\pr}$}}
\def\free{\hbox{\sl free }}
\def\hz{{\hat0}}
\def\ho{{\hat1}}
\def\tz{{\tilde0}}
\def\to{{\tilde1}}
\def\pp{\underline{p}\hskip.1pt}
\def\bneg{{\bar\neg}}
\def\tneg{{\tilde\neg}}
\def\bor{{\bar\vee}}
\def\tor{{\tilde\vee}}
\def\tand{{\tilde{\&}}}
\def\timp{{\tilde{{\rightarrow}}}}
\def\tiff{{\tilde{{\leftrightarrow}}}}
\def\bexists{{\bar\Exists}}
\def\texists{{\tilde\Exists}}
\def\tforall{{\tilde\Forall}}
\def\beq{{\bar=}}
\def\teq{{\tilde=}}
\def\bz{{\bar0}}
\def\bS{{\bar{\ro S}}}
\def\bP{{\bar{\ro P}}}
\def\bl{{\bar\le}}
\def\tS{{\tilde{\ro S}}}
\def\bp{{\bar{+}}}
\def\tp{{\tilde+}}
\def\bt{{\bar{\.}}}
\def\ttt{{\tilde\.}}
\def\ov{\hbox{`}}
\def\Sing#1{\lbrace#1\rbrace}
\let\Forall=\forall
\def\forall{\allowbreak\Forall}
\let\Exists=\exists
\def\exists{\allowbreak\Exists}
\def\co#1{#1^{\hbox{\bf c}}}
\overfullrule=0pt
