After sketching the main lines of Hilbert's program, certain well-known andinfluential interpretations of the program are critically evaluated, and analternative interpretation is presented. Finally, some recent developments inlogic related to Hilbert's program are reviewed.

In this paper are studied the properties of the proofs in PRA of provability logic sentences, i.e. of formulas which are Boolean combinations of formulas of the form PIPRA, where h is the Gödel-number of a sentence in PRA. The main result is a Normal Form Theorem on the proof-trees of provability logic sequents, which states that it is possible to split the proof into an arithmetical part, which contains only atomic formulas and has an essentially intuitionistic character, and into (...) a logical part, which is merely instrumental. Moreover, the induction rules which occur in the arithmetical part are implicit. Some applications of the Normal Form Theorem are shown in order to obtain some syntactical results on the PRA-completeness of modal logic. In particular a completeness theorem for Boolean combinations of modalities is given. (shrink)

We show that a consistent, finitely axiomatized, sequential theory cannot prove its own inconsistency on every definable cut. A corollary is that there are at least three degrees of global interpretability of theories equivalent modulo local interpretability to a consistent, finitely axiomatized, sequential theory U.

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)

Let ℸ be the set of Gödel numbers Gn of function symbols f such that PRA ⊢ and let γ be the function such that equation imageWe prove: The r. e. set ℸ is m-complete; the function γ is not primitive recursive in any class of functions {f1, f2, ⃛} so long as each fi has a recursive upper bound. This implies that γ is not primitive recursive in ℸ although it is recursive in ℸ.

Guaspari (J Symb Logic 48:777–789, 1983) conjectured that a modal formula is it essentially Σ1 (i.e., it is Σ1 under any arithmetical interpretation), if and only if it is provably equivalent to a disjunction of formulas of the form ${\square{B}}$ . This conjecture was proved first by A. Visser. Then, in (de Jongh and Pianigiani, Logic at Work: In Memory of Helena Rasiowa, Springer-Physica Verlag, Heidelberg-New York, pp. 246–255, 1999), the authors characterized essentially Σ1 formulas of languages including witness comparisons (...) using the interpretability logic ILM. In this note we give a similar characterization for formulas with a binary operator interpreted as interpretability in a finitely axiomatizable extension of IΔ 0 + Supexp and we address a similar problem for IΔ 0 + Exp. (shrink)

The modal logic of Gödel sentences, termed as GS, is introduced to analyze the logical properties of 'true but unprovable' sentences in formal arithmetic. The logic GS is, in a sense, dual to Grzegorczyk's Logic, where modality can be interpreted as 'true and provable'. As we show, GS and Grzegorczyk's Logic are, in fact, mutually embeddable. We prove Kripke completeness and arithmetical completeness for GS. GS is also an extended system of the logic of 'Essence and Accident' proposed by Marcos (...) (Bull Sect Log 34(1):43-56, 2005). We also clarify the relationships between GS and the provability logic GL and between GS and Intuitionistic Propositional Logic. (shrink)

In this note, a fully modal proof is given of some conservation results proved in a previous paper by arithmetic means. The proof is based on the extendability of Kripke models.

It is shown that for arithmetical interpretations that may include free variables it is not the Guaspari-Solovay system R that is arithmetically complete, but their system R –. This result is then applied to obtain the nonvalidity of some rules under arithmetical interpretations including free variables, and to show that some principles concerning Rosser orderings with free variables cannot be decided, even if one restricts oneself to usual proof predicates.

Given a 1-ary sentence operator , we describe L - another 1-ary operator - as as a left inverse of in a given logic if in that logic every formula is provably equivalent to L. Similarly R is a right inverse of if is always provably equivalent to R. We investigate the behaviour of left and right inverses for taken as the operator of various normal modal logics, paying particular attention to the conditions under which these logics are conservatively extended (...) by the addition of such inverses, as well as to the question of when, in such extensions, the inverses behave as normal modal operators in their own right. (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)

In this paper the PA-completeness of modal logic is studied by syntactical and constructive methods. The main results are theorems on the structure of the PA-proofs of suitable arithmetical interpretationsS of a modal sequentS, which allow the transformation of PA-proofs ofS into proof-trees similar to modal proof-trees. As an application of such theorems, a proof of Solovay's theorem on arithmetical completeness of the modal system G is presented for the class of modal sequents of Boolean combinations of formulas of the (...) form p i,m i=0, 1, 2, ... The paper is the preliminary step for a forthcoming global syntactical resolution of the PA-completeness problem for modal logic. (shrink)

