Cut elimination for systems of transparent truth with restricted initial sequents. (English) Zbl 1529.03270

Nicolai, Carlo

Notre Dame J. Formal Logic 62, No. 4, 619-642 (2021).

Summary: The paper studies a cluster of systems for fully disquotational truth based on the restriction of initial sequents. Unlike well-known alternative approaches, such systems display both a simple and intuitive model theory and remarkable proof-theoretic properties. We start by showing that, due to a strong form of invertibility of the truth rules, cut is eliminable in the systems via a standard strategy supplemented by a suitable measure of the number of applications of truth rules to formulas in derivations. Next, we notice that cut remains eliminable when suitable arithmetical axioms are added to the system. Finally, we establish a direct link between cut-free derivability in infinitary formulations of the systems considered and fixed-point semantics. Noticeably, unlike what happens with other background logics, such links are established without imposing any restriction to the premises of the truth rules.

MSC:

03F05	Cut-elimination and normal-form theorems
03A05	Philosophical and critical aspects of logic and foundations

Keywords:

cut elimination; formal theories of truth; substructural logic

References:

[1]	Beall, J. C., Spandrels of Truth, Oxford University Press, Oxford, 2009.
[2]	Burgess, J. P., “The truth is never simple,” Journal of Symbolic Logic, vol. 51 (1986), pp. 663-81. · Zbl 0634.03002 · doi:10.2307/2274021
[3]	Cantini, A., “A theory of formal truth arithmetically equivalent to \[{\mathsf{ID}_1} \],” Journal of Symbolic Logic, vol. 55 (1990), pp. 244-59. · Zbl 0713.03029 · doi:10.2307/2274965
[4]	Cantini, A., “The undecidability of Grišin’s set theory,” Studia Logica, vol. 74 (2003), pp. 345-68. · Zbl 1039.03040 · doi:10.1023/A:1025159016268
[5]	Cobreros, P., P. Egré, D. Ripley, and R. van Rooij, “Tolerant, classical, strict,” Journal of Philosophical Logic, vol. 41 (2012), pp. 347-85. · Zbl 1243.03038 · doi:10.1007/s10992-010-9165-z
[6]	Da Ré, B., and L. Rosenblatt, “Contraction, infinitary quantifiers, and omega paradoxes,” Journal of Philosophical Logic, vol. 47 (2018), pp. 611-29. · Zbl 1436.03143 · doi:10.1007/s10992-017-9441-2
[7]	Field, H., Saving Truth from Paradox, Oxford University Press, Oxford, 2008. · Zbl 1225.03006 · doi:10.1093/acprof:oso/9780199230747.001.0001
[8]	Fischer, M., “Modal predicates and their interaction,” Habilitationsschrift, Ludwig Maximilian University of Munich, Munich, 2018.
[9]	Fischer, M., and N. Gratzl, “Truth, partial logic and infinitary proof systems,” Studia Logica, vol. 106 (2018), pp. 515-40. · Zbl 1437.03160 · doi:10.1007/s11225-017-9751-y
[10]	Fjellstad, A., “A note on the cut-elimination proof in ‘Truth without contra(di)ction’,” Review of Symbolic Logic, vol. 13 (2020), pp. 882-86. · Zbl 1473.03035 · doi:10.1017/s1755020319000571
[11]	Grišin, V., “Predicate and set-theoretic calculi based on logic without the contraction rules,” Izvestiya Mathematics, vol. 18 (1982), pp. 41-59. · Zbl 0478.03009
[12]	Halbach, V., “Conservative theories of classical truth,” Studia Logica, vol. 62 (1999), pp. 353-70. · Zbl 0930.03086 · doi:10.1023/A:1005148426909
[13]	Halbach, V., and L. Horsten, “Axiomatizing Kripke’s theory of truth,” Journal of Symbolic Logic, vol. 71 (2006), pp. 677-712. · Zbl 1101.03005 · doi:10.2178/jsl/1146620166
[14]	Kotlarski, H., S. Krajewski, and A. H. Lachlan, “Construction of satisfaction classes for nonstandard models,” Canadian Mathematical Bulletin, vol. 24 (1981), pp. 283-93. · Zbl 0471.03054 · doi:10.4153/CMB-1981-045-3
[15]	Kremer, M., “Kripke and the logic of truth,” Journal of Philosophical Logic, vol. 17 (1988), pp. 225-78. · Zbl 0653.03002 · doi:10.1007/BF00247954
[16]	Kripke, S., “Outline of a theory of truth,” Journal of Philosophy, vol. 72 (1975), pp. 690-716. · Zbl 0952.03513 · doi:10.1007/BF00247954
[17]	Leigh, G. E., “Conservativity for theories of compositional truth via cut elimination,” Journal of Symbolic Logic, vol. 80 (2015), pp. 845-65. · Zbl 1376.03056 · doi:10.1017/jsl.2015.27
[18]	Leitgeb, H., “What truth depends on,” Journal of Philosophical Logic, vol. 34 (2005), pp. 155-92. · Zbl 1097.03005 · doi:10.1007/s10992-004-3758-3
[19]	Negri, S., and J. von Plato, Proof Analysis: A Contribution to Hilbert’s Last Problem, Cambridge University Press, Cambridge, 2011. · Zbl 1247.03001 · doi:10.1017/CBO9781139003513
[20]	Nicolai, C., and L. Rossi, “Principles for object-linguistic consequence: From logical to irreflexive,” Journal of Philosophical Logic, vol. 47 (2018), pp. 549-77. · Zbl 1436.03059 · doi:10.1007/s10992-017-9438-x
[21]	Nicolai, C., and L. Rossi, “A compositional theory of self-applicable consequence,” in preparation.
[22]	Pohlers, W., Proof Theory: A First Step into Impredicativity, Universitext, Springer, Berlin, 2009. · Zbl 1153.03001
[23]	Priest, G., Doubt Truth to Be a Liar, Oxford University Press, Oxford, 2005. · Zbl 1274.00014
[24]	Ripley, D., “Conservatively extending classical logic with transparent truth,” Review of Symbolic Logic, vol. 5 (2012), pp. 354-78. · Zbl 1248.03012 · doi:10.1017/S1755020312000056
[25]	Schröder-Heister, P., “Restricting initial sequents: The trade-offs between identity, contraction, cut,” pp. 339-51 in Advances in Proof Theory, edited by R. Kahle, T. Strahm, and T. Studer, vol. 28 of Progress in Computer Science and Applied Logic, Birkhäuser/Springer, Cham, 2016. · Zbl 1439.03098 · doi:10.1007/978-3-319-29198-7_10
[26]	Schwichtenberg, H., “Proof theory: Some applications of cut-elimination,” pp. 867-95 in Handbook of Mathematical Logic, edited by J. Barwise, vol. 90 of Studies in Logic and the Foundations of Mathematics, North-Holland, Amsterdam, 1977.
[27]	Troelstra, A. S., and H. Schwichtenberg, Basic Proof Theory, vol. 43 of Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, Cambridge, 1996. · Zbl 0868.03024
[28]	Zardini, E., “Truth without contra(di)ction,” Review of Symbolic Logic, vol. 4 (2011), pp. 498-535. · Zbl 1252.03018 · doi:10.1017/S1755020311000177