Traditionally, expressions in formal systems have been regarded as signifying finite inscriptions which are—at least in principle—capable of actually being written out in primitive notation. However, the fact that (first-order) formulas may be identified with natural numbers (via “Gödel numbering”) and hence with finite sets makes it no longer necessary to regard formulas as inscriptions, and suggests the possibility of fashioning “languages” some of whose formulas would be naturally identified as infinite sets. A “language” of this kind is called an infinitary language: in this article I discuss those infinitary languages which can be obtained in a straightforward manner from first-order languages by allowing conjunctions, disjunctions and, possibly, quantifier sequences, to be of infinite length. In the course of the discussion it will be seen that, while the expressive power of such languages far exceeds that of their finitary (first-order) counterparts, very few of them possess the “attractive” features (e.g., compactness and completeness) of the latter. Accordingly, the infinitary languages that do in fact possess these features merit special attention.
In §1 the basic syntax and semantics of infinitary languages are laid down; their expressive power is then displayed by means of examples. §2 is devoted to those infinitary languages which permit only finite quantifier sequences: these languages turn out to be relatively well-behaved. §3 is devoted to a discussion of the compactness problem for infinitary languages and its connection with purely set-theoretical questions concerning “large” cardinal numbers. In §4 an argument is sketched which shows that most “infinite quantifier” languages have a second-order nature and are, ipso facto, highly incomplete. §5 provides a brief account of a certain special class of sublanguages of infinitary languages for which a satisfactory generalization of the compactness theorem can be proved. This section includes a subsection on the definition of admissible sets. Historical and bibliographical remarks are provided in §6.6. Historical and Bibliographical Remarks
Bibliography
Academic Tools
Other Internet Resources
Related Entries
[size=30]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 of which we may form conjunctions and disjunctions of sets of formulas of cardinality < κ, and quantifications over sequences of variables of length < λ.
Let L — the (finitary)
base language — be an arbitrary but fixed first-order language with any number of extralogical symbols. The infinitary language L(κ,λ) has the following
basic symbols:
[/size]
- All symbols of L
- A set Var of individual variables, where the cardinality of Var (written: |Var|) is κ
- A logical operator [size=undefined]∧[/size] (infinitary conjunction)
[size]
The class of
preformulas of L(κ,λ) is defined recursively as follows:
[/size]
- Each formula of L is a preformula;
- if φ and ψ are preformulas, so are φ∧ψ and ¬φ;
- if Φ is a set of preformulas such that |Φ| < κ, then [size=undefined]∧[/size]Φ is a preformula;
- if φ is a preformula and X ⊆ Var is such that |X| < λ, then ∃Xφ is a preformula;
- all preformulas are defined by the above clauses.
[size]
If Φ is a set of preformulas indexed by a set
I, say Φ = {φ
i :
i ∈
I}, then we agree to write [size=undefined]∧[/size]Φ for:
[/size]
- اقتباس :
- [size=undefined]∧[/size]i∈I φ
[size]
or, if
I is the set of natural numbers, we write [size=undefined]∧[/size]Φ for:
[/size]
- اقتباس :
- φ0 ∧ φ1 ∧ …
[size]
If
X is a set of individual variables indexed by an ordinal α, say
X = {
xξ : ξ < α}, we agree to write (∃
xξ)
ξ<αφ for ∃
Xφ.
The logical operators ∨, →, ↔ are defined in the customary manner. We also introduce the operators [size=undefined]∨[/size] (
infinitary disjunction) and ∀ (
universal quantification) by
[/size]
- اقتباس :
- [size=undefined]∨[/size]Φ =df ¬[size=undefined]∧[/size]{ ¬φ : φ ∈ Φ}
∀Xφ =df ¬∃X¬φ,
[size]
and employ similar conventions as for [size=undefined]∧[/size], ∃ .
Thus L(κ,λ) is the infinitary language obtained from L by permitting conjunctions and disjunctions of length < κ and quantifications
[1] of length < λ. Languages L(κ,ω) are called
finite-quantifierlanguages, the rest
infinite-quantifier languages. Observe that L(ω,ω) 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(ω
1,ω), 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(ω
1,ω) by prefixing quantifiers. Such is the case, for example, for the L(ω
1,ω)-preformula
[/size]
- اقتباس :
- x0 < x1 ∧ x1 < x2 ∧ … ∧ xn < xn+1 …,
[size]
where L contains the binary relation symbol <. For this reason we make the following
[/size]
- اقتباس :
- Definition. A formula of L(κ,λ) is a preformula which contains < λ free variables. The set of all formulas of L(κ,λ) will be denoted by Form(L(κ,λ)) or simply Form(κ,λ) and the set of all sentences by Sent(L(κ,λ)) or simply Sent(κ,λ).
[size]
In this connection, observe that, in general, nothing would be gained by considering “languages”L(κ,λ) with λ > κ. For example, in the “language” L(ω,ω
1), 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(κ,λ), we next sketch its
semantics. Since the extralogical symbols of 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(κ,λ)-structure to be simply an L-structure. The notion of a formula of 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 [size=undefined]∧[/size]Φ and ∃Xφ in the definition of preformula. In these two cases we naturally define:
[/size]
- اقتباس :
- [size=undefined]∧[/size]Φ is satisfied in A (by a given sequence) ⇔ for all φ ∈ Φ, φ is satisfied in A (by the sequence);
∃Xφ is satisfied in A ⇔ there is a sequence of elements from the domain of A in bijective correspondence with X which satisfies φ in A.
[size]
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
modelfor formulas and sentences of L(κ,λ) become available. In particular, if
A is an L-structure and σ ∈
Sent(κ,λ), we shall write
A ⊨ σ for
A is a model of σ, and ⊨ σ for σ
is valid, that is, for all
A,
A⊨ σ. If Δ ⊆
Sent(κ,λ), we shall write Δ ⊨ σ for σ
is a logical consequence of Δ, that is, each model of Δ is a model of σ.
We now give some examples intended to display the expressive power of the infinitary languagesL(κ,λ) with κ ≥ ω
1. 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(ω
1,ω). 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(ω
1,ω) sentences (where
0 is a name of 0):
[/size]
- اقتباس :
- [size=undefined]∧[/size]m∈ω [size=undefined]∧[/size]n∈ω sm0 + sn0 = sm+n0
[size=undefined]∧[/size]m∈ω [size=undefined]∧[/size]n∈ω sm0 · sn0 = sm·n0
[size=undefined]∧[/size]m∈ω [size=undefined]∧[/size]n∈ω−{m} sm0 ≠ sn0
∀x[size=undefined]∨[/size]m∈ω x = sm0
[size]
The terms
snx are defined recursively by
[/size]
- اقتباس :
[size]
Characterization of the class of all finite sets in L(ω
1,ω). Here the base language has no extralogical symbols. The class of all finite sets then coincides with the class of models of theL(ω
1,ω)-sentence
[/size]
- اقتباس :
- [size=undefined]∨[/size]n∈ω ∃v0 … ∃vn∀x(x = v0 ∨ … ∨ x = vn).
[size]
Truth definition in L(ω
1,ω)
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 σ
0, σ
1, … be an enumeration of its sentences. Then the L(ω
1,ω)-formula
[/size]
- اقتباس :
- Tr(x) =df [size=undefined]∨[/size]n∈ω (x = n ∧ σn)
[size]
is a
truth predicate for L inasmuch as the sentence
[/size]
- اقتباس :
- Tr(n) ↔ σn
[size]
is valid for each
n.
Characterization of well-orderings in L(ω
1,ω
1). The base language L here includes a binary predicate symbol ≤. Let σ
1 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(ω
1,ω
1) sentence σ = σ
1 ∧ σ
2, where
[/size]
- اقتباس :
- σ2 =df (∀vn)n∈ω ∃x [[size=undefined]∨[/size]n∈ω (x = vn) ∧ [size=undefined]∧[/size]n∈ω (x ≤ vn)].
[size]
Notice that the sentence σ
2 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(ω
1,ω
1) 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(
Q0) obtained from L by adding a new quantifier symbol
Q0 and interpreting
Q0xφ(
x) as
there exist infinitely many x such that φ(
x). It is easily seen that the sentence
Q0xφ(
x) has the same models as the L(ω
1,ω)-sentence
[/size]
- اقتباس :
- ¬[size=undefined]∨[/size]n∈ω ∃v0…∃vn∀ x[φ(x) → (x = v0 ∨ … ∨ x = vn)].
[size]
Thus L(
Q0) is, in a natural sense, translatable into L(ω
1,ω). Another language translatable intoL(ω
1,ω) 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 λ, the language L(∞,λ) is defined by specifying its class of formulas,
Form(∞,λ), to be the union, over all κ ≥ λ, of the sets
Form(κ,λ). Thus L(∞,λ) allows arbitrarily long conjunctions and disjunctions, in the sense that if Φ is an arbitrary subset of
Form(∞,λ), then both [size=undefined]∧[/size]Φ and [size=undefined]∨[/size]Φ are members of
Form(∞,λ). But L(∞,λ) admits only quantifications of length < λ: all its formulas have < λ free variables. The language L(∞,∞) is defined in turn by specifying its class of formulas,
Form(∞,∞), to be the union, over all infinite cardinals λ, of the classes
Form(∞,λ). So L(∞,∞) allows arbitrarily long quantifications in addition to arbitrarily long conjunctions and disjunctions. Note that
Form(∞,λ) and
Form(∞,∞) are proper classes in the sense of Gödel-Bernays set theory. Satisfaction of formulas of L(∞,λ) and L(∞,∞) in a structure may be defined by an obvious extension of the corresponding notion forL(κ,λ).[/size]