Self-referentiality of Brouwer–Heyting–Kolmogorov semantics

The Gödel–Artemov framework offered a formalization of the Brouwer–Heyting–Kolmogorov (BHK) semantics of intuitionistic logic via classical proofs. In this framework, the intuitionistic propositional logic IPCIPC is embedded in the modal logic S4S4, S4S4 is realized in the Logic of Proofs LPLP, and LPLP has a provability interpretation in Peano Arithmetic. Self-referential LPLP-formulas of the type ‘t is a proof of a formula ϕ containing t   itself’ are permitted in the realization of S4S4 in LPLP, and if such formulas are indeed involved, it is then necessary to use fixed-point arithmetical methods to explain intuitionistic logic via provability. The natural question of whether self-referentiality can be avoided in realization of S4S4 was answered negatively by Kuznets who provided an S4S4-theorem that cannot be realized without using directly self-referential LPLP-formulas. This paper studies the question of whether IPCIPC can be embedded in S4S4 and then realized in LPLP without using self-referential formulas. We consider a general class of Gödel-style modal embeddings of IPCIPC in S4S4 and by extending Kuznetsʼ method, show that there are IPCIPC-theorems such that, under each such embedding, are mapped to S4S4-theorems that cannot be realized in LPLP without using directly self-referential formulas. Interestingly, all double-negations of tautologies that are not IPCIPC-theorems, like ¬¬(¬¬p→p)¬¬(¬¬p→p), are shown to require direct self-referentiality. Another example is found in IPC→IPC→, the purely implicational fragment of IPCIPC. This suggests that the BHK semantics of intuitionistic logic (even of intuitionistic implication) is intrinsically self-referential.This paper is an extended version of [26].