A propositional logic of explicit proofs, LP, was introduced in [S. Artemov, Explicit provability and constructive semantics, The Bulletin for Symbolic Logic 7 1–36], completing a project begun long ago by Gödel, [K. Gödel, Vortrag bei Zilsel, translated as Lecture at Zilsel’s in: S. Feferman , Kurt Gödel Collected Works III, 1938, pp. 62–113]. In fact, LP can be looked at in a more general way, as a logic of explicit evidence, and there have been several papers along these lines. (...) A major result about LP is the Realization Theorem, that says any theorem of S4 can be converted into a theorem of LP by some replacement of necessitation symbols with explicit proof terms. Thus the necessitation operator of S4 can be seen as a kind of implicit existential quantifier: there exists a proof term such that…. In this paper, quantification over evidence is introduced into LP, and it is shown that the connection between S4 necessitation and the existential quantifier becomes an explicit one. The extension of LP with quantifiers is called QLP. A semantics and an axiom system for QLP are given, soundness and completeness are established, and several results are proved relating QLP to LP and to S4. (shrink)

A formal theory of truth, alternative to tarski's 'orthodox' theory, based on truth-value gaps, is presented. the theory is proposed as a fairly plausible model for natural language and as one which allows rigorous definitions to be given for various intuitive concepts, such as those of 'grounded' and 'paradoxical' sentences.

In 1933 Godel introduced a calculus of provability (also known as modal logic S4) and left open the question of its exact intended semantics. In this paper we give a solution to this problem. We find the logic LP of propositions and proofs and show that Godel's provability calculus is nothing but the forgetful projection of LP. This also achieves Godel's objective of defining intuitionistic propositional logic Int via classical proofs and provides a Brouwer-Heyting-Kolmogorov style provability semantics for Int which (...) resisted formalization since the early 1930s. LP may be regarded as a unified underlying structure for intuitionistic, modal logics, typed combinatory logic and λ-calculus. (shrink)

Ordinary mathematical proofs—to be distinguished from formal derivations—are the locus of mathematical knowledge. Their epistemic content goes way beyond what is summarised in the form of theorems. Objections are raised against the formalist thesis that every mainstream informal proof can be formalised in some first-order formal system. Foundationalism is at the heart of Hilbert's program and calls for methods of formal logic to prove consistency. On the other hand, ‘systemic cohesiveness’, as proposed here, seeks to explicate why mathematical knowledge is (...) coherent and places the problem of reliability within the province of the philosophy of mathematics. (shrink)

Let PLω be the provability logic of IΔ0 + ω1. We prove some containments of the form L ⊆ PLω < Th(C) where L is the provability logic of PA and Th(C) is a suitable class of Kripke frames.

Ordinary mathematical proofs—to be distinguished from formal derivations—are the locus of mathematical knowledge. Their epistemic content goes way beyond what is summarised in the form of theorems. Objections are raised against the formalist thesis that every mainstream informal proof can be formalised in some first-order formal system. Foundationalism is at the heart of Hilbert's program and calls for methods of formal logic to prove consistency. On the other hand, ‘systemic cohesiveness’, as proposed here, seeks to explicate why mathematical knowledge is (...) coherent (in an informal sense) and places the problem of reliability within the province of the philosophy of mathematics. (shrink)

This papers deals with the class of axiomatic theories of truth for semantically closed languages, where the theories do not allow for standard models; i.e., those theories cannot be interpreted as referring to the natural number codes of sentences only (for an overview of axiomatic theories of truth in general, see Halbach[6]). We are going to give new proofs for two well-known results in this area, and we also prove a new theorem on the nonstandardness of a certain theory of (...) truth. The results indicate that the proof strategies for all the theorems on the nonstandardness of such theories are "essentially" of the same kind of structure. (shrink)

This paper propounds a systematic examination of the link between the Knower Paradox and provability interpretations of modal logic. The aim of the paper is threefold: to give a streamlined presentation of the Knower Paradox and related results; to clarify the notion of a syntactical treatment of modalities; finally, to discuss the kind of solution that modal provability logic provides to the Paradox. I discuss the respective strength of different versions of the Knower Paradox, both in the framework of first-order (...) arithmetic and in that of modal logic with fixed point operators. It is shown that the notion of a syntactical treatment of modalities is ambiguous between a self-referential treatment and a metalinguistic treatment of modalities, and that these two notions are independent. I survey and compare the provability interpretations of modality respectively given by Skyrms, B. (1978, The Journal of Philosophy 75: 368–387) Anderson, C.A. (1983, The Journal of Philosophy 80: 338–355) and Solovay, R. (1976, Israel Journal of Mathematics 25: 287–304). I examine how these interpretations enable us to bypass the limitations imposed by the Knower Paradox while preserving the laws of classical logic, each time by appeal to a distinct form of hierarchy. (shrink)

Gödel regarded the Dialectica interpretation as giving constructive content to intuitionism, which otherwise failed to meet reasonable conditions of constructivity. He founded his theory of primitive recursive functions, in which the interpretation is given, on the concept of computable function of finite type. I will (1) criticize this foundation, (2) propose a quite different one, and (3) note that essentially the latter foundation also underlies the Curry-Howard type theory, and hence Heyting's intuitionistic conception of logic. Thus the Dialectica interpretation (in (...) so far as its aim was to give constructive content to intuitionism) is superfluous. (shrink)

This paper is a survey of results concerning embeddings of intuitionistic propositional logic and its extensions into various classical modal systems.