Kniha, jako je tato, nemůže být tak docela dílem jediného člověka. Dovést ji do podoby koherentního celku bych nedokázal bez pomoci svých kolegů, kteří po mně text četli a upozornili mě na spoustu chyb a nedůsledností, které se v něm vyskytovaly. Můj dík v tomto směru patří zejména Vojtěchu Kolmanovi, Liboru Běhounkovi a Martě Bílkové. Za připomínky k různým částem rukopisu jsem vděčen i Pavlu Maternovi, Milanu Matouškovi, Prokopu Sousedíkovi, Vladimíru Svobodovi, Petru Hájkovi a Grahamu Priestovi. Kniha vznikla v rámci (...) projektu podpořeného grantem AV ČR číslo A0009001/00. (shrink)

Philosophers of language have drawn on metamathematical results in varied ways. Extensionalist philosophers have been particularly impressed with two, not unrelated, facts: the existence, due to Frege/Tarski, of a certain sort of semantics, and the seeming absence of intensional contexts from mathematical discourse. The philosophical import of these facts is at best murky. Extensionalists will emphasize the success and clarity of the model theoretic semantics; others will emphasize the relative poverty of the mathematical idiom; still others will question the aptness (...) of the standard extensional semantics for mathematics. In this paper I investigate some implications of the Gödel Second Incompleteness Theorem for these positions. I argue that the realm of mathematics, proof theory in particular, has been a breeding ground for intensionality and that satisfactory intensional semantic theories are implicit in certain rigorous technical accounts. (shrink)

This paper is the final part of the syntactic demonstration of the Arithmetical Completeness of the modal system G; in the preceding parts [9] and [10] the tools for the proof were defined, in particular the notion of syntactic countermodel. Our strategy is: PA-completeness of G as a search for interpretations which force the distance between G and a GL-LIN-theorem to zero. If the GL-LIN-theorem S is not a G-theorem, we construct a formula H expressing the non G-provability of S, (...) so that ⊢GL-LIN ∼ H and so that a canonical proof T of ∼ H in GL-LIN is a syntactic countermodel for S with respect to G, which has the height θ(T) equal to the distance d(S, G) of S from G. Then we define the interpretation ξ of S which represents the proof-tree T in PA. By induction on θ(T), we prove that ⊢PA Sξ and d(S, G) > 0 imply the inconsistency of PA. (shrink)

This volume is dedicated to Leo Esakia's contributions to the theory of modal and intuitionistic systems. Consisting of 10 chapters, written by leading experts, this volume discusses Esakia’s original contributions and consequent developments that have helped to shape duality theory for modal and intuitionistic logics and to utilize it to obtain some major results in the area. Beginning with a chapter which explores Esakia duality for S4-algebras, the volume goes on to explore Esakia duality for Heyting algebras and its generalizations (...) to weak Heyting algebras and implicative semilattices. The book also dives into the Blok-Esakia theorem and provides an outline of the intuitionistic modal logic KM which is closely related to the Gödel-Löb provability logic GL. One chapter scrutinizes Esakia’s work interpreting modal diamond as the derivative of a topological space within the setting of point-free topology. The final chapter in the volume is dedicated to the derivational semantics of modal logic and other related issues. (shrink)

This book provides a detailed exposition of one of the most practical and popular methods of proving theorems in logic, called Natural Deduction. It is presented both historically and systematically. Also some combinations with other known proof methods are explored. The initial part of the book deals with Classical Logic, whereas the rest is concerned with systems for several forms of Modal Logics, one of the most important branches of modern logic, which has wide applicability.

Part 1 [Hodes, 2021] “looked under the hood” of the familiar versions of the classical propositional modal logic K and its intuitionistic counterpart. This paper continues that project, addressing some familiar classical strengthenings of K and GL), and their intuitionistic counterparts. Section 9 associates two intuitionistic one-step proof-theoretic systems to each of the just mentioned intuitionistic logics, this by adding for each a new rule to those which generated IK in Part 1. For the systems associated with the intuitionistic counterparts (...) of D and T, these rules are “pure one-step”: their schematic formulations does not use □ or ♢. For the systems associated with the intuitionistic counterparts of K4, etc., these rules meet these conditions: neither □ nor ♢ is iterated; none use both □ and ♢. The join of the two systems associated with each of these familiar logics is the full one-step system for that intuitionistic logic. And further “blended” intuitionistic systems arise from joining these systems in various ways. Adding the 0-version of Excluded Middle to their intuitionistic counterparts yields the one-step systems corresponding to the familiar classical logics. Each proof-theoretic system defines a consequence relation in the obvious way. Section 10 examines inclusions between these consequence relations. Section 11 associates each of the above consequence relations with an appropriate class of models, and proves them sound with respect to their appropriate class. This allows proofs of some failures of inclusion between consequence relations. Section 12 proves that the each consequence relation is complete or weakly complete, that relative to its appropriate class of models. The Appendix presents three further results about some of the intuitionistic consequence relations discussed in the body of the paper. For Keywords, see Part 1. (shrink)

