In this paper, we investigate Rosser provability predicates whose provability logics are normal modal logics. First, we prove that there exists a Rosser provability predicate whose provability logic is exactly the normal modal logic \. Secondly, we introduce a new normal modal logic \ which is a proper extension of \, and prove that there exists a Rosser provability predicate whose provability logic includes \.

We investigate several consequences of inclusion relations between quantified provability logics. Moreover, we give a necessary and sufficient condition for the inclusion relation between quantified provability logics with respect to \ arithmetical interpretations.

Solovay proved (Israel J Math 25(3–4):287–304, 1976) that the propositional provability logic of any ∑2-sound recursively enumerable extension of PA is characterized by the propositional modal logic GL. By contrast, Montagna proved in (Notre Dame J Form Log 25(2):179–189, 1984) that predicate provability logics of Peano arithmetic and Bernays–Gödel set theory are different. Moreover, Artemov proved in (Doklady Akademii Nauk SSSR 290(6):1289–1292, 1986) that the predicate provability logic of a theory essentially depends on the choice of a binumeration of the (...) theory which is used to construct the provability predicate. In this paper, we compare predicate provability logics of I∑ n ’s. For a binumeration α(x) of a recursive theory T, let PL α(T) be the predicate provability logic of T defined by α(x). We prove that for any natural numbers i, j such that 0 < i < j, there exists a ∑1 binumeration α(x) of some recursive axiomatization of I∑ i such that ${{\sf PL}_\alpha({\rm I \Sigma}_i) \nsupseteq \bigcap_{\beta(x)}{\sf PL}_\beta({\rm I \Sigma}_j)}$ and ${{\sf PL}_\alpha({\rm I \Sigma}_i) \nsubseteq \bigcup_{\beta(x)}{\sf PL}_\beta({\rm I \Sigma}_j)}$ , where β(x) ranges over all ∑1 binumerations of recursive axiomatizations of I∑ j. (shrink)

We prove that for each recursively axiomatized consistent extension T of Peano Arithmetic and \, there exists a \ numeration \\) of T such that the provability logic of the provability predicate \\) naturally constructed from \\) is exactly \ \rightarrow \Box p\). This settles Sacchetti’s problem affirmatively.

We prove that for any recursively axiomatized consistent extension T of Peano Arithmetic, there exists a \ provability predicate of T whose provability logic is precisely the modal logic \. For this purpose, we introduce a new bimodal logic \, and prove the Kripke completeness theorem and the uniform arithmetical completeness theorem for \.

We define a liar-type paradox as a consistent proposition in propositional modal logic which is obtained by attaching boxes to several subformulas of an inconsistent proposition in classical propositional logic, and show several famous paradoxes are liar-type. Then we show that we can generate a liar-type paradox from any inconsistent proposition in classical propositional logic and that undecidable sentences in arithmetic can be obtained from the existence of a liar-type paradox. We extend these results to predicate logic and discuss Yablo’s (...) Paradox in this framework. Furthermore, we define explicit and implicit self-reference in paradoxes in the incompleteness phenomena. (shrink)

By formalizing Berry's paradox, Vopěnka, Chaitin, Boolos and others proved the incompleteness theorems without using the diagonal argument. In this paper, we shall examine these proofs closely and show their relationships. Firstly, we shall show that we can use the diagonal argument for proofs of the incompleteness theorems based on Berry's paradox. Then, we shall show that an extension of Boolos' proof can be considered as a special case of Chaitin's proof by defining a suitable Kolmogorov complexity. We shall show (...) also that Vopěnka's proof can be reformulated in arithmetic by using the arithmetized completeness theorem. (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)

Jean-Yves Béziau (‘Classical Negation can be Expressed by One of its Halves’, Logic Journal of the IGPL 7 (1999), 145–151) has given an especially clear example of a phenomenon he considers a sufficiently puzzling to call the ‘paradox of translation’: the existence of pairs of logics, one logic being strictly weaker than another and yet such that the stronger logic can be embedded within it under a faithful translation. We elaborate on Béziau’s example, which concerns classical negation, as well as (...) giving some additional background (especially from intuitionistic logic) to the example. Our interest is more on the logical exploration of the phenomenon Béziau’s case exemplifies than on the question of whether that phenomenon is (even prima facie ) paradoxical, though in Section 5 we do approach the latter question – somewhat obliquely – by considering an analogous phenomenon which it is hard to find puzzling. (shrink)

