May 06, 2026
The core of this paper is an analysis of Sandqvist’s [1] proof of completeness of a form of base-extension semantics for intuitionistic propositional logic, contrasting with Piecha and Schroeder-Heister’s demonstration of the incompleteness of a range of alternatives [2]. Base-extension semantics is a form of proof-theoretic semantics in which the meanings of logical connectives are explained relative to atomic ‘bases’. Each base establishes a primitive derivation system on a set of atomic propositions. The base-extension semantics then determines the validity of propositional formulae built from these atomic propositions via logical connectives.
Our purpose in this paper is to analyse Sandqvist’s argument as seen through the lens of the established semantics given by Kripke and Heyting, using these to relate Sandqvist’s definition to a form of continuation-passing semantics. Our analysis is presented in an essentially denotational way. It is, borrowing phrases from Schroeder-Heister’s introduction to proof-theoretic semantics [3], presented in a basically extensional fashion, making it essentially model-theoretic, and therefore not in this case addressing the intensional and epistemological aspects that are core to the proof-theoretic analysis. Our purpose here is a mathematical analysis of a completeness proof that enables us to link the structures in use to techniques taken from other areas, notably areas that deal with related issues to proof-theoretic semantics.
In Section 2, we explain, following Sandqvist [1], the elements of base-extension semantics in the setting of intuitionistic propositional logic. In Section 3, we discuss, in the context of [1], the relationship between Kripke models and Heyting algebras. In Section 4, we explain Sandqvist’s completeness proof in a way that will support our ongoing discussion. Section 5 introduces the ideas, from the semantics of computation, of a continuation and of a CPS-transform. In Section 6, we explain that the ideas of continuation and continuation-passing arise in proof theory — specifically, through the manipulation and computation of proofs. Section 7 considers the structure of Heyting algebras in more detail, showing how Sandqvist’s semantics can be seen to arise through a specific interpretation. Then with all these components available, we are able to explain, in Section 8, how Sandqvist’s semantics implicitly employs a CPS-transform — this is the main result of the paper. We conclude, in Section 9, with a discussion of the consequences of our result for a proof-relevant semantics in this setting.
Base-extension semantics is founded on the notion of a base, the function of which is to give a consequence relation on a collection of atomic propositions. We will assume for the purpose of this paper that we are given a fixed countably infinite set \(\text{At}\) of atomic propositions. Bases, \(\mathscr{A}\), \(\mathscr{B}\), … are presented as sets of deductive rules, similar in structure to natural deduction proof rules, but only involving specific atoms.
Sandqvist [1] takes the general form of a rule to be: \[((P_1 \Rightarrow a_1),\dots,(P_n \Rightarrow a_n) \Rightarrow b)\] where \(a_1 , \dots , a_n\) and \(b\) are atoms and each \(P_i\) is a possibly empty finite set of atoms.
This inductively defines a consequence relation \(\derives{B}\), the derivability in \(\mathscr{B}\) of an atom from a set of atoms: \[\begin{array}{rl} ({Ref}) & P , a \vdash_{\mathscr{B}}a \\ ({App}) & For any ((P_1 \Rightarrow a_1),\dots,(P_n \Rightarrow a_n) \Rightarrow b)\in \mathscr{B}, and finite set of atoms Q, \\ & if Q , P_1 \vdash_{\mathscr{B}}a_1 \dots\, Q , P_n \vdash_{\mathscr{B}}a_n, then Q \vdash_{\mathscr{B}}b \end{array}\] Here, the comma between (sets of) atoms is the union as standard in proof theory. The relations \(\vdash_{\mathscr{B}}\) are indeed consequence relations:
Lemma 1. If \(\mathscr{B}\) is a base, then
for any atom \(a\), \(a\vdash_{\mathscr{B}}a\)
for any atoms \(a\), \(b\) and sets of atoms \(P\), \(Q\), if \(P\vdash_{\mathscr{B}}a\) and \(a,Q\vdash_{\mathscr{B}}b\), then \(P,Q\vdash_{\mathscr{B}}b\), and
for any atom \(a\) and sets of atoms \(P\), \(Q\), if \(P\subseteq Q\) and \(P\vdash_{\mathscr{B}}a\), then \(Q\vdash_{\mathscr{B}}a\).
Proof. The first statement is immediate from (Ref), and the others are proved by induction. For example, statement 2 is proved by induction over the length of derivation of \(a,Q\vdash_{\mathscr{B}}b\). If this is an instance of (Ref), then there are two cases: \(a=b\) and \(a\neq b\), both immediate. If however it ends with an application of (App) using the rule \(((P_1 \Rightarrow a_1),\dots,(P_n \Rightarrow a_n) \Rightarrow b)\), then we have \(a,Q,P_1\vdash_{\mathscr{B}}a_1\), … \(a,Q,P_n\vdash_{\mathscr{B}}a_n\), all by shorter derivations. Hence \(P,Q,P_1\vdash_{\mathscr{B}}a_1\),…, \(P,Q,P_n\vdash_{\mathscr{B}}a_n\), and the result follows. ◻
Other authors have considered more restricted forms of atomic rule; see, for example, Piecha [4] for a discussion. But the more general form used by Sandqvist is needed to allow atomic analogues of all the usual rules for natural deduction.
Example 1.
A rule \((\Rightarrow b)\in\mathscr{B}\), with no hypotheses, says directly that \(b\) is derivable in the base (\(\vdash_{\mathscr{B}}b\)), and can be seen as encoding the assertion of \(b\) in any context \(Q\): \[\begin{prooftree} \hypo{} \infer1{Q\vdash_{\mathscr{B}}b} \end{prooftree}\]
A rule \(((\Rightarrow a_1),(\Rightarrow a_2)\Rightarrow b)\in\mathscr{B}\), where all the hypotheses are unconditional, can be seen as encoding a proof rule: \[\begin{prooftree} \hypo{Q \vdash_{\mathscr{B}}a_1} \hypo{Q \vdash_{\mathscr{B}}a_2} \infer2{Q \vdash_{\mathscr{B}}b} \end{prooftree}\]
A rule \(((\Rightarrow a),(b_1\Rightarrow c),(b_2\Rightarrow c) \Rightarrow c)\in\mathscr{B}\) can be seen as encoding an analogue of the \(\vee\)-elimination proof rule: \[\begin{prooftree} \hypo{Q\vdash_{\mathscr{B}}a} \hypo{Q,b_1\vdash_{\mathscr{B}}c} \hypo{Q,b_2\vdash_{\mathscr{B}}c} \infer3{Q\vdash_{\mathscr{B}}c} \end{prooftree}\]
More generally, the rule \(((P_1 \Rightarrow a_1),\dots,(P_n \Rightarrow a_n) \Rightarrow b)\) can be written in natural deduction style: \[\begin{prooftree} \hypo{Q,P_1 \vdash_{\mathscr{B}}a_1} \hypo{\dots} \hypo{Q,P_n\vdash_{\mathscr{B}}a_n} \infer3{Q\vdash_{\mathscr{B}}b} \end{prooftree}\] and \(Q\vdash_{\mathscr{B}}b\) is derivable iff it is the result of a complete proof tree (i.e., a proof tree with no open assumptions).
Since bases are given by sets of rules, the inclusion of these sets extends to a natural notion of the inclusion of one base in another: \(\mathscr{A} \subseteq \mathscr{B}\). This in turn gives the following monotonicity property for derivability, proved by induction:
Lemma 2. If \(\mathscr{A} \subseteq \mathscr{B}\) and \(P \vdash_{\mathscr{A}}a\), then \(P \vdash_{\mathscr{B}}a\). \(\Box\)
Moreover, derivability satisfies a form of deduction theorem:
Lemma 3. The following are equivalent, for any base \(\mathscr{B}\), atom \(a\), and sets of atoms \(P\) and \(Q\):
\(P,Q\vdash_{\mathscr{B}}a\)
For all bases \(\mathscr{C}\supseteq\mathscr{B}\), if \(Q\vdash_{\mathscr{C}}p\) holds for all \(p\in P\), then \(Q\vdash_{\mathscr{C}}a\)
\(Q\vdash_{\mathscr{B'}}a\) where \(\mathscr{B'} = \mathscr{B} \cup \{ (\Rightarrow p) \mid p\in P\}\).
Proof. (1\(\Rightarrow\)2) is immediate from monotonicity of \(\vdash_{\mathscr{D}}\) in the base \(\mathscr{D}\) (Lemma 2), and the fact that it is a consequence relation (Lemma 1). 3 is an instance of 2. 1 follows from 3 by induction over the derivation of \(Q\vdash_{\mathscr{B'}}a\). ◻
Derivability for atoms is now extended to a notion of support for propositions built from atoms using the standard logical connectives. Sandqvist’s definition for this is:
Definition 1 (support). The support relation, in which base \(\mathscr{B}\) supports* the proposition \(\phi\), written \(\Vdash_{\mathscr{B}}\phi\), is defined by recursion on the structure of \(\phi\) as follows: \[\begin{array}{lr@{\quad}c@{\quad}l} (\rm At) & \Vdash_{\mathscr{B}}a & iff &\vdash_{\mathscr{B}}a, for atom a \\ (\wedge) & \Vdash_{\mathscr{B}}\phi\wedge\psi & iff & \Vdash_{\mathscr{B}}\phi and \Vdash_{\mathscr{B}}\psi \\ (\supset) & \Vdash_{\mathscr{B}}\phi\supset\psi & iff & \phi \Vdash_{\mathscr{B}}\psi \\ (\vee) & \Vdash_{\mathscr{B}}\phi\vee\psi & iff & for every atom a and every \mathscr{C}\supseteq\mathscr{B}, if \phi\Vdash_{\mathscr{C}}a and \psi\Vdash_{\mathscr{C}}a, \\ & & & then \Vdash_{\mathscr{C}}a \\ (\bot) & \Vdash_{\mathscr{B}}\bot & iff & \Vdash_{\mathscr{B}}a, for every atom a \end{array}\] Here the clauses \((\supset)\) and \((\vee)\) refer to a relation of inference, which is denoted using the same symbol \(\Vdash_{\mathscr{\mathscr{B}}}\) with abuse of notation: \[\begin{array}{lr@{\quad}c@{\quad}l} (\rm Inf) & For \Theta \neq \emptyset, \Theta\Vdash_{\mathscr{B}}\phi & iff & for every \mathscr{C}\supseteq\mathscr{B}, if \Vdash_{\mathscr{C}}\theta for every \theta\in\Theta, \\ & & & then \Vdash_{\mathscr{C}}\phi \end{array}\] \(\Box\)*
Definition 2 (validity). The consequence relation of validity, \(\Vdash\), is given by \(\Gamma \Vdash \phi\) iff, for all bases \(\mathcal{B}\), \(\Gamma \Vdash_\mathcal{B} \phi\). \(\Box\)
Note that clause (At) states that, for an atom \(a\), \(\Vdash_{\mathscr{B}}a\) iff \(\vdash_{\mathscr{B}}a\), but this extends to consequence.
Lemma 4. For any set \(P\) of atoms, and atom \(a\), \(P\Vdash_{\mathscr{B}}a\) iff \(P\vdash_{\mathscr{B}}a\).
Proof. This follows immediately from (At), (Inf), and Lemma 3. ◻
Given the importance of intensionality in base-extension semantics, we have reproduced Sandqvist’s definition exactly. But some points are worth noting. Sandqvist does not give an interpretation of \(\top\), but could have used \[\begin{array}{l@{\quad}r@{\quad}c@{\quad}l} (\top) & \Vdash_{\mathscr{B}}\top & always & \end{array}\] The definition of inference (Inf) is directly analogous to Kripke implication, where worlds are bases and the partial order between them is inclusion. As a result the interpretation of \((\supset)\) is monotonic in the base. Other rules are also monotonic, either enforcing this directly (\(\vee\)), inheriting this from monotonicity for atoms (\(\text{At}\),\(\bot\)), or via induction over their components (\(\wedge\)).
Lemma 5. If \(\Vdash_{\mathscr{B}}\phi\) and \(\mathscr{B}\subseteq\mathscr{C}\), then \(\Vdash_{\mathscr{C}}\phi\). \(\Box\)
As a result, we have \(\Vdash_{\mathscr{B}}\phi\) if and only if for every \(\mathscr{C}\supseteq \mathscr{B}\), \(\Vdash_{\mathscr{C}}\phi\), which is the right hand side of (Inf) in the case that \(\Theta\) is empty. Hence, if we allowed inference from an empty set of hypotheses, then we would get a concept extensionally equivalent to support, and the condition that \(\Theta\) be non-empty in (Inf) can be seen as redundant.
Sandqvist notes that the interpretations he gives for \(\wedge\) and \(\supset\) are ‘traditional’. They are the ones used by most authors in the field (see e.g., Piecha [4] for a range of approaches). The interpretations of \(\bot\) and \(\vee\) are more novel. Sandqvist ascribes the interpretation for \(\bot\) to Dummett [5] and others, and indicates that the interpretation for \(\vee\) is loosely based on the elimination rule, developing previous work of Prawitz [6] and Ferreira [7] (cf. [8], [9]).
Sandqvist [1] establishes the soundness and completeness of the natural deduction calculus NJ (with consequence relation denoted \(\vdash\)) with respect to the base-extension semantics of intuitionistic propositional logic:
Theorem 1 (soundness and completeness). \(\Gamma \vdash \phi\) iff \(\Gamma \Vdash \phi\) \(\Box\)
Sandqvist’s proof of completeness for this interpretation uses the familiar method of encoding objects in more primitive forms. He encodes arbitrary propositions as chosen atoms and sets up a special base \(\mathscr{N}\) that allows him to ensure that the derivation of these atoms mimics deduction in an intuitionistic natural deduction system. So derivation corresponds to intuitionistic provability. Then he shows that the semantics he has chosen forces propositions to be logically equivalent to their corresponding atoms, whenever bases are required to extend \(\mathscr{N}\). From this completeness follows.
Herein, we intend to examine Sandqvist’s semantics and these constructions in the light of similar constructions for Kripke models and Heyting algebras, bringing out links to techniques from other areas, notably the use of continuations.
In Section 2, we noted the monotonicity property and indicated its link to Kripke models. Now we make that connection more concrete. We suppose we are given a fixed set \(\text{At}\) of atoms and a fixed set \(\mathcal{W}\) of bases over it, ordered by inclusion. This forms the frame for a Kripke model, in which the truth of an atom at a world is given by derivability and then the truth of a proposition at a world is defined by the standard Kripke clauses: \[\begin{array}{lr@{\quad}c@{\quad}l} (\text{At}) & \models_{\mathscr{B}}a & iff & \vdash_{\mathscr{B}}a, atom a\\ (\top) & \models_{\mathscr{B}}\top & always & \\ (\wedge) & \models_{\mathscr{B}}\phi\wedge\psi & iff & \models_{\mathscr{B}}\phi and \models_{\mathscr{B}}\psi \\ (\supset) & \models_{\mathscr{B}}\phi\supset\psi & iff & for every \mathscr{C}\supseteq\mathscr{B}, if \models_{\mathscr{C}}\phi, then \models_{\mathscr{C}}\psi \\ (\vee) & \models_{\mathscr{B}}\phi\vee\psi & iff & \models_{\mathscr{B}}\phi or \models_{\mathscr{B}}\psi \\ (\bot) & \models_{\mathscr{B}}\bot & never & \\ \end{array}\] There is also a form of internal consequence at a base: \[\begin{array}{lr@{\quad}c@{\quad}l} (Inf) & \Theta\models_{\mathscr{B}}\phi & iff & for every \mathscr{C}\supseteq\mathscr{B}, if \models_{\mathscr{C}}\theta for every \theta\in\Theta, then \models_{\mathscr{C}}\phi \end{array}\] As a result, the clause for \(\supset\) could be reformulated: \[\begin{array}{lr@{\quad}c@{\quad}l} (\supset) & \models_{\mathscr{B}}\phi\supset\psi & iff & \phi\models_{\mathscr{B}}\psi \end{array}\] This semantics coincides with Sandqvist’s, except for the clauses for \(\bot\) and \(\vee\), as he notes. Moreover it is also the semantics used by a number of other authors, see Piecha [4]. Note that again we have (cf. Lemma 4):
Lemma 6. For any set \(P\) of atoms, and atom \(a\), \(P\models_{\mathscr{B}}a\) iff \(P\vdash_{\mathscr{B}}a\). \(\Box\)
We can further re-frame this definition, giving the semantics of a proposition as the set of bases that support it: \[[\![\theta]\!] = \{\mathscr{B} \in \mathcal{W}\mid\; \models_{\mathscr{B}}\theta\}\] We view this as a mathematical convenience, not as a philosophical statement intended to capture the intrinsic meaning of the proposition. It does some violence to the underlying approach of proof-theoretic semantics, which is to give meaning to propositions by giving a simple account of circumstances that justify them, not by flattening that to a list of situations. Nevertheless, we contend that it is useful to see how PtS approaches appear through this lens.
This semantic viewpoint gives the possible interpretations of propositions as sets of bases. Monotonicity implies that every set \([\![\phi]\!]\) is an upwards-closed set of worlds. The upwards-closed sets of worlds form a lattice, \(\mathcal{W}^\uparrow\), in fact a complete Heyting algebra, and so we are led to the interpretation of connectives via the standard interpretation of intuitionistic propositional logic in such a structure (e.g., [10]–[12]). We have: \[\begin{array}{lrcl} (At) & [\![a]\!] & = & \{\mathscr{B} \in \mathcal{W}\mid \mathscr{B}\vdash a \} \\ (\top) & [\![\top]\!] & = & \mathcal{W}\\ (\bot) & [\![\bot]\!] & = & \emptyset \\ (\wedge) & [\![\phi\wedge\psi]\!] & = & [\![\phi]\!]\cap[\![\psi]\!] \\ (\supset) & [\![\phi\supset\psi]\!] & = & \bigcup \,\{\, U \mid U is upwards closed and U \cap [\![\phi]\!] \subseteq [\![\psi]\!] \,\} \\ (\vee) & [\![\phi\vee\psi]\!] & = & [\![\phi]\!]\cup[\![\psi]\!] \end{array}\]
Sandqvist’s interpretation differs from this, and that naturally raises the questions:
Why does it differ?
Is there some coherent approach in which it does fit?
In order to motivate our answer to these, we look closer into Sandqvist’s completeness proof.
Sandqvist’s proof of completeness uses an encoding of arbitrary propositions as atoms, and of the propositional deductive system into a base. Starting with a collection of atoms, , for every proposition \(\phi\) defined over , we introduce a new atom
(Sandqvist uses the notation \(\phi^\flat\)). The aim is to force the atom to be semantically equivalent to the proposition \(\phi\). Thus will be an atom semantically equivalent to the disjunction of the two atoms \(a\) and \(b\). Similarly for contexts \(\Gamma = \{\phi_1,\dots,\phi_n\}\) we can define $ = {
,, }\(. Sandqvist is a bit more delicate than this. His completeness argument works at the level of a given single logical consequence\)$. In order to handle this, he only needs to consider subformulae of the consequence, thus allowing a restriction to a finite number of additional atoms and a finite base. Like Sandqvist, for an atom \(a\in\text{At}\) we take \(\tikz[baseline=(a.base)]{\node(a){\phantom{a}};\node[draw,black,inner sep=2pt, rounded rectangle]{a}} =a\). We call the resulting set of atoms \(\text{At}^\ast\).
The special base \(\mathscr{N}\) is defined over \(\text{At}^\ast\) and consists of rules mimicking those of Natural Deduction. For instance, if \[\begin{prooftree} \hypo{\begin{array}{c}\\ \varphi\vee\psi \end{array}} \hypo{\begin{array}{c}[\varphi]\\ \theta\end{array}} \hypo{\begin{array}{c}[\psi]\\ \theta \end{array}} \infer3{\theta} \end{prooftree}\] is a valid instance of \(\vee\)-elimination, then \(\mathscr{N}\) contains \[((\Rightarrow \tikz[baseline=(a.base)]{\node(a){\phantom{\varphi\vee\psi}};\node[draw,black,inner sep=2pt, rounded rectangle]{\varphi\vee\psi}} ), ( \tikz[baseline=(a.base)]{\node(a){\phantom{\varphi}};\node[draw,black,inner sep=2pt, rounded rectangle]{\varphi}} \Rightarrow \tikz[baseline=(a.base)]{\node(a){\phantom{\theta}};\node[draw,black,inner sep=2pt, rounded rectangle]{\theta}} ), ( \tikz[baseline=(a.base)]{\node(a){\phantom{\varphi}};\node[draw,black,inner sep=2pt, rounded rectangle]{\varphi}} \Rightarrow \tikz[baseline=(a.base)]{\node(a){\phantom{\theta}};\node[draw,black,inner sep=2pt, rounded rectangle]{\theta}} ) \Rightarrow \tikz[baseline=(a.base)]{\node(a){\phantom{\theta}};\node[draw,black,inner sep=2pt, rounded rectangle]{\theta}} )\] the atomic rule corresponding to: \[\begin{prooftree} \hypo{\begin{array}{c}\\ \tikz[baseline=(a.base)]{\node(a){\phantom{\varphi\vee\psi}};\node[draw,black,inner sep=2pt, rounded rectangle]{\varphi\vee\psi}} \end{array} } \hypo{\begin{array}{c}[ \tikz[baseline=(a.base)]{\node(a){\phantom{\varphi}};\node[draw,black,inner sep=2pt, rounded rectangle]{\varphi}} ]\\ \tikz[baseline=(a.base)]{\node(a){\phantom{\theta}};\node[draw,black,inner sep=2pt, rounded rectangle]{\theta}} \end{array}} \hypo{\begin{array}{c}[ \tikz[baseline=(a.base)]{\node(a){\phantom{\psi}};\node[draw,black,inner sep=2pt, rounded rectangle]{\psi}} ]\\ \tikz[baseline=(a.base)]{\node(a){\phantom{\theta}};\node[draw,black,inner sep=2pt, rounded rectangle]{\theta}} \end{array}} \infer3{ \tikz[baseline=(a.base)]{\node(a){\phantom{\theta}};\node[draw,black,inner sep=2pt, rounded rectangle]{\theta}} } \end{prooftree}\] The special base \(\mathscr{N}\) consists of all such translates of all the possible instances of all of the natural deduction rules. Sandqvist minimises the size of this base by restricting to atoms representing subformulae of a given sequent. As a result, his base is finite.
Note that \(\tikz[baseline=(a.base)]{\node(a){\phantom{a}};\node[draw,black,inner sep=2pt, rounded rectangle]{a}} = a\) is a natural and handy choice, but it is not essential. If we had not identified atoms \(a\) and , then we would also have added rules enforcing that equivalence: \(((\Rightarrow a)\Rightarrow \tikz[baseline=(a.base)]{\node(a){\phantom{a}};\node[draw,black,inner sep=2pt, rounded rectangle]{a}} )\) and \(((\Rightarrow \tikz[baseline=(a.base)]{\node(a){\phantom{a}};\node[draw,black,inner sep=2pt, rounded rectangle]{a}} )\Rightarrow a)\).
Sandqvist’s proof hinges on his translation and base \(\mathscr{N}\) having two key properties, \((\dagger)\), which expresses the semantic equivalence between a formula and its translate (see section 8), and \((\ddagger)\), which expresses the equivalence between derivability in \(\mathscr{N}\) of atomic translates and provability of the original formulae in NJ, and in our notation is: \[(\ddagger) for any P and a, if P \vdash_\mathscr{N} a and if \tikz[baseline=(a.base)]{\node(a){\phantom{\Gamma}};\node[draw,black,inner sep=2pt, rounded rectangle]{\Gamma}} = P and \tikz[baseline=(a.base)]{\node(a){\phantom{\phi}};\node[draw,black,inner sep=2pt, rounded rectangle]{\phi}} = a, then \Gamma \vdash \phi \]
Proposition 2 (Sandqvist [1]). For any propositions \(\phi_1,\dots,\phi_n\), and \(\psi\): \(\tikz[baseline=(a.base)]{\node(a){\phantom{\phi_1}};\node[draw,black,inner sep=2pt, rounded rectangle]{\phi_1}} ,\dots, \tikz[baseline=(a.base)]{\node(a){\phantom{\phi_1}};\node[draw,black,inner sep=2pt, rounded rectangle]{\phi_1}} \vdash_{\mathscr{N}} \tikz[baseline=(a.base)]{\node(a){\phantom{\psi}};\node[draw,black,inner sep=2pt, rounded rectangle]{\psi}}\) iff \(\phi_1,\dots,\phi_n\vdash\psi\) is derivable in intuitionistic propositional logic.
Proof. The core idea is that a derivation \(\tikz[baseline=(a.base)]{\node(a){\phantom{\phi_1}};\node[draw,black,inner sep=2pt, rounded rectangle]{\phi_1}} ,\dots, \tikz[baseline=(a.base)]{\node(a){\phantom{\phi_n}};\node[draw,black,inner sep=2pt, rounded rectangle]{\phi_n}} \vdash_{\mathscr{N}} \tikz[baseline=(a.base)]{\node(a){\phantom{\psi}};\node[draw,black,inner sep=2pt, rounded rectangle]{\psi}}\) expressed in tree form maps to an intuitionistic proof simply by removing all the ovals (mapping the function \(\tikz[baseline=(a.base)]{\node(a){\phantom{\phi}};\node[draw,black,inner sep=2pt, rounded rectangle]{\phi}} \mapsto \phi\)), and an intuitionistic proof to a derivation by doing the reverse.
Technically, the proof in each direction is by induction, in one direction on the length of the derivation in \(\mathscr{N}\), and in the other on the structure of the proof in NJ. ◻
Note that for this to work when \(\mathscr{N}\) is restricted to subformulae of a sequent, then we need the subformula property for provability in intuitionistic logic.
Gentzen’s seminal work [13], [14] already contains the idea that the introduction rules express the core meaning of a connective and the elimination rules in some sense express the completeness of this (cf. Dummett [5]). There is a body of work establishing to what extent we can systematically derive elimination rules from certain forms of introduction rules, so-called ‘generalized elimination’ rules (cf. [15]).
One way of expressing this completeness is that we can prove the identity axiom for the application of a connective from the identity axioms for the formulae to which it is applied, and hence that the identity axiom for all formulae follows from that for atoms only. We will see the importance of this later when we use a refinement of these arguments to establish the equivalence of a proposition \(\phi\) and its atomic representative . This is easiest seen in calculi like Gentzen’s LJ [14] (we’ve removed some structural rules) \[\begin{prooftree} \hypo{} \infer1{\varphi\to\varphi} \infer1{\varphi\to\varphi\vee\psi} \hypo{} \infer1{\psi\to\psi} \infer1{\psi\to\varphi\vee\psi} \infer2{\varphi\vee\psi\to \varphi\vee\psi} \end{prooftree} \begin{prooftree} \hypo{} \infer1{\varphi\to\varphi} \hypo{} \infer1{\psi\to\psi} \infer2{\varphi,\psi\to\varphi\wedge\psi} \infer1{\varphi\wedge\psi\to \varphi\wedge\psi} \end{prooftree}\] These correspond to natural deduction proofs \[\begin{prooftree} \hypo{\varphi\vee\psi} \hypo{[\varphi]} \infer1{\varphi\vee\psi} \hypo{[\psi]} \infer1{\varphi\vee\psi} \infer3{\varphi\vee\psi} \end{prooftree} \begin{prooftree} \hypo{\varphi\wedge\psi} \infer1{\varphi} \hypo{\varphi\wedge\psi} \infer1{\psi} \infer2{\varphi\wedge\psi} \end{prooftree}\] which make the point less clear.
This form of completeness implies that the logical rules determine the connectives up to logical equivalence. So, for example, if \(\vee_1\) and \(\vee_2\) both have the introduction and elimination rules for \(\vee\), then, replacing parts of the proofs above with the analogues for \(\vee_1\) and \(\vee_2\), we have \[\begin{prooftree} \hypo{} \infer1{\varphi\to\varphi} \infer1{\varphi\to\varphi\vee_2\psi} \hypo{} \infer1{\psi\to\psi} \infer1{\psi\to\varphi\vee_2\psi} \infer2{\varphi\vee_1\psi\to \varphi\vee_2\psi} \end{prooftree} or\begin{prooftree} \hypo{\varphi\vee_1\psi} \hypo{[\varphi]} \infer1{\varphi\vee_2\psi} \hypo{[\psi]} \infer1{\varphi\vee_2\psi} \infer3{\varphi\vee_2\psi} \end{prooftree}\]
This feeds into a failed attempt to prove completeness for base-extension semantics of Intuitionistic Propositional Logic using the Kripke interpretations given above.
We want to prove the equivalence of a formula with the corresponding atom by induction on the structure of the formula.
We have \(\phi\wedge\psi \to \tikz[baseline=(a.base)]{\node(a){\phantom{\phi\wedge\psi}};\node[draw,black,inner sep=2pt, rounded rectangle]{\phi\wedge\psi}}\) : \[\begin{prooftree} \hypo{\phi\wedge\psi} \infer1[\wedge E]{\phi} \infer1[Ind]{ \tikz[baseline=(a.base)]{\node(a){\phantom{\phi}};\node[draw,black,inner sep=2pt, rounded rectangle]{\phi}} } \hypo{\phi\wedge\psi} \infer1[\wedge E]{\psi} \infer1[Ind]{ \tikz[baseline=(a.base)]{\node(a){\phantom{\psi}};\node[draw,black,inner sep=2pt, rounded rectangle]{\psi}} } \infer2[\mathscr{N}]{ \tikz[baseline=(a.base)]{\node(a){\phantom{\phi\wedge\psi}};\node[draw,black,inner sep=2pt, rounded rectangle]{\phi\wedge\psi}} } \end{prooftree}\] In particular, the last step, marked with \(\mathscr{N}\), uses the following rule in \(\mathscr{N}\): \[( (\Rightarrow\tikz[baseline=(a.base)]{\node(a){\phantom{\phi}};\node[draw,black,inner sep=2pt, rounded rectangle]{\phi}} ), (\Rightarrow\tikz[baseline=(a.base)]{\node(a){\phantom{\psi}};\node[draw,black,inner sep=2pt, rounded rectangle]{\psi}} ) \Rightarrow\tikz[baseline=(a.base)]{\node(a){\phantom{\phi \land \psi}};\node[draw,black,inner sep=2pt, rounded rectangle]{\phi \land \psi}})\] We will omit the details of the application of such \(\mathscr{N}\)-rules in the following cases.
This is to be read as a semantic argument in which the steps are validated through the soundness of intuitionistic rules (\(\wedge E\)), induction (Ind) and the soundness of the rules of \(\mathscr{N}\) for atoms. Note the structural similarity to the previous discussion of uniqueness of \(\wedge\).
Conversely, we have \(\tikz[baseline=(a.base)]{\node(a){\phantom{\phi\wedge\psi}};\node[draw,black,inner sep=2pt, rounded rectangle]{\phi\wedge\psi}} \to \phi\wedge\psi\): \[\begin{prooftree} \hypo{ \tikz[baseline=(a.base)]{\node(a){\phantom{\phi\wedge\psi}};\node[draw,black,inner sep=2pt, rounded rectangle]{\phi\wedge\psi}} } \infer1[\mathscr{N}]{ \tikz[baseline=(a.base)]{\node(a){\phantom{\phi}};\node[draw,black,inner sep=2pt, rounded rectangle]{\phi}} } \infer1[Ind]{\phi} \hypo{ \tikz[baseline=(a.base)]{\node(a){\phantom{\phi\wedge\psi}};\node[draw,black,inner sep=2pt, rounded rectangle]{\phi\wedge\psi}} } \infer1[\mathscr{N}]{ \tikz[baseline=(a.base)]{\node(a){\phantom{\psi}};\node[draw,black,inner sep=2pt, rounded rectangle]{\psi}} } \infer1[Ind]{\psi} \infer2[\wedge I]{\phi\wedge\psi} \end{prooftree}\]
Similarly, we can validate \(\phi\vee\psi \to \tikz[baseline=(a.base)]{\node(a){\phantom{\phi\vee\psi}};\node[draw,black,inner sep=2pt, rounded rectangle]{\phi\vee\psi}}\) : \[\begin{prooftree} \hypo{\phi\vee\psi} \hypo{\phi} \infer1[Ind]{ \tikz[baseline=(a.base)]{\node(a){\phantom{\phi}};\node[draw,black,inner sep=2pt, rounded rectangle]{\phi}} } \infer1[\mathscr{N}]{ \tikz[baseline=(a.base)]{\node(a){\phantom{\phi\vee\psi}};\node[draw,black,inner sep=2pt, rounded rectangle]{\phi\vee\psi}} } \hypo{\psi} \infer1[Ind]{ \tikz[baseline=(a.base)]{\node(a){\phantom{\psi}};\node[draw,black,inner sep=2pt, rounded rectangle]{\psi}} } \infer1[\mathscr{N}]{ \tikz[baseline=(a.base)]{\node(a){\phantom{\phi\vee\psi}};\node[draw,black,inner sep=2pt, rounded rectangle]{\phi\vee\psi}} } \infer3[\vee E]{ \tikz[baseline=(a.base)]{\node(a){\phantom{\phi\vee\psi}};\node[draw,black,inner sep=2pt, rounded rectangle]{\phi\vee\psi}} } \end{prooftree}\]
However, we run into problems with \(\tikz[baseline=(a.base)]{\node(a){\phantom{\phi\vee\psi}};\node[draw,black,inner sep=2pt, rounded rectangle]{\phi\vee\psi}} \to \phi\vee\psi\): \[\begin{prooftree} \hypo{ \tikz[baseline=(a.base)]{\node(a){\phantom{\phi\vee\psi}};\node[draw,black,inner sep=2pt, rounded rectangle]{\phi\vee\psi}} } \hypo{ \tikz[baseline=(a.base)]{\node(a){\phantom{\phi}};\node[draw,black,inner sep=2pt, rounded rectangle]{\phi}} } \infer1[Ind]{\phi} \infer1[\vee I]{\phi\vee\psi} \hypo{ \tikz[baseline=(a.base)]{\node(a){\phantom{\psi}};\node[draw,black,inner sep=2pt, rounded rectangle]{\psi}} } \infer1[Ind]{\psi} \infer1[\vee I]{\phi\vee\psi} \infer3[??]{\phi\vee\psi} \end{prooftree}\] This is not a valid deduction. It fails at the last step because \(\phi\vee\psi\) is not an atom, and hence the last deduction is not an instance of an atomic rule. In other words, the following rule that would pass the last step is not an atomic rule: \[(\Rightarrow ( \tikz[baseline=(a.base)]{\node(a){\phantom{\phi \lor \psi}};\node[draw,black,inner sep=2pt, rounded rectangle]{\phi \lor \psi}} ), ( \tikz[baseline=(a.base)]{\node(a){\phantom{\phi}};\node[draw,black,inner sep=2pt, rounded rectangle]{\phi}}\Rightarrow \phi \lor \psi), ( \tikz[baseline=(a.base)]{\node(a){\phantom{\psi}};\node[draw,black,inner sep=2pt, rounded rectangle]{\psi}}\Rightarrow \phi \lor \psi) \Rightarrow \phi \lor \psi )\] Nor do we have any other rule that would allow us to perform this last step. For our strategy to work, we have to find a way round this, and that is what Sandqvist did in his proof of completeness. In order to understand his approach we take a closer look at the structure of proof rules.
The proof of equivalence for conjunction just given goes through because the rules only feature components of the conjunction: \[\begin{prooftree} \hypo{\phi}\hypo{\psi}\infer2{\phi \wedge \psi} \end{prooftree} \begin{prooftree} \hypo{\phi \wedge \psi}\infer1{\phi} \end{prooftree} \begin{prooftree} \hypo{\phi \wedge \psi}\infer1{\psi} \end{prooftree}\] The rules for \(\supset\) and \(\top\) have a similar property, and hence we can find proofs of equivalence for these connectives too. However, the elimination rule for disjunction features a formula \(\chi\) which is not syntactically related to the disjunction: \[\begin{prooftree} \hypo{\phi}\infer1{\phi \vee \psi} \end{prooftree} \begin{prooftree} \hypo{\psi}\infer1{\phi \vee \psi} \end{prooftree} \begin{prooftree} \hypo{\begin{array}{c} \\ \phi \vee \psi \end{array} } \hypo{\begin{array}{c}[\phi]\\ \chi\end{array}} \hypo{\begin{array}{c}[\psi]\\ \chi\end{array}} \infer3{\chi} \end{prooftree}\] It is this proposition \(\chi\) that is causing us the problem. We need to look more closely at it. What \(\chi\) represents is the idea that our final goal in constructing the proof is not local, but is some proposition \(\chi\), potentially very different from the proposition we are currently working on. This idea also arises in the area of programming in the form of a ‘continuation’, where it has been widely studied, notably for us in the context of giving continuation-based semantics to programs and continuation passing style transformations.
In his historical survey on the origins of the concept of continuation [16], Reynolds notes that concepts recognizable as a form of continuation have been introduced a considerable number of times; for example as ‘a method of program transformation (into continuation-passing style), a style of definition interpreters [17], and a style of denotational semantics (in the sense of Scott and Strachey). Reynolds goes on to say: ’In each of these settings, by representing “the meaning of the rest of the program” as a function or procedure, continuations provide an elegant description of a variety of language constructs, including call by value and goto statements.’
So, a continuation is essentially the ‘rest of a computation’ reified as an object that we can manipulate. To put this into context, if we want to understand the computational meaning of an expression in a programming language, then we face
some important restrictions. First, the identifiers in the expression have to be resolved and given meaning. Essentially, we are working with closed terms, or at least open terms in an environment where the identifiers are bound to closed terms. Second,
languages have restrictions on what kind of expression can actually be run as a program. Many programming languages specify that a runnable program is a function ‘main’; for example, \(C\), where
main returns an integer, Java, where it returns void, or Rust, where it has to be called ‘main’, but where there is no requirement on the type that it returns.
As a result, in order to give a computational semantics for program fragments, we need a way to put them into a complete runnable setting. Moreover, most practical programming language have features that produce non-standard flow of control. Originally these included jumps and goto’s, but they still include low level features such as break, and higher-level ones such as exceptions. Continuations can be used to explain the meaning of such features.
In a continuations-based account, functions or procedures have an implicit additional argument, the continuation. This can be seen as a generalization and reification of the return address. If the function returns normally, then its return value is given as a parameter to the continuation supplied as an argument. If not, then the continuation is ignored, and another one is used instead. For example (simplifying a little) in programs with exceptions, the function of an exception handler is to provide an alternative continuation that can be used in the event of code generating that particular exception. So if code terminates normally, then the function returns using the standard continuation supplied as a parameter. And if it raises an exception it returns using the continuation provided by the exception handler.
In a typed functional setting, the continuations for an expression of type \(A\) can be represented as functions \(A \to R\), where \(R\) is the result type of a complete program. As a result, the semantics of an expression of type \(A\) is a function from continuations to results of type \((A \to R) \to R\).
The reification of continuations can be taken further, with translations from programs that do not manipulate continuations as data objects to programs that do. This is called a CPS-transform — that is, transform to continuation-passing style. Such a transformation can specify an evaluation mechanism for the source language.
Taking lambda calculus as a basic programming language, we have the standard Plotkin-Fischer call-by-value transformation [18]: \[\begin{align} [\![x]\!] & = & \lambda k. k x\\ [\![\lambda x. e ]\!]& = & \lambda k. k (\lambda x. [\![e]\!])\\ [\![f\, e]\!] & = & \lambda k. [\![f]\!] (\lambda f. [\![e]\!] (\lambda e. f e k)) \end{align}\] Note that each of these translations is an expression with head \(\lambda\) expecting a continuation argument. Moreover, if we provide an expression that also has head lambda as that continuation, and follow the standard functional programming restriction of not evaluating under lambda, then the term we are evaluating has only a single redex. This can be seen in an example reduction. Consider the term \(f\, e\), where \(f\) evaluates to \(\lambda x. e'\), and \(e\) evaluates to a value \(v\), whose CPS transform is \(\lambda k. kv\). We evaluate \(f\, e\) with continuation \(\lambda x. ?\). Then, putting the active continuation in blue, we have: \[\begin{align} [\![f\, e]\!] {\color{blue}(\lambda x. ?)} & = & (\lambda k. [\![f]\!] (\lambda f. [\![e]\!] (\lambda e. f e k))) {\color{blue}(\lambda x. ?)}\\ & \leadsto & [\![f]\!] {\color{blue}(\lambda f. [\![e]\!] (\lambda e. f e (\lambda x. ?)))}\\ & \leadsto^* & [\![\lambda x. e']\!] {\color{blue}(\lambda f. ([\![e]\!] (\lambda e. f e (\lambda x. ?)))}\\ & = & (\lambda k. k (\lambda x. [\![e']\!])) {\color{blue}(\lambda f. ([\![e]\!] (\lambda e. f e (\lambda x. ?)))}\\ & \leadsto & (\lambda f. [\![e]\!] {\color{blue}(\lambda e. f e (\lambda x. ?))}) (\lambda x. [\![e']\!])\\ & \leadsto & [\![e]\!] {\color{blue} (\lambda e. (\lambda x. [\![e']\!]) e (\lambda x. ?))}\\ & \leadsto^* & (\lambda k. k\, v) {\color{blue} (\lambda e. (\lambda x. [\![e']\!]) e {\color{blue}(\lambda x. ?)})}\\ & \leadsto & (\lambda e. (\lambda x. [\![e']\!]) e {\color{blue}(\lambda x. ?)}) \, v\\ & \leadsto & (\lambda x. [\![e']\!]) v {\color{blue}(\lambda x. ?)}\\ & \leadsto & ([\![e']\!][ x:= v]) {\color{blue}(\lambda x. ?)}\\ & \leadsto^* \end{align}\] The step from the second line to the third is immediate if \(f=\lambda x.e'\), but if not then it represents the evaluation of \(f\) to its normal form \(\lambda x.e'\). The continuation remains unchanged at the end of this process. Similarly, later we have the evaluation of \(e\) to its normal form \(v\), which is then passed to \([\![e']\!]\). As a result, assuming that we don’t evaluate under lambda’s, the transformation ensures that there is a call-by-value evaluation of the expression given to it.
Note that if we type \(x\) and \(e\) as having type \(A\), \(e'\) as having type \(B\), and \(f\) as having type \(A\to B\), then we can type \([\![x]\!]\) and \([\![e]\!]\) as having type \((A\to R)\to R\), \([\![e']\!]\) as having type \((B\to R) \to R\), and \([\![f]\!]\) as having type \(A\to (B\to R)\to R\). So we can take the CPS-transform as mapping a type \(A\) to \((A\to R)\to R\).
Once we look, it is easy to find continuations and continuation-passing in logic — in particular, through readings of proofs and rules of inference that relate to processes of computation. Readers familiar with the notion of propositions-as-types [19], [20] will see how this view underpins the approach of this section.
The ideas we discuss here can be traced back to the Brouwer-Heyting-Kolmogorov (BHK) interpretation of intuitionistic logic. In this interpretation proofs, or justifications, are interpreted as mathematical objects. A justification of \(A\supset B\) is a process for transforming a justification of \(A\) into a justification of \(B\), and when we translate this into a formal mathematical model of logical deduction, this is reified as a function. Similarly a justification of \(A\wedge B\) encapsulates justifications of \(A\) and \(B\), and is reified as an ordered pair. As a result the operations for manipulating standard connectives can be seen as instances of standard mathematical constructions. The formalization of these processes took place roughly in tandem and in the same broad community and so it is not surprising to see a degree of convergent evolution, culminating in the well-known propositions-as-types correspondence (see [19], [20] for convenient and appropriate summaries), in which we have correspondences between propositions and types, and between justifications of propositions and elements of types. Later, a third party entered the room, and we see a further link to the type systems of functional programming languages, and expressions in the language.
Let us adopt this viewpoint and examine the \(\vee\)-elimination rule: \[\begin{prooftree} \hypo{\begin{array}{c} \\ \phi \vee \psi \end{array}} \hypo{\begin{array}{c}[\phi]\\ \chi\end{array}} \hypo{\begin{array}{c}[\psi]\\ \chi\end{array}} \infer3{\chi} \end{prooftree}\] This rule can be justified by the argument that a proof such as \[\begin{prooftree} \hypo{} \ellipsis{}{\phi} \infer1[\veeI]{\phi \vee \psi} \hypo{[\phi]} \ellipsis{}{\chi} \hypo{[\psi]} \ellipsis{}{\chi} \infer3[\veeE]{\chi} \end{prooftree} \qquad\qquadcan be reduced to\qquad\qquad \begin{prooftree} \hypo{} \ellipsis{}{\phi} \ellipsis{}{\chi} \end{prooftree}\] We can see here that the conclusion of the overall proof is \(\chi\), and thus \(\chi\) is the analogue of the result of the computation. That means we can interpret a proof element \(\begin{array}{c}[\phi] \\ \chi \end{array}\) as a form of continuation.
Once we do that we can go further. We can move the formulae in the proof rule to put it in the form: \[\begin{prooftree} \hypo{\begin{array}{c}[\phi]\\\chi\end{array}} \hypo{\begin{array}{c}[\psi]\\\chi\end{array}} \infer2{\begin{array}{c}[\phi \vee \psi]\\\chi\end{array}} \end{prooftree}\]
We make a further change in notation, replacing \(\begin{array}{c}[\phi]\\ \chi \end{array}\) by \(\begin{bmatrix}\phi\\\chi\end{bmatrix}\), which we use to represent a continuation taking a proposition \(\phi\) and producing an end result \(\chi\). We can then reformulate the standard intuitionistic proof rules as introductions of propositions and introductions of continuations. In doing this we have changed the direct value-based formulations of \(\wedge\) and \(\to\) elimination into formulations that manipulate continuations, inverting the rules in the process.
\[\setlength{\arraycolsep}{1.5cm} \begin{array}{cc} \begin{prooftree} \hypo{\phi}\hypo{\psi}\infer2{\phi\wedge \psi} \end{prooftree} & \begin{prooftree} \hypo{\begin{bmatrix}\phi\\\chi\end{bmatrix}}\infer1{\begin{bmatrix}\phi\wedge \psi\\\chi\end{bmatrix}} \end{prooftree} \begin{prooftree} \hypo{\begin{bmatrix}\psi\\\chi\end{bmatrix}}\infer1{\begin{bmatrix}\phi\wedge \psi\\\chi\end{bmatrix}} \end{prooftree}\\ \\ \begin{prooftree} \hypo{\phi}\infer1{\phi\vee \psi} \end{prooftree} \begin{prooftree} \hypo{\psi}\infer1{\phi \vee \psi} \end{prooftree} & \begin{prooftree} \hypo{\begin{bmatrix}\phi\\\chi\end{bmatrix}}\hypo{\begin{bmatrix}\psi\\\chi\end{bmatrix}}\infer2{\begin{bmatrix}\phi\vee \psi\\\chi\end{bmatrix}} \end{prooftree}\\ \\ \begin{prooftree} \hypo{}\infer1{\top} \end{prooftree}\\ \\ &\begin{prooftree} \hypo{}\infer1{\begin{bmatrix}\bot\\\chi\end{bmatrix}} \end{prooftree}\\ \\ \begin{prooftree} \hypo{\begin{bmatrix}\phi\\\psi\end{bmatrix}} \infer1{\phi\to \psi} \end{prooftree}& \begin{prooftree} \hypo{\phi} \hypo{\begin{bmatrix}\psi\\\chi\end{bmatrix}} \infer2{\begin{bmatrix}\phi \to \psi\\\chi\end{bmatrix}} \end{prooftree} \end{array}\] This formulation exhibits a strict symmetry between conjunction and disjunction, true and false.
We can also see continuations in the reductive view of proof, a viewpoint that links strongly to both proof-search and logic programming. Indeed, reductive proof can be seen as a continuation-passing style account. In deductive proof, we combine complete proof-objects, and the active part of the proof is at the bottom of the proof tree. By contrast in reductive proof the object representing the current state of the computation is an incomplete proof culminating in the ultimate goal, and so is recognizable as a continuation. In this case the active part of the structure is at the top of the proof-tree.
As an example, employing a sequential presentation, consider the logic program (loosely following the set-up in [21], which lies within the scope of base-extension semantics [22]) \[\Gamma = a_1 \supset a \,,\, a_2 \supset a \,,\, a_2\] with goal \[\Gamma \;{?\!-}\;a\]
Resolution of \(a\) against \(\Gamma\) produces two matches, with \(a_1\supset a\) and \(a_2\supset a\), giving us the
two incomplete proofs \(C_1\) and \(C_2\) below, both of which can be regarded as continuations generated from the original query (the orginal continuation for the process): \[C_1 = \begin{prooftree} \hypo{\rm succeed} \infer1{\Gamma\;{?\!-}\;a_1\supset a} \hypo{\Gamma\;{?\!-}\;a_1} \infer2{\Gamma\;{?\!-}\;a}
\end{prooftree}\;\;\; and\;\;\;C_2 = \begin{prooftree} \hypo{\rm succeed} \infer1{\Gamma\;{?\!-}\;a_2\supset a} \hypo{\Gamma\;{?\!-}\;a_2} \infer2{\Gamma\;{?\!-}\;a}
\end{prooftree},\] We can view these as living in a pseudo-Python term \[\tt try: C_1 except fail: C_2\] Trying to develop \(C_1\), we resolve \(a_1\) against \(\Gamma\), which fails: \[\begin{prooftree} \hypo{\rm succeed} \infer1{\Gamma\;{?\!-}\;a_1\supset a} \hypo{\rm{fail}} \infer1{\Gamma\;{?\!-}\;a_1}
\infer2{\Gamma\;{?\!-}\;a}
\end{prooftree}\] So, we can regard this as raising the exception fail, which is then caught by the exception handler. In the continuations-based account, this error results in abandoning the current continuation, \(C_1\), and swapping in \(C_2\) as the new continuation. This is then developed, resolving \(a_2\) against \(\Gamma\) which now
succeeds and we are left with a complete proof: \[\begin{prooftree} \hypo{\rm succeed} \infer1{\Gamma\;{?\!-}\;a_2\supset a} \hypo{\rm{succeed}} \infer1{\Gamma\;{?\!-}\;a_2} \infer2{\Gamma\;{?\!-}\;a}
\end{prooftree}\]
As a result, the flow of control in a proof-search can be seen as a form of continuation passing, using the continuations to implement the raising and handling of exceptions allowing non-local control flow.
So, fragments of the standard presentation of intuitionistic propositional logic can be presented naturally as versions of continuations, and pushing that analogy leads to structural insights that are not at first apparent.
Now, the standard logical rules allow arbitrary formulae in the role of the result of a continuation. We have seen that this is linked to a problem in proving completeness. So, it seems reasonable only to allow atoms in that role. In other words, we restrict complete proofs to be proofs of atoms. We will take compound propositions as being equivalent if they are indistinguishable on this basis. This amounts to equating formulae if they cannot be distinguished in the context of the proof of an atom. This means quotienting the lattice we use for representing our semantics, or, alternatively, as we shall see, passing our formulae through a form of CPS-transform.
We now show how to move from a Heyting algebra semantics to a less discriminating one based on it. For an authoritative account of this, see Johnstone [23].
Suppose \(H\) and \(K\) are complete Heyting algebras, and \(p: H\to K\) is an order-preserving map from \(H\) onto \(K\), presenting \(K\) as a quotient of \(H\), then under reasonable conditions there is an order-preserving map back again \(i: K\to H\) such that \(p\circ i = 1_K\), and so giving an embedding of \(K\) in \(H\). If we let \(j = i \circ p : H \to H\), then we can view \(j\) as giving an approximation of an element of \(H\) by an element of \(K\). There are two ways of doing this: a best over-approximation in which \((i \circ p) h = \bigvee \{ h' \mid ph' \leq ph\}\), and a best under-approximation in which \((i\circ p) h = \bigwedge \{ h'\mid ph \leq ph'\}\). In the language of category theory, these correspond to left and right adjoints of \(p\), but in the context of partial orders this structure is often called a ‘Galois connection’. We will be concerned with the best over-approximations, and approach them by characterizing the functions \(j : H \to H\) that produce them.
Definition 3 (nucleus). If \(H\) is a complete Heyting algebra, then a nucleus* on \(H\) is a function \(j: H\to H\) such that \(j\) is*
order-preserving: if \(a\leq b\), then \(j(a) \leq j(b)\)
increasing: \(a\leq j(a)\)
idempotent: \(j^2 (a) = j(a)\)
\(\wedge\)-preserving: \(j(a\wedge b) = ja \wedge jb\).
If \(j\) is a nucleus on \(H\), then we write \(H_j\) for the set of fixpoints of \(j\), \(\{a \in H \mid a = j(a)\}\), which is of course also the image of \(j\), \(\{ j(a) \mid a \in H\}\). \(\Box\)
Lemma 7. \(H_j\) is a complete Heyting algebra.
Proof. \(H_j\) inherits its top element and meets from \(H\). First \(\top\in H_j\): \(\top \leq j \top \leq \top\), and hence \(\top = j \top\). Furthermore, if \(a,b\in H_j\), then so is \(a\wedge b\): since \(j (a\wedge b) = j(a) \wedge j(b) = a \wedge b\). Moreover, if \(\{a_\alpha \mid \alpha\in A\}\) is an arbitrary set of elements in \(H\), \(b\in H_j\), then \(a_\alpha \leq b\) for all \(\alpha\) iff \(j(\bigvee_\alpha a_\alpha) \leq b\). It follows that if \(\{a_\alpha \}_{\alpha \in A} \subseteq H_j\), then \(j(\bigvee_\alpha a_\alpha)\) is the least upper bound of \(\{a_\alpha \mid \alpha\in A\}\) in \(H_j\). It remains to show that meet distributes over sup, but \(j(\bigvee_\alpha a_\alpha) \wedge b = j(\bigvee_\alpha a_\alpha) \wedge j(b) = j((\bigvee_\alpha a_\alpha) \wedge b) = j(\bigvee_\alpha (a_\alpha \wedge b))\), as required. ◻
Lemma 8. If \(H\) is a complete Heyting algebra, and if \(j\) is a nucleus on \(H\), then, for any \(a, b\in H\), if \(b\in H_j\), then \(a\to b \in H_j\). Hence, if \(a\) and \(b\) are both in \(H_j\), then so is \(a\to b\), and it is also the exponential in \(H_j\).
Proof. We need to show \(j(a\to b) \leq a\to b\). Now \(a\wedge j(a\to b) \leq j(a) \wedge j(a\to b) = j(a\wedge (a\to b)) \leq j (b) = b\), and the result follows. ◻
The following two lemmas are both proved by easy checks on the conditions for a nucleus:
Lemma 9. If \(h\) is any element of a complete Heyting algebra \(H\), then \(\lambda a. (a\to h)\to h\) is a nucleus on \(H\). \(\Box\)
We will later use this in the case that \(h\) is the interpretation of an atom, \(b\), so that this nucleus is \(\lambda a. (a\to [\![b]\!])\to [\![b]\!]\).
Lemma 10. If \(H\) is a complete Heyting algebra, and \((j_\alpha \mid \alpha\in A)\) is a family of nuclei on \(H\), then \(\bigwedge_\alpha j_\alpha\) is also a nucleus on \(H\). \(\Box\)
If \(\text{At}\) is a collection of atoms, \(H\) is a (complete) Heyting algebra, and \(\sigma : \text{At}\to H\) is a function giving the interpretation of atoms, then there is a canonical interpretation of intuitionistic propositional logic with atoms from \(\text{At}\) in \(H\). We use \((-)_H\) to distinguish between propositional operators and the lattice operations in \(H\): \[\begin{array}{lr@{\quad}c@{\quad}l} (At) & [\![a]\!] & = & \sigma a \\ [1mm] (\top) & [\![\top]\!] & = & \top_H \\ [1mm] (\wedge) & [\![\phi\wedge\psi]\!] & = & [\![\phi]\!]\wedge_H[\![\psi]\!] \\ [1mm] (\supset) & [\![\phi\supset\psi]\!] & = & [\![\phi]\!]\to_H[\![\psi]\!] \\ [1mm] (\bot) & [\![\bot]\!] & = & \bot_H \\ [1mm] (\vee) & [\![\phi\vee\psi]\!] & = & [\![\phi]\!]\vee_H[\![\psi]\!] \end{array}\] In the case that \(H=\mathcal{W}^\uparrow\), this corresponds to the standard Kripke interpretation.
If \(j\) is a nucleus on \(H\), then, since \(H_j\) is also complete Heyting algebra, there is a canonical interpretation on \(H_j\) arising from \(j\circ \sigma\). Since \(H_j\) can be regarded as a subset of \(H\), we can regard this as a non-standard interpretation in \(H\): \[\begin{array}{l@{\quad}@{\quad}c}(At) & [\![a]\!]_j = (j \circ \sigma) a \\ [1mm] (\top) & [\![\top]\!]_j = j(\top_H) = \top_H \\ [1mm] (\wedge) & [\![\phi\wedge\psi]\!]_j = j([\![\phi]\!]_j\wedge_H[\![\psi]\!]_j) = [\![\phi]\!]_j\wedge_H[\![\psi]\!]_j \\ [1mm] (\supset) & [\![\phi\supset\psi]\!]_j = j ([\![\phi]\!]_j\to_H[\![\psi]\!]_j) = [\![\phi]\!]_j\to_H[\![\psi]\!]_j \\ [1mm] (\bot) & [\![\bot]\!]_j = j (\bot_H) \\ [1mm] (\vee) & [\![\phi\vee\psi]\!]_j = j([\![\phi]\!]_j\vee_H[\![\psi]\!]_j) \end{array}\] Sandqvist’s semantics arises from an instance of this form of interpretation.
We have shown, in Section 7, that for any atom \(b\), the function \(j_b (a) = (a\to [\![b]\!])\to [\![b]\!]\) is a nucleus on \(\mathcal{W}^\uparrow\), and hence so is \(J(a) = \bigwedge_{b\in\text{At}} j_b(a) = \bigwedge_{b\in\text{At}} (a\to [\![b]\!])\to [\![b]\!]\). We consider the interpretation of intuitionistic propositional logic in \(\mathcal{W}^\uparrow_J\).
First, the interpretation of atoms is unchanged. For any atom \(b\), we have \([\![b]\!] \leq J([\![b]\!]) = \bigwedge_{a\in\text{At}} ([\![b]\!]\to [\![a]\!])\to [\![a]\!] \leq ([\![b]\!]\to [\![b]\!])\to [\![b]\!] = [\![b]\!]\). Hence \(J[\![b]\!]=[\![b]\!]\). Second, since \(\mathcal{W}_J\) is closed in \(\mathcal{W}\) under conjunction, the interpretation of conjunction is as in \(\mathcal{W}\), and similarly for implication and true.
Lemma 11. Sandqvist’s base-extension semantics for intuitionistic propositional logic arises as the interpretation in \(\mathcal{W}^\uparrow\) arising from the nucleus \(J(b) = \bigwedge_{a\in\text{At}} (b \to [\![a]\!]) \to [\![a]\!]\).
Proof. We run through the clauses for this interpretation showing their correspondence to the Sandqvist definition. Arguments make use of the soundness of intuitionistic reasoning in the standard interpretation in \(\mathcal{W}^\uparrow\).
\([\![a]\!]_J = J [\![a]\!]\): we have \([\![a]\!] \leq J [\![a]\!] = \bigwedge_{b\in\text{At}} ([\![a]\!]\to [\![b]\!])\to [\![b]\!] \leq ([\![a]\!]\to [\![a]\!]) \to [\![a]\!] = \top\to [\![a]\!] = [\![a]\!]\). Hence \(J [\![a]\!] = [\![a]\!]\), and the interpretation is standard, as in Sandqvist.
All of these are interpreted as in a standard Kripke model in both the \(J\)-interpretation and in Sandqvist.
We have \[\begin{array}{rcl} [\![\bot]\!]_J & = & J (\bot_H) \\ & = & \bigwedge_{b\in\text{At}} (\bot_H\to [\![b]\!])\to [\![b]\!] \\ & = & \bigwedge_{b\in\text{At}} (\top_H \to [\![b]\!]) \\ & = & \bigwedge_{b\in\text{At}} [\![b]\!] \end{array}\] So, \(\mathscr{B}\in[\![\bot]\!]_J\) iff for every \(b\in\text{At}\), \(\mathscr{B}\in[\![b]\!]\) iff for every \(b\in\text{At}\) \(\vdash_{\mathscr{B}}b\), as for Sandqvist.
We have \[\begin{array}{rcl} [\![\phi\vee\psi]\!]_J & = & J([\![\phi]\!]_J\vee_H[\![\psi]\!]_J) \\ & = &\bigwedge_{b\in\text{At}} (([\![\phi]\!]_J \vee [\![\psi]\!]_J)\to [\![b]\!])\to [\![b]\!] \\ & = & \bigwedge_{b\in\text{At}} (([\![\phi]\!]_J\to [\![b]\!])\wedge([\![\psi]\!]_J\to [\![b]\!]))\to [\![b]\!] \end{array}\] So, using induction for \(\phi\) and \(\psi\), and \((\text{At})\) for \(b\), \(\mathscr{B}\in[\![\phi\vee\psi]\!]_J\) iff for every \(b\in\text{At}\), and for every \(\mathscr{C}\supseteq\mathscr{B}\), if \(\Vdash_{\mathscr{C}}({\phi}\supset {b})\wedge({\psi} \supset {b})\), then \(\Vdash_{\mathscr{C}}{b}\).
But then \(\Vdash_{\mathscr{C}}({\phi}\supset {b})\wedge({\psi} \supset {b})\) iff \(\Vdash_{\mathscr{C}}{\phi} \supset {b}\) and \(\Vdash_{\mathscr{C}}{\psi} \supset {b}\) iff \({\phi}\Vdash_{\mathscr{C}}{b}\) and \({\psi}\Vdash_{\mathscr{C}}{b}\), which reduces this to Sandqvist’s definition.
◻
As a result, Sandqvist’s interpretations of the propositional connectives, including \(\bot\) and \(\top\), can all be seen as coming from the same construction, and hence do not require different philosophical explanations.
Moreover, we can now prove the equivalence of \([\![ \tikz[baseline=(a.base)]{\node(a){\phantom{\phi}};\node[draw,black,inner sep=2pt, rounded rectangle]{\phi}} ]\!]\) and \([\![\phi]\!]_J\). If we compare this with Sandqvist’s proof [24], this amounts to demonstrating his condition \((\dagger)\): \[(\dagger)for every \phi and every\mathscr{B}\supseteq\mathscr{N}, \Vdash_{\mathscr{\mathscr{B}}} \tikz[baseline=(a.base)]{\node(a){\phantom{\phi}};\node[draw,black,inner sep=2pt, rounded rectangle]{\phi}} iff\Vdash_{\mathscr{\mathscr{B}}}\phi\] That condition is what fails if we use the original Heyting interpretation. The \(J\)-interpretation is required to make sure that it goes through.
Proposition 3. In \(\mathcal{W}^\uparrow\), we have for all bases \(\mathscr{B}\supseteq\mathscr{N}\), and for all propositions \(\phi\), \[\mathscr{B}\in[\![ \tikz[baseline=(a.base)]{\node(a){\phantom{\phi}};\node[draw,black,inner sep=2pt, rounded rectangle]{\phi}} ]\!] = [\![ \tikz[baseline=(a.base)]{\node(a){\phantom{\phi}};\node[draw,black,inner sep=2pt, rounded rectangle]{\phi}} ]\!]_Jiff \mathscr{B}\in [\![\phi]\!]_J\]
Proof. The proof is by induction on the structure of \(\phi\).
For any atom \(a\), \(\tikz[baseline=(a.base)]{\node(a){\phantom{a}};\node[draw,black,inner sep=2pt, rounded rectangle]{a}} = a\)
See the discussion in Section 4.
For any \(b\in\text{At}\), we have
and hence the rule \((\Rightarrow \tikz[baseline=(a.base)]{\node(a){\phantom{\bot}};\node[draw,black,inner sep=2pt, rounded rectangle]{\bot}} )\Rightarrow b)\) is in \(\mathscr{N}\). It follows that if \(\Vdash_{\mathscr{B}} \tikz[baseline=(a.base)]{\node(a){\phantom{\bot}};\node[draw,black,inner sep=2pt, rounded rectangle]{\bot}}\) then \(\Vdash_{\mathscr{B}}b\) for any atom \(b\). Conversely if \(\Vdash_{\mathscr{B}}b\) for any atom \(b\), then in particular \(\Vdash_{\mathscr{B}} \tikz[baseline=(a.base)]{\node(a){\phantom{\bot}};\node[draw,black,inner sep=2pt, rounded rectangle]{\bot}}\).
Recall that we previously showed \(\phi\vee\psi \to \tikz[baseline=(a.base)]{\node(a){\phantom{\phi\vee\psi}};\node[draw,black,inner sep=2pt, rounded rectangle]{\phi\vee\psi}}\) in the original Kripke interpretation. The equivalent proof holds in the \(J\)-interpretation. To show the reverse, it suffices to establish \(\tikz[baseline=(a.base)]{\node(a){\phantom{\phi\vee\psi}};\node[draw,black,inner sep=2pt, rounded rectangle]{\phi\vee\psi}} \to ((\phi\to b)\wedge (\psi \to b)) \to b\) for any atom \(b\) in the \(J\)-interpretation: \[\begin{prooftree} \hypo{ \tikz[baseline=(a.base)]{\node(a){\phantom{\phi\vee\psi}};\node[draw,black,inner sep=2pt, rounded rectangle]{\phi\vee\psi}} } \hypo{[ \tikz[baseline=(a.base)]{\node(a){\phantom{\phi}};\node[draw,black,inner sep=2pt, rounded rectangle]{\phi}} ]} \infer1[Ind]{\phi} \hypo{[(\phi\to b)\wedge (\psi \to b)]} \infer1[\wedge E]{\phi\to b} \infer2[\to E]{b} \hypo{[ \tikz[baseline=(a.base)]{\node(a){\phantom{\psi}};\node[draw,black,inner sep=2pt, rounded rectangle]{\psi}} ]} \infer1[Ind]{\psi} \hypo{[(\phi \to b)\wedge (\psi \to b)]} \infer1[\wedge E]{\psi\to b} \infer2[\to E]{b} \infer3[\mathscr{N}]{b} \infer1[\to I]{((\phi\to b)\wedge (\psi \to b))\to b} \end{prooftree}\] This now uses the elimination rule for with an atom \(b\) as target, and hence is an instance of a rule in \(\mathscr{N}\).
◻
We now have the ingredients to prove completeness. Given soundness of the interpretation, it is enough to prove the following.
Proposition 4. If \(\Phi\Vdash_{\mathscr{N}}\psi\), then \(\Phi\vdash\psi\) is provable in intuitionistic propositional logic.
Proof. We proceed through three steps. We suppose \(\Phi\Vdash_{\mathscr{N}}\psi\).
Step 1: Using Proposition 3, we translate this into a statement about atoms: \[\{ \tikz[baseline=(a.base)]{\node(a){\phantom{\phi}};\node[draw,black,inner sep=2pt, rounded rectangle]{\phi}}\mid \phi\in\Phi \} \Vdash_{\mathscr{N}} \tikz[baseline=(a.base)]{\node(a){\phantom{\psi}};\node[draw,black,inner sep=2pt, rounded rectangle]{\psi}}\]
Step 2: Using Lemma 4, we reduce this to atomic derivability: \[\{ \tikz[baseline=(a.base)]{\node(a){\phantom{\phi}};\node[draw,black,inner sep=2pt, rounded rectangle]{\phi}}\mid \phi\in\Phi \} \vdash_{\mathscr{N}} \tikz[baseline=(a.base)]{\node(a){\phantom{\psi}};\node[draw,black,inner sep=2pt, rounded rectangle]{\psi}}\]
Step 3: Finally, using Proposition 2, we conclude that \(\Phi\vdash\psi\) is provable in intuitionistic propositional logic.
◻
Of the three steps in the proof above, only the first makes any use of the semantics of propositions, and so that is the critical one in understanding the difference between Sandqvist’s semantics and the standard Kripke interpretation when it comes to completeness.
The arguments we have presented have all been couched in terms of derivability. But proof-theoretic semantics is concerned with the validity of arguments, and hence with a level of detail we have not covered, or at least have not addressed explicitly.
The propositions-as-types (Curry-Howard) correspondence gives a matching between propositions and types, proofs and terms, and reduction of proofs and evaluation of terms for a specific logic and a specific type theory. By choosing the logic and the type theory appropriately, it can be made to seem almost vacuous at a technical level. The terms of the type theory become non-graphical representations of proof-trees. But there is more to it philosophically. The type theory gives ways to construct proofs, and these are then reflected into connectives and the proof rules for them. As a result, constructions of proofs are the direct reflections of basic operations at type-theoretic level. In the Kripke context, we end up with the standard Kripke interpretation as derived from the type theory of a category of presheaves. But Sandqvist’s semantics is not that.
We have seen that there are two ways to interpret a complete Heyting algebra \(H_J\). We can look at it as an entity in its own right. This would imply that Sandqvist’s model is a standard interpretation in a non-standard model. Specifically it is an interpretation in a model in which a form of completeness of the set of atoms is baked into the structure. Categorically, it would likely be the topos of sheaves for the Joyal-Tierney topology corresponding to \(J\) [11]. We could interpret derivations and then proofs in that model.
Alternatively, we can regard \(H_J\) as a well-equipped subset of the normal world. In this context, we take propositions through an operation that makes them more complex. This is most evidently seen with atoms, where we map an atom \(a\) to \(\bigwedge_{b\in\text{At}} (a\supset b)\supset b\), which, type-theoretically, would be \(\prod_{b\in\text{At}} (a\to b)\to b\). Now there are obvious maps \(a \longrightarrow (\prod_{b\in\text{At}} (a\to b)\to b)\) and \((\prod_{b\in\text{At}} (a\to b)\to b) \longrightarrow a\), but they are not inverses and we expect that \(a\) is a retract of \(\prod_{b\in\text{At}} (a\to b)\to b\), but is not isomorphic to it. This means that we have to exercise care when we discuss the semantics of proofs.
More delicately, we have seen that the CPS transformation implicit in this non-standard semantics might impose a restriction on the admissible proof-reductions. We have not discussed this either.
Pym is grateful to University College London for its support of his sabbatical leave at the University of London’s Institute of Philosophy, and to the Institute for its generous hosting.