It is argued that an instrumentalist notion of proof such as that represented in Hilbert's viewpoint is not obligated to satisfy the conservation condition that is generally regarded as a constraint on Hilbert's Program. A more reasonable soundness condition is then considered and shown not to be counter-exemplified by Godel's First Theorem. Finally, attention is given to the question of what a theory is; whether it should be seen as a "list" or corpus of beliefs, or as a method for (...) selecting beliefs. The significance of this question for assessing "intensional" results like Godel's Second Theorem, and their bearing on Hilbert's Program are discussed. (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)

This paper investigates the conditions under which diagonal sentences can be taken to constitute paradigmatic cases of self-reference. We put forward well-motivated constraints on the diagonal operator and the coding apparatus which separate paradigmatic self-referential sentences, for instance obtained via Gödel’s diagonalization method, from accidental diagonal sentences. In particular, we show that these constraints successfully exclude refutable Henkin sentences, as constructed by Kreisel.

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.

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.

Since Montague’s work it is well known that treating a single modality as a predicate may lead to paradox. In their paper “No Future”, Horsten and Leitgeb show that if the two temporal modalities are treated as predicates paradox might arise as well. In our paper we investigate whether paradoxes of multiple modalities, such as the No Future paradox, are genuinely new paradoxes or whether they “reduce” to the paradoxes of single modalities. In order to address this question we develop (...) a notion of reducibility based on a version of Smoryński Diagonalized Operator Logic. We show that there are reducible multimodal paradoxes as well as irreducible paradoxes of interaction. In particular, we show the No Future paradox to be an irreducible paradox according to our notion of reducibility. (shrink)

Solovay's 1976 completeness result for modal provability logic employs the recursion theorem in its proof. It is shown that the uses of the recursion theorem can in this proof replaced by the diagonalization lemma for arithmetic and that, in effect, the proof neatly fits the framework of another, enriched, system of modal logic so that any arithmetical system for which this logic is sound is strong enough to carry out the proof, in particular $\text{I}\Delta _{0}+\text{EXP}$ . The method is adapted (...) to obtain a similar completeness result for the Rosser logic. (shrink)

In [6] Albert Visser shows that ILP completely axiomatizes all schemata about provability and relative interpretability that are provable in finitely axiomatized theories. In this paper we introduce a system called $\text{ILP}^{\omega}$ that completely axiomatizes the arithmetically valid principles of provability in and interpretability over such theories. To prove the arithmetical completeness of $\text{ILP}^{\omega}$ we use a suitable kind of tail models; as a byproduct we obtain a somewhat modified proof of Visser's completeness result.

In researching presuppositions dealing with logic and dynamic of belief we distinguish two related parts. The first part refers to presuppositions and logic, which is not necessarily involved with intentional operators. We are primarily concerned with classical, free and presuppositonal logic. Here, we practice a well known Strawson’s approach to the problem of presupposition in relation to classical logic. Further on in this work, free logic is used, especially Van Fraassen’s research of the role of presupposition in supervaluations logical systems. (...) At the end of the first part, presuppositional logic, advocated by S.K. Thomason, is taken into consideration. The second part refers to the presuppositions in relation to the logic of the dynamics of belief. Here the logic of belief change is taken into consideration and other epistemic notions with immanent mechanism for the presentation of the dynamics. Three representative and dominant approaches are evaluated. First, we deal with new, less classical, situation semantics. Besides Strawson’s theory, the second theory is the theory of the belief change, developed by Alchourron, Gärdenfors, and Makinson (AGM theory). At the end, the oldest, universal, and dominant approach is used, recognized as Hintikka’s approach to the analysis of epistemic notions. (shrink)

This paper contains a careful derivation of principles of Interpretability Logic valid in extensions of I0+1.

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)

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)