This paper presents a defense of Epistemic Arithmetic as used for a formalization of intuitionistic arithmetic and of certain informal mathematical principles. First, objections by Allen Hazen and Craig Smorynski against Epistemic Arithmetic are discussed and found wanting. Second, positive support is given for the research program by showing that Epistemic Arithmetic can give interesting formulations of Church's Thesis.

This paper develops the philosophy and technology needed for adding a supremum operator to the interpretability logic ILM\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\mathsf {ILM}$$\end{document} of Peano Arithmetic. It is well-known that any theories extending PA\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\mathsf {PA}$$\end{document} have a supremum in the interpretability ordering. While provable in PA\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\mathsf {PA}$$\end{document}, this fact is not reflected in the theorems of the modal (...) system ILM\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\mathsf {ILM}$$\end{document}, due to limited expressive power. Our goal is to enrich the language of ILM\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\mathsf {ILM}$$\end{document} by adding to it a new modality for the interpretability supremum. We explore different options for specifying the exact meaning of the new modality. Our final proposal involves a unary operator, the dual of which can be seen as a provability predicate satisfying the axioms of the provability logic GL\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\mathsf {GL}$$\end{document}. (shrink)

This paper investigates a first-order extension of GL called \. We outline briefly the history that led to \, its key properties and some of its toolbox: the \emph{conservation theorem}, its cut-free Gentzenisation, the ``formulators'' tool. Its semantic completeness is fully stated in the current paper and the proof is retold here. Applying the Solovay technique to those models the present paper establishes its main result, namely, that \ is arithmetically complete. As expanded below, \ is a first-order modal logic (...) that along with its built-in ability to simulate general classical first-order provability―"\" simulating the the informal classical "\"―is also arithmetically complete in the Solovay sense. (shrink)

A teacher announced to his pupils that on exactly one of the days of the following school week (Monday through Friday) he would give them a test. But it would be a surprise test; on the evening before the test they would not know that the test would take place the next day. One of the brighter students in the class then argued that the teacher could never give them the test. "It can't be Friday," she said, "since in that (...) case we'll expect it on Thurday evening. But then it can't be Thursday, since having already eliminated Friday we'll know Wednesday evening that it has to be Thursday. And by similar reasoning we can also eliminate Wednesday, Tuesday, and Monday. So there can't be a test!" The students were somewhat baffled by the situation. The teacher was well-known to be truthful, so if he said there would be a test, then it was safe to assume that there would be one. On the other hand, he also said that the test would be a surprise. But it seemed that whenever he gave the test, it wouldn't be a surprise. Well, the teacher gave the test on Tuesday, and, sure enough, the students were surprised. (shrink)

