## 1. Definition and Basic Properties of Infinitary Languages




Given a pair k, l of infinite cardinals such that l
[?] k, we define a class of infinitary languages in each of
which we may form conjunctions and disjunctions of sets of formulas of
cardinality < k, and quantifications over sequences of
variables of length < l. 




Let
 L
 -- the (finitary)
*base language* -- be an arbitrary but fixed first-order
language with any number of extralogical symbols. The infinitary
language
 L(k,l)
 has
the following *basic symbols*:


* All symbols of
 L
* A set **Var** of individual variables, where the
cardinality of **Var** (written: |**Var**|)
is k
* A logical operator
 [?]
(*infinitary conjunction*)




The class of *preformulas* of
 L(k,l)
 is defined recursively as
follows:


* Each formula of
 L
 is a
preformula;
* if ph and ps are preformulas, so are
 ph[?]ps and !ph;
* if Ph is a set of preformulas such that |Ph| < k,
then
 [?]Ph
 is a
preformula;
* if ph is a preformula and *X* [?] **Var**
is such that |*X*| < l, then [?]*X*ph is
a preformula;
* all preformulas are defined by the above clauses.




If Ph is a set of preformulas indexed by a set *I*, say
Ph = {ph*i* : *i* [?] *I*},
then we agree to write
 [?]Ph
for:



> 
> [?]*i*[?]*I* ph
> 




or, if *I* is the set of natural numbers, we write
 [?]Ph
 for:



> ph0
>  [?]
> ph1
>  [?]
> ...




If *X* is a set of individual variables indexed by an ordinal
a, say *X* = {*x*x : x <
a}, we agree to write
([?]*x*x)x<aph for
[?]*X*ph.




The logical operators
 [?],
 -,
- are defined in the customary manner. We also introduce the
operators
 [?]
 (*infinitary
disjunction*) and [?] (*universal quantification*)
by



> [?]Ph
> =*df*
>  ![?]{
> !ph : ph [?] Ph} 
> 
> 
> 
> [?]Xph =*df* ![?]X!ph,
> 
> 
> 




and employ similar conventions as for
 [?],
 [?] . 




Thus
 L(k,l)
 is
the infinitary language obtained from
 L
 by permitting conjunctions and disjunctions of length
< k and quantifications[1]
 of length <
l. Languages
 L(k,o)
 are called *finite-quantifier*
languages, the rest *infinite-quantifier* languages. Observe
that
 L(o,o)
 is
 just
 L itself.




Notice the following *anomaly* which can arise in an
infinitary language but not in a finitary one. In the language
 L(o1,o), which
allows countably infinite conjunctions but only finite quantifications,
there are preformulas with so many free variables that they cannot be
"closed" into sentences of
 L(o1,o)
 by prefixing quantifiers.
Such is the case, for example, for the
 L(o1,o)-preformula



> *x*0 < *x*1
>   [?]  *x*1
> < *x*2
>   [?]  ...
>   [?]  *xn* <
> *x**n*+1 ...,




where
 L
 contains the binary
relation symbol <. For this reason we make the following 



> **Definition**. A *formula* of
>  L(k,l)
>  is a preformula
> which contains < l free variables. The set of all formulas
>  of
>  L(k,l) will be
> denoted by **Form**(L(k,l)) or simply
> **Form**(k,l) and the set of all sentences by
> **Sent**(L(k,l)) or simply
> **Sent**(k,l).




In this connection, observe that, in general, nothing would be gained
by considering "languages"
 L(k,l)
 with l > k. For
example, in the "language"
 L(o,o1), formulas will have only
finitely many free variables, while there will be a host of "useless"
quantifiers able to bind infinitely many free
 variables.[2]




Having defined the syntax of
 L(k,l),
 we next sketch its
*semantics*. Since the extralogical symbols of
 L(k,l)
 are just those
 of
 L, and it is these symbols which
determine the form of the structures in which a given first-order
language is to be interpreted, it is natural to define an
 L(k,l)-structure
 to be
simply an
 L-structure.
 The notion
of a formula of
 L(k,l)
 being *satisfied* in an
 L-structure
***A*** (by a sequence of elements from the domain
of ***A***) is defined in the same inductive manner
as for formulas of
 L
 except that
we must add two extra clauses corresponding to the clauses for
 [?]Ph
 and [?]Xph in the
definition of preformula. In these two cases we naturally define:



> [?]Ph is satisfied
> in ***A*** (by a given sequence)  = 
> for all ph [?] Ph, ph is satisfied in
> ***A*** (by the sequence); 
> 
> 
> 
> [?]*X*ph is satisfied in ***A***
>  =  there is a sequence of elements from the domain of
> ***A*** in bijective correspondence with *X*
> which satisfies ph in ***A***.
> 
> 
> 




These informal definitions need to be tightened up in a rigorous
development, but their meaning should be clear to the reader. Now the
usual notions of *truth, validity, satisfiability*, and
*model* for formulas and sentences of
 L(k,l)
 become available. In particular, if
***A*** is an
 L-structure
 and s [?]
**Sent**(k,l), we shall write
***A***
 [?]
s
 for **A** is a model of s, and
 [?]
 s for s *is valid*,
that is, for all ***A***,
***A***
 [?]
s.
 If D [?] **Sent**(k,l), we
shall write D
 [?]
 s for
s *is a logical consequence of* D, that is, each
model of D is a model of s.




We now give some examples intended to display the expressive power
of the infinitary languages
 L(k,l)
 with k [?]
o1. In each case it is well-known that the notion in
question cannot be expressed in any first-order language.



**Characterization of the standard model of arithmetic
in**
L(o1,o). Here the *standard
model of arithmetic* is the structure **N** =
<*N*, +, *, *s*, 0> , where *N* is the set
of natural numbers, +, *, and 0 have their usual meanings, and
*s* is the successor operation. Let
 L
 be the first-order language appropriate for
**N**. Then the class of
 L-structures
 isomorphic to **N** coincides
with the class of models of the conjunction of the following
 L(o1,o)
sentences (where **0** is a name of 0):



> 
> 
> [?]*m*[?]o
> [?]*n*[?]o
> *s**m***0** +
> *s**n***0** =
> *s**m*+*n***0**
> 
> 
> 
> 
> [?]*m*[?]o
> [?]*n*[?]o
> *s**m***0**
> * *s**n***0** =
> *s**m***n***0**
> 
> 
> 
> 
> [?]*m*[?]o
> [?]*n*[?]o[?]{*m*}
> *s**m***0**
> [?] *s**n***0**
> 
> 
> 
> 
> [?]*x*[?]*m*[?]o
> *x* =
> *s**m***0**
> 
> 
> 
> 




The terms *snx* are defined recursively by



> 
> 
> 
> |  |  |  |
> | --- | --- | --- |
> | *s*0*x* |  =  | *x* |
> | *s**n*+1*x* |  =  | *s*(*snx*) |
> 
> 
> 



**Characterization of the class of all finite sets in**
L(o1,o).
Here the base language has no extralogical symbols. The class of all
finite sets then coincides with the class of models of the
 L(o1,o)-sentence