We demonstrate that, in itself and in the absence of extra premises, the following argument scheme is fallacious: The sentence A says about itself that it has a property F, and A does in fact have the property F; therefore A is true. We then examine an argument of this form in the informal introduction of Gödel’s classic (1931) and examine some auxiliary premises which might have been at work in that context. Philosophically significant as it may be, that particular (...) informal argument plays no rôle in Gödel’s technical results. Going deeper into the issue and investigating truth conditions of Gödelian sentences (i.e., those sentences which are provably equivalent to their own unprovability) will provide us with insights regarding the philosophical debate on the truth of Gödelian sentences of systems—a debate which goes back to Dummett (1963). (shrink)

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 show that the modal prepositional logicILM (interpretability logic with Montagna's principle), which has been shown sound and complete as the interpretability logic of Peano arithmetic PA (by Berarducci and Savrukov), is sound and complete as the logic ofπ 1-conservativity over eachbE 1-sound axiomatized theory containingI⌆ 1 (PA with induction restricted tobE 1-formulas). Furthermore, we extend this result to a systemILMR obtained fromILM by adding witness comparisons in the style of Guaspari's and Solovay's logicR (this will be done in a (...) separate continuation of the present paper). (shrink)

Niklas Luhmann verwendet in seiner soziologischen Systemtheorie offenbar etwas, das er den Büchern des englischen Mathematikers George Spencer Brown entnimmt. Dessen Formenkalkül ist für Luhmann, wie Günther Schulte treffend bemerkt, “Mädchen für alles, mit dem er nicht nur in der Lage ist Teezukochen, sondern auch Auto oder Straßenbahn zu fahren”. Der erste Blick in Spencer Browns Laws of Form vermittelt einen anderen Eindruck: nichts scheinen sie mit soziologischer Systemtheorie zu tun zu haben. Der vorliegende Text bearbeitet hieran anknüpfend eine recht (...) bescheidene Frage, die sich gleichwohl jedem Luhmann-Leser schon einmal gestellt haben dürfte: Was wollen die Laws of Form und was will Luhmann mit ihnen? Als Antwort ergibt sich, nach Zurückverfolgung der relevanten Fußnoten, eine gute und eine schlechte Nachricht. Die schlechte Nachricht ist, daß die Lektüre der Laws of Form offenbar niemandem wirklich weiterhelfen kann, auch Luhmann selbst nicht. Die gute ist folglich, daß dem Luhmann-Leser die Notwendigkeit erspart bleibt, einen so dunklen, weil sparsamen Kalkül zu verstehen. Das meiste nämlich, was Luhmann den Laws of Form angeblich entnimmt, steht auf den zweiten Blick nicht darin. Er wird es also ohnehin durch andere Texte begründen müssen. (shrink)

We prove that the first order theory of the fixed point algebra corresponding to an r.e. consistent theory containing arithmetic is hereditarily undecidable.

In [6] Albert Visser shows that ILP completely axiomatizes all schemata about provability and relative interpretability that are provable in finitely axiomatized theories. In this paper we introduce a system called ILP that completely axiomatizes the arithmetically valid principles of provability in and interpretability over such theories. To prove the arithmetical completeness of ILP we use a suitable kind of tail models; as a byproduct we obtain a somewhat modified proof of Visser's completeness result.

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.

Solovay's 1976 completeness result for modal provability logic employs the recursion theorem in its proof. It is shown that the uses of the recursion theorem can in this proof be replaced by the diagonalization lemma for arithmetic and that, in effect, the proof neatly fits the framework of another, enriched, system of modal logic (the so-called Rosser logic of Gauspari-Solovay, 1979) so that any arithmetical system for which this logic is sound is strong enough to carry out the proof, in (...) particular I0+EXP. The method is adapted to obtain a similar completeness result for the Rosser logic. (shrink)

The modal completeness proofs of Guaspari and Solovay (1979) for their systems R and R – are improved and the relationship between R and R – is clarified.

This paper provides several examples of how modal logic can be used in studying the XML document navigation language XPath. More specifically, we derive complete axiomatizations, computational complexity and expressive power results for XPath fragments from known results for corresponding logics. A secondary aim of the paper is to introduce XPath in a way that makes it accessible to an audience of modal logicians.

It is shown that the propositional modal logic IRM (interpretability logic with Montagna's principle and with witness comparisons in the style of Guaspari's and Solovay's logicR) is sound and complete as the logic ofII 1-conservativity over each∑ 1-sound axiomatized theory containingI∑ 1. The exact statement of the result uses the notion of standard proof predicate. This paper is an immediate continuation of our paper [HM]. Knowledge of [HM] is presupposed. We define a modal logic, called IRM, which includes both ILM (...) andR (the logic of [GS]) and prove an arithmetical completeness theorem in the style of [GS], thus showing that IRM is the logic ofII 1-conservativity with witness comparisons. The reader is recommended to have Smoryński's book [Sm] at his/her disposal. (shrink)

The Knowability Paradox purports to show that the controversial but not patently absurd hypothesis that all truths are knowable entails the implausible conclusion that all truths are known. The notoriety of this argument owes to the negative light it appears to cast on the view that there can be no verification-transcendent truths. We argue that it is overly simplistic to formalize the views of contemporary verificationists like Dummett, Prawitz or Martin-Löf using the sort of propositional modal operators which are employed (...) in the original derivation of the Paradox. Instead we propose that the central tenet of verificationism is most accurately formulated as follows: if φ is true, then there exists a proof of φ Building on the work of Artemov (Bull Symb Log 7(1): 1-36, 2001), a system of explicit modal logic with proof quantifiers is introduced to reason about such statements. When the original reasoning of the Paradox is developed in this setting, we reach not a contradiction, but rather the conclusion that there must exist non-constructed proofs. This outcome is evaluated relative to the controversy between Dummett and Prawitz about proof existence and bivalence. (shrink)