If □ is conceived as an operator, i.e., an expression that gives applied to a formula another formula, the expressive power of the language is severely restricted when compared to a language where □ is conceived as a predicate, i.e., an expression that yields a formula if it is applied to a term. This consideration favours the predicate approach. The predicate view, however, is threatened mainly by two problems: Some obvious predicate systems are inconsistent, and possible-worlds semantics for predicates of (...) sentences has not been developed very far. By introducing possible-worlds semantics for the language of arithmetic plus the unary predicate □, we tackle both problems. Given a frame (W, R) consisting of a set W of worlds and a binary relation R on W, we investigate whether we can interpret □ at every world in such a way that □ $\ulcorner A \ulcorner$ holds at a world ᵆ ∊ W if and only if A holds at every world $\upsilon$ ∊ W such that ᵆR $\upsilon$ . The arithmetical vocabulary is interpreted by the standard model at every world. Several 'paradoxes' (like Montague's Theorem, Gödel's Second Incompleteness Theorem, McGee's Theorem on the ω-inconsistency of certain truth theories, etc.) show that many frames, e.g., reflexive frames, do not allow for such an interpretation. We present sufficient and necessary conditions for the existence of a suitable interpretation of □ at any world. Sound and complete semi-formal systems, corresponding to the modal systems K and K4, for the class of all possible-worlds models for predicates and all transitive possible-worlds models are presented. We apply our account also to nonstandard models of arithmetic and other languages than the language of arithmetic. (shrink)

In philosophical logic necessity is usually conceived as a sentential operator rather than as a predicate. An intensional sentential operator does not allow one to express quantified statements such as 'There are necessary a posteriori propositions' or 'All laws of physics are necessary' in first-order logic in a straightforward way, while they are readily formalized if necessity is formalized by a predicate. Replacing the operator conception of necessity by the predicate conception, however, causes various problems and forces one to reject (...) many philosophical accounts involving necessity that are based on the use of operator modal logic. We argue that the expressive power of the predicate account can be restored if a truth predicate is added to the language of first-order modal logic, because the predicate 'is necessary' can then be replaced by 'is necessarily true'. We prove a result showing that this substitution is technically feasible. To this end we provide partial possible-worlds semantics for the language with a predicate of necessity and perform the reduction of necessities to necessary truths. The technique applies also to many other intensional notions that have been analysed by means of modal operators. (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 logic is the extension of intuitionistic logic by the linearity axiom. Symmetric Gödel logic is a logical system, the language of which is an enrichment of the language of Gödel logic with their dual logical connectives. Symmetric Gödel logic is the extension of symmetric intuitionistic logic. The proof-intuitionistic calculus, the language of which is an enrichment of the language of intuitionistic logic by modal operator was investigated by Kuznetsov and Muravitsky. Bimodal symmetric Gödel logic is a logical system, the (...) language of which is an enrichment of the language of Gödel logic with their dual logical connectives and two modal operators. Bimodal symmetric Gödel logic is embedded into an extension of Gödel–Löb logic, the language of which contains disjunction, conjunction, negation and two modal operators. The variety of bimodal symmetric Gödel algebras, that represent the algebraic counterparts of bimodal symmetric Gödel logic, is investigated. Description of free algebras and characterization of projective algebras in the variety of bimodal symmetric Gödel algebras is given. All finitely generated projective bimodal symmetric Gödel algebras are infinite, while finitely generated projective symmetric Gödel algebras are finite. (shrink)

Natural deduction systems were motivated by the desire to define the meaning of each connective by specifying how it is introduced and eliminated from inference. In one sense, this attempt fails, for it is well known that propositional logic rules underdetermine the classical truth tables. Natural deduction rules are too weak to enforce the intended readings of the connectives; they allow non-standard models. Two reactions to this phenomenon appear in the literature. One is to try to restore the standard readings, (...) for example by adopting sequent rules with multiple conclusions. Another is to explore what readings the natural deduction rules do enforce. When the notion of a model of a rule is generalized, it is found that natural deduction rules express “intuitionistic” readings of their connectives. A third approach is presented here. The intuitionistic readings emerge when models of rules are defined globally, but the notion of a local model of a rule is also natural. Using this benchmark, natural deduction rules enforce exactly the classical readings of the connectives, while this is not true of axiomatic systems. This vindicates the historical motivation for natural deduction rules. One odd consequence of using the local model benchmark is that some systems of propositional logic are not complete for the semantics that their rules express. Parallels are drawn with incompleteness results in modal logic to help make sense of this. (shrink)

This paper is concerned with a propositional modal logic with operators for necessity, actuality and apriority. The logic is characterized by a class of relational structures defined according to ideas of epistemic two-dimensional semantics, and can therefore be seen as formalizing the relations between necessity, actuality and apriority according to epistemic two-dimensional semantics. We can ask whether this logic is correct, in the sense that its theorems are all and only the informally valid formulas. This paper gives outlines of two (...) arguments that jointly show that this is the case. The first is intended to show that the logic is informally sound, in the sense that all of its theorems are informally valid. The second is intended to show that it is informally complete, in the sense that all informal validities are among its theorems. In order to give these arguments, a number of independently interesting results concerning the logic are proven. In particular, the soundness and completeness of two proof systems with respect to the semantics is proven (Theorems 2.11 and 2.15), as well as a normal form theorem (Theorem 3.2), an elimination theorem for the actuality operator (Corollary 3.6), and the decidability of the logic (Corollary 3.7). It turns out that the logic invalidates a plausible principle concerning the interaction of apriority and necessity; consequently, a variant semantics is briefly explored on which this principle is valid. The paper concludes by assessing the implications of these results for epistemic two-dimensional semantics. (shrink)

Justification logics provide frameworks for studying the fine structure of evidence and justification. Traditionally, these logics do not impose any closure requirements on justification. In this paper, we argue that for some applications they should subject justification to closure under some variety of logical consequence. Specifically, we argue, building on ideas from Beall, that the non-classical logic FDE offers a particularly attractive notion of consequence for this purpose and define a justification logic where justification is closed under FDE consequence. We (...) show the resulting logic to be sound and complete. Lastly, we discuss how the closure of justification under FDE ontrasts closure under related non-classical logics and how our approach contrasts with some alternatives. (shrink)

A conjectural inference is proposed, aimed at producing conjectural theorems from formal conjectures assumed as axioms, as well as admitting contradictory statements as conjectural theorems. To this end, we employ Paraconsistent Informational Logic, which provides a formal setting where the notion of conjecture formulated by an epistemic agent can be defined. The paraconsistent systems on which conjectural deduction is based are sequent formulations of the C-systems presented in Carnielli-Marcos [CAR 02b]. Thus, conjectural deduction may also be considered to be a (...) tool for investigating the properties of paraconsistency in general. (shrink)

The paper shows how we can add a truth predicate to arithmetic (or formalized syntactic theory), and keep the usual truth schema Tr( ) ↔ A (understood as the conjunction of Tr( ) → A and A → Tr( )). We also keep the full intersubstitutivity of Tr(>A>)) with A in all contexts, even inside of an →. Keeping these things requires a weakening of classical logic; I suggest a logic based on the strong Kleene truth tables, but with → (...) as an additional connective, and where the effect of classical logic is preserved in the arithmetic or formal syntax itself. Section 1 is an introduction to the problem and some of the difficulties that must be faced, in particular as to the logic of the →; Section 2 gives a construction of an arithmetically standard model of a truth theory; Section 3 investigates the logical laws that result from this; and Section 4 provides some philosophical commentary. (shrink)

The paper offers a solution to the semantic paradoxes, one in which (1) we keep the unrestricted truth schema “True(A)↔A”, and (2) the object language can include its own metalanguage. Because of the first feature, classical logic must be restricted, but full classical reasoning applies in “ordinary” contexts, including standard set theory. The more general logic that replaces classical logic includes a principle of substitutivity of equivalents, which with the truth schema leads to the general intersubstitutivity of True(A) with A (...) within the language.The logic is also shown to have the resources required to represent the way in which sentences (like the Liar sentence and the Curry sentence) that lead to paradox in classical logic are “defective”. We can in fact define a hierarchy of “defectiveness” predicates within the language. Contrary to claims that any solution to the paradoxes just breeds further paradoxes (“revenge problems”) involving defectiveness predicates, there is a general consistency/conservativeness proof that shows that talk of truth and the various “levels of defectiveness” can all be made coherent together within a single object language. (shrink)

The knower paradox states that the statement ‘We know that this statement is false’ leads to inconsistency. This article presents a fresh look at this paradox and some well-known solutions from the literature. Paul Égré discusses three possible solutions that modal provability logic provides for the paradox by surveying and comparing three different provability interpretations of modality, originally described by Skyrms, Anderson, and Solovay. In this article, some background is explained to clarify Égré’s solutions, all three of which hinge on (...) intricacies of provability logic and its arithmetical interpretations. To check whether Égré’s solutions are satisfactory, we use the criteria for solutions to paradoxes defined by Susan Haack and we propose some refinements of them. This article aims to describe to what extent the knower paradox can be solved using provability logic and to what extent the solutions proposed in the literature satisfy Haack’s criteria. Finally, the article offers some reflections on the relation between knowledge, proof, and provability, as inspired by the knower paradox and its solutions. (shrink)

Added by a category editor--not an official abstract. -/- Discusses the history (and reasons for the history) implicit in the title, as well as the author's view on same.

The aim of this paper is to develop a new connection between naming and necessity. I argue that Kripke’s historical account of naming presupposes the functional necessity of naming. My argument appeals to the etiological notion of function, which can be thought to capture the necessity of functionality in historical terms. It is shown that the historical account of naming entails all conditions in an etiological definition of function.

This paper replies to Nanay’s response to my recent paper. My suggestions are the following. First, “should” or “ought” does not need to be deontic. Second, etiological theories of function, like provability logic, do not need to attribute modal force to their explanans. Third, the explanans of the homological account of trait type individuation does not appeal to a trait’s etiological function, that is, what a trait should or ought to do. Finally, my reference to Cummins’s notion of function was (...) intended to note that the homological account is permitted to use this non-etiological notion of function. (shrink)

-/- 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)

