×
Dean, Walter

Montague’s paradox, informal provability, and explicit modal logic. (English) Zbl 1352.03062

Notre Dame J. Formal Logic 55, No. 2, 157-196 (2014).
Summary: 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(x)\) satisfying (T) \(P(\ulcorner\phi\urcorner)\to\phi\) and (NEC \(T\vdash\phi\therefore\;T\vdash P(\ulcorner\phi\urcorner)\) 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 QLP (the quantified logic of proofs) of Artemov’s logic of proofs (LP). QLP contains both explicit modalities \(t:\phi\) (“\(t\) is a proof of \(\phi\)”) and also proof quantifiers \((\exists x)x:\phi\) (“there exists a proof of \(\phi\)”). 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.

Cited in 1 Document

MSC:

03F03 Proof theory in general (including proof-theoretic semantics)
03F45 Provability logics and related algebras (e.g., diagonalizable algebras)
03F50 Metamathematics of constructive systems

Keywords:

Montague’s paradox; knower paradox; constructive proof; informal proof; provability logic; explicit modal logic; justification logic
PDF BibTeX XML Cite
\textit{W. Dean}, Notre Dame J. Formal Logic 55, No. 2, 157--196 (2014; Zbl 1352.03062)
Full Text: DOI Euclid
  • logo of hbz
  • logo of WorldCat

References:

[1] Anderson, C. A., “The paradox of the knower,” Journal of Philosophy , vol. 80 (1984), pp. 338-55.
[2] Artemov, S., Operational Modal Logic , Technical Report no. 95-29, Mathematical Sciences Institute, Cornell University, 1995.
[3] Artemov, S., “Explicit provability and constructive semantics,” Bulletin of Symbolic Logic , vol. 7 (2001), pp. 1-36. · Zbl 0980.03059
[4] Beeson, M. J., Foundations of Constructive Mathematics: Metamathematical Studies , vol. 6 of Ergebnisse der Mathematik und ihrer Grenzgebiete 3 , Springer, Berlin, 1985. · Zbl 0565.03028
[5] Berarducci, A., and R. Verbrugge, “On the provability logic of bounded arithmetic,” pp. 75-93 in Provability, Interpretability and Arithmetic Symposium (Utrecht, 1991) , vol. 61 of Annals of Pure and Applied Logic , 1993. · Zbl 0803.03037
[6] Bezboruah, A., and J. C. Shepherdson, “Gödel’s second incompleteness theorem for \(Q\),” Journal of Symbolic Logic , vol. 41 (1976), pp. 503-12. · Zbl 0328.02017
[7] Boolos, G., The Logic of Provability , Cambridge University Press, Cambridge, 1993. · Zbl 0891.03004
[8] Burgess, J. P., “Which modal logic is the right one?” Notre Dame Journal of Formal Logic , vol. 40 (1999), pp. 81-93. · Zbl 0972.03018
[9] Chagrov, A., and M. Zakharyashchev, “Modal companions of intermediate propositional logics,” Studia Logica , vol. 51 (1992), pp. 49-82. · Zbl 0766.03015
[10] Curry, H. B., and R. Feys, Combinatory Logic, Vol. 1: Studies in Logic and the Foundations of Mathematics , North-Holland, Amsterdam, 1958.
[11] Dean, W., “Epistemic paradox and explicit modal logic,” Ph.D. dissertation, City University of New York, New York, 2010.
[12] Dean, W., and H. Kurokawa, “Knowledge, proof and the Knower,” pp. 81-90 in Proceedings of the 12th Conference on Theoretical Aspects of Rationality and Knowledge , ACM, 2009.
[13] Dummett, M., Elements of Intuitionism , 2nd edition, vol. 39 of Oxford Logic Guides , Oxford University Press, New York, 2000. · Zbl 0949.03059
[14] Égré, P., “The Knower paradox in the light of provability interpretations of modal logic,” Journal of Logic, Language and Information , vol. 14 (2005), pp. 13-48. · Zbl 1067.03008
[15] Feferman, S., “Arithmetization of metamathematics in a general setting,” Fundamenta Mathematicae , vol. 49 (1960/1961), pp. 35-92. · Zbl 0095.24301
[16] Fitting, M., “Quantified LP,” Technical Report no. TR-2004019, CUNY Ph.D. Program in Computer Science, City University of New York, N. Y., 2004.
[17] Fitting, M., “A quantified logic of evidence,” Annals of Pure and Applied Logic , vol. 152 (2008), pp. 67-83. · Zbl 1133.03008
[18] Franks, C., The Autonomy of Mathematical Knowledge: Hilbert’s Program Revisited , Cambridge University Press, Cambridge, 2009. · Zbl 1192.00012
[19] Friedman, H., and M. Sheard, “An axiomatic approach to self-referential truth,” Annals of Pure and Applied Logic , vol. 33 (1987), pp. 1-21. · Zbl 0634.03058
[20] Gödel, K., “An interpretation of the intuitionistic propositional calculus,” pp. 301-3 in Kurt Gödel: Collected Works, Vol. I, Publications 1929-1936 , edited by S. Feferman, Oxford University Press, Oxford, 1986.
[21] Gödel, K., “On formally undecidable propositions of Principia Mathematica and related systems, I,” pp. 144-95 in Kurt Gödel: Collected Works, Vol. I, Publications 1929-1936 , edited by S. Feferman, Oxford University Press, Oxford, 1986.
[22] Gödel, K., “On intuitionistic arithmetic and number theory,” pp. 287-95 in Kurt Gödel: Collected Works, Vol. I, Publications 1929-1936 , edited by S. Feferman, Oxford University Press, Oxford, 1986.
[23] Gödel, K., “Lecture at Zilsel’s,” pp. 62-113 in Kurt Gödel: Collected Works, Vol. III, Unpublished Lectures and Essays , edited by S. Feferman, Oxford University Press, Oxford, 1995.
[24] Gödel, K., “The present situation in the foundations of mathematics,” pp. 36-53 in Kurt Gödel: Collected Works, Vol. III, Unpublished Lectures and Essays , edited by S. Feferman, Oxford University Press, Oxford, 1995.
[25] Goodman, N. D., “A theory of constructions equivalent to arithmetic,” pp. 101-20 in Intuitionism and Proof Theory (Buffalo, N.Y., 1968) , edited by J. Kino and R. Vesley, North-Holland, Amsterdam, 1970. · Zbl 0212.31301
[26] Halbach, V., Axiomatic Theories of Truth , Cambridge University Press, Cambridge, 2011. · Zbl 1223.03001
[27] Halldén, S., “A Pragmatic Approach to Modal Theory,” Acta Philosophica Fennica , vol. 16 (1963), pp. 53-64.
[28] Heyting, A., Mathematische Grundlagenforschung: Intuitionismus, Beweistheorie , Springer, Berlin, 1934. · Zbl 0009.38501
[29] Heyting, A., Intuitionism: An Introduction . North-Holland, Amsterdam, 1956. · Zbl 0070.00801
[30] Hilbert, D., and P. Bernays, Grundlagen der Mathematik, I , vol. 40 of Grundlehren der Mathematischen Wissenschaften , Springer, Berlin, 1968. · Zbl 0191.28402
[31] Isaacson, D., “Some considerations on arithmetical truth and the \(\omega\)-rule,” pp. 94-138 in Proof, Logic and Formalization , edited by M. Detlefsen, Routledge, London, 1992.
[32] Kaplan, D., and R. Montague, “A paradox regained,” Notre Dame Journal of Formal Logic , vol. 1 (1960), pp. 79-90. · Zbl 0112.00409
[33] Kreisel, G., “Foundations of intuitionistic logic,” pp. 198-210 in Logic, Methodology and Philosophy of Science (Proc. 1960 Internat. Cong.) , vol. 44 of Studies in Logic and the Foundations of Mathematics , Stanford University Press, Stanford, Calif., 1962. · Zbl 0133.24801
[34] Kreisel, G., “Mathematical logic,” pp. 95-195 in Lectures on Modern Mathematics, Vol. III , edited by T. Saaty, Wiley, New York, 1965. · Zbl 0147.24703
[35] Kreisel, G., “Church’s thesis: A kind of reducibility axiom for constructive mathematics,” pp. 121-150 in Intuitionism and Proof Theory (Buffalo, N.Y., 1968) , North-Holland, Amsterdam, 1970. · Zbl 0199.30001
[36] Kripke, S. A., “Semantical considerations on modal logic,” Acta Philosophica Fennica , vol. 16 (1963), pp. 83-94. · Zbl 0131.00602
[37] Kripke, S. A., “Outline of a theory of truth,” Journal of Philosophy , vol. 72 (1975), pp. 690-716. · Zbl 0952.03513
[38] Leitgeb, H., “Theories of truth which have no standard models,” Studia Logica , vol. 68 (2001), pp. 69-87. · Zbl 0991.03054
[39] Leitgeb, H., “On formal and informal provability,” pp. 263-299 in New Waves in Philosophy of Mathematics , edited by O. Bueno and O. Linnebo, Palgrave Macmillan, 2009. · Zbl 1261.03035
[40] McCarty, C., “Constructive validity is nonarithmetic,” Journal of Symbolic Logic , vol. 53 (1988), pp. 1036-41. · Zbl 0724.03034
[41] McGee, V., “How truthlike can a predicate be? A negative result,” Journal of Philosophical Logic , vol. 14 (1985), pp. 399-410. · Zbl 0583.03002
[42] McKinsey, J. C. C., and A. Tarski, “Some theorems about the sentential calculi of Lewis and Heyting,” Journal of Symbolic Logic , vol. 13 (1948), pp. 1-15. · Zbl 0037.29409
[43] Montague, R., “Syntactical treatments of modality, with corollaries on reflexion principles and finite axiomatizability,” Acta Philosophica Fennica , vol. 16 (1963), pp. 153-67. · Zbl 0117.01302
[44] Myhill, J., “Some remarks on the notion of proof,” Journal of Philosophy , vol. 57 (1960), pp. 461-71.
[45] Pudlák, P., “On the lengths of proofs of consistency: A survey of results,” pp. 65-86 in Collegium Logicum, Vol. 2 , vol. 2 of Collegium Logicum, Annals of the Kurt-Gödel-Society , Springer, Vienna, 1996. · Zbl 0855.03032
[46] Rav, Y., “Why do we prove theorems? Mathematical proof,” Philosophia Mathematica, Series III , vol. 7 (1999), pp. 5-41. · Zbl 0941.03003
[47] Reinhardt, W. N., “Absolute versions of incompleteness theorems,” Noûs , vol. 19 (1985), pp. 317-46. · Zbl 1366.03236
[48] Shapiro, S., “Epistemic and intuitionistic arithmetic,” pp. 11-46 in Intensional Mathematics , edited by S. Shapiro, vol. 113 of Studies in Logic and the Foundations of Mathematics , North-Holland, Amsterdam, 1985. · Zbl 0559.03036
[49] Smoryński, C., Self-reference and Modal Logic , Springer, New York, 1985. · Zbl 0596.03001
[50] Sundholm, G., “Constructions, proofs and the meaning of logical constants,” Journal of Philosophical Logic , vol. 12 (1983), pp. 151-72. · Zbl 0539.03038
[51] Tait, W. W., “Gödel’s interpretation of intuitionism,” Philosophia Mathematica, Series III , vol. 14 (2006), pp. 208-28. · Zbl 1111.03004
[52] Tarski, A., “The concept of truth in formalized languages,” pp. 152-278 in Logic, Semantics, Metamathematics , edited by A. Tarski, Oxford University Press, Oxford, 1956.
[53] Troelstra, A. S., Principles of Intuitionism , vol. 95 of Lecture Notes in Mathematics , Springer, Berlin, 1969. · Zbl 0181.00504
[54] Troelstra, A. S., and H. Schwichtenberg, Basic Proof Theory , 2nd edition, vol. 43 of Cambridge Tracts in Theoretical Computer Science , Cambridge University Press, Cambridge, 2000. · Zbl 0957.03053
[55] Troelstra, A. S., and D. van Dalen, Constructivism in Mathematics, Vol. I: An Introduction , vol. 121 of Studies in Logic and the Foundations of Mathematics , North-Holland, Amsterdam, 1988. · Zbl 0653.03040
[56] van Atten, M., “The development of intuitionistic logic,” Stanford Encyclopedia of Philosophy , edited by E. N. Zalta, published electronically April 1, 2009.
[57] Weinstein, S., “The intended interpretation of intuitionistic logic,” Journal of Philosophical Logic , vol. 12 (1983), pp. 261-70. · Zbl 0539.03037
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.