> [?]*n*[?]o
> [?]*v*0 ...
> [?]*vn*[?]*x*(*x* =
> *v*0
>  [?]
>  ...
>  [?]
>  *x* =
> *vn*).



**Truth definition in**
L(o1,o) **for a countable
base language**
L.

 Let
 L be a countable first-order
language (for example, the language of arithmetic or set theory) which
contains a name ***n*** for each natural number
*n*, and let s0, s1, ...
be an enumeration of its sentences. Then the
 L(o1,o)-formula



> **Tr**(*x*)
>  =*df* 
>  [?]*n*[?]o (*x =
> **n***
>  [?]
> s*n*)




is a *truth predicate* for
 L
 inasmuch as the sentence 



> **Tr**(***n***) -
> s*n*




is valid for each *n*. 



**Characterization of well-orderings in**
L(o1,o1). The base
language
 L
 here includes a binary
predicate symbol [?]. Let s1 be the usual
 L-sentence
 characterizing linear
orderings. Then the class of
 L-structures
 in which the interpretation of [?] is a
well-ordering coincides with the class of models of the
 L(o1,o1) sentence
s = s1
 [?]
s2, where



> s2 =*df*
> ([?]*vn*)*n*[?]o
> [?]*x*
>  [[?]*n*[?]o (*x =
> vn*)
>  [?]
>  [?]*n*[?]o
> (*x* [?] *vn*)].




Notice that the sentence s2 contains an *infinite
quantifier*: it expresses the essentially *second-order*
assertion that every countable subset has a least member. It can in
fact be shown that the presence of this infinite quantifier is
essential: the class of well-ordered structures cannot be characterized
in any finite-quantifier language. This example indicates that
infinite-quantifier languages such as
 L(o1,o1) behave rather
like second-order languages; we shall see that they share the latters'
defects (incompleteness) as well as some of their advantages (strong
expressive power). 




Many extensions of first-order languages can be *translated*
into infinitary languages. For example, consider the generalized
quantifier language
 L(*Q*0) obtained from
 L
 by adding a new quantifier symbol
*Q*0 and interpreting
*Q*0*x*ph(*x*) as *there exist
infinitely many x such that* ph(*x*). It is easily seen
that the sentence *Q*0*x*ph(*x*) has
the same models as the
 L(o1,o)-sentence



> ![?]*n*[?]o
> [?]*v*0...[?]*vn*[?]*x*[ph(*x*) - (*x = v*0
>  [?]
>  ...
>  [?]
> *x = vn*)].




Thus
 L(*Q*0)
is, in a natural sense, translatable into
 L(o1,o). Another language
translatable into
 L(o1,o) in this sense is the
*weak second-order language* obtained by adding a countable set
of monadic predicate variables to
 L
 which are then interpreted as ranging over all
*finite* sets of individuals.




Languages with arbitrarily long conjunctions, disjunctions and
(possibly) quantifications may also be introduced. For a fixed infinite
cardinal l, the language
 L([?],l)
 is defined by specifying its class
of formulas, **Form**([?],l), to be the union,
over all k [?] l, of the sets
**Form**(k,l). Thus
 L([?],l)
 allows arbitrarily long conjunctions
and disjunctions, in the sense that if Ph is an arbitrary subset of
**Form**([?],l), then both
 [?]Ph
 and
 [?]Ph
 are members of
**Form**([?],l). But
 L([?],l)
 admits only quantifications of
length < l: all its formulas have < l free
variables. The language
 L([?],[?])
 is defined in turn by specifying its
class of formulas, **Form**([?],[?]), to be the
union, over all infinite cardinals l, of the classes
**Form**([?],l). So
 L([?],[?])
 allows arbitrarily long
quantifications in addition to arbitrarily long conjunctions and
disjunctions. Note that **Form**([?],l) and
**Form**([?],[?]) are proper classes in the sense
of Godel-Bernays set theory. Satisfaction of formulas of
 L([?],l)
 and
 L([?],[?])
 in a structure may
be defined by an obvious extension of the corresponding notion for
 L(k,l).


## 2. Finite-Quantifier Languages




We have remarked that infinite-quantifier languages such as
 L(o1,o1) resemble
second-order languages inasmuch as they allow quantification over
infinite sets of individuals. The fact that this is not permitted in
finite-quantifier languages suggests that these may be in certain
respects closer to their first-order counterparts than might be evident
at first sight. We shall see that this is indeed the case, notably in
the case of
 L(o1,o). 




The language
 L(o1,o) occupies a special place
among infinitary languages because--like first-order
languages--it admits an effective *deductive apparatus*. In
fact, let us add to the usual first-order axioms and rules of inference
the new axiom scheme



> [?]Ph -
> ph




for any countable set Ph [?]
**Form**(o1,o) and any ph [?]
Ph, together with the new rule of inference 



> 
> 
> 
> |  |
> | --- |
> | ph0,
>  ph1, ..., ph*n*, ... |
> | [?]*n*[?]o
> ph*n* |
> 
> 
> 




and allow deductions to be of countable length. Writing
 [?]\*
 for deducibility in this sense, we
then have the 



> L(o1,o)-**Completeness
> Theorem**. For any s [?]
> **Sent**(o1,o),
>  [?]
>  s  = 
>  [?]\*s




As an immediate corollary we infer that this deductive apparatus is
*adequate for deductions from countable sets of premises in*
L(o1,o).
That is, with the obvious extension of notation, we have, for any
*countable* set D [?]
**Sent**(o1,o) 



> (2.1) D
>  [?]
> s
>   = 
>  D[?]\*s




This completeness theorem can be proved by modifying the usual
Henkin completeness proof for first-order logic, or by employing
Boolean-algebraic methods. Similar arguments, applied to suitable
further augmentations of the axioms and rules of inference, yield
analogous completeness theorems for many other finite-quantifier
languages.




If just deductions of countable length are admitted, then no
deductive apparatus for
 L(o1,o) can be set up which is
adequate for deductions from *arbitrary* sets of premises, that
is, for which (2.1) would hold for every set D [?]
**Sent**(o1,o), *regardless of
cardinality*. This follows from the simple observation that there
is a first-order language
 L
 and
an uncountable set G of
 L(o1,o)-sentences such that
G *has no model but every countable subset of* G
*does*. To see this, let
 L
be
 the language of arithmetic augmented by o1 new
constant symbols {***c***x : x
< o1} and let G be the set of
 L(o1,o)-sentences {s} [?]
{***c***x [?]
***c***e : x [?] e}, where
s is the
 L(o1,o)-sentence characterizing
the standard model of arithmetic. This example also shows that the
*compactness theorem* fails for
 L(o1,o) and so also for any
 L(k,l)
 with k [?]
o1.




Another result which holds in the first-order case but fails
 for
 L(k,o) with k
[?] o1 (and also for
 L(o1,o1), although
this is more difficult to prove) is the *prenex normal form
theorem*. A sentence is *prenex* if all its quantifiers
appear at the front; we give an example of an
 L(o1,o)-sentence which is not
equivalent to a conjunction of prenex sentences. Let
 L
 be the first-order language without
extralogical symbols and let s be the
 L(o1,o)-sentence which
characterizes the class of finite sets. Suppose that s were
equivalent to a conjunction



> [?]*i*[?]*I*
> s*i*




