Informal Provability, First-Order BAT Logic and First Steps Towards a Formal Theory of Informal Provability
DOI:
https://doi.org/10.12775/LLP.2021.016Keywords
non-deterministic logics, informal provability, BAT logicAbstract
BAT is a logic built to capture the inferential behavior of informal provability. Ultimately, the logic is meant to be used in an arithmetical setting. To reach this stage it has to be extended to a first-order version. In this paper we provide such an extension. We do so by constructing non-deterministic three-valued models that interpret quantifiers as some sorts of infinite disjunctions and conjunctions. We also elaborate on the semantical properties of the first-order system and consider a couple of its strengthenings. It turns out that obtaining a sensible strengthening is not straightforward. We prove that most strategies commonly used for strengthening non-deterministic logics fail in our case. Nevertheless, we identify one method of extending the system which does not.
References
Alexander, S., 2013, “A machine that knows its own code”, arXiv preprint arXiv:1305.6080. DOI: https://doi.org/10.1007/s11225-013-9491-6
Antonutti Marfori, M., 2010, “Informal proofs and mathematical rigour”, Studia Logica 96: 261–272. DOI: https://doi.org/10.1007/s11225-010-9280-4
Antonutti Marfori, M., and L. Horsten, 2016, “Epistemic Church’s thesis and absolute undecidability”, page 254 in Gödel’s Disjunction: The Scope and Limits of Mathematical Knowledge. DOI: https://doi.org/10.1093/acprof:oso/9780198759591.003.0011
Antonutti Marfori, M., and L. Horsten, 2018, “Human-effective computability”, Philosophia Mathematica 27 (1): 61–87. DOI: https://doi.org/10.1093/philmat/nky011
Arai, T., 1998, “Some results on cut-elimination, provable well-orderings, induction and reflection”, Annals of Pure and Applied Logic 95 (1–3): 93–184. DOI: https://doi.org/10.1016/s0168-0072(98)00020-7
Beklemishev, L., 1997, “Induction rules, reflection principles, and provably recursive functions”, Annals of Pure and Applied Logic 85 (3): 193–242. DOI: https://doi.org/10.1016/s0168-0072(96)00045-0
Beklemishev, L., 2003, “Proof-theoretic analysis by iterated reflection”, Archive for Mathematical Logic 42 (6): 515–55. DOI: https://doi.org/10.1007/978-3-319-22156-4_9
Bellantoni, S., and M. Hofmann, 2002, “A new ‘feasible’ arithmetic” The Journal of Symbolic Logic 67 (1): 104–116. DOI: https://doi.org/10.2178/jsl/1190150032
Carlson, T., 2016, “Collapsing knowledge and epistemic Church’s thesis”, pages 129–147 in L. Horsten and P. Welch (eds.), Gödel’s Disjunction: The scope and limits of mathematical knowledge, Oxford Scholarship Online. DOI: https://doi.org/10.1093/acprof:oso/9780198759591.003.0006
Carlson, T. J., 2000, “Knowledge, machines, and the consistency of Reinhardt’s strong mechanistic thesis”, Annals of Pure and Applied Logic 105 (1–3): 51–82. DOI: https://doi.org/10.1016/s0168-0072(99)00048-2
Enderton, H., 1977, Elements of Set Theory, Academic Press, New York. DOI: https://doi.org/10.1016/C2009-0-22079-4
Flagg, R., 1985, “Church’s thesis is consistent with epistemic arithmetic”, pages 121–172 in S. Shapiro (ed.), Intensional Mathematics, Studies in Logic and the Foundations of Mathematics, Vol. 113, North-Holland. DOI: https://doi.org/10.1016/s0049-237x(08)70142-3
Flagg, R., and H. Friedman, 1986, “Epistemic and intuitionistic formal systems”, Annals of Pure and Applied Logic 32 (1): 53–60. DOI: https://doi.org/10.1016/0168-0072(86)90043-6
Friedman, H., and M. Sheard, 1989, “The equivalence of the disjunction and existence properties for modal arithmetic”, The Journal of Symbolic Logic 54 (4): 1456–1459. DOI: https://doi.org/10.2307/2274825
Goodman, N. D., 1984, “Epistemic arithmetic is a conservative extension of intuitionistic arithmetic”, Journal of Symbolic Logic 49 (1): 192–203. DOI: https://doi.org/10.2307/2274102
Goodman, N. D., 1986, “Flagg realizability in arithmetic”, The Journal of Symbolic Logic 51 (2): 387–392. DOI: https://doi.org/10.2307/2274062
Halbach, V., 2011, Axiomatic Theories of Truth, Cambridge University Press.
Halbach, V., and L. Horsten, 2000, “Two proof-theoretic remarks on EA + ECT”, Mathematical Logic Quarterly 46 (4): 461–466. DOI: doi.org/10.1002/1521-3870(200010)46:4<461::aid-malq461>3.0.co;2-i
Heylen, J., 2013, “Modal-epistemic arithmetic and the problem of quantifying in”, Synthese 190 (1): 89–111. DOI: https://doi.org/10.1007/s11229-012-0154-3
Horsten, L., 1994, “Modal-epistemic variants of Shapiro’s system of epistemic arithmetic”, Notre Dame Journal of Formal Logic 35 (2): 284–291. DOI: https://doi.org/10.1305/ndjfl/1094061865
Horsten, L., 1996, “Reflecting in epistemic arithmetic”, The Journal of Symbolic Logic 61: 788–801. DOI: https://doi.org/10.2307/2275785
Horsten, L., 1997, “Provability in principle and controversial constructivistic principles”, Journal of Philosophical Logic 26 (6): 635–660. DOI: https://doi.org/10.1023/a:1017954806119
Horsten, L., 1998, “In defence of epistemic arithmetic”, Synthese 116: 1–25.DOI: https://doi.org/10.1023/A:1005016405987
Horsten, L., 2002, “An axiomatic investigation of provability as a primitive predicate”, pages 203–220 in V. Halbach and L. Horsten (eds.), Principles of Truth, Hansel-Hohenhausen. DOI: https://doi.org/10.1515/9783110332728.203
Horsten, L., 2006, “Formalizing Church’s thesis”, Church’s Thesis After 70: 253–267. DOI: https://doi.org/10.1515/9783110325461.253
Kearns, J. T., 1981, “Modal semantics without possible worlds”, The Journal of Symbolic Logic 46 (1): 77–86. DOI: https://doi.org/10.2307/2273259
Koellner, P., 2016, “Gödel’s disjunction”, in L. Horsten and P. Welch (eds.), Gödel’s Disjunction: The Scope and Limits of Mathematical Knowledge, Oxford Scholarship Online. DOI: https://doi.org/10.1093/acprof:oso/9780198759591.003.0007
Kripke, S. A., 1975, “Outline of a theory of truth”, Journal of Philosophy 72 (19): 690–716. DOI: https://doi.org/10.2307/2024634
Leitgeb, H., 2009, “On formal and informal provability”, pages 263–299 in O. Bueno and Ø. Linnebo (eds.), New Waves in Philosophy of Mathematics, New York: Palgrave Macmillan. DOI: https://doi.org/10.1057/9780230245198_13
Montague, R., 1963, “Syntactical treatments of modality, with corollaries on reflexion principles and finite axiomatizability”, Acta Philosophica Fennica (16): 153–167. DOI: https://doi.org/10.2307/2271809
Myhill, J., 1960, “Some remarks on the notion of proof”, Journal of Philosophy 57 (14): 461–471. DOI: https://doi.org/10.2307/2023664
Omori, H., and D. Skurt, 2016, “More modal semantics without possible worlds”, IfCoLog Journal of Logics and their Applications 3 (5): 815–845.
Pawlowski, P., and R. Urbaniak, 2018, “Many-valued logic of informal provability: A non-deterministic strategy”, The Review of Symbolic Logic 11 (2): 207–223. DOI: https://doi.org/10.1017/S1755020317000363
Rav, Y., 1999, “Why do we prove theorems?”, Philosophia Mathematica 7 (1): 5–41. DOI: https://doi.org/10.1093/philmat/7.1.5
Rav, Y., 2007, “A critique of a formalist-mechanist version of the justification of arguments in mathematicians’ proof practices”, Philosophia Mathematica 15 (3): 291–320. DOI: https://doi.org/10.1093/philmat/nkm023
Reinhardt, W. N., 1985, “The consistency of a variant of, Church’s thesis with an axiomatic theory of an epistemic notion”, Revista Colombiana de Matemáticas 19 (1-2): 177–200.
Reinhardt, W. N., 1986, “Epistemic theories and the interpretation of Gödel’s incompleteness theorems”, Journal of Philosophical Logic 15 (4): 427–74. DOI: https://doi.org/10.1007/bf00243392
Rin, B. G., and S. Walsh, 2016, “Realizability semantics for quantified modal logic: Generalizing Flagg’s 1985 construction”, The Review of Symbolic Logic 9 (4): 752–809. DOI: https://doi.org/10.1017/S1755020316000095
Shapiro, S., 1985, “Epistemic and intuitionistic arithmetic”, in S. Shapiro (ed.), Intensional Mathematics, Studies in Logic and the Foundations of Mathematics, Vol. 113, North-Holland. DOI: https://doi.org/10.1016/s0049-237x(08)70138-1
Stern, J., 2015, Toward Predicate Approaches to Modality, Trends in Logic, Springer. DOI: https://doi.org/10.1007/978-3-319-22557-9
Tanswell, F., 2015, “A problem with the dependence of informal proofs on formal proofs”, Philosophia Mathematica 23 (3): 295–310. DOI: https://doi.org/10.1093/philmat/nkv008
Downloads
Published
How to Cite
Issue
Section
License
Copyright (c) 2021 Logic and Logical Philosophy
This work is licensed under a Creative Commons Attribution-NoDerivatives 4.0 International License.
Stats
Number of views and downloads: 1295
Number of citations: 0
