\documentclass[%
version=last,%
a5paper,
10pt,%
headings=small,%
bibliography=totoc,%
index=totoc,%o
twoside,%
leqno,%
cleardoublepage=empty,%
%open=any,%
parskip=half,%
%draft=false,%
draft=true,%
%DIV=classic,%
DIV=11,%
headinclude=true,%
pagesize]%{scrreprt}
{scrartcl}

%\usepackage[notref,notcite]{showkeys}
\renewcommand{\theequation}{\fnsymbol{equation}}

\usepackage[headsepline]{scrpage2}
\pagestyle{scrheadings}
\clearscrheadings
\ohead{\pagemark}
\ihead{Tarski's 1950 ICM Address}

\usepackage{hfoldsty}
\usepackage[neverdecrease]{paralist}
\usepackage{url}


\usepackage{relsize} % Here \smaller scales by 1/1.2; \relscale{X} scales by X

\renewenvironment{quote}{\begin{list}{}
{\relscale{.90}\setlength{\leftmargin}{0.05\textwidth}
\setlength{\rightmargin}{\leftmargin}}
\item[]}
{\end{list}}


\usepackage{amsmath,amsthm,amssymb,bm,upgreek,mathrsfs}
%\usepackage[all]{xy}

\usepackage{stmaryrd} % for \mapsfrom

\newcommand{\Forall}[1]{\forall#1\;}
\newcommand{\Exists}[1]{\exists#1\;}

\usepackage[mathcal]{euscript}
\newcommand{\tf}[1]{\mathcal{#1}} % ``Tarski's font''

\newcommand{\F}{\mathbf F}
\newcommand{\EF}{\mathbf{EF}}
\newcommand{\AF}{\mathbf{AF}}
\newcommand{\AC}[1][]{\mathbf{AC}_{#1}}
\newcommand{\AT}{\mathbf{AT}}
\newcommand{\ACL}{\mathbf{ACL}}

\DeclareMathOperator{\spectrum}{Spec}
\newcommand{\spec}[1]{\spectrum(#1)}

\newcommand{\conc}{\mathbin{\hat{\ }}}
\newcommand{\sig}{\mathscr S}
\newcommand{\str}[1]{\mathfrak{#1}}
\newcommand{\size}[1]{\lvert#1\rvert}
\DeclareMathOperator{\setMod}{Mod}
\newcommand{\sMod}[1]{\setMod(#1)}
\newcommand{\Mod}[2][]{\mathbf{Mod}_{#1}(#2)}
\newcommand{\Moda}[1]{\mathbf{Mod}^*(#1)}
\newcommand{\Str}{\mathbf{Str}}
\DeclareMathOperator{\sentences}{Sen}
\newcommand{\Sen}{\sentences}
\newcommand{\modsim}{/\mathord{\sim}}
\newcommand{\pow}[1]{\mathscr P(#1)}
\newcommand{\inv}{{}^{-1}}

\newcommand{\Cat}[1]{\bm{\mathsf{#1}}}
\newcommand{\Top}{\Cat{Top}}
\newcommand{\Frm}{\Cat{Frm}}
\newcommand{\Loc}{\Cat{Loc}}
\newcommand{\Grp}{\Cat{Grp}}
\newcommand{\Set}{\Cat{Set}}
\DeclareMathOperator{\domain}{dom}
\newcommand{\dom}[1]{\domain(#1)}
\DeclareMathOperator{\points}{pt}
\newcommand{\pt}[1]{\points(#1)}
\DeclareMathOperator{\homoms}{Hom}
\newcommand{\Hom}[1]{\homoms(#1)}
\newcommand{\bel}[1]{\left[#1\right]}

\newcommand{\Sn}[1][\sig]{\sentences_{\sig}}
\newcommand{\Sna}[1][\sig]{\sentences^*_{\sig}}
\DeclareMathOperator{\formulas}{Fm}
\newcommand{\Fm}[1][\sig]{\formulas_{#1}}
\DeclareMathOperator{\freevariables}{fv}
\newcommand{\fv}[1]{\freevariables(#1)}
\DeclareMathOperator{\variables}{v}
\newcommand{\vr}[1]{\variables(#1)}
\DeclareMathOperator{\theory}{Th}
\newcommand{\Th}[1]{\theory(#1)}
\newcommand{\Tha}[1]{\theory^*(#1)}
\renewcommand{\emptyset}{\varnothing}
\renewcommand{\setminus}{\smallsetminus}
\renewcommand{\leq}{\leqslant}
\renewcommand{\nleq}{\nleqslant}
\renewcommand{\geq}{\geqslant}
\renewcommand{\phi}{\varphi}
%\newcommand{\Or}{\;\lor\;}
\newcommand{\Or}{\;\mathrel{\text{\textsc{or}}}\;}
\renewcommand{\models}{\vDash}
\newcommand{\nmodels}{\nvDash}
\newcommand{\included}{\subseteq}
\newcommand{\includes}{\supseteq}
\newcommand{\pincluded}{\subset}
\newcommand{\liff}{\Leftrightarrow}
\newcommand{\lto}{\Rightarrow}



\newtheorem{theorem}{Theorem}
\newtheorem{definition}[theorem]{Definition}

\newtheorem{corollary}[theorem]{Corollary}
\newtheorem{lemma}{Lemma}

\theoremstyle{definition}

\newtheorem{example}[theorem]{Example}

\theoremstyle{remark}
\newtheorem{remark}[theorem]{Remark}

\begin{document}

\title{Tarski's 1950 ICM Address}
\author{David Pierce}
\date{September 15, 2014}
\publishers{Mimar Sinan Fine Arts University\\
\url{http://mat.msgsu.edu.tr/~dpierce/}}
\maketitle

An \textbf{algebraic system} is just a structure in our sense: 
a nonempty set with some operations, relations, and distinguished elements.

The paper will assume there are finitely many of these operations, relations,
and distinguished elements.

For [even greater] simplicity, all systems
will be of the form $\langle A,+\rangle$, where $+$ is a binary operation;
the system is denoted by $\str A$.
With the common ambiguity, Tarski writes about
\begin{quote}
  systems $\str A=\langle A,+\rangle$ 
formed by a set $A$ and one binary operation $+$.
\end{quote}
These will be called \textbf{algebras,}
and the \emph{set} of all algebras will be $\tf A$.
A footnote justifies calling this a set:
we may assume $A$ is always a subset of some predetermined set $U$.

The \textbf{arithmetic of algebras} is the first-order logic 
(Tarski says \emph{lower predicate calculus}) of algebras.
An \textbf{arithmetical class} is the set of algebras
in which a certain sentence of the arithmetic of algebras holds.

Sentences are \emph{sentential functions} without free variables.

\textbf{Sentential functions} (our formulas) 
are defined recursively from the \emph{atomic} sentential functions.
The variables in these are from the list
\begin{equation*}
  x,x',x'',\dots,x^{(k)},\dots
\end{equation*}
Also the atomic sentences are, in our terms, \emph{unnested:}
just
\begin{align*}
  x^{(k)}&=x^{(l)},&x^{(k)}+x^{(l)}&=x^{(m)}.
\end{align*}
We define
\begin{align*}
  I_{k,l}&=\{y\in A^{\omega}\mid y_k=y_l\},&
S_{k,l,m}&=\{y\in A^{\omega}\mid y_k+y_l=y_m\}
\end{align*}
(Tarski does not use the set-builder notation here,
but will later).
Sentence construction now corresponds to some operations on $\pow{A^{\omega}}$ 
(our notation), namely 
\begin{description}
  \item[set addition] $\cup$, 
\item[set multiplication] $\cap$,
\item[complementation] $\overline X=A^{\omega}-X$,
\item[outer cylindrification] 
$\nabla_kX=\{y\in A^{\omega}\mid\Exists x(x\in X\And x_k=y_k)\}$,
\item[inner cylindrification] 
$\Delta_kX=\{y\in A^{\omega}\mid\Forall x(x_k=y_k\implies x\in X)\}$.
\end{description}
A sentential function $\Phi$ determines a function $\tf F$
whose domain is $\tf A$ 
(that is, in Tarski's symbolism, $D(\tf F)=\tf A$),
and then $\tf F(\str A)$ consists of those elements of $A^{\omega}$ 
that satisfy $\Phi$.

\begin{definition}
The set of all functions $\tf F$ such that $D(\tf F)=\tf A$,
and $\tf F(\str A)\included A^{\omega}$
for all $\str A$ in $\tf A$, 
will be denoted by
\begin{equation*}
\F.
\end{equation*}
When $\Phi$ is $I_{k,l}$ and $S_{k,l,m}$ as above,
then $\tf F$ is respectively
\begin{align*}
  &\tf I_{k,l},&&\tf S_{k,l,m}
\end{align*}
(here Tarski does use set-builder notation,
with explanation).
These are called \textbf{elementary functions;}
the set of all of them will be denoted by
\begin{equation*}
  \EF.
\end{equation*}
\end{definition}

\begin{definition}
The operations on $\pow{A^{\omega}}$ defined earlier
induce the corresponding pointwise operations on $\F$;
we also have $\bigcup$ and $\bigcap$.
\end{definition}

\begin{definition}
  Also the relation $\included$ of \textbf{inclusion} on $\pow{A^{\omega}}$
induces a relation with the same symbol on $\F$.
Also $\F$ contains functions $\tf Z$ and $\tf U$ given by
\begin{align*}
  \tf Z(\str A)&=\emptyset,&\tf U(\str A)&=A^{\omega}
\end{align*}
(Tarski uses $\Lambda$ ``as usual'' for $\emptyset$.)
\end{definition}

\begin{theorem}
  These are the \textbf{zero} and \textbf{unit} elements
of $\F$ as a \textbf{complete atomistic Boolean algebra}
with $\bigcup$ and $\bigcap$ as \textbf{join} and \textbf{meet,}
and $\included$ as \textbf{inclusion.}
\end{theorem}

\begin{theorem}
  For all $\tf F$ and $\tf G$ in $\F$ and $k$ and $l$ in $\omega$,
  \begin{align*}
    &
  \begin{gathered}
    \nabla_k\tf Z=\tf Z,\\
\tf F\included\nabla_k\tf F,\\
\nabla_k(\tf F\cap\nabla_k\tf G)=\nabla_k(\tf F\cap\tf G),\\
\overline{\nabla_k\tf F}=\Delta_k\overline{\tf F},\\
\nabla_k\nabla_l\tf F=\nabla_k\nabla_l\tf F,
  \end{gathered}&
    &
  \begin{gathered}
\Delta_k\tf U=\tf U,\\
\Delta_k\tf F\included\tf F,\\
\Delta_k(\tf F\cup\Delta_k\tf G)=\Delta_k(\tf F\cup\tf G),\\
\overline{\Delta_k\tf F}=\nabla_k\overline{\tf F},\\
\Delta_k\Delta_l\tf F=\Delta_k\Delta_l\tf F,
  \end{gathered}
  \end{align*}
\end{theorem}

\begin{theorem}
  For all $\tf F$ in $\F$ and $k$, $l$, and $m$ in $\omega$,
  \begin{gather*}
    \tf I_{k,k}=\tf U,\\
k\neq m\And l\neq m\implies\tf I_{k,l}=\nabla_m(\tf I_{k,m}\cap\tf I_{l,m}),\\
k\neq l\implies
\nabla_k(\tf I_{k,l}\cap\tf F)\cap\nabla_k(\tf I_{k,l}\cap\overline{\tf F})=\tf Z.
  \end{gather*}
\end{theorem}

All identities on $\F$ 
involving $\bigcup$, $\bigcap$, $\overline{\ }$, $\nabla_k$, $\Delta_k$, 
$\tf Z$, $\tf U$, and $\tf I_{k,l}$
can be derived formally from Theorems 4--6,
according to unpublished work by L. H. Chin, F. B. Thompson, and Tarski.

\begin{theorem}
  For every $\tf F$ in $\F$, the following are equivalent:
  \begin{itemize}
  \item 
$\Delta_k\tf F=\tf F$ for all $k$ in $\omega$,
  \item 
$\nabla_k\tf F=\tf F$ for all $k$ in $\omega$,
\item
there is no $\str A$ 
for which $\tf F(\str A)$ is not $\emptyset$ or $A^{\omega}$.
  \end{itemize}
\end{theorem}

\begin{definition}
  The intersection of the family of all subsets of $\F$
that include $\EF$ 
and are closed under $\cup$, $\overline{\ }$, and the $\nabla_k$ 
is the set of \textbf{arithmetical functions,}
denoted by
\begin{equation*}
  \AF.
\end{equation*}
\end{definition}

\begin{theorem}
  $\EF\included\AF$, and $\AF$
 closed under $\cup$, $\cap$, $\overline{\ }$, 
and the $\nabla_k$ and $\Delta_k$.
\end{theorem}

\begin{theorem}
  $\AF$ is countable 
(``denumerable, \emph{i.e.}\ of the power $\aleph_0$'').
\end{theorem}

\begin{theorem}[Canonical Representation]
The elements of $\AF$ are precisely the elements
\begin{equation*}
  O_1O_2\cdots O_n(\tf G)
\end{equation*}
of $\F$,
where each $O_i$ is $\nabla_k$ or $\Delta_k$,
and $\tf G$ is a finite union of finite intersections 
of elements of $\EF$ and their complements.
\end{theorem}

\begin{theorem}
  For every $\tf F$ in $\AF$
there are only finitely many $k$ for which $\Delta_k\tf F\neq\tf F$
(or $\nabla_k\tf F=\tf F$).
\end{theorem}

The set $\{k\in\omega\mid\Delta_k\tf F\neq\tf F\}$ 
is the \textbf{dimension index} of $\tf F$.

Now we have the key passage:
\begin{quote}
Much deeper than all the preceding 
is the \emph{compactness theorem for arithmetical functions}:

\begin{theorem}
  If $\mathbf K\included\AF$ 
and $\bigcap(\tf F\mid\tf F\in\mathbf K)=\tf Z$,
then there is a finite set $\mathbf L\included\mathbf K$
for which $\bigcap(\tf F\mid\tf F\in\mathbf L)=\tf Z$.
\end{theorem}

A mathematical proof of Theorem 13 is rather involved.
On the other hand, this theorem easily reduces to a metamathematical result
which is familiar from the literature,
in fact to G\"odel's completeness theorem for elementary logic.%%%%%
\footnote{For a proof of G\"odel's theorem see, e.g., 
[L. Henkin, \emph{The completeness of the first-order functional calculus,} 
J. Symbolic Logic vol.\ 14 (1949) pp.~159--166].  [Tarski's note.]}
\end{quote}

\begin{definition}
  If $\tf F\in\F$,  we let
  \begin{equation*}
    \tf{CL}(\tf F)
=\{\str A\mid\str A\in\tf A,\tf F(\str A)=A^{\omega}\}.
  \end{equation*}
This is an \textbf{arithmetical class,}
provided $\tf F\in\AF$.
The family of all arithmetical classes is
\begin{equation*}
  \AC.
\end{equation*}
\end{definition}

An element of $\F$ with empty dimension index 
is a \textbf{simple function.}

\begin{theorem}
Every arithmetical class is $\tf{CL}(\tf F)$ 
for a simple arithmetical function $\tf F$.  
\end{theorem}

As arithmetical functions correspond to sentential functions,
so simple arithmetical functions correspond to sentences.

\begin{theorem}
  $\AC$ is a field of subsets of $\tf A$,
that is, a Boolean subalgebra of $\pow{\tf A}$;
and it is countable.
\end{theorem}

\begin{quote}
%  \begin{minipage}{0.9\textwidth}
    \begin{theorem}
      If $\mathbf K\included\AC$ 
and $\bigcap(\tf X\mid\tf X\in\mathbf K)=\Lambda$,
then there is a finite family $\mathbf L\included\mathbf K$ such that
$\bigcap(\tf X\mid\tf X\in\mathbf L)=\Lambda$.
    \end{theorem}

This theorem---the \emph{compactness theorem for arithmetical classes}---%
is clearly a corollary of Theorem 13.
As an improvement of Theorem 17 we obtain

    \begin{theorem}
      If $\mathbf K\included\AC$ 
and $\bigcap(\tf X\mid\tf X\in\mathbf K)\in\AC$,
then there is a finite family $\mathbf L\included\mathbf K$ such that
$\bigcap(\tf X\mid\tf X\in\mathbf L)=\bigcap(\tf X\mid\tf X\in\mathbf K)$.
    \end{theorem}

An especially important particular case of Theorems 17 and 18 is given in the following theorem.

\begin{theorem}
  If $\tf S_n\in\AC$, 
$\tf S_{n+1}\included\tf S_n$ 
and $\tf S_{n+1}\neq\tf S_n$ for every $n\in\omega$,
then $\bigcap(\tf S_n\mid n\in\omega)\neq\Lambda$ and,
more generally,
 $\bigcap(\tf S_n\mid n\in\omega)\notin\AC$.
\end{theorem}
%  \end{minipage}
\end{quote}

Theorems 17--19 can be dualized,
since $\AC$ is closed under complementation.

A sample application:

\begin{theorem}
  A set of finite algebras is in $\AC$
if and only if it is closed under isomorphism
and there is a bound on the size of its elements.
\end{theorem}

If $K$ is a family of sets, we denote by
\begin{align*}
  &K_{\sigma},&&K_{\delta}
\end{align*}
the closures under countable unions and intersections, respectively.
Thus the elements of $\AC[\delta]$
are the sets of algebras characterized by a system of arithmetical sentences.

By G. Birkhoff,
a set of algebras closed under isomorphism and direct products
is in $\AC[\delta]$.

\begin{definition}
  If every element of $\AC$ contains both or neither of $\str A$ and $\str B$,
then these are \textbf{arithmetically equivalent} 
[\emph{i.e.}\ elementarily equivalent], and we write
\begin{equation*}
  \str A\equiv\str B.
\end{equation*}
\end{definition}

\begin{theorem}
  For all algebras $\str A$ and $\str B$,
  \begin{equation*}
    \str A\cong\str B\implies\str A\equiv\str B,
  \end{equation*}
and ``the two formulas are equivalent'' if the algebras are finite.
\end{theorem}

There is ``a mathematical translation of a familiar metamathematical result---%
in fact, of an extension of the L\"owenheim--Skolem theorem'':

\begin{theorem}
  If $\str A$ has infinite power $\alpha$,
then for every infinite cardinal $\beta$,
there is an algebra $\str B$ such that
\begin{gather*}
  \str A\equiv\str B,\\
\beta\leqq\alpha\implies\str B\included\str A.
\end{gather*}
\end{theorem}

\begin{quote}
  The following theorem is a rather special consequence of Theorem 13;
as will be seen later,
it has many interesting applications.

\begin{theorem}
If $\str A\in\tf A$, and if $\tf F_n\in\AF$
and $\tf F_{n+1}(\str A)\included\tf F_n(\str A)\neq\Lambda$
for every natural $n$,
then there is an algebra $\str B\in\tf A$ such that
$\str A\equiv\str B$ and $\bigcap(\tf F_n(\str B)\mid n\in\omega)\neq\Lambda$.
\end{theorem}
\end{quote}

\begin{definition}
  The sets $\{\str B\mid\str A\equiv\str B\}$ are \textbf{arithmetical types.}
The family of these is
\begin{equation*}
  \AT.
\end{equation*}
\end{definition}

``In metamathematical terminology, a set of algebras is an arithmetical type
if it is axiomatically characterized by means of a complete and consistent
system of arithmetical sentences.''
For the meaning of completeness, we are referred to the second part (p.\ 283)
of Tarski's \emph{Grundz\"uge des Systemenkalk\"uls,} 
First part, Fund.\ Math.\ vol.\ 25 (1935) pp.\ 503-526.  
Second part, Fund.\ Math.\ vol.\ 26 (1936) pp.\ 283-301.
(This is in the Woodger anthology
as \emph{Foundations of the Calculus of Systems.})

\begin{theorem}
 $\{\str B\mid\str A\equiv\str B\}=\bigcap(\tf X\mid\str A\in\tf X\in\AC)$,
and $\AT$ has power $2^{\aleph_0}$.  
\end{theorem}

Thus $\AT\included\AC[\delta]$.
If an algebra is finite, its arithmetical type is in $\AC$,
but not conversely.

\begin{theorem}
  There is a one-to-one correspondence
  \begin{align*}
    \tf S&\mapsto\{\tf X\mid\tf X\in\AC\And\tf S\cap\tf X=\Lambda\},\\
\bigcap(\tf X\mid\tf X\in\AC-\mathbf I)&\mapsfrom\mathbf I
  \end{align*}
between $\AT$ and $\spec{\AC}$
(the set of prime ideals of $\AC$).
%arithmetical types and prime ideals of $\AC$.
\end{theorem}

\begin{definition}
  Subsets of $\tf A$ that are closed under $\equiv$ 
are \textbf{arithmetically closed,}
and the family of arithmetically closed sets is
\begin{equation*}
  \ACL.
\end{equation*}
\end{definition}

\begin{theorem}
  The elements of $\ACL$ are precisely the unions
$\bigcup(\tf X\mid\tf X\in\mathbf K)$, where $\mathbf K\included\AT$.
The power of $\ACL$ is $2^{2^{\aleph_0}}$.
\end{theorem}

\begin{theorem}
  $\ACL$ is a complete field of subsets of $\tf A$
and thus a complete atomistic Boolean algebra.
$\AC\included\ACL$ (as Boolean algebras),
and $\AT$ is the set of atoms of $\ACL$.
\end{theorem}

By Theorem 27,
$\ACL$ is isomorphic to $\pow{\spec{\AC}}$.
By Stone's theory, we obtain a topology on $\tf A$ as follows.
Given a subset $\tf X$ of $\tf A$, we define
\begin{equation*}
  \tf C(\tf X)=\bigcap(\tf Y\mid\tf X\included\tf Y\in\AC).
\end{equation*}
Then $\tf A$ is a topological space with closure operation $\tf C$.
It is 
``not a topological space in the narrower sense (i.e., not a $T_1$-space)'';
but we can make it so by identifying $\str A$ and $\str B$ 
if $\tf C(\{\str A\})=\tf C(\{\str B\})$, that is, $\str A\equiv\str B$.
The new space is the \textbf{arithmetical space over} $\tf A$.
Its points are the arithmetical types.
``The point sets of the space are arbitrary (not sets, but) unions of points,''
so (by Theorem 27) they coincide with the arithmetically closed sets.
The families of closed and open sets are $\AC[\delta]$ and $\AC[\sigma]$.
By Theorem 17,
\begin{equation*}
  \AC[\delta]\cap\AC[\sigma]=\AC.
\end{equation*}
The arithmetical space over $\tf A$ is:
\begin{itemize}
\item 
totally disconnected,
\item
separable by Theorem 16,
\item
bicompact by Theorem 17 
(and thus by ``the completeness of elementary logic'').
\end{itemize}
For the relations of topology to metamathematics, we are referred to
A. Mostowski, 
\emph{Abz\"ahlbare Boolesche K\"orper 
und ihre Anwendung auf die allgemeine Metamathematik,} 
Fund.\ Math.\ vol.\ 29 (1937) pp.\ 34--53.

One may ``relativize'' the foregoing to a subset $\tf V$ of $\tf A$,
though results like Theorems 17--19 will require $\tf V$ to be in $\AC[\delta]$.

One wants to describe the arithmetical classes relative to $\tf V$.
To do this, one may
\begin{enumerate}
\item 
identify some of these, to be called basic classes;
\item
show that the Boolean algebra $\str B$ generated by the basic classes
is the Boolean algebra of all arithmetical classes;
\item
establish a criterion for determining whether two arithmetical classes
(given as Boolean combinations of basic classes) are the same.
\end{enumerate}
The ``crucial point consists in showing that'' 
$\str B$ is closed under the $\nabla_k$.
This is the ``method of eliminating quantifiers.''

This has been carried out for:
\begin{enumerate}[1)]
\item 
Abelian groups,
\item
algebraically closed fields,
\item
Boolean algebras,
\item
well ordered systems.
\end{enumerate}
For example, let $\tf V$ be the set of all algebraically closed fields,
and, $p$ being $0$ or prime, 
let $\tf C_p$ be the set of algebraically closed fields of characteristic $p$.
If $p$ is prime, then $\tf C_p$ is in $\AC(\tf V)$.
These $\tf C_p$ are basic in the sense above.

\begin{quote}
  When new notions are introduced in mathematics,
the question of their usefulness and applicability is often raised.
Mathematicians want to know
whether the discussion of the new notions
leads to interesting results
whose significance is not restricted
to the intrinsic development of the theory of these notions.
We believe that the theory of arithmetical classes
has good chances to pass the test of applicability.
\end{quote}
This is because of ``Theorem 13 and its consequences
(Theorems 17, 19, 24)''---note that Tarski does not say
the compactness theorem.

For example, for every ordered ring 
there is an ``arithmetically equivalent'' ring with a non-Archimedean order.

From Tarski's result 
that any two real closed fields are arithmetically equivalent,
it follows that every arithmetically closed set
that contains a real closed field contains all of them:
\begin{quote}
This extension is immediate 
once the completeness theorem for real closed fields
has been translated into the language of arithmetic classes;
however, it could hardly be derived
in a purely metamathematical (syntactical) way
from the completeness theorem itself---%
unless we allow ourselves to apply
some rather intricate semantical notions and methods.
\end{quote}

\end{document}