The problem of Uniqueness and Explicit Definability of Fixed Points for Interpretability Logic is considered. It turns out that Uniqueness is an immediate corollary of a theorem of Smoryński.

-/- Provability logic is a modal logic that is used to investigate what arithmetical theories can express in a restricted language about their provability predicates. The logic has been inspired by developments in meta-mathematics such as Gödel’s incompleteness theorems of 1931 and Löb’s theorem of 1953. As a modal logic, provability logic has been studied since the early seventies, and has had important applications in the foundations of mathematics. -/- From a philosophical point of view, provability logic is interesting because (...) the concept of provability in a fixed theory of arithmetic has a unique and non-problematic meaning, other than concepts like necessity and knowledge studied in modal and epistemic logic. Furthermore, provability logic provides tools to study the notion of self-reference. (shrink)

This paper studies a propositional logic which is obtained by interpreting implication as formal provability. It is also the logic of finite irreflexive Kripke Models.A Kripke Model completeness theorem is given and several completeness theorems for interpretations into Provability Logic and Peano Arithmetic.

To the standard propositional modal system of provability logic constants are added to account for the arithmetical fixed points introduced by Bernardi-Montagna in [5]. With that interpretation in mind, a system LR of modal propositional logic is axiomatized, a modal completeness theorem is established for LR and, after that, a uniform arithmetical (Solovay-type) completeness theorem with respect to PA is obtained for LR.

This paper deals with the system of modal logicGL, in particular with a formulation of it in terms of sequents. We prove some proof theoretical properties ofGL that allow to get the cut-elimination theorem according to Gentzen's procedure, that is, by double induction on grade and rank.

We present an axiomatization for Basic Propositional Calculus BPC and give a completeness theorem for the class of transitive Kripke structures. We present several refinements, including a completeness theorem for irreflexive trees. The class of intermediate logics includes two maximal nodes, one being Classical Propositional Calculus CPC, the other being E1, a theory axiomatized by T → ⊥. The intersection CPC ∩ E1 is axiomatizable by the Principle of the Excluded Middle A V ∨ ⌝A. If B is a formula (...) such that → B is not derivable, then the lattice of formulas built from one propositional variable p using only the binary connectives, is isomorphically preserved if B is substituted for p. A formula → B is derivable exactly when B is provably equivalent to a formula of the form → A) →. (shrink)

This paper, a sequel to Models for normal intuitionistic modal logics by M. Boi and the author, which dealt with intuitionistic analogues of the modal system K, deals similarly with intuitionistic analogues of systems stronger than K, and, in particular, analogues of S4 and S5. For these prepositional logics Kripke-style models with two accessibility relations, one intuitionistic and the other modal, are given, and soundness and completeness are proved with respect to these models. It is shown how the holding of (...) formulae characteristic for particular logics is equivalent to conditions for the relations of the models. Modalities in these logics are also investigated. (shrink)

A (normal) system of propositional modal logic is said to be complete iff it is characterized by a class of (Kripke) frames. When we move to modal predicate logic the question of completeness can again be raised. It is not hard to prove that if a predicate modal logic is complete then it is characterized by the class of all frames for the propositional logic on which it is based. Nor is it hard to prove that if a propositional modal (...) logic is incomplete then so is the predicate logic based on it. But the interesting question is whether a complete propositional modal logic can have an incomplete extension. In 1967 Kripke announced the incompleteness of a predicate extension of S4. The purpose of the present article is to present several such systems. In the first group it is the systems with the Barcan Formula which are incomplete, while those without are complete. In the second group it is those without the Barcan formula which are incomplete, while those with the Barcan Formula are complete. But all these are based on propositional systems which are characterized by frames satisfying in each case a single first-order sentence. (shrink)

