Formalizing Axiomatic Theories of Truth
Summary
We investigate the possibility of formalizing the proof of the conservativity of TB in Halbach [1, p. 55f], in the interactive theorem prover Lean. Lean is based on dependent type theory, which has a natural connection to the Brouwer-Heyting-Kolmogorov (BHK) interpretation of intuitionistic logic via the Curry-Howard correspondence, effectively reducing checking for proof correctness to type-correctness.
The theorem prover already features an extensive library of undergraduate math, called mathlib, but so far little work in Axiomatic Theories of Truth has been formalized. Hence, we present our conceptual work of explicitizing implicit steps in Halbach's proof as well as their translation to Lean's type theory, focusing on lessons to be drawn for the future work in the formalization in this area of research.
[1] Volker Halbach. Axiomatic Theories of Truth. Cambridge University Press, 1 edition, 2011.