Stephen Cole Kleene was one of the greatest logicians of the twentieth century and this book is the influential textbook he wrote to teach the subject to the next generation. It was first published in 1952, some twenty years after the publication of Godel's paper on the incompleteness of arithmetic, which marked, if not the beginning of modern logic. The 1930s was a time of creativity and ferment in the subject, when the notion of computable moved from the realm of (...) philosophical speculation to the realm of science. This was accomplished by the work of Kurt Gode1, Alan Turing, and Alonzo Church, who gave three apparently different precise definitions of computable. When they all turned out to be equivalent, there was a collective realization that this was indeed the right notion. Kleene played a key role in this process. One could say that he was there at the beginning of modern logic. He showed the equivalence of lambda calculus with Turing machines and with Godel's recursion equations, and developed the modern machinery of partial recursive functions. This textbook played an invaluable part in educating the logicians of the present. It played an important role in their own logical education.". (shrink)

This volume examines the notion of an analytic proof as a natural deduction, suggesting that the proof's value may be understood as its normal form--a concept with significant implications to proof-theoretic semantics.

A proof is given that the set of maximal intermediate propositional logics with the disjunction property and the set of maximal intermediate predicate logics with the disjunction property and the explicit definability property have the power of continuum. To prove our results, we introduce various notions which might be interesting by themselves. In particular, we illustrate a method to generate wide sets of pairwise "constructively incompatible constructive logics". We use a notion of "semiconstructive" logic and define wide sets of "constructive" (...) logics by representing the "constructive" logics as "limits" of decreasing sequences of "semiconstructive" logics. Also, we introduce some generalizations of the usual filtration techniques for propositional logics. For instance, "filtrations over rank formulas" are used to show that any two different logics belonging to a suitable uncountable set of "constructive" logics are "constructively incompatible". (shrink)

Infinitely many intermediate propositional logics with the disjunction property are defined, each logic being characterized both in terms of a finite axiomatization and in terms of a Kripke semantics with the finite model property. The completeness theorems are used to prove that any two logics are constructively incompatible. As a consequence, one deduces that there are infinitely many maximal intermediate propositional logics with the disjunction property.

For intermediate logics, there is obtained in the paper an algebraic equivalent of the disjunction propertyDP. It is proved that the logic of finite binary trees is not maximal among intermediate logics withDP. Introduced is a logicND, which has the only maximal extension withDP, namely, the logicML of finite problems.

The paper considers certain properties of intermediate and moda propositional logics.The first part contains a proof of the theorem stating that each intermediate logic is closed under the Kreisel-Putnam rule xyz/(xy)(xz).

Given an intermediate prepositional logic L, denote by L –d its disjuctionless fragment. We introduce an infinite sequence {J n}n1 of propositional formulas, and prove:(1)For any L: L –d =I –d (I=intuitionistic logic) if and only if J n L for every n 1.

This paper is a survey of results concerning the disjunction property, Halldén-completeness, and other related properties of intermediate prepositional logics and normal modal logics containing S4.

This is the second part of a paper devoted to the study of the maximal intermediate propositional logics with the disjunction property , whose first part has appeared in this journal with the title “A method to single out maximal propositional logics with the disjunction property I”. In the first part we have explained the general results upon which a method to single out maximal constructive logics is based and have illustrated such a method by exhibiting the Kripke semantics of (...) maximal constructive logics extending the logic ST of Scott, for which, in turn, a semantical characterization in terms of Kripke frames has been given. In the present part we complete the illustration of the method of the first part, having in mind some aspects which might be interesting for a classification of the maximal constructive logics, and an application of the heuristic content of the method to detect the nonmaximality of apparently maximal constructive logics. Thus, on the one hand we introduce the logic AST , which is compared with ST and is seen as a logic “alternative” to it, in a sense which will be precisely explained. We provide a Kripke semantics for AST and show that there are maximal constructive logics which neither are extensions of ST nor are extensions of AST. Finally, we give a further application of the results of the first part by exhibiting the Kripke semantics of a maximal constructive logic extending AST. On the other hand, we compare the maximal constructive logics presented in both parts of the paper with a constructive logic introduced by Maksimova , which has been conjectured to be maximal by Chagrov and Zacharyashchev ; from this comparison a disproof of the conjecture arises. (shrink)