Infinitary Logic

First published Sun Jan 23, 2000; substantive revision Wed Sep 6, 2023

Traditionally, expressions in formal systems have been regarded assignifying finite inscriptions which are—at least inprinciple—capable of actually being written out in primitivenotation. However, the fact that (first-order) formulas may beidentified with natural numbers (via “Gödelnumbering”) and hence with finitesets makes it nolonger necessary to regard formulas as inscriptions, and suggests thepossibility of fashioning “languages” some of whoseformulas would be naturally identified asinfinite sets. A“language” of this kind is called aninfinitarylanguage: in this article I discuss those infinitary languageswhich can be obtained in a straightforward manner from first-orderlanguages by allowing conjunctions, disjunctions and, possibly,quantifier sequences, to be of infinite length. In the course of thediscussion it will be seen that, while the expressive power of suchlanguages far exceeds that of their finitary (first-order)counterparts, very few of them possess the “attractive”features (e.g., compactness and completeness) of thelatter. Accordingly, the infinitary languages that do in fact possessthese features merit special attention.

In §1 the basic syntax and semantics of infinitary languages arelaid down; their expressive power is then displayed by means ofexamples. §2 is devoted to those infinitary languages whichpermit only finite quantifier sequences: these languages turn out tobe relatively well-behaved. §3 is devoted to a discussion ofthecompactness problem for infinitary languages and itsconnection with purely set-theoretical questions concerning“large” cardinal numbers. In §4 an argument issketched which shows that most “infinite quantifier”languages have asecond-order nature and are,ipsofacto, highly incomplete. §5 provides a brief account of acertain special class of sublanguages of infinitary languages forwhich a satisfactory generalization of the compactness theorem can beproved. This section includes a subsection on the definition ofadmissible sets. Historical and bibliographical remarks are providedin §6.

1. Definition and Basic Properties of Infinitary Languages

Given a pair κ, λ of infinite cardinals such that λ≤ κ, we define a class of infinitary languages in each ofwhich we may form conjunctions and disjunctions of sets of formulas ofcardinality < κ, and quantifications over sequences ofvariables of length < λ.

LetL — the (finitary)base language — be an arbitrary but fixed first-orderlanguage with any number of extralogical symbols. The infinitarylanguageL(κ,λ) hasthe followingbasic symbols:

All symbols ofL
A setVar of individual variables, where thecardinality ofVar (written: |Var|)is κ
A logical operator (infinitary conjunction)

The class ofpreformulas ofL(κ,λ) is defined recursively asfollows:

Each formula ofL is apreformula;
if φ and ψ are preformulas, so are φ∧ψ and ¬φ;
if Φ is a set of preformulas such that |Φ| < κ,then Φ is apreformula;
if φ is a preformula andX ⊆Varis such that |X| < λ, then ∃Xφ isa preformula;
all preformulas are defined by the above clauses.

If Φ is a set of preformulas indexed by a setI, sayΦ = {φ_i :i ∈I},then we agree to write Φfor:

_i∈I φ

or, ifI is the set of natural numbers, we write Φ for:

φ₀ ∧φ₁ ∧…

IfX is a set of individual variables indexed by an ordinalα, sayX = {x_ξ : ξ <α}, we agree to write(∃x_ξ)_ξ<αφ for∃Xφ.

The logical operators ∨, →,↔ are defined in the customary manner. We also introduce theoperators (infinitarydisjunction) and ∀ (universal quantification)by

Φ=_df ¬{¬φ : φ ∈ Φ}
∀Xφ =_df ¬∃X¬φ,

and employ similar conventions as for , ∃ .

ThusL(κ,λ) isthe infinitary language obtained fromL by permitting conjunctions and disjunctions of length< κ and quantifications^[1] of length <λ. LanguagesL(κ,ω) are calledfinite-quantifierlanguages, the restinfinite-quantifier languages. ObservethatL(ω,ω) is justL itself.

Notice the followinganomaly which can arise in aninfinitary language but not in a finitary one. In the languageL(ω₁,ω), whichallows countably infinite conjunctions but only finite quantifications,there are preformulas with so many free variables that they cannot be“closed” into sentences ofL(ω₁,ω) by prefixing quantifiers.Such is the case, for example, for theL(ω₁,ω)-preformula

x₀ <x₁ ∧ x₁<x₂ ∧ … ∧ x_n <x_n+1 …,

whereL contains the binaryrelation symbol <. For this reason we make the following

Definition. Aformula ofL(κ,λ) is a preformulawhich contains < λ free variables. The set of all formulas ofL(κ,λ) will bedenoted byForm(L(κ,λ)) or simplyForm(κ,λ) and the set of all sentences bySent(L(κ,λ)) or simplySent(κ,λ).

In this connection, observe that, in general, nothing would be gainedby considering “languages”L(κ,λ) with λ > κ. Forexample, in the “language”L(ω,ω₁), formulas will have onlyfinitely many free variables, while there will be a host of “useless”quantifiers able to bind infinitely many free variables.^[2]

Having defined the syntax ofL(κ,λ), we next sketch itssemantics. Since the extralogical symbols ofL(κ,λ) are just those ofL, and it is these symbols whichdetermine the form of the structures in which a given first-orderlanguage is to be interpreted, it is natural to define anL(κ,λ)-structure to besimply anL-structure. The notionof a formula ofL(κ,λ) beingsatisfied in anL-structureA (by a sequence of elements from the domainofA) is defined in the same inductive manneras for formulas ofL except thatwe must add two extra clauses corresponding to the clauses for Φ and ∃Xφ in thedefinition of preformula. In these two cases we naturally define:

Φ is satisfiedinA (by a given sequence) ⇔ for all φ ∈ Φ, φ is satisfied inA (by the sequence);
∃Xφ is satisfied inA ⇔ there is a sequence of elements from the domain ofA in bijective correspondence withXwhich satisfies φ inA.

These informal definitions need to be tightened up in a rigorousdevelopment, but their meaning should be clear to the reader. Now theusual notions oftruth, validity, satisfiability, andmodel for formulas and sentences ofL(κ,λ) become available. In particular, ifA is anL-structure and σ ∈Sent(κ,λ), we shall writeA ⊨σ forA is a model of σ, and ⊨ σ for σis valid,that is, for allA,A ⊨σ. If Δ ⊆Sent(κ,λ), weshall write Δ ⊨ σ forσis a logical consequence of Δ, that is, eachmodel of Δ is a model of σ.

We now give some examples intended to display the expressive powerof the infinitary languagesL(κ,λ) with κ ≥ω₁. In each case it is well-known that the notion inquestion cannot be expressed in any first-order language.

Characterization of the standard model of arithmeticinL(ω₁,ω). Here thestandardmodel of arithmetic is the structureN =⟨N, +, ·,s, 0⟩, whereN is the setof natural numbers, +, ·, and 0 have their usual meanings, ands is the successor operation. LetL be the first-order language appropriate forN. Then the class ofL-structures isomorphic toN coincideswith the class of models of the conjunction of the followingL(ω₁,ω)sentences (where0 is a name of 0):

_m∈ω_n∈ωs^m0 +sⁿ0 =s^m+n0
_m∈ω_n∈ωs^m0·sⁿ0 =s^m·n0
_m∈ω_n∈ω−{m}s^m0≠sⁿ0
∀x_m∈ωx =s^m0

