The Friedman-Sheard programme in intuitionistic logic (Q2915893)

In a major proposal for an axiomatic theory of truth, \textit{H. Friedman} and \textit{M. Sheard} [Ann. Pure Appl. Logic 33, 1--21 (1987; Zbl 0634.03058)] introduced twelve desirable properties of truth, called optional axioms, expressed in a language with a unary truth predicate, and have determined nine maximal consistent subsets of the twelve axioms as the only consistent maximal subsets. The logic used to determine the consistencies and inconsistencies was classical, which gives rise to the question regarding its intuitionistic counterpart. It is to this question that the present paper is devoted. Extending Heyting arithmetic, conceived as including function symbols for all primitive recursive functions, with a unary truth predicate \(T\) (whose underlying logic is classical) and with three axioms (ensuring the preservation of \(T\)-truth under implication, the \(T\)-truth of all non-logical axioms of primitive recursive arithmetic, and the \(T\)-truth of all intuitionistically valid first-order formulas inside that language), the authors analyze the consistent subsets of not only the twelve optional axioms, but also of a set of fifteen axioms (three additional truth axioms become natural candidates in the intuitionistic setting), and find that there are still nine maximal consistent subsets for the initial twelve optional axioms, the consistencies and inconsistencies being proved intuitionistically, using intuitionistic Kripke \(\omega\)-structures. It is somewhat surprising that most of the inconsistencies detected by Friedman and Sheard are derivable using the weaker intuitionistic logic. If one adds to the fifteen optional axioms an axiom stating that \(T\) considers the excluded middle to hold, then one gets fourteen maximal consistent theories, and if one adds the law of the excluded middle itself then one gets fifteen maximal consistent theories.