The goal of this paper is to explore the significance of Montague’s paradox—that is, any arithmetical theory $T\supseteq Q$ over a language containing a predicate $P$ satisfying $P\rightarrow \varphi $ and $T\vdash \varphi \,\therefore\,T\vdash P$ is inconsistent—as a limitative result pertaining to the notions of formal, informal, and constructive provability, in their respective historical contexts. To this end, the paradox is reconstructed in a quantified extension $\mathcal {QLP}$ of Artemov’s logic of proofs. $\mathcal {QLP}$ contains both explicit modalities $t:\varphi $ (...) and also proof quantifiers $x:\varphi $. In this system, the basis for the rule NEC is decomposed into a number of distinct principles governing how various modes of reasoning about proofs and provability can be internalized within the system itself. A conceptually motivated resolution to the paradox is proposed in the form of an argument for rejecting the unrestricted rule NEC on the basis of its subsumption of an intuitively invalid principle pertaining to the interaction of proof quantifiers and the proof-theorem relation expressed by explicit modalities. (shrink)

The question, "Which modal logic is the right one for logical necessity?," divides into two questions, one about model-theoretic validity, the other about proof-theoretic demonstrability. The arguments of Halldén and others that the right validity argument is S5, and the right demonstrability logic includes S4, are reviewed, and certain common objections are argued to be fallacious. A new argument, based on work of Supecki and Bryll, is presented for the claim that the right demonstrability logic must be contained in S5, (...) and a more speculative argument for the claim that it does not include S4.2 is also presented. (shrink)