The termssⁿx are defined recursively by

s⁰x = x
sⁿ⁺¹x = s(sⁿx)

Characterization of the class of all finite sets inL(ω₁,ω).Here the base language has no extralogical symbols. The class of allfinite sets then coincides with the class of models of theL(ω₁,ω)-sentence

_n∈ω∃v₀ …∃v_n∀x(x =v₀ ∨ … ∨x =v_n).

Truth definition inL(ω₁,ω)for a countablebase languageL. LetL be a countable first-orderlanguage (for example, the language of arithmetic or set theory) whichcontains a namen for each natural numbern, and let σ₀, σ₁, …be an enumeration of its sentences. Then theL(ω₁,ω)-formula

Tr(x) =_df _n∈ω (x =n ∧σ_n)

is atruth predicate forL inasmuch as the sentence

Tr(n) ↔σ_n

is valid for eachn.

Characterization of well-orderings inL(ω₁,ω₁). The baselanguageL here includes a binarypredicate symbol ≤. Let σ₁ be the usualL-sentence characterizing linearorderings. Then the class ofL-structures in which the interpretation of ≤ is awell-ordering coincides with the class of models of theL(ω₁,ω₁) sentenceσ = σ₁ ∧σ₂, where

σ₂ =_df(∀v_n)_n∈ω∃x [_n∈ω (x =v_n) ∧_n∈ω(x ≤v_n)].

Notice that the sentence σ₂ contains aninfinitequantifier: it expresses the essentiallysecond-orderassertion that every countable subset has a least member. It can infact be shown that the presence of this infinite quantifier isessential: the class of well-ordered structures cannot be characterizedin any finite-quantifier language. This example indicates thatinfinite-quantifier languages such asL(ω₁,ω₁) behave ratherlike second-order languages; we shall see that they share the latters'defects (incompleteness) as well as some of their advantages (strongexpressive power).

Many extensions of first-order languages can betranslatedinto infinitary languages. For example, consider the generalizedquantifier languageL(Q₀) obtained fromL by adding a new quantifier symbolQ₀ and interpretingQ₀xφ(x) asthere existinfinitely many x such that φ(x). It is easily seenthat the sentenceQ₀xφ(x) hasthe same models as theL(ω₁,ω)-sentence

¬_n∈ω∃v₀…∃v_n∀x[φ(x) → (x = v₀ ∨ … ∨x = v_n)].

ThusL(Q₀)is, in a natural sense, translatable intoL(ω₁,ω). Another languagetranslatable intoL(ω₁,ω) in this sense is theweak second-order language obtained by adding a countable setof monadic predicate variables toL which are then interpreted as ranging over allfinite sets of individuals.

Languages with arbitrarily long conjunctions, disjunctions and(possibly) quantifications may also be introduced. For a fixed infinitecardinal λ, the languageL(∞,λ) is defined by specifying its classof formulas,Form(∞,λ), to be the union,over all κ ≥ λ, of the setsForm(κ,λ). ThusL(∞,λ) allows arbitrarily long conjunctionsand disjunctions, in the sense that if Φ is an arbitrary subset ofForm(∞,λ), then both Φ and Φ are members ofForm(∞,λ). ButL(∞,λ) admits only quantifications oflength < λ: all its formulas have < λ freevariables. The languageL(∞,∞) is defined in turn by specifying itsclass of formulas,Form(∞,∞), to be theunion, over all infinite cardinals λ, of the classesForm(∞,λ). SoL(∞,∞) allows arbitrarily longquantifications in addition to arbitrarily long conjunctions anddisjunctions. Note thatForm(∞,λ) andForm(∞,∞) are proper classes in the senseof Gödel-Bernays set theory. Satisfaction of formulas ofL(∞,λ) andL(∞,∞) in a structure maybe defined by an obvious extension of the corresponding notion forL(κ,λ).

2. Finite-Quantifier Languages

We have remarked that infinite-quantifier languages such asL(ω₁,ω₁) resemblesecond-order languages inasmuch as they allow quantification overinfinite sets of individuals. The fact that this is not permitted infinite-quantifier languages suggests that these may be in certainrespects closer to their first-order counterparts than might be evidentat first sight. We shall see that this is indeed the case, notably inthe case ofL(ω₁,ω).

The languageL(ω₁,ω) occupies a special placeamong infinitary languages because—like first-orderlanguages—it admits an effectivedeductive apparatus. Infact, let us add to the usual first-order axioms and rules of inferencethe new axiom scheme

Φ →φ

for any countable set Φ ⊆Form(ω₁,ω) and any φ ∈Φ, together with the new rule of inference

φ₀, φ₁, …, φ_n, …
_n∈ωφ_n

and allow deductions to be of countable length. Writing ⊢* for deducibility in this sense, wethen have the

L(ω₁,ω)-CompletenessTheorem. For any σ ∈Sent(ω₁,ω), ⊨ σ ⇔ ⊢*σ

As an immediate corollary we infer that this deductive apparatus isadequate for deductions from countable sets of premises inL(ω₁,ω).That is, with the obvious extension of notation, we have, for anycountable set Δ ⊆Sent(ω₁,ω)

(2.1) Δ ⊨σ ⇔ Δ⊢*σ

This completeness theorem can be proved by modifying the usualHenkin completeness proof for first-order logic, or by employingBoolean-algebraic methods. Similar arguments, applied to suitablefurther augmentations of the axioms and rules of inference, yieldanalogous completeness theorems for many other finite-quantifierlanguages.

If just deductions of countable length are admitted, then nodeductive apparatus forL(ω₁,ω) can be set up which isadequate for deductions fromarbitrary sets of premises, thatis, for which (2.1) would hold for every set Δ ⊆Sent(ω₁,ω),regardless ofcardinality. This follows from the simple observation that thereis a first-order languageL andan uncountable set Γ ofL(ω₁,ω)-sentences such thatΓhas no model but every countable subset of Γdoes. To see this, letLbe the language of arithmetic augmented by ω₁ newconstant symbols {c_ξ : ξ< ω₁} and let Γ be the set ofL(ω₁,ω)-sentences {σ} ∪{c_ξ ≠c_η : ξ ≠ η}, whereσ is theL(ω₁,ω)-sentence characterizingthe standard model of arithmetic. This example also shows that thecompactness theorem fails forL(ω₁,ω) and so also for anyL(κ,λ) with κ ≥ω₁.

Another result which holds in the first-order case but fails forL(κ,ω) with κ≥ ω₁ (and also forL(ω₁,ω₁), althoughthis is more difficult to prove) is theprenex normal formtheorem. A sentence isprenex if all its quantifiersappear at the front; we give an example of anL(ω₁,ω)-sentence which is notequivalent to a conjunction of prenex sentences. LetL be the first-order language withoutextralogical symbols and let σ be theL(ω₁,ω)-sentence whichcharacterizes the class of finite sets. Suppose that σ wereequivalent to a conjunction

_i∈Iσ_i

of prenexL(ω₁,ω)-sentencesσ_i. Then each σ_i isof the form

Q₁x₁ …Q_nx_nφ_i(x₁,…,x_n),