of prenex
 L(o1,o)-sentences
s*i*. Then each s*i* is
of the form 



> *Q*1*x*1 ...
> *Q*n*xn*
> ph*i*(*x*1*,...,
> xn*),




where each *Qk* is [?] or [?] and
ph*i* is a (possibly infinitary) conjunction or
disjunction of formulas of the form *xk* =
*xl* or *xk* [?]
*xl*. Since each s*i* is a
sentence, there are only finitely many variables in each
ph*i*, and it is easy to see that each
ph*i* is then equivalent to a first-order formula.
Accordingly each s*i* may be taken to be a
first-order sentence. Since s is assumed to be equivalent to the
conjunction of the s*i*, it follows that
s and the set D = {s*i* :
*i* [?] *I*} have the same models. But obviously
s, and hence also D, have models of all finite
cardinalities; the compactness theorem for sets of first-order
sentences now implies that D, and hence also s, has an
infinite model, contradicting the definition of s. 




Turning to the *Lowenheim-Skolem theorem*, we find that
the *downward* version has adequate generalizations to
 L(o1,o) (and,
indeed, to all infinitary languages). In fact, one can show in much the
same way as for sets of first-order sentences that if D [?]
**Sent**(o1,o) has an infinite
model of cardinality [?] |D|, it has a model of cardinality the
larger of
 0, |D|.
In particular, any
 L(o1,o)-sentence with an infinite
model has a countable model.




On the other hand, the *upward* Lowenheim-Skolem theorem
in its usual form *fails* for all infinitary languages. For
example, the
 L(o1,o)-sentence characterizing
the standard model of arithmetic has a model of cardinality
 0 but no models of any other
cardinality. However, all is not lost here, as we shall see.




We define the *Hanf number* **h(L)** of a
language L to be the least cardinal k such that, if an
**L**-sentence has a model of cardinality k, it has
models of arbitrarily large cardinality. The existence of
**h(L)** is readily established. For each
**L**-sentence s not possessing models of
arbitrarily large cardinality let k(s) be the least
cardinal k such that s does not have a model of cardinality
k. If l is the supremum of all the k(s), then,
if a sentence of **L** has a model of cardinality
l, it has models of arbitrarily large cardinality.




Define the cardinals m(a) recursively by



> 
> 
> 
> |  |  |  |
> | --- | --- | --- |
> | m(0) |  =  | 0 |
> | m(a+1) |  =  | 2m(a) |
> | m(l) |  =  | [?]a<l m(a),
> for limit l. |
> 
> 
> 




Then it can be shown that 



> **h**(L(o1,o)) =
> m(o1),




similar results holding for other finite-quantifier languages. The
values of the Hanf numbers of infinite-quantifier languages such
 as
 L(o1,o1) are sensitive
to the presence or otherwise of large cardinals, but must in any case
greatly exceed that of
 L(o1,o). 




A result for
 L
 which
generalizes to
 L(o1,o) but to no other
infinitary language is the



> **Craig Interpolation Theorem**: If
> s,t [?] **Sent**(o1,o)
> are such that
>  [?]
>  s -
> t, then there is th [?]
> **Sent**(o1,o) such that
>  [?]
>  s - th and
>  [?]
>  th - t, and each
> extralogical symbol occurring in th occurs in both s and
> t.




The proof is a reasonably straightforward extension of the first-order
case. 




Finally, we mention one further result which generalizes nicely
 to
 L(o1,o)
but to no other infinitary language. It is well known that, if
***A*** is any finite
 L-structure
 with only finitely many relations, there is
an
 L-sentence
 s
characterizing ***A*** up to isomorphism. For
 L(o1,o) we have
the following generalization known as



> **Scott's Isomorphism Theorem**. If
> ***A*** is a countable
>  L-structure
>  with only countably many relations, then
> there is an
>  L(o1,o)-sentence whose class of
> countable models coincides with the class of
>  L-structures
>  isomorphic with
> ***A***.




The restriction to *countable* structures is essential because
countability cannot in general be expressed by an
 L(o1,o)-sentence. 




The language
 L([?],o)
 may also be counted as a
finite-quantifier language. The concept of equivalence of structures
with respect to this language is of especial significance: we call two
(similar) structures ***A*** and
***B*** ([?],o)-*equivalent*,
written ***A*** [?][?]o
***B***, if the same sentences of
 L([?],o)
 hold in both
***A*** and ***B***. This
relation can, first of all, be characterized in terms of the notion of
partial isomorphism. A *partial isomorphism* between
***A*** and ***B*** is a
nonempty family *P* of maps such that:


* For each *p* [?] *P*, dom(*p*) is a
substructure of ***A***, ran(*p*) is a
substructure of **B**, and *p* is an isomorphism of
its domain onto its range; and
* If *p* [?] *P*, *a* [?]
***A***, *b* [?]
***B***, then there exist *r*, *s*
[?] *P* both extending *p* such that *a* [?]
dom(*r*), *b* [?] ran(*s*) ("back and forth"
property).




If a partial isomorphism exists between ***A***
and ***B***, we say that
***A*** and ***B*** are
partially isomorphic and write ***A***
[?]*p* **B**. We
then have



> **Karp's Partial Isomorphism Theorem.**
>   
> 
>  For any similar structures ***A***,
> ***B***, ***A***
> [?][?]o ***B*** =
> ***A***
> [?]*p*
> ***B***.




There is also a version of Scott's isomorphism theorem for
 L([?],o),
 namely,



> (2.2) Given any structure ***A***,
> there is an
>  L([?],o)-sentence
>  s such that, for all
> structures ***B***, ***A***
> [?]*p*
> ***B*** = ***B***
>  [?]
>  s.




Partial isomorphism and ([?],o)-equivalence are related to
the notion of *Boolean isomorphism*. To define this we need to
introduce the idea of a Boolean-valued model of set theory. Given a
complete Boolean algebra *B*, the *universe*
*V*(*B*) *of B-valued sets*, also known
as the *B-extension of the universe V of sets*, is obtained by
first defining, recursively on a,



> *V*a(*B*) 
>  =
> {*x*: *x* is a function
>  [?]
>  range(*x*) [?] *B*
>  [?]
>  [?]x<a[domain(*x*) [?]
> *V*x(*B*)]}




and then setting



> *V*(*B*) = {*x*:
> [?]a(*x* [?]
> *V*a(*B*))}.




Members of *V*(*B*) are called *B-valued
sets*. It is now easily seen that a *B*-valued set is
precisely a *B*-valued function with domain a set of
*B*-valued sets. Now let **L** be the first-order
language of set theory and let
**L**(*B*) be the language obtained by
adding to **L** a name for each element of
*V*(*B*) (we shall use the same symbol for the
element and its name). One can now construct a mapping
[*](*B*) of the (sentences of the) language
**L**(*B*) into *B*: for each
sentence s of **L**(*B*), the
element [s](*B*) of *B* is the "Boolean
truth value" of s in *V*(*B*). This
mapping [*](*B*) is defined so as to send all
the theorems of Zermelo-Fraenkel set theory to the top element 1 of
*B*, i.e., to "truth"; accordingly,
*V*(*B*) may be thought of as a
*Boolean-valued model of set theory*. In general, if
[s](*B*) = 1, we say that s is
*valid* in *V*(*B*), and write
*V*(*B*)
 [?]