Abstract : In this paper, it is argued that Leibniz’s view that necessity is grounded in the availability of a demonstration is incorrect and furthermore, can be shown to be so by using Leibniz’s own examples of infinite analyses. First, I show that modern mathematical logic makes clear that Leibniz’s "infinite analysis" view of contingency is incorrect. It is then argued that Leibniz's own examples of incommensurable lines and convergent series undermine, rather than bolster his view by providing examples of (...) necessary mathematical truths that are not demonstrable. Finally, it is argued that a more modern view on convergent series would, in certain respects, help support some claims he makes about the necessity of mathematical truths, but would still not yield a viable theory of necessity due to remaining problems with other logical, mathematical, and modal claims. (shrink)

This paper aims to vindicate the thesis that cognitive computational properties are abstract objects implemented in physical systems. I avail of the equivalence relations countenanced in Homotopy Type Theory, in order to specify an abstraction principle for epistemic intensions. The homotopic abstraction principle for epistemic intensions provides an epistemic conduit into our knowledge of intensions as abstract objects. I examine, then, how intensional functions in Epistemic Modal Algebra are deployed as core models in the philosophy of mind, Bayesian perceptual psychology, (...) and the program of natural language semantics in linguistics, and I argue that this provides abductive support for the truth of homotopic abstraction. Epistemic modality can thus be shown to be both a compelling and a materially adequate candidate for the fundamental structure of mental representational states, comprising a fragment of the Language of Thought. (shrink)

In our introduction we make some remarks on the main topics of this issue: assertion and proof. We briefly describe how each of the papers in the present publication has contributed from either different or complementary perspectives to the logical reflection on assertion and proof, while also specifying the relation between them.

This paper attempts to address the question what logical strength theories of truth have by considering such questions as: If you take a theory T and add a theory of truth to it, how strong is the resulting theory, as compared to T? It turns out that, in a wide range of cases, we can get some nice answers to this question, but only if we work in a framework that is somewhat different from those usually employed in discussions of (...) axiomatic theories of truth. These results are then used to address a range of philosophical questions connected with truth, such as what Tarski meant by "essential richness" and the so-called conservativeness argument against deflationism. -/- This draft dates from about 2009, with some significant updates having been made around 2011. Around then, however, I decided that the paper was becoming unmanageable and that I was trying to do too many things in it. I have therefore exploded the paper into several pieces, which will be published separately. These include "Disquotationalism and the Compositional Principles", "The Logical Strength of Compositional Principles", "Consistency and the Theory of Truth", and "What Is Essential Richness?" You should probably read those instead, since this draft remains a bit of a mess. Terminology and notation are inconsistent, and some of the proofs aren't quite right. So, caveat lector. I make it public only because it has been cited in a few places now. (shrink)