where eachQ_k is ∀ or ∃ andφ_i is a (possibly infinitary) conjunction ordisjunction of formulas of the formx_k =x_l orx_k ≠x_l. Since each σ_i is asentence, there are only finitely many variables in eachφ_i, and it is easy to see that eachφ_i is then equivalent to a first-order formula.Accordingly each σ_i may be taken to be afirst-order sentence. Since σ is assumed to be equivalent to theconjunction of the σ_i, it follows thatσ and the set Δ = {σ_i :i ∈I} have the same models. But obviouslyσ, and hence also Δ, have models of all finitecardinalities; the compactness theorem for sets of first-ordersentences now implies that Δ, and hence also σ, has aninfinite model, contradicting the definition of σ.

Turning to theLöwenheim-Skolem theorem, we find thatthedownward version has adequate generalizations toL(ω₁,ω) (and,indeed, to all infinitary languages). In fact, one can show in much thesame way as for sets of first-order sentences that if Δ ⊆Sent(ω₁,ω) has an infinitemodel of cardinality ≥ |Δ|, it has a model of cardinality thelarger of ℵ₀, |Δ|.In particular, anyL(ω₁,ω)-sentence with an infinitemodel has a countable model.

On the other hand, theupward Löwenheim-Skolem theoremin its usual formfails for all infinitary languages. Forexample, theL(ω₁,ω)-sentence characterizingthe standard model of arithmetic has a model of cardinality ℵ₀ but no models of any othercardinality. However, all is not lost here, as we shall see.

We define theHanf numberh(L) of alanguage L to be the least cardinal κ such that, if anL-sentence has a model of cardinality κ, it hasmodels of arbitrarily large cardinality. The existence ofh(L) is readily established. For eachL-sentence σ not possessing models ofarbitrarily large cardinality let κ(σ) be the leastcardinal κ such that σ does not have a model of cardinalityκ. If λ is the supremum of all the κ(σ), then,if a sentence ofL has a model of cardinalityλ, it has models of arbitrarily large cardinality.

Define the cardinals μ(α) recursively by

μ(0) = ℵ₀
μ(α+1) = 2^μ(α)
μ(λ) = ∑_α<λ μ(α),for limit λ.

Then it can be shown that

h(L(ω₁,ω)) =μ(ω₁),

similar results holding for other finite-quantifier languages. Thevalues of the Hanf numbers of infinite-quantifier languages such asL(ω₁,ω₁) are sensitiveto the presence or otherwise of large cardinals, but must in any casegreatly exceed that ofL(ω₁,ω).

A result forL whichgeneralizes toL(ω₁,ω) but to no otherinfinitary language is the

Craig Interpolation Theorem: Ifσ,τ ∈Sent(ω₁,ω)are such that ⊨ σ →τ, then there is θ ∈Sent(ω₁,ω) such that ⊨ σ → θ and ⊨ θ → τ, and eachextralogical symbol occurring in θ occurs in both σ andτ.

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

Finally, we mention one further result which generalizes nicely toL(ω₁,ω)but to no other infinitary language. It is well known that, ifA is any finiteL-structure with only finitely many relations, there isanL-sentence σcharacterizingA up to isomorphism. ForL(ω₁,ω) we havethe following generalization known as

Scott's Isomorphism Theorem. IfA is a countableL-structure with only countably many relations, thenthere is anL(ω₁,ω)-sentence whose class ofcountable models coincides with the class ofL-structures isomorphic withA.

The restriction tocountable structures is essential becausecountability cannot in general be expressed by anL(ω₁,ω)-sentence.

The languageL(∞,ω) may also be counted as afinite-quantifier language. The concept of equivalence of structureswith respect to this language is of especial significance: we call two(similar) structuresA andB (∞,ω)-equivalent,writtenA ≡_∞ωB, if the same sentences ofL(∞,ω) hold in bothA andB. Thisrelation can, first of all, be characterized in terms of the notion ofpartial isomorphism. Apartial isomorphism betweenA andB is anonempty familyP of maps such that:

For eachp ∈P, dom(p) is asubstructure ofA, ran(p) is asubstructure ofB, andp is an isomorphism ofits domain onto its range; and
Ifp ∈P,a ∈A,b ∈B, then there existr,s∈P both extendingp such thata ∈dom(r),b ∈ ran(s) (“back and forth”property).

If a partial isomorphism exists betweenAandB, we say thatA andB arepartially isomorphic and writeA_pB. Wethen have

Karp's Partial Isomorphism Theorem.
For any similar structuresA,B,A≡_∞ωB ⇔A_pB.

There is also a version of Scott's isomorphism theorem forL(∞,ω), namely,

(2.2) Given any structureA,there is anL(∞,ω)-sentence σ such that, for allstructuresB,A_pB ⇔B ⊨ σ.

Partial isomorphism and (∞,ω)-equivalence are related tothe notion ofBoolean isomorphism. To define this we need tointroduce the idea of a Boolean-valued model of set theory. Given acomplete Boolean algebraB, theuniverseV^(B)of B-valued sets, also knownas theB-extension of the universe V of sets, is obtained byfirst defining, recursively on α,

V_α^(B) ={x:x is a function ∧ range(x) ⊆B ∧ ∃ξ<α[domain(x) ⊆V_ξ^(B)]}

and then setting

V^(B) = {x:∃α(x ∈V_α^(B))}.

Members ofV^(B) are calledB-valuedsets. It is now easily seen that aB-valued set isprecisely aB-valued function with domain a set ofB-valued sets. Now letL be the first-orderlanguage of set theory and letL^(B) be the language obtained byadding toL a name for each element ofV^(B) (we shall use the same symbol for theelement and its name). One can now construct a mapping[·]^(B) of the (sentences of the) languageL^(B) intoB: for eachsentence σ ofL^(B), theelement [σ]^(B) ofB is the “Booleantruth value” of σ inV^(B). Thismapping [·]^(B) is defined so as to send allthe theorems of Zermelo-Fraenkel set theory to the top element 1 ofB, i.e., to “truth”; accordingly,V^(B) may be thought of as aBoolean-valued model of set theory. In general, if[σ]^(B) = 1, we say that σ isvalid inV^(B), and writeV^(B) ⊨σ.

Now eachx ∈V has a canonical representativex inV^(B), satisfying

x =y iffV^(B) ⊨x =y
x ∈y iffV^(B) ⊨x ∈y

We say that two similar structuresA,B are Boolean isomorphic, writtenA_bB, if, forsome complete Boolean algebraB, we haveV^(B) ⊨AB, that is, if there is a Booleanextension of the universe of sets in which the canonicalrepresentatives ofA andB are isomorphic with Boolean value 1. It canthen be shown that:

(2.3)A≡_∞ωB ⇔A_bB.

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

There is a “terminal” object 1 such that, for any objectX, there is a unique mapX → 1 (for 1 we maytake any one-element set, in particular, {0}).
Any pair of objectsX,Y has a Cartesian productX×Y.
for any pair of objects one can form the “exponential” objectY^X of all maps fromX →Y.
There is a “truth-value” object Ω such that for each objectX there is a natural correspondence between subobjects(subsets) ofX and mapsX → Ω. (ForΩ we may take the set 2 = {0,1}; mapsX → Ωare thencharacteristic functions onX.)