s.




Now each *x* [?] *V* has a canonical representative

*x* in *V*(*B*), satisfying



> 
> *x* = *y* iff *V*(*B*)
>  [?]
>  *x* = *y*
>   
> 
> *x* [?] *y* iff *V*(*B*)
>  [?]
>  *x* [?]
> 
> *y*




We say that two similar structures ***A***,
***B*** are Boolean isomorphic, written
***A***
[?]*b* ***B***, if, for
some complete Boolean algebra *B*, we have
*V*(*B*)
 [?]
***A***
[?]
***B***, that is, if there is a Boolean
extension of the universe of sets in which the canonical
representatives of ***A*** and
***B*** are isomorphic with Boolean value 1. It can
then be shown that: 



> (2.3) ***A***
> [?][?]o ***B*** =
> ***A***
> [?]*b*
> ***B***.




This result can be strengthened through category-theoretic formulation.
For this we require the concept of a(n) (elementary) *topos*. To
introduce this concept, we start with the familiary category of
**Set** of sets and mappings. **Set** has the
following key properties: 


1. There is a "terminal" object 1 such that, for any object
*X*, there is a unique map *X* - 1 (for 1 we may
take any one-element set, in particular, {0}).
2. Any pair of objects *X*,Y has a Cartesian product *X*
x *Y*.
3. for any pair of objects one can form the "exponential" object
*Y**X* of all maps from *X* -
*Y*.
4. There is a "truth-value" object O such that for each object
*X* there is a natural correspondence between subobjects
(subsets) of *X* and maps *X* - O. (For
O we may take the set 2 = {0,1}; maps *X* - O
are then *characteristic functions* on *X*.)




All four of these conditions can be formulated in category-theoretic
language -- a category satisfying them is called a *topos*.
The category **Set** is a topos; so also are (i) the
category **Set**(*B*) of Boolean-valued
sets and mappings in any Boolean extension
*V*(*B*) of the universe of sets; (ii) the
category of sheaves of sets on a topological space; (iii) the category
of all diagrams of maps of sets



> *X*0 - *X*1 -
> *X*2 - ...




The objects of each of these categories may be regarded as sets
which are *varying* in some manner: in case (i) over a
*Boolean algebra*; in case (ii) over a topological
*space*; in case (iii) over (discrete) time. A topos may be
conceived, then, as a universe of "variable" sets. The familiar
category **Set** is the special limiting case of a topos
in which the "variation" of the objects has been reduced to zero.




Just as in set theory, "logical operators" can be defined on the
truth-value object in any topos. These are maps !: O -
O;
 [?], [?], =: O x O - O
corresponding to the logical operations of negation, conjunction,
disjunction and implication. With these operations, O becomes a
Heyting algebra, thus embodying in general the laws not of classical
but of intutionistic logic. In this sense intuitionistic logic is
"internalized" in a topos: intuitionistic logic is the logic of
variable sets. (Of course, classical logic is internalized in certain
toposes, for instance **Set** and
**Set**(*B*) for any complete Boolean
algebra *B*.)




Any topos may be conceived as possible "universe of discourse" in
which mathematical assertions may be interpreted and mathematical
constructions may be performed. Mathematical assertions are rendered
interpretable in a topos
 E
 by
expression within
 E's
*internal language* -- a type-theoretic version of the
usual language of set theory. In a manner analogous to Boolean-valued
validity, one can introduce an appropriate notion of validity in
 E
 of a sentence s of its
internal language. Again, we write
 E

 [?] s for
"s is valid in
 E".




A topos
 E
 is said to be
*full* if, for any set *I*, the *I*-fold
copower[3]
 [?]*I*1 of its terminal object exists
 in
 E.
 [?]*I*1 may be thought of as the
canonical representative in
 E
 of
the set *I*; accordingly, we write it simply as
*I*. (In *V*(*B*) this coincides
with *I* as previously defined.) All the toposes
mentioned above are full.




Now let
 E
 be a full topos. If
***A*** = (*A*, *R*, ...) is a
structure, write ***A*** for
(*A*, *R*, ...). 
Two structures
***A*** and ***B*** are said to
be *topos isomorphic*, written ***A***
[?]*t*
***B***, if, for some topos
 E
 defined over the category of sets, we have
 E

 [?] *A*
[?]
*B*. In other words two structures are topos isomorphic
if their canonical representatives are isomorphic in the internal
language of some topos. It can then be shown that



> (2.4) ***A***
> [?][?]o ***B*** =
> ***A***
> [?]*t*
> ***B***.




Accordingly ([?],o)-equivalence may be regarded as
isomorphism in the extremely general context of universes of "variable"
sets. In this respect ([?],o)-equivalence is an "invariant"
notion of isomorphism.


## 3. The Compactness Property




As we have seen, the compactness theorem in its usual form fails for
all infinitary languages. Nevertheless, it is of some interest to
determine whether infinitary languages satisfy some suitably modified
version of the theorem. This so-called *compactness problem*
turns out to have a natural connection with purely set-theoretic
questions involving "large" cardinal numbers. 




We construct the following definition. Let k be an infinite
cardinal. A language **L** is said to be
k-*compact* (resp. *weakly*
k*-compact*) if whenever D is a set of
**L**-sentences (resp. a set of
**L**-sentences of cardinality [?] k) and each
subset of D of cardinality < k has a model, so does
D. Notice that the usual compactness theorem for
 L
 is precisely the assertion that
 L is o-compact. One reason for
 according significance to the k-compactness property is the
 following. Call **L** k-*complete*
 (resp. *weakly* k-*complete*) if there is a
 deductive system
***P*** for **L** with deductions of
length < k such that, if D is a
***P***-consistent[4]
 set of
**L**-sentences (resp. such that |D| [?] k),
then D has a model. Observe that such a
***P*** will be adequate for deductions from
arbitrary sets of premises (of cardinality [?] k) in the sense
of SS2. It is easily seen that if **L** is
k-complete or weakly k-complete, then **L** is
k-compact or weakly k-compact. Thus, if we can show that a
given language is *not* (weakly) k-compact, then there can
be no deductive system for it with deductions of length < k
adequate for deductions from arbitrary sets of premises (of cardinality
[?] k).




It turns out, in fact, that most languages
 L(k,l)
 fail to be even weakly
k-compact, and, for those that are, k must be an
exceedingly *large* cardinal. We shall need some
definitions.




An infinite cardinal k is said to be *weakly
inaccessible* if



> 
> 
> (a) l < k - l+ <
> k, (where l+ denotes the cardinal successor of
> l), and 
> 
> 
> 
> (b) | *I* | < k and l*i* <
> k (for all *i* [?] *I*) =
> [?]*i*[?]*I*
> l*i* < k.
> 
> 
> 




If in addition 



> 
> 
> (c) l < k = 2l <
> k,
> 
> 




then k is said to be (*strongly*)*inaccessible*.
Since
 0 is inaccessible,
it is normal practice to confine attention to those inaccessible, or
weakly inaccessible, cardinals that exceed
 0. Accordingly, inaccessible or weakly