odel-L¨ ob computability logic. In order to make things relatively self-contained, I sketch the essential ideas of GL, and discuss the significance of its fixpoint theorem. Then I give the algorithm embodied in the program in a little more detail. It should be emphasized that nothing new is presented here — all the theory and methodology are due to others. The main interest is, in a sense, psychological. The approach taken here has been declared in the literature, more than once, (...) to be of theoretical interest only, being too unwieldly in practice. Experimentation shows this is not so provided formulas are not too complicated. A copy of the program can be obtained by ftp from venus.gc.cuny.edu. It is in the subdirectory “/pub/fitting,” under the name “glfixpt.pro.” Log on as “anonymous” and use your full e-mail address as password. If there are difficulties with ftp, send e-mail to the author at mlfl[email protected]. The Prolog code is standard, and should run under any implementation, though minor modifications may be necessary for some systems. These modifications are described in the last section, and also in the program itself. (shrink)

Kripke-style models with two accessibility relations, one intuitionistic and the other modal, are given for analogues of the modal systemK based on Heyting's prepositional logic. It is shown that these two relations can combine with each other in various ways. Soundness and completeness are proved for systems with only the necessity operator, or only the possibility operator, or both. Embeddings in modal systems with several modal operators, based on classical propositional logic, are also considered. This paper lays the ground for (...) an investigation of intuitionistic analogues of systems stronger thanK. A brief survey is given of the existing literature on intuitionistic modal logic. (shrink)

In this paper we use “generic submodels” to prove that each normal extension of G.3 (K4.3W) has the finite model property, by which we establish that each proper normal extension of G.3 is G.3Altn for some n≥0.

Traces the development of recursive functions from their origins in the late nineteenth century to the mid-1930s, with particular emphasis on the work and influence of Kurt Gödel.

Using only propositional connectives and the provability predicate of a Σ1-sound theory T containing Peano Arithmetic we define recursively enumerable relations that are complete for specific natural classes of relations, as the class of all r. e. relations, and the class of all strict partial orders. We apply these results to give representations of these classes in T by means of formulas.

The core ideas of the dialogicalapproach to modal propositional logic are explainedby means of an elementary example. Subsequently,ways of extending this approach to the system G ofso-called provability logic are checked, therebyraising the question whether the dialogician is inneed of shaping his Nichtverzögerungsregel(non-delay-rule), in order to get it sufficiently precise,in different ways for different modal systems.

The systems T N and T M show that necessity can be consistently construed as a predicate of syntactical objects, if the expressive/deductive power of the system is deliberately engineered to reflect the power of the original object language operator. The system T N relies on salient limitations on the expressive power of the language L N through the construction of a quotational hierarchy, while the system T Mrelies on limiting the scope of the modal axioms schemas to the sublanguage (...) L infM +, which corresponds exactly with the restrictive hierarchy of L N. The fact that L infM + is identical to the image of the metalinguistic mapping C + from the normal operator system into L M reveals that iterated operator modality is implicitly hierarchical, and that inconsistency is produced by applying the principles of the modal logic to formulas which have no natural analogues in the operator development. Thus the contradiction discovered by Montague can be diagnosed as the result of instantiating the axiom schemas with modally ungrounded formulas, and thereby adding radically new modal axioms to the predicate system.The predicate treatment of necessity differs significantly from that of the operator in that the cumulative models for the predicate system are strictly first-order. Possible worlds are not used as model-theoretic primitives, but rather alternate models are appealed to in order to specify the extension of N, which is semantically construed as a first-order predicate. In this manner, the intensional aspects of modality are built into the mode of specifying the particular set of objects which the denotation function assigns to N, rather than in the specification of the basic truth conditions for modal formulas. Intensional phenomena are thereby localised to the special requirements for determining the extension of a particular predicate, and this does not constitute a structural modification of the first-order models, but rather limits the relevant class of models to those which possess an appropriate denotation function. (shrink)

Modal Platonism utilizes "weak" logical possibility, such that it is logically possible there are abstract entities, and logically possible there are none. Modal Platonism also utilizes a non-indexical actuality operator. Modal Platonism is the EASY WAY, neither reductionist nor eliminativist, but embracing the Platonistic language of abstract entities while eliminating ontological commitment to them. Statement of Modal Platonism. Any consistent statement B ontologically committed to abstract entities may be replaced by an empirically equivalent modalization, MOD(B), not so ontologically committed. This (...) equivalence is provable using Modal/Actuality Logic S5@. Let MAX be a strong set theory with individuals. Then the following Schematic Bombshell Result (SBR) can be shown: MAX logically yields [T is true if and only if MOD(T) is true], for scientific theories T. The proof utilizes Stephen Neale's clever model-theoretic interpretation of Quantified Lewis S5, which I extend to S5@. (shrink)