All four of these conditions can be formulated in category-theoreticlanguage — a category satisfying them is called atopos.The categorySet is a topos; so also are (i) thecategorySet^(B) of Boolean-valuedsets and mappings in any Boolean extensionV^(B) of the universe of sets; (ii) thecategory of sheaves of sets on a topological space; (iii) the categoryof all diagrams of maps of sets

X₀ →X₁ →X₂ → …

The objects of each of these categories may be regarded as setswhich arevarying in some manner: in case (i) over aBoolean algebra; in case (ii) over a topologicalspace; in case (iii) over (discrete) time. A topos may beconceived, then, as a universe of “variable” sets. The familiarcategorySet is the special limiting case of a toposin which the “variation” of the objects has been reduced to zero.

Just as in set theory, “logical operators” can be defined on thetruth-value object in any topos. These are maps ¬: Ω →Ω; ∧, ∨, ⇒: Ω × Ω → Ωcorresponding to the logical operations of negation, conjunction,disjunction and implication. With these operations, Ω becomes aHeyting algebra, thus embodying in general the laws not of classicalbut of intutionistic logic. In this sense intuitionistic logic is“internalized” in a topos: intuitionistic logic is the logic ofvariable sets. (Of course, classical logic is internalized in certaintoposes, for instanceSet andSet^(B) for any complete BooleanalgebraB.)

Any topos may be conceived as possible “universe of discourse” inwhich mathematical assertions may be interpreted and mathematicalconstructions may be performed. Mathematical assertions are renderedinterpretable in a toposE byexpression withinE'sinternal language — a type-theoretic version of theusual language of set theory. In a manner analogous to Boolean-valuedvalidity, one can introduce an appropriate notion of validity inE of a sentence σ of itsinternal language. Again, we writeE ⊨ σ for“σ is valid inE”.

A toposE is said to befull if, for any setI, theI-foldcopower^[3] ∐_I1 of its terminal object exists inE. ∐_I1 may be thought of as thecanonical representative inE ofthe setI; accordingly, we write it simply asI. (InV^(B) this coincideswithI as previously defined.) All the toposesmentioned above are full.

Now letE be a full topos. IfA = (A,R, …) is astructure, writeA for(A,R, …). Two structuresA andB are said tobetopos isomorphic, writtenA_tB, if, for some toposE defined over the category of sets, we haveE ⊨AB. In other words two structures are topos isomorphicif their canonical representatives are isomorphic in the internallanguage of some topos. It can then be shown that

(2.4)A≡_∞ωB ⇔A_tB.

Accordingly (∞,ω)-equivalence may be regarded asisomorphism in the extremely general context of universes of “variable”sets. In this respect (∞,ω)-equivalence is an “invariant”notion of isomorphism.

3. The Compactness Property

As we have seen, the compactness theorem in its usual form fails forall infinitary languages. Nevertheless, it is of some interest todetermine whether infinitary languages satisfy some suitably modifiedversion of the theorem. This so-calledcompactness problemturns out to have a natural connection with purely set-theoreticquestions involving “large” cardinal numbers.

We construct the following definition. Let κ be an infinitecardinal. A languageL is said to beκ-compact (resp.weaklyκ-compact) if whenever Δ is a set ofL-sentences (resp. a set ofL-sentences of cardinality ≤ κ) and eachsubset of Δ of cardinality < κ has a model, so doesΔ. Notice that the usual compactness theorem forL is precisely the assertion thatL is ω-compact. One reason for according significance to the κ-compactness property is the following. CallL κ-complete (resp.weakly κ-complete) if there is a deductive systemP forL with deductions oflength < κ such that, if Δ is aP-consistent^[4] set ofL-sentences (resp. such that |Δ| ≤ κ),then Δ has a model. Observe that such aP will be adequate for deductions fromarbitrary sets of premises (of cardinality ≤ κ) in the senseof §2. It is easily seen that ifL isκ-complete or weakly κ-complete, thenL isκ-compact or weakly κ-compact. Thus, if we can show that agiven language isnot (weakly) κ-compact, then there canbe no deductive system for it with deductions of length < κadequate for deductions from arbitrary sets of premises (of cardinality≤ κ).

It turns out, in fact, that most languagesL(κ,λ) fail to be even weaklyκ-compact, and, for those that are, κ must be anexceedinglylarge cardinal. We shall need somedefinitions.

An infinite cardinal κ is said to beweaklyinaccessible if

(a) λ < κ → λ⁺ <κ, (where λ⁺ denotes the cardinal successor ofλ), and
(b) | I | < κ and λ_i <κ (for alli ∈I) ⇒∑_i∈Iλ_i < κ.

If in addition

(c) λ < κ ⇒ 2^λ <κ,

then κ is said to be (strongly)inaccessible.Since ℵ₀ is inaccessible,it is normal practice to confine attention to those inaccessible, orweakly inaccessible, cardinals that exceed ℵ₀. Accordingly, inaccessible or weaklyinaccessible cardinals will always be taken to beuncountable.It is clear that such cardinals—if they exist—must beextremely large; and indeed the Gödel incompleteness theoremimplies that the existence of even weakly inaccessible cardinals cannotbe proved from the usual axioms of set theory.

Let us call a cardinal κcompact (resp.weaklycompact) if the languageL(κ,κ) is κ-compact (resp. weaklyκ-compact). Then we have the following results:

(3.1) ℵ₀is compact. This is, of course, just a succinct way ofexpressing the compactness theorem for first-order languages.
(3.2) κ isweakly compact ⇒L(κ,ω) isweaklyκ-compact ⇒ κ isweaklyinaccessible. Accordingly, it is consistent (with the usual axiomsof set theory) to assume that no languageL(κ,ω) with κ ≥ ω₁is weakly κ-compact, or,a fortiori, weaklyκ-complete.
(3.3) Suppose κ is inaccessible. Then κ isweaklycompact ⇔ L(κ,ω) isweaklyκ-compact. Also, Also κ is weakly compact ⇒there is a set of κinaccessibles beforeκ. Thus a weakly compact inaccessible cardinal is exceedinglylarge; in particular it cannot be the first, second, …,n^th, … inaccessible.
(3.4) κis compact ⇒ κisinaccessible. (But, by the result immediately above, the conversefails.)

LetConstr stand for Gödel's axiom ofconstructibility; recall thatConstr is consistentwith the usual axioms of set theory.

(3.5)IfConstrholds, thenthere are no compact cardinals.
(3.6)AssumeConstrand letκbe inaccessible. Then κis weaklycompact ⇔L(ω₁,ω)is weaklyκ-compact for allL.
(3.7)IfConstrholds, then there areno cardinals κfor whichL(ω₁,ω)is compact.Accordingly, it is consistent with the usual axioms of set theory tosuppose that there is no cardinal κ such that all languagesL(ω₁,ω) areκ-complete. This result is to be contrasted with the fact thatall first-order languages are ω-complete.

The import of these results is that the compactness theorem failsvery badly for most languagesL(κ,λ) with κ ≥ω₁.

Some historical remarks are in order here. In the 1930smathematicians investigated various versions of the so-calledmeasure problem for sets, a problem which arose in connectionwith the theory of Lebesgue measure on the continuum. In particular,the following very simple notion of measure was formulated. IfX is a set, a (countably additive two-valued nontrivial)measure onX is a map μ on the power setPX to the set {0, 1} satisfying:

(a) μ(X) = 1,
(b) μ({x}) = μ(∅) = 0 for allx∈X, and
(c) ifA is any countable family ofmutually disjoint subsets ofX, then μ(∪A) =∑{μ(Y) :Y ∈A}.

Obviously, whether a given set supports such a measure depends onlyon its cardinality, so it is natural to define a cardinal κ to bemeasurable if all sets of cardinality κ support ameasure of this sort. It was quickly realized that a measurablecardinal must be inaccessible, but the falsity of the converse was notestablished until the 1960s when Tarski showed that measurablecardinals are weakly compact and his student Hanf showed that thefirst, second, etc. inaccessibles are not weakly compact (cf. (3.3)).Although the conclusion that measurable cardinals must be monstrouslylarge is now normally proved without making the detour through weakcompactness and infinitary languages, the fact remains that these ideaswere 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 theGödel completeness theorem which of course says that theset of all valid formulas of any first-order languageL can be generated from a simple setof axioms by means of a few straightforward rules of inference. A majorconsequence of this theorem is that, if the formulas ofL are coded as natural numbers in someconstructive way, then the set of (codes of) valid sentences isrecursively enumerable. Thus, the completeness of afirst-order language implies that the set of its valid sentences isdefinable in a particularly simple way. It would accordinglyseem reasonable, given anarbitrary languageL, to turn this implication around and suggest that,if the set of validL-sentences isnotdefinable in some simple fashion, thenno meaningfulcompleteness result can be established forL, or, aswe shall say, thatL isincomplete. In thissection we are going to employ this suggestion in sketching a proofthat “most”infinite quantifier languages are incomplete inthis sense.

Let us first introduce the formal notion ofdefinability asfollows. IfL is a language,A anL-structure, andX a subset of the domainA ofA, we say thatX isdefinableinA by a formula φ(x,y₁,…,y_n) ofL if there is a sequencea₁,…,a_n of elements ofA such thatX is the subset of all elementsx ∈A for which φ(x,a₁,…,a_n) holds inA.

Now writeVal(L) for the set of all thevalidL-sentences, i.e., those that hold ineveryL-structure. In order to assign a meaning to thestatement “Val(L) is definable”, we have tospecify

a structureC(L)—thecodingstructure forL;
a particular one-one map—thecoding map—ofthe set of formulas ofL into the domain ofC(L).

Then, if we identifyVal(L) with its image inC(L) under the coding map,we shall interpret the statement “Val(L) isdefinable” as the statement “Val(L), regardedas a subset of the domain ofC(L), is definable inC(L) by a formula ofL.”

For example, whenL is the first-order languageL of arithmetic, Gödeloriginally used as coding structure the standard model ofarithmetic ℕ and as coding map the well-knownfunction obtained from the prime factorization theorem for naturalnumbers. The recursive enumerability ofVal(L) then means simply that the set ofcodes (“Gödel numbers”) of members ofVal(L) is definable in ℕ by anL-formula of the form ∃yφ(x, y), where φ(x,y) is a recursive formula.

Another, equivalent, coding structure for the first-order languageof arithmetic is the structure^[5]⟨H(ω), ∈ ⨡H(ω)⟩ ofhereditarily finite sets, where a setx ishereditarily finite ifx, its members, its members ofmembers, etc., are all finite. This coding structure takes account ofthe fact that first-order formulas are naturally regarded as finitesets.

Turning now to the case in whichL is an infinitarylanguageL(κ,λ),what would be a suitable coding structure in this case? We remarked atthe beginning that infinitary languages were suggested by thepossibility of thinking of formulas as set-theoretical objects, so letus try to obtain our coding structure by thinking about what kind ofset-theoretical objects we should take infinitary formulas to be. Giventhe fact that, for eachφ∈Form(κ,λ), φ and itssubformulas, subsubformulas, etc., are all of length <κ,^[6] a moment's reflection reveals thatformulas ofL(κ,λ)“correspond” to setsx hereditarily of cardinality <κ in the sense thatx, its members, its members ofmembers, etc., are all of cardinality < κ. The collection ofall such sets is writtenH(κ).H(ω) isthe collection ofhereditarily finite sets introduced above,andH(ω₁) that of allhereditarilycountable sets.

For simplicity let us suppose that the only extralogical symbol ofthe base languageL is the binarypredicate symbol∈ (the discussion is easily extended tothe case in whichL containsadditional extralogical symbols). Guided by the remarks above, ascoding structure forL(κ,λ) we take the structure,

H(κ)=_df ⟨H(κ), ∈ ⨡H(κ)⟩.

Now we can define the coding map ofForm(κ,λ) intoH(κ). First, to each basic symbols ofL(κ,λ) we assign acode object^⌈s^⌉ ∈H(κ) asfollows. Let {v_ξ: ξ < κ} be anenumeration of the individual variables ofL(κ,λ).

Symbol Code Object Notation
¬ 1 ^⌈¬^⌉
∧ 2 ^⌈∧^⌉
3 ^⌈^⌉
∃ 4 ^⌈∃^⌉
∈ 5 ^⌈∈^⌉
= 6 ^⌈=^⌉
v_ξ ⟨0,ξ⟩ ^⌈v_ξ^⌉

Then, to each φ ∈Form(κ,λ) weassign the code object^⌈φ^⌉ recursively as follows:

^⌈v_ξ =v_η^⌉ =_df ⟨^⌈v_ξ^⌉,^⌈=^⌉,^⌈v_η^⌉⟩,
^⌈v_ξ∈v_η^⌉ =_df ⟨^⌈v_ξ^⌉,^⌈∈^⌉,^⌈v_η^⌉⟩;

for φ, ψ ∈Form(κ,λ),

^⌈φ ∧ ψ^⌉ =_df ⟨^⌈φ^⌉,^⌈∧^⌉,^⌈ψ^⌉⟩
^⌈¬φ^⌉ =_df ⟨^⌈¬^⌉,^⌈φ^⌉⟩
^⌈∃Xφ^⌉ =_df ⟨^⌈∃^⌉, {^⌈x^⌉:x ∈X},^⌈φ^⌉⟩;

and finally if Φ ⊆Form(κ,λ)with |Φ|< κ,

^⌈Φ^⌉ =_df ⟨^⌈^⌉, {^⌈φ^⌉: φ ∈ Φ}⟩.

The map φ ↦^⌈φ^⌉ fromForm(κ,λ) intoH(κ) is easily seen to be one-one and is the requiredcoding map. Accordingly, we agree to identifyVal(L(κ,λ)) with its image inH(κ) under this coding map.

When isVal(L(κ,λ)) adefinable subset ofH(κ)? In order to answer thisquestion we require the following definitions.

AnL-formula is called aΔ₀-formula if it is equivalent to a formulain which all quantifiers are of the form∀x∈y or ∃x∈y(i.e., ∀x(x∈y → …)or ∃x(x∈y ∧ …)). AnL-formula is a Σ₁-formula ifit is equivalent to one which can be built up from atomic formulas andtheir negations using only the logical operators ∧, ∨,∀x∈y, ∃x. A subsetX of a setA is said to be Δ₀ (resp.Σ₁)on A if it is definable in the structure⟨A, ∈ ⨡A⟩ by a Δ₀- (resp.Σ₁-) formula ofL.

