Annual Meeting of the Association for Symbolic Logic: Philadelphia 1981
S OF PAPERS 457 is only provable if one of the alternatives is provable, and so, by G6del's construction of formally undecidable formulae (x)A(x) with primitive recursive A, each of the systems considered contains A for which -n(x)A(x) -+ (Ex)-nA(x) is not provable. Corollary. Consider Heyting's predicate calculus (HPC) and define strong completeness as follows; for all formulae 9f of HPC, if P1, ..., Pk are the predicate symbols of .(PL., Pk), and if, for all domains of individuals and predicates Pi* defined there, .(PL*, . Pk*) holds then the formula ?(PL, . . ., Pk) is provable in HPC. Gbdel observed (personal communication) that if strong completeness of HPC is intuitionistically provable, then so is -,(x)A (x) -> (Ex) -nA (x) for each primitive recursive A. Thus, strong completeness of HPC is not provable in HA, and since (IA) contains the fan theorem it is not even provable by means of the latter. Note that our nonderivability result for HA cannot be obtained by means of the (classical) realizability interpretation nor by G6del's interpretation (IN, para. 3) since the implication is true for each primitive recursive A on both interpretations. ROBERT MCNAUGHTON. Logical problems in the description of the behavior of automata. The behavior of an automaton, as opposed to its structure, deals with the relation between inputs and outputs; more precisely, the exact manner in which the inputs determine the outputs. In this talk I investigate the capability of several languages for describing the behavior of automata. Some of these languages are in the form of symbolic logic; others are not. Some theorems are proved about the adequacy of these languages, and problems for future logical research are pointed out. ALAN Ross ANDERSON and NUEL D. BELNAP, Jr. A modification of Ackermann's "rigorous implication". Following a suggestion of Feys, we thus translate Ackermann's strenge Implikation (XXII 327). We consider three systems, all of which we take to be contributions to the problem of formalizing entailment: Ackermann's system II', consisting of his axioms (1)(15), rules (c) -(6); Ackermann's H", got by adding axioms (16)(17) and rule (e) to II'; and a new system E (for "entailment"), consisting of axioms (2)(15) together with (1') (((A A) & (B B)) C) C, and rules (c) (modus ponens for ->), and (i) (adjunction). (I) Two remarks of Ackermann require correction. A theory of modality equivalent to that of II" is available in II', the required definition of impossibility UA being A -> A -> A; hence (16)(17) and (e) are unnecessary. And MMA -> MA is provable in all three systems. So also in fact is M.MA 4-* M-MM.MA, whence it follows by an argument of Parry (V 37) that the three systems distinguish just those fourteen modalities distinguished by S4. (II) None of the three systems contains or is contained in any of the following: SI, S2, S3, M (Feys-von Wright), but all three are contained in S4. Adding B -> (A -> A) to any of the systems yields S4. (III) E contains the full two-valued system (with A : B defined as A v B), and has as derived rules (6) and a rule of necessitation. E has the same theorems as II' without (y) (though adding (y) to E does not yield II'). (IV) Define proof that A entails B as a proof of B from hypothesis A which satisfies the following conditions: (a) stars can be prefixed to steps of the proof as required by the following rules: (i) the hypothesis is starred; (ii) a step introduced as an axiom is not starred; (iii) the conclusion of an application of (a) is starred if and only if at least one premiss is starred; (iv) the conclusion of an application of (i) is starred if both premisses are starred, and unstarred if both premisses are unstarred (and no use of (i) has one premiss starred and the other unstarred); 458 ABSTRACTS OF PAPERS and (b), in consequence of the rules of (a), B has a star. (The conditions are designed to explicate what we might mean by saying that B "really depends on" A (Ackermann's logischer Zusammenhang).) Our principal interest in E (as opposed to II' and fI") is that for E we have the following: Entailment theorem. F A -+ B if and only if there is a proof that A entails B. J. W. ADDISON. Some consequences of the axiom of constructibility. (The abstract has already appeared in Notices of the American Mathematical Society, Vol. 5, December 1958, p. 845.) RAYMOND M. SMULLYAN. Theories with effectively inseparable nuclei. We shall refer to the set of G6del numbers of the provable sentences and the set of G6del numbers of the refutable sentences of a theory T as the nuclei of T. We call T a Rosser theory iff every disjoint pair (A, B) of r.e. sets is strongly separable in the theory, in the sense that there exists a formula F(x) such that for every n E A, F(n) is provable, and for every n E B, F(n) is refutable in T. It is easy to show that the nuclei of a Rosser theory are recursively inseparable in fact effectively inseparable; a fortiori every Rosser theory is essentially creative (i.e. all its consistent extensions are creative). In fact we easily prove the stronger theorem "Let (A, B) be strongly separable in T. Then (1) If (A, B) are recursively inseparable, so are the nuclei of T; (2) If (A, B) are effectively inseparable, so are the nuclei of T." [This theorem is a strengthening of Kleene's symmetric form of Godel's theorem; it is also a strengthening of a result of Feferman this JOURNAL, vol. 22 (1957), page 170, Corollary 3.] We show that if T, is interpretable or relatively interpretable in T2 then: (1) If T1 has recursively inseparable nuclei, so does T2; (2) Likewise with "effectively inseparable." [Two sets a. and P are called effectively inseparable iff there exists a recursive function f(x, y) such that for any two numbers i and j which are indices of disjoint r.e. supersets Ad and cw1 of a and fi, f(i, j) is outside both coi and Wp.] By our methods, many theories shown by Tarski to be essentially undecidable, and subsequently shown by Feferman to be essentially creative, can now be shown to have effectively inseparable nuclei. In particular, the elementary theories of nondensely ordered rings and non-densely ordered commutative rings (with or without unit) have effectively inseparable nuclei. ANDRZEJ MOSTowsKI and CZESLAW RYLL-NARDZEWSKI. Representability of sets in models of axiomatic theories. Let S be a consistent axiomatizable theory with standard formalization and {Fn(x)} a recursive sequence of formulas of S with one free variable x. For any model M of S and any a in M write StsfMFn(a) if a satisfies F,(x) in M. Call a set X of integers representable in M by a with respect to the sequence {Fn(x)} if n E X StsfMF.(a). THEOREM 1: For every sequence Xj of non-recursive sets {Xj} there is a model M of S in which none of the sets X; is representable by any a in M with respect to any recursive sequence {F,(x)}. This theorem is proved by considering the space i consisting of prime ideals of the Lindenbaum algebra of S and by showing that those ideals which determine models with the required property form a residual GS-set in S. Let G, be a recursive sequence of closed formulas. Call a set X of integers definable in S with respect to the sequence {GJ} if n E X -[G, is provable in S]. From theorem 1 one obtains immediately THEOREM 2: For every sequence {Xj} of non-recursive sets there is a consistent extension S' of S such that none of the sets Xj is definable in S' with respect to any recursive sequence {GJ}. Theorem 1 was proved by the first author for a single set X2, a particular system S and a particular sequence {Fn(x)}; the generalization and the proof using topological methods were obtained by the second author. ABSTRACTS OF PAPERS 459S OF PAPERS 459 DANIEL LACOMBE. A convenient definition for f/nctionals. Let F., be the set of all functions of p non-negative integers with non-negative integers values, PF, the set of all partial functions of p variables, FF2, the set of all partial functions of p variables with finite domains of definition. Using certain subsets of FFa x ... x FF, x FFm (where possibly some of the a, . . .,1, m are null) we define: (A) the pseudo-functionals (which involve possible contradictions); (B) the functionals (which are the same as the consistent pseudo-functionals, and are continuous mappings of PFa x ... x PF1 into PFm); (C) the totally functionalizing functionals (which induce continuous mappings of Fa x ... x F, into Fm); (A'), (B'), (C') respectively obtained from (A),. (B), (C) by adding a recursivity condition; and (D) the restricted recursive functionals (among which are most of the usual recursive functionals, for instance the Iu-schema). (A') [(B')] are equivalent to partial recursive [everywhere defined] functionals in the sense of KLEENE. We study these different classes and their applications, and give a normal form for (B'). This method is easily extended to many other topological spaces. Proceeding by induction on the type we can obtain the countable functionals (which correspond to (C)) and the recursively countable functionals (which correspond to (C')) as defined by KLEENE and KREISEL; but for these higher types the notion of countability thus defined is not identical with the notion of continuity. MARIAN BOYKAN POUR-EL. Computable functionals. In the search for an adequate definition of the intuitive notion "computable functional" the definitions of partial recursive functional and effective operation have occupied a prominent place. An open question concerning the relationship between these two definitions is whether every effective operation is a partial recursive functional. We answer this question in the negative. THEOREM I. There exist effective operations which are not partial recursive functionals. The original proof was obtained by topologizing the space of number-theoretic functions and exhibiting an effective operation which is discontinuous at certain points of its domain. Since a partial recurs