Failed attempts to provide semantics for intuitionistic logic have a history of leaving behind useful structures. For example, Kleene’s realizability and Medvedev’s finite problems semantics are of theoretical interest, in spite of validating nonintuitionistic theorems
Proof-theoretic validity is another example that can be added to this list. Proof-theoretic validity first appeared in Prawitz’s work in the 1970s via the following definition:
Definition 1 (Schroeder-Heister).
Let S be a set of inference rules containing only atomic formulas, called an atomic base. An argument is a proof-like structure and an argument
${\mathcal {D}}$
is a valid argument if it is S-valid for all S, where S-valid is defined as follows:
-
(1.1) If
${\mathcal {D}}$
is a closed argument constructed from rules in S then it is S-valid. -
(1.2) If
${\mathcal {D}}$
is a closed argument ending in an introduction rule of the intuitionistic propositional calculus, then it is S-valid if its immediate subarguments are S-valid. -
(1.3) If
${\mathcal {D}}$
is a closed argument which does not end in an introduction rule then it is S-valid if it reduces to an S-valid argument. -
(1.4) If
${\mathcal {D}}$
is an open argument concluding
$\varphi $
with open assumptions
$\varphi _0,\dots ,\varphi _n$
then it is S-valid if for all atomic systems
$S'$
extending S, and all closed
$S'$
-valid arguments
${\mathcal {D}}_0,\dots ,{\mathcal {D}}_n$
of
$\varphi _0,\dots ,\varphi _n$
, the following argument is
$S'$
-valid:
Prawitz’s conjecture states that all and only the theorems of intuitionistic propositional logic (IPC) have valid arguments. However, which formulas have valid arguments is sensitive to the treatment of the atomic base. We can adjust what counts as an inference rule and what counts as an extension. For example adding atomic rules which allow the discharge of assumptions changes what is valid. The following presentation makes it explicit that the notion of extension of an atomic base can be varied by writing
$\mathfrak {S}$
for the set of allowable extensions:
Definition 2. A pair
$(\mathfrak {S}, \vDash _{\mathfrak {S}})$
is a PTV semantics if
$\mathfrak {S}$
is a set of atomic bases, and if for every S in
$\mathfrak {S}$
,
$\vDash ^{\mathfrak {S}}_S$
satisfies the following:
$$ \begin{align} \vDash^{\mathfrak{S}}_Sp\Longleftrightarrow& \ \text{ there is a proof using only rules in }S \text{ of }p,\end{align} $$
$$ \begin{align} \vDash^{\mathfrak{S}}_S\varphi\wedge\psi\Longleftrightarrow& \ \vDash^{\mathfrak{S}}_S\varphi\text{ and }\vDash^{\mathfrak{S}}_S\psi, \end{align} $$
$$ \begin{align} \vDash^{\mathfrak{S}}_S\varphi\vee\psi\Longleftrightarrow& \ \vDash^{\mathfrak{S}}_S\varphi\text{ or }\vDash^{\mathfrak{S}}_S\psi, \end{align} $$
$$ \begin{align} \vDash^{\mathfrak{S}}_S\psi\rightarrow\varphi\Longleftrightarrow& \ \psi\vDash^{\mathfrak{S}}_S\varphi, \end{align} $$
$$ \begin{align} \phantom{aaaaaaaaaaaaaa}\Gamma\vDash^{\mathfrak{S}}_S\varphi\Longleftrightarrow& \ [\forall S'\supseteq S(S'\in\mathfrak{S}\text{ and }\vDash^{\mathfrak{S}}_{S'}\Gamma\Rightarrow\vDash^{\mathfrak{S}}_{S'}\varphi)]. \end{align} $$
and further
$\vDash _{\mathfrak {S}}$
is defined from
$\vDash ^{\mathfrak {S}}_S$
as follows:
$$ \begin{align} \Gamma\vDash_{\mathfrak{S}}\varphi\Longleftrightarrow\forall S\in\mathfrak{S}, \Gamma\vDash^{\mathfrak{S}}_S\varphi. \end{align} $$
There is also an approach which removes the reference to extensions by superset in (2).
1 Piecha and Schroeder-Heister’s general result
Piecha and Schroeder-Heister’s paper builds on their earlier paper Piecha, T., et al. Failure of Completeness in Proof-Theoretic Semantics. Journal of Philosophical Logic, vol. 44 (2015), no. 3, pp. 321–335, which demonstrated incompleteness for the PTV semantics with higher-order atomic rules. They use an abstract presentation of the semantics to generalise this result.
Definition 3. Let an abstract semantics be given by a set of objects
$\mathfrak {S}$
such that for every
$S\in \mathfrak {S}$
there is a consequence relation
$\vDash ^{\mathfrak {S}}_S$
and
$\vDash _{\mathfrak {S}}$
satisfying conditions (3), the
$\wedge $
,
$\vee $
, and
$\rightarrow $
property from Definition 2 plus:
$$ \begin{align} \kern-30pt &\varphi\vDash^{\mathfrak{S}}_S\varphi, \end{align} $$
$$ \begin{align} &&\Gamma\vDash^{\mathfrak{S}}_S\varphi\text{ and }\varphi\vDash^{\mathfrak{S}}_S\psi\Longrightarrow& \ \Gamma\vDash^{\mathfrak{S}}_S\psi, \end{align} $$
$$ \begin{align} &&\Gamma\vDash^{\mathfrak{S}}_S\varphi\Longrightarrow& \ \Gamma,\psi\vDash^{\mathfrak{S}}_S\varphi, \end{align} $$
$$ \begin{align} &&\Gamma\vDash_{\mathfrak{S}}\varphi\Longleftrightarrow& \ \text{For all }S\in\mathfrak{S}:(\vDash^{\mathfrak{S}}_S\Gamma\Longrightarrow\vDash^{\mathfrak{S}}_S\varphi), \end{align} $$
$$ \begin{align} &&\Gamma\vdash_{\text{IPC}}\varphi\Longrightarrow& \ \Gamma\vDash_{\mathfrak{S}}\varphi. \end{align} $$
Note that classical model theory meets this definition with
$\mathfrak {S}$
being the set of all models, while Kripke semantics does not because there are Kripke models where
$\mathcal {K}\vDash \varphi \vee \psi $
but neither
$\mathcal {K}\vDash \varphi $
nor
$\mathcal {K}\vDash \psi $
hold. (Though
$\mathcal {K},w\vDash \varphi $
or
$\mathcal {K},w\vDash \psi $
will hold for each world w.) PTV semantics meet the conditions laid out in this definition.
Piecha and Schroder-Heister show that adding one more condition to this list, the generalised disjunction property, ensures that any semantics meeting the abstract description is superintuitionistic. Let
$\mathcal {L}_{\wedge ,\rightarrow ,\bot }$
be the disjunction-free formulas.
Definition 4.
$\text {GDP}(\vDash ) $
holds if, whenever
$\Gamma \vDash \varphi \vee \psi $
and
$\Gamma \subseteq \mathcal {L}_{\wedge ,\rightarrow ,\bot }$
then
$\Gamma \vDash \varphi $
or
$\Gamma \vDash \psi $
.
They then prove that an abstract semantics
$\vDash _{\mathfrak {S}}$
with
$GDP(\vDash ^{\mathfrak {S}}_S)$
for all
$S\in \mathfrak {S}$
satisfies Harrop’s rule (sometimes called the Krisel–Putnam rule or split):
$$ \begin{align} \frac{\neg\varphi\rightarrow(\psi\vee\chi)}{(\neg\varphi\rightarrow\psi)\vee(\neg\varphi\rightarrow\chi)} \end{align} $$
which is a rule that is admissible but not derivable in IPC. Given the following conditions:
$$\begin{align} \Gamma\vDash_{\mathfrak{S}}\varphi\Longleftrightarrow \ (\vDash_S^{\mathfrak{S}}\Gamma\Longrightarrow\vDash_S^{\mathfrak{S}}\varphi). \\
\text{There is }f:\mathfrak{S}\rightarrow\mathcal{P}(\mathcal{L}_{\wedge,\rightarrow,\bot})\text{ such} \text{ that for all }S, \Gamma, \varphi: \qquad\nonumber\end{align}$$
$$\begin{align} \Gamma\vDash^{\mathfrak{S}}_S\varphi \Longleftrightarrow \Gamma,f(S)\vDash^{\mathfrak{S}}\varphi.\\
\text{There is }g:\mathcal{P}(\mathcal{L}_{\wedge,\rightarrow,\bot})\rightarrow\mathfrak{S}\text{ such} \text{ that for all }S, \Gamma\subseteq\mathcal{L}_{\wedge,\rightarrow,\bot}, \varphi: \nonumber\end{align}$$
$$\begin{align}\Gamma\vDash^{\mathfrak{S}}_S\varphi \Longleftrightarrow \vDash^{\mathfrak{S}}_{S\cup g(\Gamma)}\varphi.\end{align} $$
They then show that IPC is incomplete for any abstract semantics
$\vDash _{\mathfrak{S}}$
with one of these properties.
Theorem 5. (
$\vDash _S$
) and Import imply
$GDP(\vDash ^{\mathfrak {S}}_S)$
for all
$S\in \mathfrak {S}$
.
From which it follows that we know any abstract semantics with these properties satisfies Harrop’s rule. And from this it follows immediately that intuitionistic logic is incomplete with regards to them.
Theorem 6. Export plus completeness implies
$GDP(\vDash ^{\mathfrak {S}}_S)$
for all
$S\in \mathfrak {S}$
.
This does not necessarily imply that Harrop’s rule is satisfied but it does prove that systems with Export cannot be complete.
Prawitz’s conjecture applied to a variety of proposed definitions for proof-theoretic validity is shown to be false by these results. Export is true on Definition 2 no matter how one picks the set of bases and
$\vDash _S$
is satisfied by the notion without extensions of bases. However, there are notions that escape as Piecha and Schroeder-Heister point out in their discussion of the definition in Goldfarb, W. On Dummett’s “Proof-Theoretic Justifications of Logical Laws”. Advances in Proof-Theoretic Semantics, edited by Piecha, T. and Schroeder-Heister, P., Springer, 2016, pp. 195–210.
2 Gheorghiu, Gu, and Pym’s application to subintuitionistic logics
Sandqvist, T. Base-Extension Semantics for Intuitionistic Sentential Logic. Logic Journal of the IGPL, vol. 23 (2015), no. 5, pp. 719–731, gets around Piecha and Schroeder-Heister’s results by changing the definition of
$\vee $
to
$$ \begin{align} \Vdash_{S}\varphi\vee\psi\Longleftrightarrow \ \forall S'\supseteq S: (\varphi\Vdash_{S'}p \ \& \ \psi\Vdash_{S'}p\Longrightarrow \Vdash_{S'}p). \end{align} $$
While this no longer can be understood in the manner of Definition 1, it can still be thought of as an approach within proof-theoretic semantics. As Gheorghiu et al. point out, it can be seen as representing the elimination rule, rather than the introduction rule, for
$\vee $
.
Gheorghiu et al. extend this approach to intuitionistic multiplicative linear logic by having a multiset of atomic formulas as resources in addition to an atomic base. With this, they are able to prove completeness for their semantics with respect to intuitionistic multiplicative linear logic.
Intuitionistic multiplicative logic has the connectives
$\otimes $
and
$\multimap $
. It also has 
to represent multiset union as opposed to set union. The changes made to treatment of bases involve the addition of a multiset of atoms P.
Definition 7. An atomic base is defined as a set of rules
$\left ({P}_1 \triangleright {p}_1, \ldots , {P}_n \triangleright {p}_n\right ) \Rightarrow {p}$
. We then define
$\vdash _S$
as a relation between the multiset of atoms P and an atom p such that
$p\vdash _Sp$
and
(App) If 
for
$i=1, \ldots , n$
and
$\left ({P}_1 \triangleright {p}_1, \ldots , {P}_n \triangleright {p}_n\right ) \Rightarrow {p} \in S$
, then 
.
With these modifications of the atomic bases in place the following semantics are give:
Definition 8. IMLL-PTV semantics is defined as follows:
$$ \begin{align} \Vdash^P_Sp\Longleftrightarrow& \ P\vdash_Sp, \end{align} $$
$$ \begin{align} \Vdash^P_S\psi\multimap\varphi\Longleftrightarrow& \ \psi\Vdash^P_S\varphi, \end{align} $$
And they show that this consequence relation can be given a completeness theorem.
Theorem 9. IMLL-PTV semantics is sound and complete for intuitionistic multiplicative linear logic.
3 Oliveira’s completeness via pragmatist approach
Oliveira’s notion of proof-theoretic validity may be the most distinctive of the methods we consider here. He develops Dummett’s pragmatist approach where, rather than taking the introduction rules as the definitions, the elimination rules are used. The paper has a powerful result in favour of this approach: the resulting system is sound and complete for intuitionistic logic and there are no considerations of atomic formulas at all. In explaining the result I will assume the reader is familiar with the terminology for the proof of normalization in Troelstra, A. S., and Schwichtenberg, H. Basic Proof Theory. Cambridge University Press (2000).
Oliveira’s formalism does not have atomic bases. The base case for valid arguments involves any canonical argument with all its subarguments also canonical. This allows open arguments to be valid without further consideration, unlike in the approaches considered above. To describe when an argument is valid on this approach we need two other notions. First the notion of canonical argument needs to be adapted to the pragmatist approach:
Definition 10. An argument
${\mathcal {D}}$
from
$\Gamma $
to
$\varphi $
is canonical if for both:
-
1.
${\mathcal {D}}$
and -
2. all subarguments
${\mathcal {D}}'$
for the minor premises of an
$\vee $
-like elimination rule,
there is an assumption
$\psi $
of
${\mathcal {D}}/{\mathcal {D}}'$
such that every formula on its branch is the major premiss of an elimination rule.
This definition is a natural modification of the notion of a introduction canonical argument for elimination rules.
Definition 11. A complementation for an argument
${{\mathcal {D}}\atop \varphi }$
from
$\Gamma $
to
$\varphi $
is
${{{\mathcal {D}} \atop \varphi } \atop {\mathcal {D}}'}$
where
${\mathcal {D}}'$
is such that:
-
1.
$\varphi $
is such that every formula on its branch in
${\mathcal {D}}'$
is the major premiss of an elimination rule, -
2. the conclusion is atomic,
-
3. it is not more complex than
${\mathcal {D}}$
.
Complementation is the analogue of substitution of closed arguments for open assumptions in Definition 1. Which gives the following pragmatist definition of valid argument:
Definition 12. An argument is valid if:
-
1. it is canonical and all its critical subarguments are valid and of lower complexity,
-
2. given any complementation there is a valid canonical argument from at most the same assumptions to the same conclusion.
With the definition of validity in place we can state Oliveira’s main result, the soundness and completeness of the semantics for IPC:
Theorem 13. There is a valid argument from assumptions in
$\Gamma $
to
$\varphi $
iff
$\Gamma \vdash _{\text {IPC}}\varphi $
.
