Abstract Can one extend crisp Peano arithmetic PA by a possibly many-valued predicate Tr(x) saying “xis true” and satisfying the “dequotation schema” for all sentences φ? This problem is investigated in the frame of Łukasiewicz infinitely valued logic.

Abstract Rational Pavelka logic extends Łukasiewicz infinitely valued logic by adding truth constants r̄ for rationals in [0. 1]. We show that this is a conservative extension. We note that this shows that provability degree can be defined in Łukasiewicz logic. We also give a counterexample to a soundness theorem of Belluce and Chang published in 1963.

Unfold/fold transformations have been used in logic programming for some years to transform programs into more efficient ones. We describe recent work on the extent to which these transformations produce programs which are equivalent to the original one. Various notions of equivalence are considered: same success set; finite failure set; least Herbrand model; completion. This is used to illustrate the rather unsatisfactory relationship between logic programming and logic shown by the wide variety of different declarative semantics proposed for logic programs.

‘In successful pruning it is very necessary to know a certain amount about your subject’s mode of living. In particular it is essential to understand the factors which influence vigour, because pruning is so very much related to and governed by degree of growth. It is for these reasons that the opening pages deal with theoretical information which is of importance if the subject is to be properly understood.’ Simple Pruning, N. Catchpole, W. & H. L. Collingridge Ltd, 1930.

For the first Gödel incompleteness theorem, the existence in a formal system of arithmetic L of a sentence which is neither provable nor refutable, all that is required of the formula Th(x) of L used to express the notion ‘x is the g.n. (gödel number) of a theorem of L’ is mere numeralwise correctness, i.e. that for a numeral n, Th(n) is provable in L iff n is the g.n. of a theorem of L. It is well known that much more is needed for the second Gödel incompleteness theorem, the unprovability in L of the formula Con =df ¬(∃y, z)(Th(y) ∧ Th(z) ∧ neg(z, y)), which (if neg expresses negation) expresses the consistency of L. Conditions sufficient for this second theorem, more or less as stated by Hilbert-Bernays [1, p. 286] and elegantly formulated by Löb [2] may with a cavalier disregard for the distinction between use and mention be stated thus: The result of the first incompleteness theorem: there is a sentence G such that ⊢G ↔ ¬Th G), together with, if ⊢A then ⊢Th A, if ⊢(A → B) then ⊢(Th A → Th B), ⊢(Th A → Th Th A). On the other hand Feferman [3], Kreisel [4, p. 154] and Jeroslow [9] have given examples of systems and consistency formulae, based on numeralwise correct formulae Th(x), which are provable within the system.

H. Wang ("Circuit synthesis by solving sequential Boolean equations," Zeit. für Math. Logik und Grundlagen der Math., vol. 5 pp. 291-322, 1959) pointed out that sequential Boolean equations, obtained by adding a sequential operator to take care of the time element to the ordinary Boolean operations, provided a convenient language for expressing conditions to be satisfied by circuits or automata. Among other things he described algorithms for deciding whether an equation has a solution, and for deciding whether it has a solution with finite delay. The present paper presents algorithms which are thought to be more efficient.

article Free Access Share on Computability of Recursive Functions Authors: J. C. Shepherdson University of Bristol, England and University of California, Berkeley University of Bristol, England and University of California, BerkeleyView Profile , H. E. Sturgis University of California, Berkeley University of California, BerkeleyView Profile Authors Info & Claims Journal of the ACMVolume 10Issue 2April 1963 pp 217–255https://doi.org/10.1145/321160.321170Published:01 April 1963Publication History 298citation1,685DownloadsMetricsTotal Citations298Total Downloads1,685Last 12 Months134Last 6 weeks25 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my Alerts New Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF

The main purpose of this note is to prove (theorem 11, § 5) that, in any interpretation of the formalisation of Aristotelian syllogistic given by Łukasiewicz [4], it is always possible to associate with each element a a non-null sub-class φ ( a ) of some ‘universal’ class V in such a way that ‘ Aab’ (all a are b ), ‘ Iab ’ (some a are b ) are equivalent respectively to ‘ φ ( a ) is contained in φ ( b )’, ‘ φ ( a ) has a non-null intersection with φ ( b )’. Similarly (theorem 6, §4) we show that in Wedberg's system [14] with primitives ‘ Aab ’, ‘ a ’ (not a ), it is possible to find a mapping a → φ ( a ) as above such that ‘ Aab ’ is equivalent to ‘ φ ( a ) is contained in φ( b )’ and φ( a ‘ is equal to φ( a )’, the complement of φ( a ) with respect to V . Thus, if we make the preliminary step of identifying elements a , b such that Aab and Aba both hold (i.e. taking equivalence classes with respect to the relation Aab & Aba ), we are left with essentially only one kind of interpretation for these systems, namely the ‘normal’ interpretation by classes. Slupecki [11], [12] has proved that Łukasiewicz's system is a complete and decidable theory of the relations of inclusion and intersection of non-null classes, and Wedberg [14] has proved that his system is a complete and decidable theory of the relation of inclusion and the operation of complementation for nonnull, non-universal classes. Using the above-mentioned embedding theorem, we are able to obtain (theorems 9, 6, §§ 5, 4) very simple proofs of these results.