inaccessible cardinals will always be taken to be *uncountable*.
It is clear that such cardinals--if they exist--must be
extremely large; and indeed the Godel incompleteness theorem
implies that the existence of even weakly inaccessible cardinals cannot
be proved from the usual axioms of set theory. 




Let us call a cardinal k *compact* (resp. *weakly
compact*) if the language
 L(k,k)
 is k-compact (resp. weakly
k-compact). Then we have the following results:



> (3.1)
>  0
> *is compact*. This is, of course, just a succinct way of
> expressing the compactness theorem for first-order languages. 
> 
> 
> 
> (3.2) k is *weakly compact* =
>  L(k,o)
>  is *weakly*
> k-*compact* = k is *weakly
> inaccessible*. Accordingly, it is consistent (with the usual axioms
> of set theory) to assume that no language
>  L(k,o)
>  with k [?] o1
> is weakly k-compact, or, *a fortiori*, weakly
> k-complete.
> 
> 
> 
> 
> (3.3) Suppose k is inaccessible. Then k is *weakly
> compact*  = 
>  L(k,o)
>  is *weakly*
> k-*compact*. Also, Also k is weakly compact =
> *there is a set of* k *inaccessibles before*
> k. Thus a weakly compact inaccessible cardinal is exceedingly
> large; in particular it cannot be the first, second, ...,
> *nth*, ... inaccessible.
> 
> 
> 
> 
> (3.4) k *is compact* = k *is
> inaccessible*. (But, by the result immediately above, the converse
> fails.)
> 
> 
> 




Let **Constr** stand for Godel's axiom of
constructibility; recall that **Constr** is consistent
with the usual axioms of set theory. 



> (3.5) *If* **Constr** *holds, then
> there are no compact cardinals*. 
> 
> 
> 
> (3.6) *Assume* **Constr** *and let*
> k *be inaccessible. Then* k *is weakly
> compact* =
>  L(o1,o) *is weakly*
> k-*compact for all*
> L.
> 
> 
> 
> 
> (3.7) *If* **Constr** *holds, then there are
> no cardinals* k *for which*
> L(o1,o) *is compact*.
> Accordingly, it is consistent with the usual axioms of set theory to
> suppose that there is no cardinal k such that all languages
>  L(o1,o) are
> k-complete. This result is to be contrasted with the fact that
> *all* first-order languages are o-complete.
> 
> 
> 




The import of these results is that the compactness theorem fails
very badly for most languages
 L(k,l)
 with k [?]
o1.




Some historical remarks are in order here. In the 1930s
mathematicians investigated various versions of the so-called
*measure problem* for sets, a problem which arose in connection
with the theory of Lebesgue measure on the continuum. In particular,
the following very simple notion of measure was formulated. If
*X* is a set, a (countably additive two-valued nontrivial)
*measure* on *X* is a map m on the power set
**P***X* to the set {0, 1} satisfying:



> (a) m(*X*) = 1, 
> 
> 
> 
> (b) m({*x*}) = m([?]) = 0 for all *x*
> [?]*X*, and
> 
> 
> 
> 
> (c) if ***A*** is any countable family of
> mutually disjoint subsets of *X*, then
>  m([?]***A***) =
> [?]{m(*Y*) : *Y* [?]
> ***A***}.
> 
> 
> 




Obviously, whether a given set supports such a measure depends only
on its cardinality, so it is natural to define a cardinal k to be
*measurable* if all sets of cardinality k support a
measure of this sort. It was quickly realized that a measurable
cardinal must be inaccessible, but the falsity of the converse was not
established until the 1960s when Tarski showed that measurable
cardinals are weakly compact and his student Hanf showed that the
first, second, etc. inaccessibles are not weakly compact (cf. (3.3)).
Although the conclusion that measurable cardinals must be monstrously
large is now normally proved without making the detour through weak
compactness and infinitary languages, the fact remains that these ideas
were used to establish the result in the first instance.


## 4. Incompleteness of Infinite-Quantifier Languages




Probably the most important result about first-order languages is the
*Godel completeness theorem* which of course says that the
set of all valid formulas of any first-order language
 L
 can be generated from a simple set
of axioms by means of a few straightforward rules of inference. A major
consequence of this theorem is that, if the formulas of
 L
 are coded as natural numbers in some
constructive way, then the set of (codes of) valid sentences is
*recursively enumerable*. Thus, the completeness of a
first-order language implies that the set of its valid sentences is
*definable* in a particularly simple way. It would accordingly
seem reasonable, given an *arbitrary* language
**L**, to turn this implication around and suggest that,
if the set of valid **L**-sentences is *not*
definable in some simple fashion, then *no* meaningful
completeness result can be established for **L**, or, as
we shall say, that **L** is *incomplete*. In this
section we are going to employ this suggestion in sketching a proof
that "most" *infinite quantifier* languages are incomplete in
this sense. 




Let us first introduce the formal notion of *definability* as
follows. If **L** is a language,
***A*** an **L**-structure, and
*X* a subset of the domain *A* of
***A***, we say that *X* is *definable
in* ***A*** by a formula ph(*x,
y*1,...,*yn*) of
**L** if there is a sequence
*a*1,...,*an* of elements of
*A* such that *X* is the subset of all elements
*x* [?] *A* for which ph(*x,
a*1,...,*an*) holds in
***A***.




Now write *Val*(**L**) for the set of all the
*valid* **L**-sentences, i.e., those that hold in
every **L**-structure. In order to assign a meaning to the
statement "*Val*(**L**) is definable", we have to
specify


1. a structure
***C***(**L**)--the *coding
structure* for **L**;
2. a particular one-one map--the *coding map*--of
the set of formulas of **L** into the domain of
***C***(**L**).




Then, if we identify *Val*(**L**) with its image in
***C***(**L**) under the coding map,
we shall interpret the statement "*Val*(**L**) is
definable" as the statement "*Val*(**L**), regarded
as a subset of the domain of
***C***(**L**), is definable in
***C***(**L**) by a formula of
**L**." 




For example, when **L** is the first-order
 language
 L of arithmetic, Godel
originally used as coding structure the standard model of
arithmetic N and as coding map the well-known
function obtained from the prime factorization theorem for natural
numbers. The recursive enumerability of
 *Val*(L)
 then means simply that the set of
codes ("Godel numbers") of members of
 *Val*(L) is definable in
 N by an
 L-formula
 of the form [?]*y*ph(*x, y*), where ph(*x,
y*) is a recursive formula.




Another, equivalent, coding structure for the first-order language
of arithmetic is the structure[5]
<*H*(o), [?] [?]   *H*(o)>  of
*hereditarily finite sets*, where a set *x* is
*hereditarily finite* if *x*, its members, its members of
members, etc., are all finite. This coding structure takes account of
the fact that first-order formulas are naturally regarded as finite
sets.




Turning now to the case in which **L** is an infinitary
language
 L(k,l),
what
 would be a suitable coding structure in this case? We remarked at
the beginning that infinitary languages were suggested by the
possibility of thinking of formulas as set-theoretical objects, so let
us try to obtain our coding structure by thinking about what kind of
set-theoretical objects we should take infinitary formulas to be. Given
the fact that, for each
ph[?]**Form**(k,l), ph and its
subformulas, subsubformulas, etc., are all of length <
k,[6]
 a moment's reflection reveals that