For example, if we identify the set of natural numbers with the setH(ω) of hereditarily finite sets in the usual way, thenfor eachX ⊆H(ω) we have:

X is Δ₀ onH(ω)⇔X is recursive
X is Σ₁ onH(ω) ⇔X is recursively enumerable.

Thus the notions of Δ₀- and Σ₁-setmay be regarded as generalizations of the notions ofrecursiveandrecursively enumerable set, respectively.

The completeness theorem forLimplies thatVal(L)— regarded as a subset ofH(ω) — isrecursively enumerable, and hence Σ₁ onH(ω). Similarly, the completeness theorem forL(ω₁,ω) (see§2) implies thatVal(L(ω₁,ω)) — regarded as asubset ofH(ω₁) — isΣ₁ onH(ω₁). However, thispleasant state of affairs collapses completely as soon asL(ω₁,ω₁) is reached.For one can prove

Scott's Undefinability Theorem forL(ω₁,ω₁).Val(L(ω₁,ω₁))is notdefinable inH(ω₁)even by anL(ω₁,ω₁)-formula;hence a fortioriVal(L(ω₁,ω₁))isnot Σ₁onH(ω₁).

This theorem is proved in much the same way as the well-known resultthat the set of (codes of) valid sentences of the second-order languageof arithemeticL² isnot second-order definable in its coding structure ℕ. To get this latter result, one first observes that ℕ is characterized by a singleL²-sentence, and then showsthat, if the result were false, then “truth in ℕ” forL²-sentences would be definable by anL²-formula, therebyviolating Tarski's theorem on the undefinability of truth.

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

(4.1)Characterizability of the coding structureH(ω₁)inL(ω₁,ω₁): there is anL(ω₁,ω₁)-sentenceτ₀ such that, for allL-structuresA,A ⊨ τ₀ ⇔ AH(ω₁).
(4.2)Undefinability of truth forL(ω₁,ω₁)-sentencesin the coding structure: there is noL(ω₁,ω₁)-formulaφ(v₀) such that, for allL(ω₁, ω₁)-sentencesσ,H(ω₁) ⊨ σ↔φ(^⌈σ^⌉).
(4.3)There is a termt(v₀,v₁)ofL(ω₁,ω₁)suchthat, for each pair of sentences σ, τofL(ω₁,ω₁),H(ω₁) ⊨ [t(^⌈σ^⌉,^⌈τ^⌉) =^⌈σ → τ^⌉].

(4.1) is proved by analyzing the set-theoretic definition ofH(ω₁) and showingthat it can be “internally” formulated inL(ω₁,ω₁). (4.2) isestablished in much the same way as Tarski's theorem on theundefinability of truth for first- or second-order languages. (4.3) isobtained by formalizing the definition of the coding map σ ↦^⌈σ^⌉ inL(ω₁,ω₁).

Armed with these facts, we can obtain Scott's undefinability theoremin the following way. Suppose it were false; then there would be anL(ω₁,ω₁)-formulaθ(v₀) such that, for allL(ω₁,ω₁)-sentencesσ,

(4.4)H(ω₁) ⊨ θ(^⌈σ^⌉) iff σ ∈Val(L(ω₁,ω₁)).

Let τ₀ be the sentence given in (4.1). Then we have, forallL(ω₁,ω₁)-sentencesσ,

H(ω₁) ⊨ σ iff (τ₀ →σ) ∈Val(L(ω₁,ω₁)),

so that, by (4.4),

H(ω₁) ⊨ σ iff H(ω₁) ⊨ θ(^⌈τ₀ → σ^⌉).

Ift is the term given in (4.3), it would follow that

H(ω₁) ⊨ σ↔θ(t(^⌈τ₀^⌉,^⌈σ^⌉)).

Now write φ(v₀) for theL(ω₁,ω₁)-formulaθ(t(^⌈τ₀^⌉,^⌈σ^⌉)). Then

H(ω₁) ⊨ σ↔φ(^⌈σ^⌉),

contradicting (4.2), and completing the proof.

ThusVal(L(ω₁,ω₁)) is notdefinableeven by anL(ω₁,ω₁)-formula,soa fortioriL(ω₁,ω₁) isincomplete. Similar arguments show that Scott's undefinability theoremcontinues to hold when ω₁ is replaced by any successorcardinal κ⁺; accordingly the languagesL(κ⁺,κ⁺) are allincomplete.^[7]

5. Sublanguages ofL(ω₁,ω) and the Barwise Compactness Theorem

Given what we now know about infinitary languages, it would seem thatL(ω₁,ω) isthe only one to be reasonably well behaved. On the other hand, thefailure of the compactness theorem to generalize toL(ω₁,ω) in anyuseful fashion is a severe drawback as far as applications areconcerned. Let us attempt to analyze this failure in more detail.

Recall from §4 that we may code the formulas of a first-orderlanguageL as hereditarily finitesets, i.e., as members ofH(ω). In that case each finiteset of (codes of)L-sentences isalso a member ofH(ω), and it follows that thecompactness theorem forL can bestated in the form:

(5.1) If Δ ⊆Sent(L) is such that each subsetΔ₀ ⊆ Δ, Δ₀ ∈H(ω) has a model, so does Δ.

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

(5.2) If Δ ⊆Sent(L) and σ ∈Sent(L) satisfyΔ ⊨ σ, then there is adeductionD of σ from Δ such thatD ∈H(ω).^[8]

In §2 we remarked that the compactness theorem forL(ω₁,ω) failsvery strongly; in fact, we constructed a set Γ ⊆Sent(ω₁,ω) such that

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

Recall also that we introduced the notion ofdeduction inL(ω₁,ω); sincesuch deductions are of countable length it quickly follows from (5.3)that

(5.4) There is a sentence^[9]σ ∈Sent(ω₁,ω) such that Γ ⊨ σ, but there is nodeduction of σ inL(ω₁,ω) fromΓ.

Now the formulas ofL(ω₁, ω) can be coded as membersofH(ω₁), and itis clear thatH(ω₁) is closed under the formation ofcountable subsets and sequences. Accordingly (5.3) and (5.4) may bewritten:

(5.3bis) Each Γ₀ ⊆ Γsuch that Γ₀ ∈H(ω₁) has a model, but Γ doesnot;
(5.4bis) There is a sentence σ ∈Sent(ω₁,ω) such that Γ ⊨ σ, but there is nodeductionD ∈H(ω₁) of σ from Γ.

It follows that (5.1) and (5.2) fail when “L” is replaced by “L(ω₁,ω)” and “H(ω)” by “H(ω₁)”. Moreover, it can be shown thatthe set Γ ⊆Sent(ω₁,ω) in (5.3bis) and (5.4bis) may be taken to beΣ₁ onH(ω₁). Thus thecompactness and generalized completeness theorems fail even forΣ₁-sets ofL(ω₁, ω)-sentences.

We see from (5.4bis) that the reason why the generalizedcompleteness theorem fails for Σ₁-sets inL(ω₁,ω) isthat, roughly speaking,H(ω₁) is not “closed”under the formation of deductions from Σ₁-sets ofsentences inH(ω₁). So in order to remedythis it would seem natural to replaceH(ω₁)by setsA which are, in some sense, closed under the formationof such deductions, and then to consider just those formulas whosecodes are inA.

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