In [1] Myhill gave a system K in which much of the classical theory of rational and real numbers could be carried out but which was nevertheless complete; this was achieved by sacrificing the notions of negation and universal quantification and introducing instead the ancestral as a primitive idea. He mentioned two ways of dealing with real numbers in K; the first was to use the half-section corresponding to x, i.e. the class of rationals r satisfying r ≤, x; the second was to use the whole-section corresponding to x, i.e. the relation between rationals r, s which holds when r ≤ x and x ≤ s. In [2] he proved various theorems about the relation between these two forms of definition. In particular he proved that every bounded class of half-sections definable in K has a least bound definable in K. In a footnote he said, ‘This theorem risks triviality because it is doubtful whether there exists such a bounded class.’ We show in this note that this is the case; in fact there are not even any definable classes consisting entirely of classes of rationals. It is not difficult to see how this happens; since K has no negation, any statement matrix A (α) defining a class of classes of sequences is satisfied by α = V, where V is the class of all sequences. Thus there are no classes which consist entirely of half-sections. The same is true for whole-sections, showing that Conjecture I of [1], viz. ‘Not every bounded class of whole-sections definable in K has a least bound definable in K’, is trivially false. Since it may be of some intrinsic interest, we give below a more complete description of the classes of classes of sequences which are definable in K (or rather in K1 see below) than is necessary merely in order to prove the above assertion.

In this third and last paper on inner models we consider some of the inherent limitations of the method of using inner models of the type defined in 1.2 for the proof of consistency results for the particular system of set theory under consideration. Roughly speaking this limitation may be described by saying that practically no further consistency results can be obtained by the construction of models satisfying the conditions of theorem 1.5, i.e., conditions 1.31, 1.32, 1.33, 1.51, viz.: This applies in particular to the ‘complete models’ defined in 1.4. Before going on to a precise statement of these limitations we shall consider now the theorem on which they depend. This is concerned with a particular type of complete model examples of which we call “proper complete models”; they are those complete models which are essentially interior to the universe, those whose classes are sets of the universe constituting a class thereof, i.e., those for which the following proposition is true: The main theorem of this paper is that the statement that there are no models of this kind can be expressed formally in the same way as the axioms A, B, C and furthermore it can be proved that if the axiom system A, B, C is consistent then so is the system consisting of axioms A, B, C, plus this new hypothesis that there exist no proper complete models. When combined with the axiom ‘V = L’ introduced by Gödel in (1) this new hypothesis yields a system in which any normal complete model which exists has for its universal class V, the universal class of the original system.

In this paper we continue the study of inner models of the type studied inInner models for set theory—Part I.The present paper is concerned exclusively with a particular kind of model, the ‘super-complete models’ defined in section 2.4 of I (page 186). The condition (c) of 2.4 and the completeness condition 1.42 imply that such a model is uniquely determined when its universal class Vmis given. Writing condition (c) and the completeness conditions 1.41, 1.42 in terms of Vm, we may state the definition in the form: 3.1. Dfn.A classVmis said to determine a super-complete model if the model whose basic notions are defined by , satisfies axiomsA, B, C. N. B. This definition is not necessarily metamathematical in nature. If desired, it could be written out quite formally as the definition of a notion ‘SCM(U)’ (‘Udetermines a super-complete model’) thus: whereψ(U) is the propositional function expressing in terms ofUthe fact that the model determined byUaccording to 3.1 satisfies the relativization of axioms A, B, C. E.g. corresponding to axiom A1m, i.e., ,ψ(U) contains the equivalent term . All the relativized axioms can be similarly expressed in this way by first writing out the relativized form (after having replaced all defined symbols which occur by the corresponding formulae in primitive notation) and then replacing ‘(Am)ϕ(Am) by which is in turn replaced by , and similarly replacing ‘(xm)ϕ(xm)’ by ‘(xm)ϕ(xm)’ by ‘(X)(X ϵ U ▪ ⊃ ▪ ϕ(X)), and Thusψ(U) is obtained in primitive notation.

One of the standard ways of proving the consistency of additional hypotheses with the basic axioms of an axiom system is by the construction of what may be described as ‘inner models.’ By starting with a domain of individuals assumed to satisfy the basic axioms an inner model is constructed whose domain of individuals is a certain subset of the original individual domain. If such an inner model can be constructed which satisfies not only the basic axioms but also the particular additional hypothesis under consideration, then this affords a proof that if the basic axiom system is consistent then so is the system obtained by adding to this system the new hypothesis. This method has been applied to axiom systems for set theory by many authors, including v. Neumann (4), Mostowski (5), and more recently Gödel (1), who has shown by this method that if the basic axioms of a certain axiomatic system of set theory are consistent then so is the system obtained by adding to these axioms a strong form of the axiom of choice and the generalised continuum hypothesis. Having been shown in this striking way the power of this method it is natural to inquire whether it has any limitations or whether by the construction of a sufficiently ingenious inner model one might hope to decide other outstanding consistency questions, such as the consistency of the negations of the axiom of choice and continuum hypothesis. In this and two following papers we prove some general theorems concerning inner models for a certain axiomatic system of set theory which lead to the result that as far as a fairly large family of inner models are concerned this method of proving consistency has been exhausted, that no essentially new consistency results can be obtained by the use of this kind of model.