formulas of
 L(k,l)
"correspond"
 to sets *x hereditarily of cardinality* <
k in the sense that *x*, its members, its members of
members, etc., are all of cardinality < k. The collection of
all such sets is written *H*(k). *H*(o) is
the collection of *hereditarily finite* sets introduced above,
and *H*(o1) that of all *hereditarily
countable* sets.




For simplicity let us suppose that the only extralogical symbol of
the base language
 L
 is the binary
predicate symbol [?] (the discussion is easily extended to
the case in which
 L
 contains
additional extralogical symbols). Guided by the remarks above, as
coding structure for
 L(k,l)
 we take the structure,



> H(k)
> =*df* <*H*(k), [?] [?] 
> *H*(k)> .




Now we can define the coding map of
**Form**(k,l) into
 H(k).
 First, to each basic symbol *s*
 of
 L(k,l) we assign a
code object
 [?]*s*[?] [?] *H*(k) as
follows. Let {*v*x: x < k} be an
enumeration of the individual variables of
 L(k,l).




> 
> 
> 
> |  |  |  |
> | --- | --- | --- |
> | **Symbol** | **Code Object** | **Notation** |
> | ! | 1 | [?]![?] |
> | [?] | 2 | [?][?][?] |
> | [?] | 3 | [?][?][?] |
> | [?] | 4 | [?][?][?] |
> | [?] | 5 | [?] [?]
> [?] |
> | = | 6 | [?]=[?] |
> | *v*x | <0,x>  | [?]*v*x[?] |
> 
> 
> 




Then, to each ph [?] **Form**(k,l) we
assign the code object
 [?]ph[?] recursively as follows: 



> [?]*v*x =
> *v*e[?]
>  =*df* 
>  <[?]*v*x[?],
>  [?]=[?],
>  [?]*v*e[?]> , 
> 
> 
> [?]*v*x
> [?] *v*e[?]  =*df* 
>  <[?]*v*x[?],
>  [?][?][?],
>  [?]*v*e[?]> ;
> 
> 
> 




for ph, ps [?] **Form**(k,l), 



> [?]ph
>  [?]
> 
>  ps[?]  =*df* 
>  <[?]ph[?],
>  [?][?][?],
>  [?]ps[?]>  
> 
> 
> [?]!ph[?]  =*df* 
>  <[?]![?],
>  [?]ph[?]> 
> 
> 
> 
> [?][?]*X*ph[?]  =*df* 
>  <[?][?][?],
>  {[?]*x*[?]:
> *x* [?] *X*},
>  [?]ph[?]> ;
> 
> 
> 




and finally if Ph [?] **Form**(k,l)
with |Ph|
< k, 



> [?][?]Ph[?]  =*df* 
>  <[?][?][?],
>  {[?]ph[?]: ph [?] Ph}> .




The map 
ph - [?]ph[?] from **Form**(k,l) into
*H*(k) is easily seen to be one-one and is the required
coding map. Accordingly, we agree to identify *Val*(L(k,l)) with its image in
*H*(k) under this coding map.




When is *Val*(L(k,l)) a *definable* subset of
 H(k)?
 In order to answer this
question we require the following definitions.




An
 L-formula
 is called a
D0-*formula* if it is equivalent to a formula
in which all quantifiers are of the form
[?]*x*[?]*y* or [?]*x*[?]*y*
(i.e., [?]*x*(*x*[?]*y* - ...)
or [?]*x*(*x*[?]*y*
 [?]
 ...)). An
 L-formula
 is a S1-*formula* if
it is equivalent to one which can be built up from atomic formulas and
their negations using only the logical operators
 [?],

 [?],
[?]*x*[?]*y*, [?]*x*. A subset
*X* of a set *A* is said to be D0 (resp.
S1) *on A* if it is definable in the structure
<*A*, [?] [?]  *A*>  by a D0- (resp.
S1-) formula of
 L.




For example, if we identify the set of natural numbers with the set
*H*(o) of hereditarily finite sets in the usual way, then
for each *X* [?] *H*(o) we have:



> *X* is D0 on *H*(o)
> = *X* is recursive 
> 
> 
> *X* is S1 on *H*(o) =
> *X* is recursively enumerable.
> 
> 
> 




Thus the notions of D0- and S1-set
may be regarded as generalizations of the notions of *recursive*
and *recursively enumerable* set, respectively. 




The completeness theorem for
 L
implies
 that *Val*(L)
-- regarded as a subset of *H*(o) -- is
recursively enumerable, and hence S1 on
*H*(o). Similarly, the completeness theorem for
 L(o1,o) (see
SS2) implies that *Val*(L(o1,o)) -- regarded as a
subset of *H*(o1) -- is
S1 on *H*(o1). However, this
pleasant state of affairs collapses completely as soon as
 L(o1,o1) is reached.
For one can prove



> **Scott's Undefinability Theorem for**
> L(o1,o1).
> *Val*(L(o1,o1)) *is not
> definable in*
> H(o1) *even by an*
> L(o1,o1)-*formula*;
> *hence* a fortiori *Val*(L(o1,o1)) *is
> not* S1 *on*
> *H*(o1).




This theorem is proved in much the same way as the well-known result
that the set of (codes of) valid sentences of the second-order language
of arithemetic
 L2 is
not second-order definable in its coding structure
 N.
 To get this latter result, one first observes that
 N
 is characterized by a single
 L2-sentence, and then shows
that, if the result were false, then "truth in
 N"
 for
 L2-sentences would be definable by an
 L2-formula, thereby
violating Tarski's theorem on the undefinability of truth. 




Accordingly, to prove Scott's undefinability theorem along the above
lines, one needs to establish:



> 
> (4.1) *Characterizability of the coding structure*
> H(o1)
> *in*
> L(o1,o1): there is
>  an
>  L(o1,o1)-sentence
> t0 such that, for all
>  L-structures
>  ***A***, ***A***
>  [?]
>  t0  = 
> ***A***
> [?]
> H(o1).
> 
> 
> 
> 
> (4.2) *Undefinability of truth for*
> L(o1,o1)-*sentences*
> *in the coding structure*: there is no
>  L(o1,o1)-formula
> ph(*v*0) such that, for all
>  L(o1, o1)-sentences
> s, H(o1)
>  [?]
>  s-ph([?]s[?]).
> 
> 
> 
> 
> (4.3) *There is a term* *t*(*v*0,
> *v*1) *of*
> L(o1,o1) *such
> that, for each pair of sentences* s, t *of*
> L(o1,o1),
>  H(o1)
>   [?] 
>  [*t*([?]s[?],[?]t[?])
>  = [?]s -
>  t[?]].
> 
> 
> 




(4.1) is proved by analyzing the set-theoretic definition of
 H(o1) and showing
that it can be "internally" formulated in
 L(o1,o1). (4.2) is
established in much the same way as Tarski's theorem on the
undefinability of truth for first- or second-order languages. (4.3) is
obtained by formalizing the definition of the coding map s
 -
 [?]s[?] in
 L(o1,o1). 