First, we identify the symbols and formulas ofL(ω₁,ω) withtheir codes inH(ω₁), as in §4. For eachcountable transitive^[10] setA, let

L_A =Form(L(ω₁,ω)) ∩A.

We say thatL_A is asublanguage ofL(ω₁,ω) if thefollowing conditions are satisfied:

L ⊆L_A
if φ, ψ ∈L_A, then φ ∧ ψ ∈L_A and ¬φ ∈L_A
if φ ∈L_A andx ∈A,then ∃xφ ∈L_A
if φ(x) ∈L_A andy ∈A,then φ(y) ∈L_A
if φ ∈L_A, every subformula of φ is inL_A
if Φ ⊆L_A and Φ ∈A, then Φ ∈L_A.

The notion of deduction inL_A is defined in the customary way;if Δ is a set of sentences ofL_A and φ ∈L_A, then adeduction of φ from Δ inL_A is a deduction of φ fromΔ inL(ω₁,ω) every formula of which is inL_A. We say that φ isdeducible from Δ inL_A if there is a deductionD of φ from Δ inL_A; under theseconditions we write Δ ⊢_A φ. In general,D will not be a member ofA; inorder to ensure that such a deduction can be found inA itwill be necessary to impose further conditions onA.

LetA be a countable transitive set such thatL_A is asublanguage ofL(ω₁, ω) and let Δ be a setof sentences ofL_A. We say thatA (or, byabuse of terminology,L_A) is Δ-closed if,for any formula φ ofL_A such that Δ ⊢_A φ, there is adeductionD of φ from Δ such thatD ∈A. It can be shown that theonly countable language which is Δ-closed forarbitraryΔ is the first-order languageL, i.e., whenA =H(ω). HoweverJ. Barwise discovered that there are countable setsA ⊆H(ω₁) whose corresponding languagesL_A differ fromL and yet are Δ-closedfor all Σ₁-sets of sentencesΔ. Such setsA are calledadmissible sets;roughly speaking, they are extensions of the hereditarily finite setsin 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.LetAbe a countable admissible set and let Δbe a setof sentences ofL_Awhich isΣ₁on A.If each Δ′⊆ Δsuch that Δ′ ∈ Ahas amodel, then so does Δ.

The presence of “Σ₁” here indicates that this theoremis a generalization of the compactness theorem forrecursivelyenumerable sets of sentences.

Another version of the Barwise compactness theorem, useful forconstructing models of set theory, is the following. LetZFC be the usual set of axioms for Zermelo-Fraenkelset theory, including the axiom of choice. Then we have:

5.5 Theorem.Let A be a countabletransitive set such thatA = ⟨A,∈ ⨡A⟩is a model ofZFC.If Δis a set of sentences ofL_Awhich isdefinable inA by a formula of the language of settheory and if each Δ′ ⊆ Δsuchthat Δ′ ∈A has a model, so doesΔ.

To conclude, we give a simple application of this theorem. LetA = ⟨A, ∈ ⨡A⟩ bea model ofZFC. A modelB =⟨B, E⟩ ofZFC is said to be aproper end-extension ofA if (i)A ⊆B, (ii)A ≠B, (iii)a ∈A, b ∈B,bEa ⇒b∈A. Thus a proper end-extension of a model ofZFC is a proper extension in which no “new” elementcomes “before” any “old” element. As our application of5.5 we prove

5.6 Theorem.Each countabletransitive model ofZFC has a properend-extension.
Proof. LetA =⟨A, ∈ ⨡A⟩ be a transitive model ofZFC and letL bethe first-order language of set theory augmented by a namea for eacha ∈A, and anadditional constantc. Let Δ be the set ofL_A-sentencescomprising:
all axioms ofZFC;
c ≠a, for eacha∈A;
∀x(x∈a→_b∈ax =b), for eacha ∈A;
a∈b, for eacha ∈b ∈A.
It is easily shown that Δ is a subset ofA which isdefinable inA by a formula of the languageof set theory. Also, each subset Δ′ ⊆ Δ suchthat Δ′ ∈A has a model. For the setC of alla ∈A for whicha occurs in Δ′ belongs toA— since Δ′ does — and so, if we interpretc as any member of the (necessarily nonempty) setA − C, thenA is a model ofΔ′. Accordingly, (5.5) implies that Δ has a model⟨B, E⟩. If we interpret each constantaas the elementa ∈A, then ⟨B, E⟩is a proper end-extension ofA. The proof iscomplete.

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

5.1 Definition of the Concept of Admissible Set

A nonempty transitive setA is said to beadmissiblewhen the following conditions are satisfied:

ifa, b ∈A, then {a, b}∈A and ∪A ∈A;
ifa ∈A andX ⊆A is Δ₀ onA, thenX ∩a ∈A;
ifa ∈A,X ⊆A isΔ₀ onA, and∀x∈a∃y(<x,y> ∈X), then, for someb ∈A,∀x∈a∃y∈b(<x,y>∈X).

Condition (ii) — the Δ₀-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 Δ₀-replacement scheme.

It is quite easy to see that ifA is a transitive set suchthat <A, ∈ |A> is a model ofZFC, thenA is admissible. More generally,the result continues to hold when the power set axiom is omitted fromZFC, so that bothH(ω) andH(ω₁) are admissible. However, since thelatter is uncountable, the Barwise compactness theorem fails to applyto it.

6. Historical and Bibliographical Remarks

§§1 and2. Infinitarypropositional and predicate languages seem to have made their firstexplicit appearance in print with the papers of Scott and Tarski [1958]and Tarski [1958]. The completeness theorem forL(ω₁,ω), as well as for otherinfinitary languages, was proved by Karp [1964]. The Hanf numbercalculations forL(ω₁,ω) were first performed byMorley [1965]. The nondefinability of well-orderings infinite-quantifier languages was proved by Karp [1965] and Lopez-Escobar[1966]. The interpolation theorem forL(ω₁,ω) was proved byLopez-Escobar [1965] and Scott's isomorphism theorem forL(ω₁,ω) byScott [1965]. Negri [2021] extends the idea of geometric logic originating intopos theory toL(ω₁,ω).

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].

§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 notedin Tarski [1962].

§4. Concerning the undefinability theoremforL(ω₁,ω₁).Carol Karp remarks (1964, 166), “At the International Congressof Logic, Methodology and the Philosophy of Science at StanfordUniversity in 1960, Dana Scott circulated an outline of a proof of theimpossibility of a complete definable formal system for (γ+,γ+) languages with a single two-place predicate symbol inaddition to the equality symbol.” Scott never published hisresult, and a fully detailed proof first appeared in Karp [1964].The approach to the theorem adopted here is based on the account givenin Dickmann [1975].

§5. The original motivation for the resultspresented in this section came from Kreisel; in his [1965] he pointedout that there were no compelling grounds for choosing infinitaryformulas solely on the grounds of “length”, and proposed instead thatdefinability or “closure” criteria be employed. Kreisel's suggestionwas taken up with great success by Barwise [1967], where hiscompactness theorem was proved. The notion of admissible set is due toPlatek [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 infinitarylanguages and large cardinals can be found in Chapter 10 of Drake[1974].

