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 [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.

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)

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)

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)

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)

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)

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)

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

This paper is a comparative study of the propositional intuitionistic (non-modal) and classical modal languages interpreted in the standard way on transitive frames. It shows that, when talking about these frames rather than conventional quasi-orders, the intuitionistic language displays some unusual features: its expressive power becomes weaker than that of the modal language, the induced consequence relation does not have a deduction theorem and is not protoalgebraic. Nevertheless, the paper develops a manageable model theory for this consequence and its extensions (...) which also reveals some unexpected phenomena. The balance between the intuitionistic and modal languages is restored by adding to the former one more implication. (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 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.

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.

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.

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

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)

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)

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.

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)

The book provides a historical and systematic exposition of the semantic theory of truth formulated by Alfred Tarski in the 1930s. This theory became famous very soon and inspired logicians and philosophers. It has two different, but interconnected aspects: formal-logical and philosophical. The book deals with both, but it is intended mostly as a philosophical monograph. It explains Tarski’s motivation and presents discussions about his ideas as well as points out various applications of the semantic theory of truth to philosophical (...) problems. (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 \.

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.

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)

Paradox is a logical phenomenon. Usually, it is produced in type theory, on a type Ω of “truth values”. A formula Ψ (i.e., a term of type Ω) is presented, such that Ψ↔¬Ψ (with negation as a term¬∶Ω→Ω)-whereupon everything can be proved: In Sect. 1 we describe a general pattern which many constructions of the formula Ψ follow: for example, the well known arguments of Cantor, Russell, and Gödel. The structure uncovered behind these paradoxes is generalized in Sect. 2. This (...) allows us to show that Reynolds' [R] construction of a typeA ≃℘℘A in polymorphic λ-calculus cannot be extended, as conjectured, to give a fixed point ofevery variable type derived from the exponentiation: for some (contravariant) types, such a fixed point causes a paradox.Pursueing the idea that $$\frac{{{\text{type theory}}}}{{{\text{categorical interpretation}}}} = \frac{{{\text{(propositional) logic}}}}{{{\text{Lindebaum algebra}}}}$$ the language of categories appears here as a natural medium for logical structures. It allows us to abstract from the specific predicates that appear in particular paradoxes, and to display the underlying constructions in “pure state”. The essential role of cartesian closed categories in this context has been pointed out in [L]. The paradoxes studied here remain within the limits of the cartesian closed structure of types, as sketched in this Lawvere's seminal paper — and do not depend on any logical operations on the type Ω. Our results can be translated in simply typed λ-calculus in a straightforward way (although some of them do become a bit messy). (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.

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 ℸ.

We investigate, for several modal logics but concentrating on KT, KD45, S4 and S5, the set of formulas B for which ${\square B}$ is provably equivalent to ${\square A}$ for a selected formula A (such as p, a sentence letter). In the exceptional case in which a modal logic is closed under the (‘cancellation’) rule taking us from ${\square C \leftrightarrow \square D}$ to ${C \leftrightarrow D}$ , there is only one formula B, to within equivalence, in this inverse image, (...) as we shall call it, of ${\square A}$ (relative to the logic concerned); for logics for which the intended reading of “ ${\square}$ ” is epistemic or doxastic, failure to be closed under this rule indicates that from the proposition expressed by a knowledge- or belief-attribution, the propositional object of the attitude in question cannot be recovered: arguably, a somewhat disconcerting situation. More generally, the inverse image of ${\square A}$ may comprise a range of non-equivalent formulas, all those provably implied by one fixed formula and provably implying another—though we shall see that for several choices of logic and of the formula A, there is not even such an ‘interval characterization’ of the inverse image (of ${\square A}$ ) to be found. (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.

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 is an attempt to bring together two separated areas of research: classical mathematics and metamathematics on the one side, non-monotonic reasoning on the other. This is done by simulating nonmonotonic logic through antitonic theory extensions. In the first half, the specific extension procedure proposed here is motivated informally, partly in comparison with some well-known non-monotonic formalisms. Operators V and, more generally, U are obtained which have some plausibility when viewed as giving nonmonotonic theory extensions. In the second half, (...) these operators are treated from a mathematical and metamathematical point of view. Here an important role is played by U -closed theories and U -fixed points. The last section contains results on V-closed theories which are specific for V. (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.

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

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 onself to "usual" proof predicates.

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)