Armed with these facts, we can obtain Scott's undefinability theorem
in the following way. Suppose it were false; then there would be
 an
 L(o1,o1)-formula
th(*v*0) such that, for all
 L(o1,o1)-sentences
s,



> (4.4)
>  H(o1)
>  [?]
> 
>  th([?]s[?])
>  iff   s [?] *Val*(L(o1,o1)).




Let t0 be the sentence given in (4.1). Then we have, for
all
 L(o1,o1)-sentences
s, 



> H(o1)
>  [?]
>  s   iff   (t0 -
> s) [?] *Val*(L(o1,o1)),




so that, by (4.4), 



> H(o1)
>  [?]
>  s   iff  
>  H(o1)
>  [?]
> 
>  th([?]t0 -
>  s[?]).




If *t* is the term given in (4.3), it would follow that 



> H(o1)
>  [?]
>  s-th(*t*([?]t0[?],
>  [?]s[?])).




Now write ph(*v*0) for the
 L(o1,o1)-formula
th(*t*([?]t0[?],
 [?]s[?])). Then 



> H(o1)
>  [?]
> 
>  s-ph([?]s[?]),




contradicting (4.2), and completing the proof. 




Thus *Val*(L(o1,o1)) is not
definable *even by an*
L(o1,o1)-*formula*,
so *a fortiori*
L(o1,o1) is
incomplete. Similar arguments show that Scott's undefinability theorem
continues to hold when o1 is replaced by any successor
cardinal k+; accordingly the languages
 L(k+,k+) are all
incomplete.[7]


## 5. Sublanguages of L(o1,o) and the Barwise Compactness Theorem




Given what we now know about infinitary languages, it would seem
 that
 L(o1,o) is
the only one to be reasonably well behaved. On the other hand, the
failure of the compactness theorem to generalize to
 L(o1,o) in any
useful fashion is a severe drawback as far as applications are
concerned. Let us attempt to analyze this failure in more detail. 




Recall from SS4 that we may code the formulas of a first-order
language
 L
 as hereditarily finite
sets, i.e., as members of *H*(o). In that case each finite
set of (codes of)
 L-sentences
 is
also a member of *H*(o), and it follows that the
compactness theorem for
 L
 can be
stated in the form:



> (5.1) If D [?] **Sent**(L) is such that each subset
> D0 [?] D, D0 [?]
> *H*(o) has a model, so does D.




Now it is well-known that (5.1) is an immediate consequence of the
*generalized completeness theorem* for
 L,
 which, stated in a form similar to that of (5.1),
becomes the assertion: 



> (5.2) If D [?] **Sent**(L) and s [?]
> **Sent**(L) satisfy
> D
>  [?]
>  s, then there is a
> deduction ***D*** of s from D such that
> ***D*** [?]
>  *H*(o).[8]




In SS2 we remarked that the compactness theorem for
 L(o1,o) fails
very strongly; in fact, we constructed a set G [?]
**Sent**(o1,o) such that 



> (5.3) Each countable subset of G has a model but
> G does not.




Recall also that we introduced the notion of *deduction* in
 L(o1,o); since
such deductions are of countable length it quickly follows from (5.3)
that 



> (5.4) There is a
>  sentence[9]s
>  [?]
> **Sent**(o1,o) such that
>  G
>  [?] s, but there is no
> deduction of s in
>  L(o1,o) from
> G.




Now the formulas of
 L(o1, o) can be coded as members
of
 H(o1), and it
is clear that
 H(o1) is closed under the formation of
countable subsets and sequences. Accordingly (5.3) and (5.4) may be
written: 



> (5.3 *bis*) Each G0 [?] G
> such that G0 [?]
>  H(o1) has a model, but G does
> not; 
> 
> 
> 
> (5.4 *bis*) There is a sentence s [?]
> **Sent**(o1,o) such that
>  G
>  [?] s, but there is no
> deduction ***D*** [?]
> *H*(o1) of s from G.
> 
> 
> 




It follows that (5.1) and (5.2) fail when
 "L" is replaced by
 "L(o1,o)" and
 "H(o)" by
 "H(o1)". Moreover, it can be shown that
the set G [?]
**Sent**(o1,o) in (5.3
*bis*) and (5.4 *bis*) may be taken to be
S1 on *H*(o1). Thus the
compactness and generalized completeness theorems fail even for
S1-sets of
 L(o1, o)-sentences. 




We see from (5.4 *bis*) that the reason why the generalized
completeness theorem fails for S1-sets in
 L(o1,o) is
that, roughly speaking, *H*(o1) is not "closed"
under the formation of deductions from S1-sets of
sentences in *H*(o1). So in order to remedy
this it would seem natural to replace *H*(o1)
by sets *A* which are, in some sense, closed under the formation
of such deductions, and then to consider just those formulas whose
codes are in *A*.




We now give a sketch of how this can be done.




First, we identify the symbols and formulas of
 L(o1,o) with
their codes in *H*(o1), as in SS4. For each
countable
 transitive[10]
 set *A*, let



> L*A* = **Form**(L(o1,o)) [?]
> *A*.




We say that
 L*A* is a *sublanguage* of
 L(o1,o) if the
following conditions are satisfied: 


1. L
 [?]
 L*A*
2. if ph, ps [?]
 L*A*, then ph
 [?]
 ps [?]
 L*A* and !ph [?]
 L*A*
3. if ph [?]
 L*A* and *x* [?] *A*,
then [?]*x*ph [?]
 L*A*
4. if ph(*x*) [?]
 L*A* and *y* [?] *A*,
then ph(*y*) [?]
 L*A*
5. if ph [?]
 L*A*, every subformula of ph is
 in
 L*A*
6. if Ph [?]
 L*A* and Ph [?] *A*,
 then
 [?]Ph [?]
 L*A*.




The notion of deduction in
 L*A* is defined in the customary way;
if D is a set of sentences of
 L*A* and ph [?]
 L*A*, then a
*deduction* of ph from D in
 L*A* is a deduction of ph from
D in
 L(o1,
o) every formula of which is in
 L*A*. We say that ph is
*deducible* from D in
 L*A* if there is a deduction
***D*** of ph from D in
 L*A*; under these
conditions we write D
 [?]*A* ph. In general,
***D*** will not be a member of *A*; in
order to ensure that such a deduction can be found in *A* it
will be necessary to impose further conditions on *A*. 




Let *A* be a countable transitive set such that
 L*A* is a
sublanguage of
 L(o1, o) and let D be a set
of sentences of
 L*A*. We say that *A* (or, by
abuse of terminology,
 L*A*) is D-*closed* if,
for any formula ph of
 L*A* such that D
 [?]*A* ph, there is a
deduction ***D*** of ph from D such that
***D*** [?] *A*. It can be shown that the
only countable language which is D-closed for *arbitrary*
D is the first-order language
 L,
 i.e., when *A* = *H*(o). However
J. Barwise discovered that there are countable sets *A* [?]
*H*(o1) whose corresponding languages
 L*A* differ
 from
 L and yet are D-closed
*for all* S1-*sets of sentences*
D. Such sets *A* are called *admissible sets*;
roughly speaking, they are extensions of the hereditarily finite sets
in which recursion theory--and hence proof theory--are still
 possible (for the full definition, see Section 5.1 below).