Bibliography

Aczel, P., 1973, “Infinitary Logic and the BarwiseCompactness Theorem”,Proceedings of the 1971 BertrandRussell Memorial Logic Conference (Uldum, Denmark), J. Bell,J. Cole, G. Priest, and A. Slomson (eds.), Leeds: Bertrand RussellMemorial Logic Conference, 234–277.
Barwise, J., 1967,Infinitary Logic and Admissible Sets.Ph.D. Thesis, Stanford University.
–––, 1973, “Back and Forth throughInfinitary Logic. Studies in Model Theory”, inStudies inMathematics (Volume 8), Buffalo: Mathematical Association ofAmerican, pp. 5–34.
–––, 1975,Admissible Sets andStructures, Berlin: Springer-Verlag.
Barwise, J. and S. Feferman (eds.), 1985,Handbook of Model-Theoretic Logics, New York:Springer-Verlag.
Baumgartner, J., 1974, “The Hanf number for completeL_ω₁,ωsentences (without GCH)”,Journal of Symbolic Logic, 39: 575–578.
Bell, J. L., 1970, “Weak Compactness in RestrictedSecond-Order Languages”,Bulletin of the Polish Academy ofSciences, 18: 111–114.
–––, 1972, “On the Relationship betweenWeak Compactness inL_{ω₁, ω},L_{ω₁, ω₁}, and Restricted Second-Order Languages”,Archive for Mathematical Logic, 15: 74–78.
–––, 1974, “On CompactCardinals”,Zeitschrift für Mathematical Logik undGrundlagen der Mathematik, 20: 389–393.
–––, 1981, “Isomorphism of Structures inS-toposes”,Journal of Symbolic Logic, 43 (3):449–459.
Chang, C.C., 1968, “Some Remarks on the Model Theory ofInfinitary Languages”. inThe Syntax and Semantics ofInfinitary Languages (Lecture Notes in Mathematics: Volume 72),J. Barwise (ed.), Springer-Verlag, Berlin, 36-63.
Dickmann, M. A., 1975,Large Infinitary Languages,Amsterdam: North-Holland.
Drake, F.R., 1974,Set Theory: An Introduction to LargeCardinals, Amsterdam: North-Holland Publishing Company.
Ellentuck, E., 1976, “CategoricityRegained”,Journal of Symbolic Logic, 41 (3):639–643.
Hanf, W. P., 1964,Incompactness in Languages with InfinitelyLong Expressions, Amsterdam: North-Holland.
Karp, C., 1964,Languages with Expressions of InfiniteLength, Amsterdam: North-Holland.
–––, 1965, “Finite-QuantifierEquivalence” inThe Theory of Models, J. Addison,L. Henkin, and A. Tarski (eds.), Amsterdam: North-Holland,407–412.
Keisler, H. J., 1974,Model Theory for Infinitary Logic,Amsterdam: North-Holland.
Keisler, H. J., and Julia F. Knight, 2004, “Barwise:Infinitary Logic And Admissible Sets”,Journal of SymbolicLogic, 10(1): 4–36
Kolaitis, P. and M. Vardi, 1992, “Fixpoint Logicvs. Infinitary Logic in Finite-Model Theory,”Proceedings ofthe Seventh Annual IEEE Symposium on Logic in Computer Science (LICS'92), IEEE, pp. 46-57;available online,doi:10.1109/LICS.1992.185518
Kreisel, G., 1965, “Model-Theoretic Invariants, Applications toRecursive and Hyperarithmetic Operations”, inThe Theory ofModels, J. Addison, L. Henkin, and A. Tarski (eds.), Amsterdam:North-Holland, 190-205.
Kueker, D., 1975, “Back-and-forth arguments in infinitary languages”, inInfinitary Logic: In Memoriam Carol Karp (Lecture Notes in Mathematics: Volume 492), D. Kueker (ed.), Berlin: Springer-Verlag.
Lopez-Escobar, E. G. K., 1965, “An Interpolation Theorem forInfinitely Long Sentences”,Fundamenta Mathematicae,57: 253–272.
–––, 1966, “On DefiningWell-Orderings”,Fundamenta Mathematicae, 59:13–21.
Makkai, M., 1977, “Admissible Sets and Infinitary Logic”,Handbook of Mathematical Logic, J. Barwise (ed.), Amsterdam:North-Holland, 233-282.
Morley, M., 1965, “Omitting Classes ofElements”,The Theory of Models, J. Addison, L. Henkin,and A. Tarski (eds.), Amsterdam: North-Holland, 265-273.
Nadel, M., 1985,“L_ω₁,ωand Admissible Fragments”, in J. Barwise and S. Feferman (eds.)1985, 271–287.
Negri, Sara, 2021, “Geometric Rules in InfinitaryLogic”, in O. Arieli and A. Zamansky (eds.),Arnon Avron onSemantics and Proof Theory of Non-Classical Logics, Cham: Springer,265–293. doi:10.1007/978-3-030-71258-7_12
Platek, R., 1966,Foundations of Recursion Theory, Ph.D.Thesis, Stanford University.
Scott, D., 1961, “Measurable Cardinals and ConstructibleSets”,Bulletin of the Academy of Polish Sciences, 9:521–524.
–––, 1965, “Logic with Denumerably LongFormulas and Finite Strings of Quantifiers”,The Theory ofModels, J. Addison, L. Henkin, and A. Tarski (eds.), Amsterdam:North-Holland, 329-341.
Scott, D., and A. Tarski, 1958, “The sentential calculuswith infinitely long expressions”,ColloquiumMathematicum, 16: 166–170.
Shelah, Saharon, 2012, “Nice infinitarylogics”,Journal of the American Mathematical Society,25: 395-427,available online,doi:10.1090/S0894-0347-2011-00712-1
Tarski, A., 1939, “Ideale in völlständingenMengenkörpern I”,Fundamenta Mathematicae, 32:140–150.
–––, 1958, “Remarks on predicate logicwith infinitely long expressions”,ColloquiumMathematicum, 16: 171–176.
–––, 1962, “Some problems and resultsrelevant to the foundations of set theory”, in E, Nagel,P. Suppes and A. Tarski (eds.),Logic, Methodology and Philosophy ofScience, Stanford: Stanford University Press, 123-135.
Ulam, S., 1930, “Zur Masstheorie in der algemeinen Mengenlehre”,Fundamenta Mathematicae, 16: 140–150.

Academic Tools

How to cite this entry.
Preview the PDF version of this entry at theFriends of the SEP Society.
Look up topics and thinkers related to this entry at the Internet Philosophy Ontology Project (InPhO).
Enhanced bibliography for this entryatPhilPapers, with links to its database.

Other Internet Resources

A Primer on Infinitary Logic, by David Marker (Mathematics, Statistics, and Computer Science, University of Illinois/Chicago).

Open access to the SEP is made possible by a world-wide funding initiative.
The Encyclopedia Now Needs Your Support
Please Read How You Can Help Keep the Encyclopedia Free

Browse

About

Support SEP

Mirror Sites

View this site from another server:

USA (Main Site)Philosophy, Stanford University

Info about mirror sites

Library of Congress Catalog Data: ISSN 1095-5054

Movatterモバイル変換