On PC∆-classes in the theory of models

Makkai, Mihály (1964) On PC∆-classes in the theory of models. A MAGYAR TUDOMÁNYOS AKADÉMIA MATEMATIKAI KUTATÓ INTÉZETÉNEK KÖZLEMÉNYEI, 9 (1-2). pp. 159-194.

Preview

Text cut_MATKUTINT_1964_1_-_2_pp159_-_194.pdf - Published Version Download (16MB) | Preview

Abstract

In this paper we present some results concerning certain special PC∆-classes.¹ In § 1 we enumerate notations, definitions and some wellknown results to be used in the paper. In § 2 we expose a generalization of a theorem of Kleene [5]. Kleene's theorem asserts the following. Let ∑ be a set of sentences in the first order predicate calculus over a language L containing only finitely many predicate and function symbols and suppose that ∑ satisfies the following conditions: (a) ∑ contains its all consequences, (b) ∑ is recursively enumerable with respect to a natural Gödel numbering. In this case the theory ∑ is „finitely axiomatizable using additional predicate symbols" i.e. we can give a formula F in an enlarged language L' ⊃ L, such that for any formula G of the original language L G is derivable from F if and only if G ∈ ∑. The derivability notion used here is based upon a usual formal system of the first order predicate calculus; the identity symbol is treated as the other predicate symbols. A first step in strengthening Kleene's theorem would be to require from the class of the L-reducts of all models of F to be identical with the class of all models of E in the language L. This strong form is not true, only the weaker statement that an F exists such that the infinite relational systems of the two mentioned classes are the same. We make also a second step in the generalization essential for the applications, namely allow ∑ to contain denumerable infinitely many additional symbols besides the finitely many symbols of L. Our requirement that ∑ is recursively enumerable has t o have the meaning that ∑ is recursively enumerable under a natural Gödel numbering based upon an enumeration of the additional symbols, in which the number of arguments of the i-th predicate is a recursive function of i. In this way we shall introduce the class PC∆ᵣₑc of classes of relational systems as follows. К ∈ PC∆ᵣₑc if К is the class of the L-reducts of the models of a recursively enumerable set ∑ of sentences of an enlarged language L'. The recursive enumeration mentioned in this definition is based upon an enumeration of the symbols of L' as above. So we can formulate our generalization of Kleene's theorem as follows (Theorem 1 in § 2). If L₀ is a finite language, К is a class of relational systems of L₀, and К ∈ PC∆ᵣₑc then K∞ ∈ PC where K∞ is the class of the infinite systems of K. In later sections there will be applications of this theorem. Our proof is based upon the same idea as Kleene's proof, namely we treat formulae as elements which are able to form values of the individual variables by the help of a Gödel numbering. The main point in the construction of the above F is a reproduction of the inductive semantical definition of the notion of a sequence of elements satisfying a formula in a relational system. A trivial example shows that the conclusion К ∈ PC, even if we require ∑ to be a recursive set of sentences of L. However we do not know whether the similar improvements in Corollary 3, 5, 5', 9 hold. Our conjecture is that they do not hold. The main work in Kleene [5] is devoted to a strictly constructive treatment. Kleene proves also a variant of the mentioned theorem for the intuitionistic predicate calculus. Naturally our proof is of no constructive character, consequently our theorem does not imply Kleene's results in a strict sense. Our proof technically differs from Kleene's one. We use Robinson's system as described in [4] to deal with recursive functions and predicates and thus we need to adjoin only eight new symbols to L₀ to get L. In § 3 we introduce the following construction of relational systems. Let L be a language containing only predicate symbols and no function symbols. Let

Actions (login required)

Edit Item