From Barwise's result one obtains immediately the



> **Barwise Compactness Theorem.** *Let*
> A *be a countable admissible set and let* D *be a set
> of sentences of*
> L*A* *which is*
> S1 *on* A. *If each* D'
> [?] D *such that* D' [?] A *has a
> model, then so does* D.




The presence of "S1" here indicates that this theorem
is a generalization of the compactness theorem for *recursively
enumerable* sets of sentences. 




Another version of the Barwise compactness theorem, useful for
constructing models of set theory, is the following. Let
**ZFC** be the usual set of axioms for Zermelo-Fraenkel
set theory, including the axiom of choice. Then we have:



> **5.5 Theorem**. *Let A be a countable
> transitive set such that **A*** = <*A*,
> [?] [?]  *A*>  *is a model of **ZFC***.
> *If* D *is a set of sentences of*
> L*A* *which is
> definable in **A** by a formula of the language of set
> theory and if each* D' [?] D *such
> that* D' [?] *A has a model, so does*
> D.




To conclude, we give a simple application of this theorem. Let
***A*** = <*A*, [?] [?]  *A*>  be
a model of **ZFC**. A model ***B*** =
<*B, E*>  of **ZFC** is said to be a
*proper end-extension* of ***A*** if (i)
***A*** [?] ***B***, (ii)
***A*** [?] ***B***, (iii)
*a* [?] *A, b* [?] *B*, *bEa* =
*b*[?]*A*. Thus a proper end-extension of a model of
**ZFC** is a proper extension in which no "new" element
comes "before" any "old" element. As our application of
**5.5** we prove 



> **5.6 Theorem**. *Each countable
> transitive model of **ZFC** has a proper
> end-extension*. 
> 
> 
> **Proof**. Let ***A*** =
> <*A*, [?] [?]  *A*>  be a transitive model of
> **ZFC** and let
>  L
>  be
> the first-order language of set theory augmented by a name
> **a** for each *a* [?] *A*, and an
> additional constant **c**. Let D be the set of
>  L*A*-sentences
> comprising:
> 
> 
> * all axioms of **ZFC**;
> * **c** [?] **a**, for each *a*
> [?] *A*;
> * [?]*x*(*x* [?] **a**
> -
>  [?]*b*[?]*a* *x* =
> **b**), for each *a* [?] *A*;
> * **a** [?] **b**, for each
> *a* [?] *b* [?] *A*.
> 
> 
> 
> 
> It is easily shown that D is a subset of *A* which is
> definable in ***A*** by a formula of the language
> of set theory. Also, each subset D' [?] D such
> that D' [?] *A* has a model. For the set
> *C* of all *a* [?] *A* for which
> **a** occurs in D' belongs to *A*
> -- since D' does -- and so, if we interpret
> **c** as any member of the (necessarily nonempty) set
> *A [?] C*, then ***A*** is a model of
> D'. Accordingly, (5.5) implies that D has a model
> <*B, E*> . If we interpret each constant **a**
> as the element *a* [?] *A*, then <*B, E*> 
> is a proper end-extension of ***A***. The proof is
> complete.
> 
> 




The reader will quickly see that the first-order compactness theorem
will not yield this result. 


### 5.1 Definition of the Concept of Admissible Set




A nonempty transitive set *A* is said to be *admissible*
when the following conditions are satisfied: 


1. if *a, b* [?] *A*, then {*a, b*}
[?] *A* and [?]*A* [?] *A*;
2. if *a* [?] *A* and *X* [?]
*A* is D0 on *A*, then *X* [?]
*a* [?] *A*;
3. if *a* [?] *A*, *X* [?] *A* is
D0 on *A*, and
[?]*x*[?]*a*[?]*y*(<*x*,*y*>
 [?] *X*), then, for some *b* [?] *A*,
[?]*x*[?]*a*[?]*y*[?]*b*(<*x*,*y*>
[?] *X*).




Condition (ii) -- the D0-*separation scheme* --
is a restricted version of Zermelo's axiom of separation. Condition
(iii) -- a similarly weakened version of the axiom of replacement --
may be called the D0-*replacement scheme*. 




It is quite easy to see that if *A* is a transitive set such
that <*A*, [?] | *A*> is a model of
**ZFC**, then *A* is admissible. More generally,
the result continues to hold when the power set axiom is omitted from
**ZFC**, so that both *H*(o) and
*H*(o1) are admissible. However, since the
latter is uncountable, the Barwise compactness theorem fails to apply
to it.


## 6. Historical and Bibliographical Remarks




SSSS**1** and **2**. Infinitary
propositional and predicate languages seem to have made their first
explicit appearance in print with the papers of Scott and Tarski [1958]
and Tarski [1958]. The completeness theorem for
 L(o1,o), as well as for other
infinitary languages, was proved by Karp [1964]. The Hanf number
calculations for
 L(o1,o) were first performed by
Morley [1965]. The nondefinability of well-orderings in
finite-quantifier languages was proved by Karp [1965] and Lopez-Escobar
[1966]. The interpolation theorem for
 L(o1,o) was proved by
Lopez-Escobar [1965] and Scott's isomorphism theorem for
 L(o1,o) by
Scott [1965]. Negri [2021] extends the idea of geometric logic originating in
topos theory to L(o1,o).




Karp's partial isomorphism theorem was first proved in Karp [1965];
see also Barwise [1973]. Result (2.2) appears in Chang [1968], result
(2.3) in Ellentuck [1976] and result (2.4) in Bell [1981].




SS**3**. Results (3.2) and (3.3) are due to Hanf
[1964], with some refinements by Lopez-Escobar [1966] and Dickmann
[1975], while (3.4) was proved by Tarski. Result (3.5) is due to Scott
[1961], (3.6) to Bell [1970] and [1972]; and (3.7) to Bell [1974].
Measurable cardinals were first considered by Ulam [1930] and Tarski
[1939]. The fact that measurable cardinals are weakly compact was noted
in Tarski [1962].




SS**4**. Concerning the undefinability theorem
for L(o1,o1).
Carol Karp remarks (1964, 166), "At the International Congress
of Logic, Methodology and the Philosophy of Science at Stanford
University in 1960, Dana Scott circulated an outline of a proof of the
impossibility of a complete definable formal system for (g+,
g+) languages with a single two-place predicate symbol in
addition to the equality symbol." Scott never published his
result, and a fully detailed proof first appeared in Karp [1964].
The approach to the theorem adopted here is based on the account given
in Dickmann [1975].




SS**5**. The original motivation for the results
presented in this section came from Kreisel; in his [1965] he pointed
out that there were no compelling grounds for choosing infinitary
formulas solely on the grounds of "length", and proposed instead that
definability or "closure" criteria be employed. Kreisel's suggestion
was taken up with great success by Barwise [1967], where his
compactness theorem was proved. The notion of admissible set is due to
Platek [1966]. Theorem (5.6) is taken from Keisler [1974].




For further reading on the subject of infinitary languages, see Aczel
[1973], Dickmann [1975], Karp [1964], Keisler [1974], and Makkai
[1977]. A useful account of the connection between infinitary
languages and large cardinals can be found in Chapter 10 of Drake
[1974].