The problem of Common Knowledge will be considered in two classes of models: a class K.* of Kripke models and a class S of Scott models. Two modal logic systems will be defined. Those systems, KC and MC, include an axiomatisation of Common Knowledge. We prove determination of each system by the corresponding class of models. MSC: 03B45, 68T25.

In a classical 1976 paper, Solovay proved the arithmetical completeness of the modal logic GL; provability of a formula in GL coincides with provability of its arithmetical interpretations of it in Peano Arithmetic. In that paper, he also provided an axiomatic system GLS and proved arithmetical completeness for GLS; provability of a formula in GLS coincides with truth of its arithmetical interpretations in the standard model of arithmetic. Proof theory for GL has been studied intensively up to the present day. (...) However, it might sound somewhat strange that no proof theory for GLS was ever developed nor even suggested thus far, except for the axiomatic system offered by Solovay. In this paper, we develop a proof theory for GLS based on the sequent calculus method. We provide a sequent calculus for GLS and prove the cut-elimination and some standard consequences of it: the interpolation and definability theorems. As another consequence of cut-elimination, we also prove the equivalence of GL and GLS with respect to a special form of formulas which we call Gödel sentences, using a purely proof-theoretical method. (shrink)

The logic of 'elsewhere,' i.e., of a sentence operator interpretable as attaching to a formula to yield a formula true at a point in a Kripke model just in case the first formula is true at all other points in the model, has been applied in settings in which the points in question represent spatial positions, as well as in the case in which they represent moments of time. This logic is applied here to the alethic modal case, in which (...) the points are thought of as possible worlds, with the suggestion that its deployment clarifies aspects of a position explored by John Divers under the name 'modal agnosticism.' In particular, it makes available a logic whose Halldén incompleteness explicitly registers the agnostic element of the position - its neutrality as between modal realism and modal anti-realism. (shrink)

Sambin [6] proved the normalization theorem for GL, the modal logic of provability, in a sequent calculus version called by him GLS. His proof does not take into account the concept of reduction, commonly used in normalization proofs. Bellini [1], on the other hand, gave a normalization proof for GL using reductions. Indeed, Sambin's proof is a decision procedure which builds cut-free proofs. In this work we formalize this procedure as a recursive function and prove its recursiveness in an arithmetically (...) formalizable way, concluding that the normalization of GL can be formalized in PA. MSC: 03F05, 03B35, 03B45. (shrink)

S. SHAPIRO (ed.), Intensional Mathematics (Studies in Logic and the Foundations of Mathematics, vol. 11 3). Amsterdam: North-Holland, 1985. v + 230 pp. $38.50/100Df.

The problem of Uniqueness and Explicit Definability of Fixed Points for Interpretability Logic is considered. It turns out that Uniqueness is an immediate corollary of a theorem of Smoryski.

We study a modal system ¯T, that extends the classical (prepositional) modal system T and whose language is provided with modal operators M inn (nN) to be interpreted, in the usual kripkean semantics, as there are more than n accessible worlds such that.... We find reasonable axioms for ¯T and we prove for it completeness, compactness and decidability theorems.

This paper is the first of a series of three articles that present the syntactic proof of the PA-completeness of the modal system G, by introducing suitable proof-theoretic objects, which also have an independent interest. We start from the syntactic PA-completeness of modal system GL-LIN, previously obtained in [7], [8], and so we assume to be working on modal sequents S which are GL-LIN-theorems. If S is not a G-theorem we define here a notion of syntactic metric d(S, G): we (...) calculate a canonical characteristic fomula H of S (char(S)) so that ⊢G ∼ H → (∼S) and ⊢GL-LIN ∼ H, and the complexity σ of ∼ H gives the distance d(S, G) of S from G. Then, in order to produce the whole completeness proof as an induction on this d(S, G), we introduce the tree-interpretation of a modal sequent Q into PA, that sends the letters of Q into PA-formulas describing the properties of a GL-LIN-proof P of Q: It is also a d(*, G)-metric linked interpretation, since it will be applied to a proof-tree T of ∼ H with H = char(S) and σ(∼ H) = d(S, G). (shrink)