# A note on schematic validity and completeness in Prawitz's semantics

Antonio Piccolomini d'Aragona

► To cite this version:

Antonio Piccolomini d'Aragona. A note on schematic validity and completeness in Prawitz's semantics. Francesco Bianchini; Vincenzo Fano; Pierluigi Graziani. Current topics in logic and the philosophy of science. Papers from SILFS 2022 postgraduate conference, 4, Società Italiana di Logica e Filosofia delle Scienze (SILFS), 2024, 978-1-84890-455-2. hal-04573084

HAL Id: hal-04573084

https://hal.science/hal-04573084

Submitted on 13 May 2024

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
<figure><img src="image_1.png" /></figure>

HAL
open science

# A note on schematic validity and completeness in Prawitz's semantics

Antonio Piccolomini d'Aragona

► To cite this version:

Antonio Piccolomini d'Aragona. A note on schematic validity and completeness in Prawitz's semantics. Francesco Bianchini; Vincenzo Fano; Pierluigi Graziani. Current topics in logic and the philosophy of science. Papers from SILFS 2022 postgraduate conference, 4, Società Italiana di Logica e Filosofia delle Scienze (SILFS), 2024, 978-1-84890-455-2. hal-04573084

HAL Id: hal-04573084

https://hal.science/hal-04573084v1

Submitted on 13 May 2024

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_2.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
A NOTE ON SCHEMATIC VALIDITY AND
COMPLETENESS IN PRAWITZ'S SEMANTICS

ANTONIO PICCOLOMINI D'ARAGONA

Institute of Philosophy, Czech Academy of Sciences

piccolomini@flu.cas.cz

# 1 Introduction

Prawitz's semantics, an instance of proof-theoretic semantics [1, 13], has come in basically two forms: semantics of valid arguments – SVA, see e.g. [9] – and theory of grounds – ToG, see e.g. [10]. Here, I shall focus mostly on SVA, and I will only occasionally refer to ToG.

SVA is based on the notion of valid argument. The latter is inspired by Prawitz's normalisation results for Gentzen's Natural Deduction [8], stating that derivations for $Γ ⊢ A$ can be transformed, through suitable reductions, to derivations for $Γ* ⊆ Γ ⊢ A$ without detours. A detour is given by a formula which occurs both as conclusion of an introduction, and as a major premise of an elimination.

In intuitionistic logic, Prawitz's theorems imply what Schroeder-Heister called the fundamental corollary [12]: A is a theorem iff there is a closed derivation of A ending by an introduction. This may confirm Gentzen's claim that introductions fix meaning, while eliminations are unique functions of the introductions [2].

Prawitz's well-known inversion principle [8] that a by-introduction proof of A contains (part of) what is needed for drawing consequences

<footnote>I thank Cesare Cozzo, Ansten Klev, Ivo Pezlar, Thomas Piecha, Paolo Pistone, Dag Prawitz, Peter Schroeder-Heister and Will Stafford for helpful comments. Work on this article was supported by grant LQ300092101 from the Czech Academy of Sciences</footnote>
A NOTE ON SCHEMATIC VALIDITY AND
COMPLETENESS IN PRAWITZ'S SEMANTICS

ANTONIO PICCOLOMINI D'ARAGONA

Institute of Philosophy, Czech Academy of Sciences

piccolomini@flu.cas.cz

# 1 Introduction

Prawitz's semantics, an instance of proof-theoretic semantics [1, 13], has come in basically two forms: semantics of valid arguments – SVA, see e.g. [9] – and theory of grounds – ToG, see e.g. [10]. Here, I shall focus mostly on SVA, and I will only occasionally refer to ToG.

SVA is based on the notion of valid argument. The latter is inspired by Prawitz's normalisation results for Gentzen's Natural Deduction [8], stating that derivations for $Γ ⊢ A$ can be transformed, through suitable reductions, to derivations for $Γ* ⊆ Γ ⊢ A$ without detours. A detour is given by a formula which occurs both as conclusion of an introduction, and as a major premise of an elimination.

In intuitionistic logic, Prawitz's theorems imply what Schroeder-Heister called the fundamental corollary [12]: A is a theorem iff there is a closed derivation of A ending by an introduction. This may confirm Gentzen's claim that introductions fix meaning, while eliminations are unique functions of the introductions [2].

Prawitz's well-known inversion principle [8] that a by-introduction proof of A contains (part of) what is needed for drawing consequences

<footnote>I thank Cesare Cozzo, Ansten Klev, Ivo Pezlar, Thomas Piecha, Paolo Pistone, Dag Prawitz, Peter Schroeder-Heister and Will Stafford for helpful comments. Work on this article was supported by grant LQ300092101 from the Czech Academy of Sciences</footnote>
of A, can thus undergo a semantic reading: arbitrary inferences may be *justified* by transformations on proofs of the major premises. An argument in general can be said to be valid when its arbitrary inferences are so justified. This might happen relative to some underlying atomic proof-system, meant to determine non-logical meanings, or hold irrespective of such systems, and thus qualify as logical.

In the SVA-inspired framework of some other authors, which with Sandqvist [11] we may call *Base Semantics*, the role of justifications and proof-structures is limited to atomic proof-systems. Validity of arguments is replaced by a consequence relation among formulas, which may once again be relative to given atomic proof-systems, or hold on all such systems, i.e. be logical.

Works in the Base Semantics tradition have shown that intuitionistic completeness depends on peculiar features of atomic proof-systems – see [5] for an overview, while later examples are [6, 14, 15, 16]. Building upon a result of [7], I here prove incompleteness of intuitionistic logic with respect to a variant of SVA, and so show that, under a certain reading, Base Semantics copes with an approach where justifications and proof-structures are not disregarded. However, I also point out that the passage from Base Semantics to SVA is non-trivial, since the adaptation of the result of [7] to SVA seems to force an understanding of reductions as *non-schematic* functions from and to proof-structures.

In particular, I shall argue that a more “schematic” understanding of reductions blocks certain proofs of soundness of classical logic, which instead obtain when reductions are non-schematic. This may mean that a substantive part of the constructive nature of Prawitz’s semantics stems from a certain understanding of reductions, rather than just from the fact that the approach is proof-based.

Although SVA and Base Semantics can be (and have been) developed for full first-order logic, intuitionistic (in)completeness is mostly discussed at a propositional level. I accordingly limit myself to propositional logic. Moreover, in proving intuitionistic incompleteness, I use classical logic at the meta-level. This is however sufficient for raising my point.
of A, can thus undergo a semantic reading: arbitrary inferences may be *justified* by transformations on proofs of the major premises. An argument in general can be said to be valid when its arbitrary inferences are so justified. This might happen relative to some underlying atomic proof-system, meant to determine non-logical meanings, or hold irrespective of such systems, and thus qualify as logical.

In the SVA-inspired framework of some other authors, which with Sandqvist [11] we may call *Base Semantics*, the role of justifications and proof-structures is limited to atomic proof-systems. Validity of arguments is replaced by a consequence relation among formulas, which may once again be relative to given atomic proof-systems, or hold on all such systems, i.e. be logical.

Works in the Base Semantics tradition have shown that intuitionistic completeness depends on peculiar features of atomic proof-systems – see [5] for an overview, while later examples are [6, 14, 15, 16]. Building upon a result of [7], I here prove incompleteness of intuitionistic logic with respect to a variant of SVA, and so show that, under a certain reading, Base Semantics copes with an approach where justifications and proof-structures are not disregarded. However, I also point out that the passage from Base Semantics to SVA is non-trivial, since the adaptation of the result of [7] to SVA seems to force an understanding of reductions as *non-schematic* functions from and to proof-structures.

In particular, I shall argue that a more “schematic” understanding of reductions blocks certain proofs of soundness of classical logic, which instead obtain when reductions are non-schematic. This may mean that a substantive part of the constructive nature of Prawitz’s semantics stems from a certain understanding of reductions, rather than just from the fact that the approach is proof-based.

Although SVA and Base Semantics can be (and have been) developed for full first-order logic, intuitionistic (in)completeness is mostly discussed at a propositional level. I accordingly limit myself to propositional logic. Moreover, in proving intuitionistic incompleteness, I use classical logic at the meta-level. This is however sufficient for raising my point.
The article is structured as follows. In Section 2 I give an outline of (a variant of) SVA. In Section 3 I define (a variant of) Base Semantics, and prove incompleteness of intuitionistic logic with respect to it – specifically, soundness of excluded middle with respect to it. In Section 4 I adapt the incompleteness proof to SVA in such a way as to stick to Prawitz’s original idea of a semantics where justifications and proof-structures do play an active role. In Section 5 I discuss the incompleteness result of Section 4 with reference to a notion of justification understood on different degrees of strength. In the concluding remarks, I finally suggest some tentative proposals for accounting for a “schematic” notion of reduction, in terms of restrictions on the form of open valid arguments, of Pezlar selector, and of linearity conditions on replacement of variable parts in proof-structures.

## 2 SVA (over a base)

Prawitz’s normalisation obtains through reduction functions from and to Gentzen’s Natural Deduction derivations, whose iteration eventually normalise application arguments while keeping the conclusion and not expanding the assumptions-set. For disjunction detours, such a function is e.g.

$$ \frac{\begin{array}{c} \mathcal{D}_1 \\ \frac{A_i \quad (\forall I), i = 1, 2 \quad \mathcal{D}_2 \quad \mathcal{D}_3 \quad \mathcal{D}_i}{A_1 \lor A_2 \quad B \quad B \quad (\forall E)} \end{array}}{B} \underset{\phi \searrow}{\Rightarrow} \frac{\begin{array}{c} \mathcal{D}_1 \\ [A_i] \\ \mathcal{D}_{i+1} \\ B \end{array}}{B} $$

This is brought to a semantic level by SVA, through a suitable generalisation of the notions of derivation and reduction towards, respectively, the notions of argument structure and justification, relative to a background language $\mathcal{L}$ which will be here given as follows.

**Definition 1.** The grammar of the language $\mathcal{L}$ is

$$ X := p \mid \bot \mid X \land X \mid X \lor X \mid X \rightarrow X. $$
The article is structured as follows. In Section 2 I give an outline of (a variant of) SVA. In Section 3 I define (a variant of) Base Semantics, and prove incompleteness of intuitionistic logic with respect to it – specifically, soundness of excluded middle with respect to it. In Section 4 I adapt the incompleteness proof to SVA in such a way as to stick to Prawitz’s original idea of a semantics where justifications and proof-structures do play an active role. In Section 5 I discuss the incompleteness result of Section 4 with reference to a notion of justification understood on different degrees of strength. In the concluding remarks, I finally suggest some tentative proposals for accounting for a “schematic” notion of reduction, in terms of restrictions on the form of open valid arguments, of Pezlar selector, and of linearity conditions on replacement of variable parts in proof-structures.

## 2 SVA (over a base)

Prawitz’s normalisation obtains through reduction functions from and to Gentzen’s Natural Deduction derivations, whose iteration eventually normalise application arguments while keeping the conclusion and not expanding the assumptions-set. For disjunction detours, such a function is e.g.

$$ \frac{\begin{array}{c} \mathcal{D}_1 \\ \frac{A_i}{A_1 \lor A_2} (\lor_I), i = 1, 2 \\ \hline B \end{array}}{\lor_E} \quad \begin{array}{c} [A_1] \quad [A_2] \\ \mathcal{D}_2 \quad \mathcal{D}_3 \\ B \quad B \end{array} \quad \begin{array}{c} \mathcal{D}_1 \\ [A_i] \\ \mathcal{D}_{i+1} \\ \hline B \end{array} \quad \begin{array}{c} \phi_\vee \\ \implies \end{array} $$

This is brought to a semantic level by SVA, through a suitable generalisation of the notions of derivation and reduction towards, respectively, the notions of argument structure and justification, relative to a background language $\mathcal{L}$ which will be here given as follows.

**Definition 1.** The grammar of the language $\mathcal{L}$ is

$$ X := p \mid \bot \mid X \land X \mid X \lor X \mid X \rightarrow X. $$
The $p$-s and $\perp$ are atoms, $\perp$ being a constant symbol for the absurd. As done above, I use capital Latin letter as variables for formulas of $\mathcal{L}$, while capital Greek letters will be used as variables for sets of formulas. Negation is defined by

$$ \neg A \stackrel{def}{=} A \to \perp. $$

Just like in Model Theory, also in SVA we have structures which fix the meaning of the non-logical components of $\mathcal{L}$, and thus serve as induction-base for the definition of the semantic core-notions. Unlike Model Theory, however, these structures are not sets (or values) onto which non-logical components are mapped, but atomic systems, i.e. sets of rules that establish the semantic behaviour of atoms – and thus determine constructively the meaning of the components they involve. Atomic systems can be defined in different ways, depending on different desiderata one may have – see [6] – and yielding different outcomes for validity-related concepts such as completeness – see [5]. Here, I will understand them as sets of production rules, i.e. I will not allow premises to be lower-level rules, nor will I allow for discharge of assumptions at the atomic level.

**Definition 2.** An atomic base $\mathfrak{B}$ over $\mathcal{L}$ is a (countable) set of rules

$$ \frac{A_1, \dots, A_n}{B} $$

where $n \ge 0$, $A_i$, $B$ are atoms of $\mathcal{L}$ and $A_i \neq \perp$ ($i \le n$).

Derivations on $\mathfrak{B}$ are defined in a usual inductive way. The derivability relation on $\mathfrak{B}$ is written $\vdash_{\mathfrak{B}}$, while the derivations-set of $\mathfrak{B}$ is written $\text{DER}_{\mathfrak{B}}$. I always require bases to be consistent.

**Definition 3.** $\mathfrak{B}$ is consistent if $\text{iff } \vdash_{\mathfrak{B}} \perp$.

**Definition 4.** An argument structure over $\mathcal{L}$ is a pair $(T, f)$ such that $T$ is a tree whose nodes are either empty, in which case they are always top-nodes, or formulas of $\mathcal{L}$, and $f$ is a function defined on a subset $\Gamma$ of non-empty top-nodes of $T$ such that, for every $A \in \Gamma$, $f(A)$ is below $A$ in $T$.
The p-s and ⊥ are atoms, ⊥ being a constant symbol for the absurd. As done above, I use capital Latin letter as variables for formulas of $\mathcal{L}$, while capital Greek letters will be used as variables for sets of formulas. Negation is defined by

$$ \neg A \stackrel{def}{=} A \to \bot. $$

Just like in Model Theory, also in SVA we have structures which fix the meaning of the non-logical components of $\mathcal{L}$, and thus serve as induction-base for the definition of the semantic core-notions. Unlike Model Theory, however, these structures are not sets (or values) onto which non-logical components are mapped, but atomic systems, i.e. sets of rules that establish the semantic behaviour of atoms – and thus determine constructively the meaning of the components they involve. Atomic systems can be defined in different ways, depending on different desiderata one may have – see [6] – and yielding different outcomes for validity-related concepts such as completeness – see [5]. Here, I will understand them as sets of production rules, i.e. I will not allow premises to be lower-level rules, nor will I allow for discharge of assumptions at the atomic level.

**Definition 2.** An atomic base $\mathfrak{B}$ over $\mathcal{L}$ is a (countable) set of rules

$$ \frac{A_1, \dots, A_n}{B} $$

where $n \ge 0$, $A_i$, $B$ are atoms of $\mathcal{L}$ and $A_i \neq \bot$ ($i \le n$).

Derivations on $\mathfrak{B}$ are defined in a usual inductive way. The derivability relation on $\mathfrak{B}$ is written $\vdash_{\mathfrak{B}}$, while the derivations-set of $\mathfrak{B}$ is written $DER_{\mathfrak{B}}$. I always require bases to be consistent.

**Definition 3.** $\mathfrak{B}$ is consistent if $\mathrm{iff} \nvdash_{\mathfrak{B}} \bot$.

**Definition 4.** An argument structure over $\mathcal{L}$ is a pair $(T, f)$ such that $T$ is a tree whose nodes are either empty, in which case they are always top-nodes, or formulas of $\mathcal{L}$, and $f$ is a function defined on a subset $\Gamma$ of non-empty top-nodes of $T$ such that, for every $A \in \Gamma$, $f(A)$ is below $A$ in $T$.
Given $\mathcal{D} = \langle T, f \rangle$ where $T$ has top-nodes $\Gamma$ and root $A$, I call $\Gamma$ the *assumptions* of $\mathcal{D}$ and $A$ the *conclusion* of $\mathcal{D}$ – thus $f$ is an *assumptions-discharge*.

**Definition 5.** $\mathcal{D}$ is closed iff all its assumptions are discharged, otherwise it is open.

Where $\Gamma$ is the set of the open assumptions of a $\mathcal{D}$ with conclusion $A$, I shall say that $\mathcal{D}$ is an argument structure from $\Gamma$ to $A$, and I shall indicate it by

$$ \begin{array}{c} \Gamma \\ \mathcal{D} \\ A \end{array} $$

**Definition 6.** Given $\mathcal{D}$ from $\Gamma$ to $A$ and $\sigma$ a function such that, for every $B \in \Gamma$, $\sigma(B)$ is a (closed) argument structure with conclusion $B$, a (closed) $\sigma$-instance $\mathcal{D}^{\sigma}$ of $\mathcal{D}$ is the argument structure obtained from $\mathcal{D}$ by replacing every $B \in \Gamma$ with $\sigma(B)$.

**Definition 7.** An inference is a triple $\langle\langle\mathcal{D}_1, \dots, \mathcal{D}_n\rangle, A, \delta\rangle$, where $\delta$ is an indication of assumptions which may be discharged by the inference. The argument structure associated to the inference, indicated by

$$ \frac{\mathcal{D}_1, \dots, \mathcal{D}_n}{A} \delta $$

is obtained by conjoining the trees of the $\mathcal{D}_i$-s through a root-node $A$, and by expanding the assumptions-discharges of the $\mathcal{D}_i$-s according to $\delta$. A rule is a set of inferences, whose elements are called instances of the rule.

I shall assume that rules can be described schematically, e.g. standard introduction rules in Gentzen's Natural Deduction,

$$ \frac{\begin{array}{c} A \\ A \wedge B \end{array}}{A \wedge B} (\wedge_I) \quad \frac{A_i}{A_1 \vee A_2} (\vee_I), \quad i = 1, 2 \quad \frac{B}{A \to B} (\to_I) $$

**Definition 8.** $\mathcal{D}$ is canonical iff it is associated to an instance of an introduction rule, otherwise it is non-canonical.
Given $\mathcal{D} = \langle T, f \rangle$ where $T$ has top-nodes $\Gamma$ and root $A$, I call $\Gamma$ the *assumptions* of $\mathcal{D}$ and $A$ the *conclusion* of $\mathcal{D}$ – thus $f$ is an *assumptions-discharge*.

**Definition 5.** $\mathcal{D}$ is closed iff all its assumptions are discharged, otherwise it is open.

Where $\Gamma$ is the set of the open assumptions of a $\mathcal{D}$ with conclusion $A$, I shall say that $\mathcal{D}$ is an argument structure from $\Gamma$ to $A$, and I shall indicate it by

$$ \begin{array}{c} \Gamma \\ \mathcal{D} \\ A \end{array} $$

**Definition 6.** Given $\mathcal{D}$ from $\Gamma$ to $A$ and $\sigma$ a function such that, for every $B \in \Gamma$, $\sigma(B)$ is a (closed) argument structure with conclusion $B$, a (closed) $\sigma$-instance $\mathcal{D}^{\sigma}$ of $\mathcal{D}$ is the argument structure obtained from $\mathcal{D}$ by replacing every $B \in \Gamma$ with $\sigma(B)$.

**Definition 7.** An inference is a triple $\langle\langle\mathcal{D}_1, \dots, \mathcal{D}_n\rangle, A, \delta\rangle$, where $\delta$ is an indication of assumptions which may be discharged by the inference. The argument structure associated to the inference, indicated by

$$ \frac{\mathcal{D}_1, \dots, \mathcal{D}_n}{A} \delta $$

is obtained by conjoining the trees of the $\mathcal{D}_i$-s through a root-node $A$, and by expanding the assumptions-discharges of the $\mathcal{D}_i$-s according to $\delta$. A rule is a set of inferences, whose elements are called instances of the rule.

I shall assume that rules can be described schematically, e.g. standard introduction rules in Gentzen's Natural Deduction,

$$ \frac{\begin{array}{c} A \\ A \wedge B \end{array}}{A \wedge B} (\wedge_I) \quad \frac{A_i}{A_1 \vee A_2} (\vee_I), \quad i = 1, 2 \quad \frac{B}{A \to B} (\to_I) $$

**Definition 8.** $\mathcal{D}$ is canonical iff it is associated to an instance of an introduction rule, otherwise it is non-canonical.
**Definition 9.** Given a rule *R*, a justification of *R* is a constructive function *φ* defined on the set of the argument structures *D* associated to some sub-set of *R* such that, for every *D* ∈ *D*,

• *D* is from Γ to A ⇒ *φ*(*D*) is from Γ* to A, and

• for every σ, φ is defined on σ and φ(σ) = φ( D ) σ .

For example, the reduction $\phi_\vee$ for eliminating maximal disjunctions
from Natural Deduction derivations, which has been defined at the
beginning of this section, can be understood semantically as a jus-
tification showing that elimination of disjunction ($\vee_E$) can be safely
removed, *salva provability*, when its major premise has been obtained
by ($\vee_I$). Observe that $\phi_\vee$ needs not be defined on all the applications
of ($\vee_E$). Via Definition 12 below, applications whose major premise
is proved via ($\vee_I$) only suffice for showing the rule to be justified in
the sense hinted at above.

I take the notion of (*immediate*) *sub-structure* of *D* to be clear
enough at this point, so I will not define it explicitly. The same I will
do with the notion of *substitution* of a sub-structure *D*\* by an argu-
ment structure *D*\*\* in an argument structure *D*, written *D*[*D*\*\*/*D*\*]
– observe that this already occurs in Definition 6. The application of
substitution may require re-indexing the discharge functions associ-
ated to the argument structures, but I shall not deal with these details
here.

**Definition 10.** Given a set of justifications *J*, *D* immediately reduces
to *D*\* relative to *J*, written *D* ≤\*<sub>*l*</sub>*D*\*, iff *D* = *D*\* or, for some sub-
structure *D*\*\* of *D* and some *φ* ∈ *J*, *φ* is defined on *D*\*\* and *D*\* =
*D*[*φ*(*D*\*\*)/*D*\*\*]. *D* reduces to *D*\* relative to *J*, written *D* ≤\*\*<sub>*l*</sub>*D*\*, iff
there is a sequence *D* = *D*<sub>1</sub> ≤\*\*<sub>*l*</sub>*D*<sub>2</sub> ≤\*\*<sub>*l*</sub> ... ≤\*\*<sub>*l*</sub>*D*<sub>*n*−1</sub> ≤\*\*<sub>*l*</sub>*D*<sub>*n*</sub> = *D*\*.

**Definition 11.** An argument is a pair $\langle \mathcal{D}, \mathcal{J} \rangle$.

**Definition 12.** $\langle \mathcal{D}, \mathcal{J} \rangle$ is valid on $\mathfrak{B}$ iff

• *D* is closed *⇒*
**Definition 9.** Given a rule $R$, a justification of $R$ is a constructive function $\phi$ defined on the set of the argument structures $\mathcal{D}$ associated to some sub-set of $R$ such that, for every $\mathcal{D} \in \mathcal{D}$,

• $\mathcal{D}$ is from $\Gamma$ to $A \Rightarrow \phi(\mathcal{D})$ is from $\Gamma^* \subseteq \Gamma$ to $A$, and

• for every $\sigma$, $\phi$ is defined on $\mathcal{D}^\sigma$ and $\phi(\mathcal{D}^\sigma) = \phi(\mathcal{D})^\sigma$.

For example, the reduction $\phi_\vee$ for eliminating maximal disjunctions from Natural Deduction derivations, which has been defined at the beginning of this section, can be understood semantically as a justification showing that elimination of disjunction $(\vee_E)$ can be safely removed, *salva provability*, when its major premise has been obtained by $(\vee_I)$. Observe that $\phi_\vee$ needs not be defined on all the applications of $(\vee_E)$. Via Definition 12 below, applications whose major premise is proved via $(\vee_I)$ only suffice for showing the rule to be justified in the sense hinted at above.

I take the notion of (*immediate*) *sub-structure* of $\mathcal{D}$ to be clear enough at this point, so I will not define it explicitly. The same I will do with the notion of *substitution* of a sub-structure $\mathcal{D}^*$ by an argument structure $\mathcal{D}^{**}$ in an argument structure $\mathcal{D}$, written $\mathcal{D}[\mathcal{D}^{**}/\mathcal{D}^*]$ – observe that this already occurs in Definition 6. The application of substitution may require re-indexing the discharge functions associated to the argument structures, but I shall not deal with these details here.

**Definition 10.** Given a set of justifications $\mathfrak{J}$, $\mathcal{D}$ immediately reduces to $\mathcal{D}^*$ relative to $\mathfrak{J}$, written $\mathcal{D} \leq_l^{\mathfrak{J}} \mathcal{D}^*$, iff $\mathcal{D} = \mathcal{D}^*$ or, for some sub-structure $\mathcal{D}^{**}$ of $\mathcal{D}$ and some $\phi \in \mathfrak{J}$, $\phi$ is defined on $\mathcal{D}^{**}$ and $\mathcal{D}^* = \mathcal{D}[\phi(\mathcal{D}^{**})/\mathcal{D}^{**}]$. $\mathcal{D}$ reduces to $\mathcal{D}^*$ relative to $\mathfrak{J}$, written $\mathcal{D} \leq_l^{\mathfrak{J}} \mathcal{D}^*$, iff there is a sequence $\mathcal{D} = \mathcal{D}_1 \leq_l^{\mathfrak{J}} \mathcal{D}_2 \leq_l^{\mathfrak{J}} \dots \leq_l^{\mathfrak{J}} \mathcal{D}_{n-1} \leq_l^{\mathfrak{J}} \mathcal{D}_n = \mathcal{D}^*$.

**Definition 11.** An argument is a pair $\langle \mathcal{D}, \mathfrak{J} \rangle$.

**Definition 12.** $\langle \mathcal{D}, \mathfrak{J} \rangle$ is valid on $\mathfrak{B}$ iff

• $\mathcal{D}$ is closed $\Rightarrow$
- the conclusion of $\mathcal{D}$ is an atom $\Rightarrow \mathcal{D} \leq^{\mathfrak{J}} \mathcal{D}^*$ for $\mathcal{D}^* = \langle T, \emptyset \rangle$ and $T \in \text{DER}_{\mathfrak{B}}$ closed;

- the conclusion of $\mathcal{D}$ is not an atom $\Rightarrow \mathcal{D} \leq^{\mathfrak{J}} \mathcal{D}^*$ for $\mathcal{D}^*$ closed canonical with immediate sub-structures valid on $\mathfrak{B}$ when paired with $\mathfrak{J}$;

* $\mathcal{D}$ is open from $\Gamma$ to $A \Rightarrow \text{for every } \sigma, \text{ every } B \in \Gamma$ and every extension $\mathfrak{J}^+$ of $\mathfrak{J}$, if $\langle \sigma(B), \mathfrak{J}^+ \rangle$ is valid on $\mathfrak{B}$, then $\langle \mathcal{D}^\sigma, \mathfrak{J}^+ \rangle$ is valid on $\mathfrak{B}$.

Let us prove that $\langle \mathcal{D}, \{\phi_\vee\} \cup \mathfrak{J}_2 \cup \mathfrak{J}_3 \rangle$ is valid on any $\mathfrak{B}$, where $\mathcal{D}$ is the structure

$$ \frac{\begin{array}{c} [A_1] \\ \mathcal{D}_2 \\ A_1 \lor A_2 \end{array} \quad \begin{array}{c} [A_2] \\ \mathcal{D}_3 \\ B \end{array}}{B} (\vee_E) $$

and $\langle \mathcal{D}_2, \mathfrak{J}_2 \rangle$ and $\langle \mathcal{D}_3, \mathfrak{J}_3 \rangle$ are open valid on $\mathfrak{B}$ from $A_1$ and $A_2$ respectively to $B$. By the second clause of Definition 12, we must prove that, for every $\langle \mathcal{D}_1, \{\phi_\vee\} \cup \mathfrak{J}_2 \cup \mathfrak{J}_3 \rangle^+$ valid on $\mathfrak{B}$ where $\mathcal{D}_1$ is closed and has conclusion $A_1 \lor A_2$, we have that $\langle \mathcal{D}[\mathcal{D}_1/A_1 \lor A_2], \{\phi_\vee\} \cup \mathfrak{J}_2 \cup \mathfrak{J}_3 \rangle^+$ is valid on $\mathfrak{B}$. Since $\langle \mathcal{D}_1, \{\phi_\vee\} \cup \mathfrak{J}_2 \cup \mathfrak{J}_3 \rangle^+$ is closed valid on $\mathfrak{B}$, by the first clause of Definition 12, there is a closed canonical $\mathcal{D}_1^*$ with conclusion $A_1 \lor A_2$ such that $\mathcal{D}_1 \leq_{\{\phi_\vee\} \cup \mathfrak{J}_2 \cup \mathfrak{J}_3}^* \mathcal{D}_1^*$, and $\langle \mathcal{D}_1^*, \{\phi_\vee\} \cup \mathfrak{J}_2 \cup \mathfrak{J}_3 \rangle^+$ is valid on $\mathfrak{B}$. Also, $\mathcal{D}_1 \leq_{\{\phi_\vee\} \cup \mathfrak{J}_2 \cup \mathfrak{J}_3}^* \mathcal{D}_1^*$ obviously implies $\mathcal{D} \leq_{\{\phi_\vee\} \cup \mathfrak{J}_2 \cup \mathfrak{J}_3}^* \mathcal{D}^*$, where $\mathcal{D}^*$ is closed of the form

$$ \frac{\begin{array}{c} \mathcal{D}_1^* \\ A_i \\ \hline A_1 \lor A_2 \end{array}}{B} (\vee_I), i = 1, 2 \quad \begin{array}{c} [A_1] \\ \mathcal{D}_2 \\ B \end{array} \quad \begin{array}{c} [A_2] \\ \mathcal{D}_3 \\ B \end{array} (\vee_E) $$

We must show that $\langle \mathcal{D}^*, \{\phi_\vee\} \cup \mathfrak{J}_2 \cup \mathfrak{J}_3 \rangle^+$ is valid on $\mathfrak{B}$, since this implies $\langle \mathcal{D}[\mathcal{D}_1/A_1 \lor A_2], \{\phi_\vee\} \cup \mathfrak{J}_2 \cup \mathfrak{J}_3 \rangle^+$ valid on $\mathfrak{B}$ which in turn, by the arbitrary choice of $\langle \mathcal{D}_1, \{\phi_\vee\} \cup \mathfrak{J}_2 \cup \mathfrak{J}_3 \rangle^+$, implies our result. Since $\phi_\vee \in \{\phi_\vee\} \cup \mathfrak{J}_2 \cup \mathfrak{J}_3)^+$, we have that $\mathcal{D}^* \leq_{\{\phi_\vee\} \cup \mathfrak{J}_2 \cup \mathfrak{J}_3}^* \mathcal{D}^{**}$, with $\mathcal{D}^{**}$ closed of the form
- the conclusion of $\mathcal{D}$ is an atom $\Rightarrow \mathcal{D} \leq^{\mathfrak{J}} \mathcal{D}^*$ for $\mathcal{D}^* = \langle T, \emptyset \rangle$ and $T \in \text{DER}_{\mathfrak{B}}$ closed;

- the conclusion of $\mathcal{D}$ is not an atom $\Rightarrow \mathcal{D} \leq^{\mathfrak{J}} \mathcal{D}^*$ for $\mathcal{D}^*$ closed canonical with immediate sub-structures valid on $\mathfrak{B}$ when paired with $\mathfrak{J}$;

* $\mathcal{D}$ is open from $\Gamma$ to $A \Rightarrow$ for every $\sigma$, every $B \in \Gamma$ and every extension $\mathfrak{J}^+$ of $\mathfrak{J}$, if $\langle \sigma(B), \mathfrak{J}^+ \rangle$ is valid on $\mathfrak{B}$, then $\langle \mathcal{D}^\sigma, \mathfrak{J}^+ \rangle$ is valid on $\mathfrak{B}$.

Let us prove that $\langle \mathcal{D}, \{\phi_\vee\} \cup \mathfrak{J}_2 \cup \mathfrak{J}_3 \rangle$ is valid on any $\mathfrak{B}$, where $\mathcal{D}$ is the structure

$$ \frac{\begin{array}{c} [A_1] \\ \mathcal{D}_2 \\ A_1 \lor A_2 \end{array} \quad \begin{array}{c} [A_2] \\ \mathcal{D}_3 \\ B \end{array}}{B} (\vee_E) $$

and $\langle \mathcal{D}_2, \mathfrak{J}_2 \rangle$ and $\langle \mathcal{D}_3, \mathfrak{J}_3 \rangle$ are open valid on $\mathfrak{B}$ from $A_1$ and $A_2$ respectively to $B$. By the second clause of Definition 12, we must prove that, for every $\langle \mathcal{D}_1, \{\phi_\vee\} \cup \mathfrak{J}_2 \cup \mathfrak{J}_3 \rangle^+$ valid on $\mathfrak{B}$ where $\mathcal{D}_1$ is closed and has conclusion $A_1 \lor A_2$, we have that $\langle \mathcal{D}[\mathcal{D}_1/A_1 \lor A_2], \{\phi_\vee\} \cup \mathfrak{J}_2 \cup \mathfrak{J}_3 \rangle^+$ is valid on $\mathfrak{B}$. Since $\langle \mathcal{D}_1, \{\phi_\vee\} \cup \mathfrak{J}_2 \cup \mathfrak{J}_3 \rangle^+$ is closed valid on $\mathfrak{B}$, by the first clause of Definition 12, there is a closed canonical $\mathcal{D}_1^*$ with conclusion $A_1 \lor A_2$ such that $\mathcal{D}_1 \leq_{\{\phi_\vee\} \cup \mathfrak{J}_2 \cup \mathfrak{J}_3} \mathcal{D}_1^*$, and $\langle \mathcal{D}_1^*, \{\phi_\vee\} \cup \mathfrak{J}_2 \cup \mathfrak{J}_3 \rangle^+$ is valid on $\mathfrak{B}$. Also, $\mathcal{D}_1 \leq_{\{\phi_\vee\} \cup \mathfrak{J}_2 \cup \mathfrak{J}_3} \mathcal{D}_1^*$ obviously implies $\mathcal{D} \leq_{\{\phi_\vee\} \cup \mathfrak{J}_2 \cup \mathfrak{J}_3} \mathcal{D}^*$, where $\mathcal{D}^*$ is closed of the form

$$ \frac{\begin{array}{c} \mathcal{D}_1^* \\ A_i \\ \hline A_1 \lor A_2 \end{array}}{B} (\vee_I), i = 1, 2 \quad \begin{array}{c} [A_1] \\ \mathcal{D}_2 \\ B \end{array} \quad \begin{array}{c} [A_2] \\ \mathcal{D}_3 \\ B \end{array} (\vee_E) $$

We must show that $\langle \mathcal{D}^*, \{\phi_\vee\} \cup \mathfrak{J}_2 \cup \mathfrak{J}_3 \rangle^+$ is valid on $\mathfrak{B}$, since this implies $\langle \mathcal{D}[\mathcal{D}_1/A_1 \lor A_2], \{\phi_\vee\} \cup \mathfrak{J}_2 \cup \mathfrak{J}_3 \rangle^+$ valid on $\mathfrak{B}$ which in turn, by the arbitrary choice of $\langle \mathcal{D}_1, \{\phi_\vee\} \cup \mathfrak{J}_2 \cup \mathfrak{J}_3 \rangle^+$, implies our result. Since $\phi_\vee \in \{\phi_\vee\} \cup \mathfrak{J}_2 \cup \mathfrak{J}_3)^+$, we have that $\mathcal{D}^* \leq_{\{\phi_\vee\} \cup \mathfrak{J}_2 \cup \mathfrak{J}_3} \mathcal{D}^{**}$, with $\mathcal{D}^{**}$ closed of the form
$$ \begin{array}{l} \mathcal{D}_1^* \\ [A_i] \\ \mathcal{D}_{i+1} \\ B \end{array} $$

Since we assumed $\langle \mathcal{D}_{i+1}, \mathfrak{J}_{i+1} \rangle$ to be open valid on $\mathfrak{B}$, by the second clause of Definition 12 $\langle \mathcal{D}^{**}, (\{\phi_\vee\} \cup \mathfrak{J}_2 \cup \mathfrak{J}_3)^+ \rangle$ is closed valid on $\mathfrak{B}$, whence we are done.

### 3 Base semantics

Since argumental validity essentially depends on atomic provability on the base, on reducibility of non-canonical configurations to suitable introduction forms, and on assumptions-closure in the open-arguments case, we may decide to prune Definition 12 by just focusing on formulas, i.e. by dropping argument structures and justifications out.

This leads to Base Semantics, which I give in a somewhat simplified version as what [7] calls *non-extension* semantics.

**Definition 13.** $\Gamma \models_{\mathfrak{B}} A \text{ iff:}$

$$ (a) \quad \Gamma = \emptyset \Rightarrow $$

$$ (At) \quad A \text{ is an atom} \Rightarrow \vdash_{\mathfrak{B}} A; $$

$$ (\wedge) \quad A = B \wedge C \Rightarrow \models_{\mathfrak{B}} B \text{ and } \models_{\mathfrak{B}} C; $$

$$ (\vee) \quad A = B \vee C \Rightarrow \models_{\mathfrak{B}} B \text{ or } \models_{\mathfrak{B}} C; $$

$$ (\rightarrow) \quad A = B \rightarrow C \Rightarrow B \models_{\mathfrak{B}} C; $$

(b) $\Gamma \neq \emptyset \Rightarrow (\models_{\mathfrak{B}} \Gamma \Rightarrow \models_{\mathfrak{B}} A)$, where $\models_{\mathfrak{B}} \Gamma$ means $\models_{\mathfrak{B}} B$ for every $B \in \Gamma$.

**Definition 14.** $\Gamma \models A \text{ iff, for every } \mathfrak{B}, \Gamma \models_{\mathfrak{B}} A$.

We can now give an easy incompleteness proof for intuitionistic logic – IL. In fact, we can even prove soundness of classical logic (which is expected by the use of the latter in the meta-language).

**Proposition 1.** For every $\mathfrak{B}$, $\models_{\mathfrak{B}} A \lor \neg A$.
$$ \begin{array}{l} \mathcal{D}_1^* \\ [A_i] \\ \mathcal{D}_{i+1} \\ B \end{array} $$

Since we assumed $\langle \mathcal{D}_{i+1}, \mathfrak{J}_{i+1} \rangle$ to be open valid on $\mathfrak{B}$, by the second clause of Definition 12 $\langle \mathcal{D}^{**}, (\{\phi_\vee\} \cup \mathfrak{J}_2 \cup \mathfrak{J}_3)^+ \rangle$ is closed valid on $\mathfrak{B}$, whence we are done.

### 3 Base semantics

Since argumental validity essentially depends on atomic provability on the base, on reducibility of non-canonical configurations to suitable introduction forms, and on assumptions-closure in the open-arguments case, we may decide to prune Definition 12 by just focusing on formulas, i.e. by dropping argument structures and justifications out.

This leads to Base Semantics, which I give in a somewhat simplified version as what [7] calls *non-extension* semantics.

**Definition 13.** $\Gamma \models_{\mathfrak{B}} A \text{ iff:}$

$$ (a) \quad \Gamma = \emptyset \Rightarrow $$

$$ (At) \quad A \text{ is an atom} \Rightarrow \vdash_{\mathfrak{B}} A; $$

$$ (\wedge) \quad A = B \wedge C \Rightarrow \models_{\mathfrak{B}} B \text{ and } \models_{\mathfrak{B}} C; $$

$$ (\vee) \quad A = B \vee C \Rightarrow \models_{\mathfrak{B}} B \text{ or } \models_{\mathfrak{B}} C; $$

$$ (\rightarrow) \quad A = B \rightarrow C \Rightarrow B \models_{\mathfrak{B}} C; $$

(b) $\Gamma \neq \emptyset \Rightarrow (\models_{\mathfrak{B}} \Gamma \Rightarrow \models_{\mathfrak{B}} A)$, where $\models_{\mathfrak{B}} \Gamma$ means $\models_{\mathfrak{B}} B$ for every $B \in \Gamma$.

**Definition 14.** $\Gamma \models A \text{ iff, for every } \mathfrak{B}, \Gamma \models_{\mathfrak{B}} A$.

We can now give an easy incompleteness proof for intuitionistic logic – IL. In fact, we can even prove soundness of classical logic (which is expected by the use of the latter in the meta-language).

**Proposition 1.** For every $\mathfrak{B}$, $\models_{\mathfrak{B}} A \lor \neg A$.
*Proof.* For $\mathfrak{B}$ arbitrary, by using classical logic in the meta-language, either $\models_{\mathfrak{B}} A$ or $\not\models_{\mathfrak{B}} A$. If $\models_{\mathfrak{B}} A$, then $\models_{\mathfrak{B}} A \lor \neg A$ by ($\lor$). If instead $\not\models_{\mathfrak{B}} A$, then $A \models_{\mathfrak{B}} \perp$ holds vacuously by (b). Hence, $\models_{\mathfrak{B}} \neg A$ by ($\rightarrow$), and $\models_{\mathfrak{B}} A \lor \neg A$ by ($\lor$). The result now follows from the arbitrariness of $\mathfrak{B}$. $\square$

**Proposition 2.** $\models A \lor \neg A$.

**Theorem 1.** There are $\Gamma$ and $A$ such that $\Gamma \models A$ and $\Gamma \not\vdash_{IL} A$.

Except for the reference to atomic bases – which is in a sense peculiar to Prawitzian approaches – this is essentially the same as what one obtains in BHK-semantics with classical meta-language.

The crucial results of intuitionistic incompleteness to be found in literature on Base Semantics are of course much more significant than the one provided by Theorem 1 – and, accordingly, their proofs require a much more fine-grained framework than the one I put forward here. In [7], incompleteness of intuitionistic logic is e.g. referred to *Harrop rule*, whose validity via Definition 14 is proved without using classical logic in the meta-language.<fnref n="1" /> The adaptation of the Base Semantics framework to SVA that I present in Section 4 below can be extended to these more refined approaches; likewise, the critical remarks about the principles of Base Semantics I provide in Section 5 below also holds for more detailed accounts – both in Base Semantics and in adaptations of it to SVA. Thus, the toy-example that, in the (trivialising) context of a classical meta-language, I discuss in Sections 4 and 5, are enough for raising my points. A comprehensive treatment of the issue can be developed in future works.<fnref n="2" />

<footnote n="1">¹It should be however remarked that, in [7], the rule from premise $A \rightarrow (B \lor C)$ to conclusion $(A \rightarrow B) \lor (A \rightarrow C)$ – with no restrictions on $A$ – is proved to be valid according to Definition 14, by using classical meta-logic and (b) in Definition 13. This can be easily adapted to the SVA-framework along the lines of Section 4 below. I shall not dwell upon this here, as the use of classical meta-logic validates excluded middle, which immediately implies intuitionistic incompleteness (both in Base Semantics and in a suitably modified version of SVA).</footnote>

<footnote n="2">²Let me just remark that the fundamental results proved in [7] require some additional principles, called *Import* and *Export*, and possibly higher-level rules at the atomic level – i.e. atomic rules where the discharge of assumptions is allowed.</footnote>
*Proof.* For $\mathfrak{B}$ arbitrary, by using classical logic in the meta-language, either $\models_{\mathfrak{B}} A$ or $\not\models_{\mathfrak{B}} A$. If $\models_{\mathfrak{B}} A$, then $\models_{\mathfrak{B}} A \lor \neg A$ by ($\lor$). If instead $\not\models_{\mathfrak{B}} A$, then $A \models_{\mathfrak{B}} \perp$ holds vacuously by (b). Hence, $\models_{\mathfrak{B}} \neg A$ by ($\rightarrow$), and $\models_{\mathfrak{B}} A \lor \neg A$ by ($\lor$). The result now follows from the arbitrariness of $\mathfrak{B}$. $\square$

**Proposition 2.** $\models A \lor \neg A$.

**Theorem 1.** There are $\Gamma$ and $A$ such that $\Gamma \models A$ and $\Gamma \not\vdash_{IL} A$.

Except for the reference to atomic bases – which is in a sense peculiar to Prawitzian approaches – this is essentially the same as what one obtains in BHK-semantics with classical meta-language.

The crucial results of intuitionistic incompleteness to be found in literature on Base Semantics are of course much more significant than the one provided by Theorem 1 – and, accordingly, their proofs require a much more fine-grained framework than the one I put forward here. In [7], incompleteness of intuitionistic logic is e.g. referred to *Harrop rule*, whose validity via Definition 14 is proved without using classical logic in the meta-language.<fnref n="1" /> The adaptation of the Base Semantics framework to SVA that I present in Section 4 below can be extended to these more refined approaches; likewise, the critical remarks about the principles of Base Semantics I provide in Section 5 below also holds for more detailed accounts – both in Base Semantics and in adaptations of it to SVA. Thus, the toy-example that, in the (trivialising) context of a classical meta-language, I discuss in Sections 4 and 5, are enough for raising my points. A comprehensive treatment of the issue can be developed in future works.<fnref n="2" />

<footnote n="1">¹It should be however remarked that, in [7], the rule from premise $A \rightarrow (B \lor C)$ to conclusion $(A \rightarrow B) \lor (A \rightarrow C)$ – with no restrictions on $A$ – is proved to be valid according to Definition 14, by using classical meta-logic and (b) in Definition 13. This can be easily adapted to the SVA-framework along the lines of Section 4 below. I shall not dwell upon this here, as the use of classical meta-logic validates excluded middle, which immediately implies intuitionistic incompleteness (both in Base Semantics and in a suitably modified version of SVA).</footnote>

<footnote n="2">²Let me just remark that the fundamental results proved in [7] require some additional principles, called *Import* and *Export*, and possibly higher-level rules at the atomic level – i.e. atomic rules where the discharge of assumptions is allowed.</footnote>
# 4 A kind of intuitionistic SVA-incompleteness

The obvious strategy – also suggested by [7] – for moving from Base Semantics to SVA, is that of starting from the following equivalence:

(EQ) $\Gamma \models_{\mathfrak{B}} A$ iff there is $\langle \mathcal{D}, \mathfrak{J} \rangle$ from $\Gamma$ to $A$ valid on $\mathfrak{B}$.

Condition (a) in Definition 13 holds in SVA under (EQ), so we may just translate Proposition 1 via (EQ), after observing that, with classical logic in the meta-language, condition (b) in Definition 13 also holds under (EQ) in SVA – proof omitted.

However, I prefer to stick to a strict SVA-formulation, which will allow me to remark some points that might be concealed when argument structures and justifications are entirely dropped out.

**Proposition 3.** For every $\mathfrak{B}$, there is a closed argument for $A \lor \neg A$ valid on $\mathfrak{B}$.

*Proof.* Let $\mathfrak{B}$ be arbitrary. By reasoning classically, either there is a closed valid argument for $A$, or there is not. Suppose there is not, and consider

$$ \mathcal{D}^* = \frac{A}{\perp} $$

Then, $\langle \mathcal{D}^*, \emptyset \rangle$ is vacuously valid on $\mathfrak{B}$, and so is $\langle \mathcal{D}^{**}, \emptyset \rangle$, where $\mathcal{D}^{**}$ is

$$ \frac{1}{\frac{[A]}{\perp} \xrightarrow{A \to \perp} I}, 1 $$

The *Import* principle says that, roughly, some assumptions may generate new atomic rules: $\Gamma \models_{\mathfrak{B}} A \Leftrightarrow \models_{\mathfrak{B} \cup \Sigma \Gamma} A$. Together with higher-level atomic rules, this yields validity of Harrop rule via Definition 14 in non-extensions semantics. The *Export* principle says instead that, roughly, (first-level) atomic rules generate new assumptions: $\Gamma \models_{\mathfrak{B} \cup \Sigma} A \Leftrightarrow \Gamma, \Delta^\Sigma \models_{\mathfrak{B}} A$. This yields validity of Harrop rule via Definition 14 for *extension* semantics, namely Base Semantics where condition (b) in Definition 13 is given a monotonic form: $\Gamma \models_{\mathfrak{B}} A \Leftrightarrow$ for all $\mathcal{C} \supseteq \mathfrak{B}$, $(\models_{\mathcal{C}} \Gamma \Rightarrow \models_{\mathcal{C}} A)$.
# 4 A kind of intuitionistic SVA-incompleteness

The obvious strategy – also suggested by [7] – for moving from Base Semantics to SVA, is that of starting from the following equivalence:

(EQ) $\Gamma \models_{\mathfrak{B}} A$ iff there is $\langle \mathcal{D}, \mathfrak{J} \rangle$ from $\Gamma$ to $A$ valid on $\mathfrak{B}$.

Condition (a) in Definition 13 holds in SVA under (EQ), so we may just translate Proposition 1 via (EQ), after observing that, with classical logic in the meta-language, condition (b) in Definition 13 also holds under (EQ) in SVA – proof omitted.

However, I prefer to stick to a strict SVA-formulation, which will allow me to remark some points that might be concealed when argument structures and justifications are entirely dropped out.

**Proposition 3.** For every $\mathfrak{B}$, there is a closed argument for $A \lor \neg A$ valid on $\mathfrak{B}$.

*Proof.* Let $\mathfrak{B}$ be arbitrary. By reasoning classically, either there is a closed valid argument for $A$, or there is not. Suppose there is not, and consider

$$ \mathcal{D}^* = \frac{A}{\perp} $$

Then, $\langle \mathcal{D}^*, \emptyset \rangle$ is vacuously valid on $\mathfrak{B}$, and so is $\langle \mathcal{D}^{**}, \emptyset \rangle$, where $\mathcal{D}^{**}$ is

$$ \frac{1}{\frac{[A]}{\perp} \xrightarrow{A \to \perp} I}, 1 $$

<footnote>The *Import* principle says that, roughly, some assumptions may generate new atomic rules: $\Gamma \models_{\mathfrak{B}} A \Leftrightarrow \models_{\mathfrak{B} \cup \Sigma \Gamma} A$. Together with higher-level atomic rules, this yields validity of Harrop rule via Definition 14 in non-extensions semantics. The *Export* principle says instead that, roughly, (first-level) atomic rules generate new assumptions: $\Gamma \models_{\mathfrak{B} \cup \Sigma} A \Leftrightarrow \Gamma, \Delta^\Sigma \models_{\mathfrak{B}} A$. This yields validity of Harrop rule via Definition 14 for *extension* semantics, namely Base Semantics where condition (b) in Definition 13 is given a monotonic form: $\Gamma \models_{\mathfrak{B}} A \Leftrightarrow$ for all $\mathcal{C} \supseteq \mathfrak{B}$, $(\models_{\mathcal{C}} \Gamma \Rightarrow \models_{\mathcal{C}} A)$.</footnote>
Then, $\langle \mathcal{D}, \{\kappa_1\} \rangle$ is valid on $\mathfrak{B}$, where $\mathcal{D}$ is

$$ \overline{A \lor \neg A} $$

and $\kappa_1$ is the constant function defined by

$$ \mathcal{D} \implies \frac{\mathcal{D}^{**}}{\neg A \quad A \lor \neg A} (\lor_I) $$

Suppose there is a closed $\langle \mathcal{D}^{***}, \mathfrak{J} \rangle$ for $A$ valid on $\mathfrak{B}$. Then $\langle \mathcal{D}, \{\kappa_2\} \cup \mathfrak{J} \rangle$ is valid on $\mathfrak{B}$, where $\kappa_2$ is the constant function defined by

$$ \mathcal{D} \implies \frac{\mathcal{D}^{***}}{A \quad A \lor \neg A} (\lor_I) $$

The result now follows by arbitrariness of $\mathfrak{B}$.

□

A similar result for classical reduction ad absurdum can be found in [9]. Observe that, in Proposition 3, the role of (b) in Definition 13 is played by empty sets of justifications or by constant functions. Definition 14 via (EQ) now gives a kind incompleteness of $\mathbb{I}L$.

**Definition 15.** $\Gamma \models_{\Delta} A$ iff, for every $\mathfrak{B}$, there is $\langle \mathcal{D}, \mathfrak{J} \rangle$ from $\Gamma$ to $A$ valid on $\mathfrak{B}$.

**Proposition 4.** $\models_{\Delta} A \lor \neg A$.

**Theorem 2.** There are $\Gamma$ and $A$ such that $\Gamma \models_{\Delta} A$ and $\Gamma \not\models_{\mathbb{I}L} A$.

# 5 Schematicity

When read against the original formulation of SVA in [9], the proof of Proposition 3 implies a number of aspects which may be so modified as to obtain a different reading of $\models_{\Delta}$ than the one I have proposed in the previous section. First, we may invert the quantifiers in Definition 15.

**Definition 16.** $\Gamma \models_{\Delta}^* A$ iff, for some $\langle \mathcal{D}, \mathfrak{J} \rangle$ from $\Gamma$ to $A$ and every $\mathfrak{B}$, $\langle \mathcal{D}, \mathfrak{J} \rangle$ is valid on $\mathfrak{B}$.
Then, $\langle \mathcal{D}, \{\kappa_1\} \rangle$ is valid on $\mathfrak{B}$, where $\mathcal{D}$ is

$$ \overline{A \lor \neg A} $$

and $\kappa_1$ is the constant function defined by

$$ \mathcal{D} \implies \frac{\mathcal{D}^{**}}{\neg A \quad A \lor \neg A} (\lor_I) $$

Suppose there is a closed $\langle \mathcal{D}^{***}, \mathfrak{J} \rangle$ for $A$ valid on $\mathfrak{B}$. Then $\langle \mathcal{D}, \{\kappa_2\} \cup \mathfrak{J} \rangle$ is valid on $\mathfrak{B}$, where $\kappa_2$ is the constant function defined by

$$ \mathcal{D} \implies \frac{\mathcal{D}^{***}}{A \quad A \lor \neg A} (\lor_I) $$

The result now follows by arbitrariness of $\mathfrak{B}$.

□

A similar result for classical reduction ad absurdum can be found in [9]. Observe that, in Proposition 3, the role of (b) in Definition 13 is played by empty sets of justifications or by constant functions. Definition 14 via (EQ) now gives a kind incompleteness of $\mathbf{IL}$.

**Definition 15.** $\Gamma \models_{\Delta} A$ iff, for every $\mathfrak{B}$, there is $\langle \mathcal{D}, \mathfrak{J} \rangle$ from $\Gamma$ to $A$ valid on $\mathfrak{B}$.

**Proposition 4.** $\models_{\Delta} A \lor \neg A$.

**Theorem 2.** There are $\Gamma$ and $A$ such that $\Gamma \models_{\Delta} A$ and $\Gamma \not\models_{\mathbf{IL}} A$.

# 5 Schematicity

When read against the original formulation of SVA in [9], the proof of Proposition 3 implies a number of aspects which may be so modified as to obtain a different reading of $\models_{\Delta}$ than the one I have proposed in the previous section. First, we may invert the quantifiers in Definition 15.

**Definition 16.** $\Gamma \models_{\Delta}^* A$ iff, for some $\langle \mathcal{D}, \mathfrak{J} \rangle$ from $\Gamma$ to $A$ and every $\mathfrak{B}$, $\langle \mathcal{D}, \mathfrak{J} \rangle$ is valid on $\mathfrak{B}$.
Our proof for Theorem 2 does not directly apply to $|\Delta|$. Yet, the proof of Proposition 3 shows that, for every $\mathfrak{B}$, there is a set of justifications $\mathfrak{J}^{\mathfrak{B}}$ such that $\langle \mathfrak{D}, \mathfrak{J}^{\mathfrak{B}} \rangle$ valid on $\mathfrak{B}$, where $\mathfrak{D}$ is the axiom $A \lor \neg A$, i.e.

$$ \mathfrak{J}^{\mathfrak{B}} = \begin{cases} \{\kappa_1\} & \text{if } \nvdash_{\mathfrak{B}} A \\ \{\kappa_2\} \cup \mathfrak{J} & \text{otherwise} \end{cases} $$

with $\mathfrak{J}$ as required in the proof of Proposition 3. One idea for applying Theorem 2 to $|\Delta|$ may thus be that of modifying Definition 9 so as to have justifications defined, not from argument structures to argument structures, but from subsets of $\mathfrak{S} \times \mathfrak{B}$ to arguments, where $\mathfrak{S}$ is the sets of the argument structures over $\mathcal{L}$ and $\mathfrak{B}$ is the class of atomic bases. In this way, we may set

$$ \mathrm{Ch}(\mathfrak{D}, \mathfrak{B}) = (\mathfrak{D}, \mathfrak{J}^{\mathfrak{B}}). $$

$\mathrm{Ch}$ would thus behave like a choice function picking the right justifications set on each base, so $\langle \mathfrak{D}, \mathrm{Ch} \rangle$ is valid on every $\mathfrak{B}$ – we remark that this strategy requires a number of changes in the formal apparatus of Section 2, which eventually lead to ToG where, roughly, justifications of rules are embedded into inference steps – see [4].

Another alternative would be to put all the $\mathfrak{J}^{\mathfrak{B}}$-s into the justifications set for $\mathfrak{D}$, so that $\langle \mathfrak{D}, \cup_{\mathfrak{B} \in \mathfrak{B}} \mathfrak{J}^{\mathfrak{B}} \rangle$ be valid on every $\mathfrak{B}$. Contrarily to the previous solution, this move does not require we touch Definition 9 at all.

A final option, which is similar to that where we take the union-set of the justifications set of each base, but which, similarly to the choice function strategy, involves a modification of Definition 9, amounts to following [12], namely, replacing, so to say, the justifications with their graph.<fnref n="3" /> Let me give in this case more details than I have done so far.

<footnote n="3">³There are here some subtleties which I cannot deal with. In the approach inspired by [12], one normally allows for alternative justifications for one and the same argument structure – a possibility I have left open in Definition 9. In general, one can show that from any justifications set one can extract what, in Definition 17 below, I call a r-sequence; if alternative justifications are permitted, the inverse holds too. Something similar obtains concerning the relationship between validity of Definition 12 and what I call SH-validity in Definition 20 below: if alternative justifications are not permitted, then the implication holds only for closed argument structures, otherwise one has an equivalence between the notions.</footnote>
Our proof for Theorem 2 does not directly apply to $|\Delta|$. Yet, the proof of Proposition 3 shows that, for every $\mathfrak{B}$, there is a set of justifications $\mathfrak{J}^{\mathfrak{B}}$ such that $\langle \mathfrak{D}, \mathfrak{J}^{\mathfrak{B}} \rangle$ valid on $\mathfrak{B}$, where $\mathfrak{D}$ is the axiom $A \lor \neg A$, i.e.

$$ \mathfrak{J}^{\mathfrak{B}} = \begin{cases} \{\kappa_1\} & \text{if } \nvdash_{\mathfrak{B}} A \\ \{\kappa_2\} \cup \mathfrak{J} & \text{otherwise} \end{cases} $$

with $\mathfrak{J}$ as required in the proof of Proposition 3. One idea for applying Theorem 2 to $|\Delta|$ may thus be that of modifying Definition 9 so as to have justifications defined, not from argument structures to argument structures, but from subsets of $\mathfrak{S} \times \mathfrak{B}$ to arguments, where $\mathfrak{S}$ is the sets of the argument structures over $\mathcal{L}$ and $\mathfrak{B}$ is the class of atomic bases. In this way, we may set

$$ \mathrm{Ch}(\mathfrak{D}, \mathfrak{B}) = (\mathfrak{D}, \mathfrak{J}^{\mathfrak{B}}). $$

Ch would thus behave like a choice function picking the right justifications set on each base, so $\langle \mathfrak{D}, \mathrm{Ch} \rangle$ is valid on every $\mathfrak{B}$ – we remark that this strategy requires a number of changes in the formal apparatus of Section 2, which eventually lead to ToG where, roughly, justifications of rules are embedded into inference steps – see [4].

Another alternative would be to put all the $\mathfrak{J}^{\mathfrak{B}}$-s into the justifications set for $\mathfrak{D}$, so that $\langle \mathfrak{D}, \cup_{\mathfrak{B} \in \mathfrak{B}} \mathfrak{J}^{\mathfrak{B}} \rangle$ be valid on every $\mathfrak{B}$. Contrarily to the previous solution, this move does not require we touch Definition 9 at all.

A final option, which is similar to that where we take the union-set of the justifications set of each base, but which, similarly to the choice function strategy, involves a modification of Definition 9, amounts to following [12], namely, replacing, so to say, the justifications with their graph.<fnref n="3" /> Let me give in this case more details than I have done so far.

<footnote n="3">³There are here some subtleties which I cannot deal with. In the approach inspired by [12], one normally allows for alternative justifications for one and the same argument structure – a possibility I have left open in Definition 9. In general, one can show that from any justifications set one can extract what, in Definition 17 below, I call a r-sequence; if alternative justifications are permitted, the inverse holds too. Something similar obtains concerning the relationship between validity of Definition 12 and what I call SH-validity in Definition 20 below: if alternative justifications are not permitted, then the implication holds only for closed argument structures, otherwise one has an equivalence between the notions.</footnote>
First of all, the modified Definition 9 now reads as follows.

**Definition 17.** A reduction is a pair $\langle \mathcal{D}^1, \mathcal{D}^2 \rangle$ where $\mathcal{D}^2$ has the same conclusion, and at most the same assumptions as $\mathcal{D}^1$. A r-system is a set of reductions. A r-sequence $\langle \mathcal{D}_1^1, \mathcal{D}_1^2 \rangle, \dots, \langle \mathcal{D}_n^1, \mathcal{D}_n^2 \rangle$ such that, for every $i \le n$, $\mathcal{D}_{i-1}^2 = \mathcal{D}_i^1$, is said to be from $\mathcal{D}_1^1$ to $\mathcal{D}_n^2$.

Let us modify accordingly Definitions 10, 11 and 12.

**Definition 18.** Given a r-system $\Sigma$, $\mathcal{D}$ reduces to $\mathcal{D}^*$ relative to $\Sigma$, written $\mathcal{D} \le^\Sigma \mathcal{D}^*$, iff $\Sigma$ contains a r-sequence from $\mathcal{D}$ to $\mathcal{D}^*$.

**Definition 19.** An argument is a pair $\langle \mathcal{D}, \Sigma \rangle$.

**Definition 20.** $\langle \mathcal{D}, \Sigma \rangle$ is SH-valid on $\mathfrak{B}$ iff the same conditions as in Definition 12 hold, with $\mathfrak{J}$ and $\le^\mathfrak{J}$ replaced by $\Sigma$ and $\le^\Sigma$ respectively.

It is now easy to see that the following obtains.

**Proposition 5.** For every $\mathfrak{B}$, there is closed $\langle \mathcal{D}, \Sigma \rangle$ for $A \lor \neg A$ SH-valid on $\mathfrak{B}$.

*Proof.* Basically the same as proof of Proposition 3, where the relevant reductions are $\langle \mathcal{D}, \kappa_1(\mathcal{D}) \rangle$ and $\langle \mathcal{D}, \kappa_2(\mathcal{D}) \rangle$, respectively. $\square$

This shows that, for every $\mathfrak{B}$, there is a r-system $\Sigma_{\mathfrak{B}}$ such that $\langle \mathcal{D}, \Sigma_{\mathfrak{B}} \rangle$ is valid on $\mathfrak{B}$ – where $\mathcal{D}$ is the axiom $A \lor \neg A$. Let us now give the following definition of logical validity.

**Definition 21.** $\Gamma \models_{\Delta}^{SH} A$ iff, for some $\langle \mathcal{D}, \Sigma \rangle$ from $\Gamma$ to $A$ and every $\mathfrak{B}$, $\langle \mathcal{D}, \Sigma \rangle$ is SH-valid on $\mathfrak{B}$.

Thus we have what follows.

**Proposition 6.** $\models_{\Delta}^{SH} A \lor \neg A$.

*Proof.* Take $\langle \mathcal{D}, \Sigma \rangle$ with $\mathcal{D}$ the axiom $A \lor \neg A$, and $\Sigma = \bigcup_{\mathfrak{B} \in \mathcal{B}} \Sigma_{\mathfrak{B}}$. $\square$

**Theorem 3.** There are $\Gamma$ and $A$ such that $\Gamma \models_{\Delta}^{SH} A$ and $\Gamma \not\models_{\Gamma'} A$.
First of all, the modified Definition 9 now reads as follows.

**Definition 17.** A reduction is a pair $\langle \mathcal{D}^1, \mathcal{D}^2 \rangle$ where $\mathcal{D}^2$ has the same conclusion, and at most the same assumptions as $\mathcal{D}^1$. A r-system is a set of reductions. A r-sequence $\langle \mathcal{D}_1^1, \mathcal{D}_1^2 \rangle, \dots, \langle \mathcal{D}_n^1, \mathcal{D}_n^2 \rangle$ such that, for every $i \le n$, $\mathcal{D}_{i-1}^2 = \mathcal{D}_i^1$, is said to be from $\mathcal{D}_1^1$ to $\mathcal{D}_n^2$.

Let us modify accordingly Definitions 10, 11 and 12.

**Definition 18.** Given a r-system $\Sigma$, $\mathcal{D}$ reduces to $\mathcal{D}^*$ relative to $\Sigma$, written $\mathcal{D} \le^\Sigma \mathcal{D}^*$, iff $\Sigma$ contains a r-sequence from $\mathcal{D}$ to $\mathcal{D}^*$.

**Definition 19.** An argument is a pair $\langle \mathcal{D}, \Sigma \rangle$.

**Definition 20.** $\langle \mathcal{D}, \Sigma \rangle$ is SH-valid on $\mathfrak{B}$ iff the same conditions as in Definition 12 hold, with $\mathfrak{J}$ and $\le^\mathfrak{J}$ replaced by $\Sigma$ and $\le^\Sigma$ respectively.

It is now easy to see that the following obtains.

**Proposition 5.** For every $\mathfrak{B}$, there is closed $\langle \mathcal{D}, \Sigma \rangle$ for $A \lor \neg A$ SH-valid on $\mathfrak{B}$.

*Proof.* Basically the same as proof of Proposition 3, where the relevant reductions are $\langle \mathcal{D}, \kappa_1(\mathcal{D}) \rangle$ and $\langle \mathcal{D}, \kappa_2(\mathcal{D}) \rangle$, respectively. $\square$

This shows that, for every $\mathfrak{B}$, there is a r-system $\Sigma_{\mathfrak{B}}$ such that $\langle \mathcal{D}, \Sigma_{\mathfrak{B}} \rangle$ is valid on $\mathfrak{B}$ – where $\mathcal{D}$ is the axiom $A \lor \neg A$. Let us now give the following definition of logical validity.

**Definition 21.** $\Gamma \models_{\Delta}^{SH} A$ iff, for some $\langle \mathcal{D}, \Sigma \rangle$ from $\Gamma$ to $A$ and every $\mathfrak{B}$, $\langle \mathcal{D}, \Sigma \rangle$ is SH-valid on $\mathfrak{B}$.

Thus we have what follows.

**Proposition 6.** $\models_{\Delta}^{SH} A \lor \neg A$.

*Proof.* Take $\langle \mathcal{D}, \Sigma \rangle$ with $\mathcal{D}$ the axiom $A \lor \neg A$, and $\Sigma = \bigcup_{\mathfrak{B} \in \mathcal{B}} \Sigma_{\mathfrak{B}}$. $\square$

**Theorem 3.** There are $\Gamma$ and $A$ such that $\Gamma \models_{\Delta}^{SH} A$ and $\Gamma \not\models_{IL} A$.
There is however a clear sense in which neither Ch, nor $\cup_{\mathfrak{B} \in \mathfrak{B}} \mathfrak{J}_{\mathfrak{B}}$ or $\cup_{\mathfrak{B} \in \mathfrak{B}} \Sigma_{\mathfrak{B}}$ can be said to be or to consist of *schematic* justifications, where by schematic we may provisionally mean that the justification can be expressed as a *rule for rewriting argument structures*, similar to the reduction for removing disjunction detours that we have seen at the beginning of Section 2. Ch is obviously not so, since it is not even defined on argument structures only, but on pairs of arguments structures and bases. Even if it is in a sense schematic, it hence differs significantly in spirit from $\phi_\vee$.

On the other hand, $\cup_{\mathfrak{B} \in \mathfrak{B}} \mathfrak{J}^{\mathfrak{G}}$ contains of course a schematic justification, i.e. $\kappa_1$. But the $\kappa_2$ we take on each base cannot be assumed to be schematic. This is a constant function which points the axiom $A \lor \neg A$ to a fixed closed argument structure for $A \lor \neg A$ obtained by introducing disjunction below a closed argument structure for $A$, where the latter is given. Clearly, we have no guarantee that the closed argument structure thereby obtained has a form that is invariant over all bases, and hence that $\kappa_2$ can be described as a rewriting scheme. Also, we have no information at all about $\mathfrak{J}$, i.e. the justifications sets for the closed argument structure for $A$ (if any). For essentially the same reasons, we may not be able to describe $\Sigma$ in proof of Proposition 6.

Under a suitable description of this notion of schematicity, we may thus modify $|=^*_{\Delta}$ in Definition 16, so as to obtain a further notion of logical consequence.

**Definition 22.** $\Gamma \models^s_{\Delta} A$ iff, there is $\mathcal{D}$ from $\Gamma$ to $A$ such that, for some schematic $\mathfrak{J}$ and every $\mathfrak{B}, \langle \mathcal{D}, \mathfrak{J} \rangle$ is valid on $\mathfrak{B}$.

This somewhat stricter reading may cope with constructivist desiderata. The validity of excluded middle may be no longer provable, even with classical meta-logic.

# 6 Conclusion

Prawitz's original aim was that of developing a constructive semantics which accounted for IL [9]. Investigations into proof-theoretic semantics
There is however a clear sense in which neither Ch, nor $\bigcup_{\mathfrak{B} \in \mathbb{B}} \mathfrak{J}_{\mathfrak{B}}$ or $\bigcup_{\mathfrak{B} \in \mathbb{B}} \Sigma_{\mathfrak{B}}$ can be said to be or to consist of *schematic* justifications, where by schematic we may provisionally mean that the justification can be expressed as a *rule for rewriting argument structures*, similar to the reduction for removing disjunction detours that we have seen at the beginning of Section 2. Ch is obviously not so, since it is not even defined on argument structures only, but on pairs of arguments structures and bases. Even if it is in a sense schematic, it hence differs significantly in spirit from $\phi_\vee$.

On the other hand, $\bigcup_{\mathfrak{B} \in \mathbb{B}} \mathfrak{J}^{\mathfrak{G}}$ contains of course a schematic justification, i.e. $\kappa_1$. But the $\kappa_2$ we take on each base cannot be assumed to be schematic. This is a constant function which points the axiom $A \lor \neg A$ to a fixed closed argument structure for $A \lor \neg A$ obtained by introducing disjunction below a closed argument structure for $A$, where the latter is given. Clearly, we have no guarantee that the closed argument structure thereby obtained has a form that is invariant over all bases, and hence that $\kappa_2$ can be described as a rewriting scheme. Also, we have no information at all about $\mathfrak{J}$, i.e. the justifications sets for the closed argument structure for $A$ (if any). For essentially the same reasons, we may not be able to describe $\Sigma$ in proof of Proposition 6.

Under a suitable description of this notion of schematicity, we may thus modify $|=^*_{\Delta}$ in Definition 16, so as to obtain a further notion of logical consequence.

**Definition 22.** $\Gamma \models_{\Delta}^s A$ iff, there is $\mathcal{D}$ from $\Gamma$ to A such that, for some schematic $\mathfrak{J}$ and every $\mathfrak{B}$, $\langle \mathcal{D}, \mathfrak{J} \rangle$ is valid on $\mathfrak{B}$.

This somewhat stricter reading may cope with constructivist desiderata. The validity of excluded middle may be no longer provable, even with classical meta-logic.

# 6 Conclusion

Prawitz's original aim was that of developing a constructive semantics which accounted for IL [9]. Investigations into proof-theoretic semantics
tics have instead shown that IL is in general *not* complete, or that it
is so only on condition that atomic bases undergo certain constraints
– see [5] for an overview, while more recent findings are [7, 14, 15, 16].
However, these incompleteness (or restricted completeness) results are
normally referred to a Base Semantics approach, where justifications
and proof-structures are dropped out. In some cases, such results
can be adapted to the SVA approach, but this may require under-
standing reductions in a non-schematic way, say, as choice-functions
defined also on bases, or as non-recursive sets of justifications or of
reductions sequences in Schroeder-Heister’s sense. If we require more
schematicity, the adaptation may fail, e.g., even with classical logic in
the meta-language, we may no longer be able to prove the validity of
excluded middle in the object-language. This would speak in favour of
Prawitz’s original semantic project being constructive in two strictly
interrelated ways, namely, not just because SVA is based on a notion
of valid argument (i.e. of proof), but *also* because this notion is given
in terms of reductions which amount to concrete rewriting rules for
proof-structures.

Of course, the question now becomes how schematicity should be
more precisely defined. I will conclude by hinting at two possible
strategies for dealing with this topic.

First, one may consider the possibility of relaxing the notion of
open validity, i.e. an open valid argument 〈*D*, *J*〉 is such that *D* re-
duces to canonical form relative to *J* even when its assumptions *are*
*not* replaced by closed structures which be valid relative to expansions
of *J*. Observe that this *does not hold* in SVA. For example, take the
base given by the rules

$\frac{p}{p} \quad \frac{p}{q}$

and consider the rule

$\frac{r}{q \lor s}$

justified by a $\phi$ such that
tics have instead shown that IL is in general *not* complete, or that it
is so only on condition that atomic bases undergo certain constraints
– see [5] for an overview, while more recent findings are [7, 14, 15, 16].
However, these incompleteness (or restricted completeness) results are
normally referred to a Base Semantics approach, where justifications
and proof-structures are dropped out. In some cases, such results
can be adapted to the SVA approach, but this may require under-
standing reductions in a non-schematic way, say, as choice-functions
defined also on bases, or as non-recursive sets of justifications or of
reductions sequences in Schroeder-Heister’s sense. If we require more
schematicity, the adaptation may fail, e.g., even with classical logic in
the meta-language, we may no longer be able to prove the validity of
excluded middle in the object-language. This would speak in favour of
Prawitz’s original semantic project being constructive in two strictly
interrelated ways, namely, not just because SVA is based on a notion
of valid argument (i.e. of proof), but *also* because this notion is given
in terms of reductions which amount to concrete rewriting rules for
proof-structures.

Of course, the question now becomes how schematicity should be
more precisely defined. I will conclude by hinting at two possible
strategies for dealing with this topic.

First, one may consider the possibility of relaxing the notion of
open validity, i.e. an open valid argument 〈*D*, *J*〉 is such that *D* re-
duces to canonical form relative to *J* even when its assumptions *are*
*not* replaced by closed structures which be valid relative to expansions
of *J*. Observe that this *does not hold* in SVA. For example, take the
base given by the rules

$\frac{p}{p} \quad \frac{p}{q}$

and consider the rule

$$
\frac{r}{q \lor s}
$$

justified by a *ϕ* such that
$$ \frac{\overline{\frac{p}{r}}}{q \lor s} \implies \frac{\overline{\frac{p}{q}}}{q \lor s} (\lor_I) $$

Then, $\langle \mathcal{D}, \phi \rangle$ is valid on our base, where $\mathcal{D}$ is

$$ \frac{p}{q \lor s} $$

It may nonetheless be the case that open structures whose assumptions have some peculiar feature may be computable to canonical form relative to some base-independent justifications, namely, justifications which be schematic in the broad sense understood here. A solution of this kind may come from Pezlar's selector [3] for the Split rule

$$ \frac{A \to B \lor C}{(A \to B) \lor (A \to C)} $$

with A Harrop formula, showing that open proofs of the implicational premise involve sufficient computational content for them to reduce to canonical form under trivial *ad hoc* proofs of the antecedent.

Alternatively, one may put a sort of linearity constraint on justifications, like the one put by Definition 9 on applications of justifications to instances of open structures. We may require the same for the structures which the justification is defined on. If we go back to the reduction for disjunction detours, we see that it consists of a *constant* part, i.e. the order of the formulas on the left- and right-hand side of the arrow, and of a *variable* part, given by variables for argument structures. Let us express this as a linear operation $\lor E$ on typed proof-objects as happens in ToG, and let us indicate with $\text{inj}$ a function for obtaining a proof of $A_1 \lor A_2$ from one of either $A_1$ or $A_2$. Then, the rule enjoys the following linearity condition: for any $f_1^1, f_2^1 : (A_1)B, f_1^2, f_2^2 : (A_2)B$ and $x_1^i, x_2^i : A_i$ ($i = 1, 2$),

$$ \begin{align*} \begin{array}{l} \lor E(\text{inj}(x_1^i)[x_2^i/x_1^i], f_1^1(y_1)[f_2^1/f_1^1], f_1^2(y_2)[f_2^2/f_1^2]) = \\ = (\lor E(\text{inj}(x_1^i), f_1^1(y_1), f_1^2(y_2))) [x_2^i, f_2^1, f_2^2/x_1^i, f_1^1, f_1^2] = \\ = f_1^i(x_1^i)[x_2^i, f_2^1, f_2^2/x_1^i, f_1^1, f_1^2] = f_1^i(x_1^i)[x_2^i, f_2^i/x_1^i, f_1^i]. \end{array} \end{align*} $$
$$ \frac{\overline{\frac{p}{r}}}{q \lor s} \implies \frac{\overline{\frac{p}{q}}}{q \lor s} (\lor_I) $$

Then, $\langle \mathcal{D}, \phi \rangle$ is valid on our base, where $\mathcal{D}$ is

$$ \frac{p}{q \lor s} $$

It may nonetheless be the case that open structures whose assumptions have some peculiar feature may be computable to canonical form relative to some base-independent justifications, namely, justifications which be schematic in the broad sense understood here. A solution of this kind may come from Pezlar's selector [3] for the Split rule

$$ \frac{A \to B \lor C}{(A \to B) \lor (A \to C)} $$

with A Harrop formula, showing that open proofs of the implicational premise involve sufficient computational content for them to reduce to canonical form under trivial *ad hoc* proofs of the antecedent.

Alternatively, one may put a sort of linearity constraint on justifications, like the one put by Definition 9 on applications of justifications to instances of open structures. We may require the same for the structures which the justification is defined on. If we go back to the reduction for disjunction detours, we see that it consists of a *constant* part, i.e. the order of the formulas on the left- and right-hand side of the arrow, and of a *variable* part, given by variables for argument structures. Let us express this as a linear operation $\lor E$ on typed proof-objects as happens in ToG, and let us indicate with **inj** a function for obtaining a proof of $A_1 \lor A_2$ from one of either $A_1$ or $A_2$. Then, the rule enjoys the following linearity condition: for any $f_1^1, f_2^1 : (A_1)B, f_1^2, f_2^2 : (A_2)B$ and $x_1^i, x_2^i : A_i$ ($i = 1, 2$),

$$ \begin{align*} \begin{array}{l} \lor E(\mathbf{inj}(x_1^i)[x_2^i/x_1^i], f_1^1(y_1)[f_2^1/f_1^1], f_1^2(y_2)[f_2^2/f_1^2]) = \\ = (\lor E(\mathbf{inj}(x_1^i), f_1^1(y_1), f_1^2(y_2)))[x_2^i, f_2^1, f_2^2/x_1^i, f_1^1, f_1^2] = \\ = f_1^i(x_1^i)[x_2^i, f_2^1, f_2^2/x_1^i, f_1^1, f_1^2] = f_1^i(x_1^i)[x_2^i, f_2^i/x_1^i, f_1^i]. \end{array} \end{align*} $$
where $y_1 : A_1, y_2 : A_2$, and both are bound by $\forall E$. This may become a definitive condition for justifications, that is, we only allow for justifications $\phi$ such that, for every replacement $\sigma$ of proof-variables in the argument $x$ of $\phi$,

$$ \phi(x^{\sigma}) = (\phi(x))^{\sigma}. $$

## References

[1] Francez, N. (2015). *Proof-theoretic semantics*. London, College Publications.

[2] Gentzen, G. (1935). Untersuchungen über das logische Schließen I, II, *Mathematische Zeitschrift*, 39, 176–210, 405–431.

[3] Pezlar, I. (2023). Constructive Validity of a Generalized Kreisel-Putnam Rule. https://arxiv.org/abs/2311.15376

[4] Piccolomini d’Aragona, A. (2022). *Prawitz’s Epistemic Grounding. An Investigation into the Power of Deduction*. Cham, Springer.

[5] Piecha, T. (2016). Completeness in Proof-Theoretic Semantics. In T. Piecha, P. Schroeder-Heister (eds), *Advances in Proof-Theoretic Semantics*, Cham, Springer, 231–251.

[6] Piecha, T., Schroeder-Heister, P. (2016). Atomic Systems in Proof-Theoretic Semantics: Two Approaches. In J. Redmond, O. Pombo Martin, A. Nepomuceno Fernández (eds), *Epistemology, Knowledge and the Impact of Interaction*, Cham, Springer, 47–62.

[7] Piecha, T., Schroeder-Heister, P. (2019). Incompleteness of Intuitionistic Propositional Logic with respect to Proof-Theoretic Semantics, *Studia Logica*, 107 (1), 233–246.

[8] Prawitz, D. (1965). *Natural Deduction. A Proof-Theoretical Study*. Stockholm, Almqvist & Wiskell.
where $y_1 : A_1, y_2 : A_2$, and both are bound by $\forall E$. This may become a definitive condition for justifications, that is, we only allow for justifications $\phi$ such that, for every replacement $\sigma$ of proof-variables in the argument $x$ of $\phi$,

$$ \phi(x^{\sigma}) = (\phi(x))^{\sigma}. $$

## References

[1] Francez, N. (2015). *Proof-theoretic semantics*. London, College Publications.

[2] Gentzen, G. (1935). Untersuchungen über das logische Schließen I, II, *Mathematische Zeitschrift*, 39, 176–210, 405–431.

[3] Pezlar, I. (2023). Constructive Validity of a Generalized Kreisel-Putnam Rule. https://arxiv.org/abs/2311.15376

[4] Piccolomini d’Aragona, A. (2022). *Prawitz’s Epistemic Grounding. An Investigation into the Power of Deduction*. Cham, Springer.

[5] Piecha, T. (2016). Completeness in Proof-Theoretic Semantics. In T. Piecha, P. Schroeder-Heister (eds), *Advances in Proof-Theoretic Semantics*, Cham, Springer, 231–251.

[6] Piecha, T., Schroeder-Heister, P. (2016). Atomic Systems in Proof-Theoretic Semantics: Two Approaches. In J. Redmond, O. Pombo Martin, A. Nepomuceno Fernández (eds), *Epistemology, Knowledge and the Impact of Interaction*, Cham, Springer, 47–62.

[7] Piecha, T., Schroeder-Heister, P. (2019). Incompleteness of Intuitionistic Propositional Logic with respect to Proof-Theoretic Semantics, *Studia Logica*, 107 (1), 233–246.

[8] Prawitz, D. (1965). *Natural Deduction. A Proof-Theoretical Study*. Stockholm, Almqvist & Wiskell.
[9] Prawitz, D. (1973). Towards a Foundation of a General Proof Theory. In P. Suppes, L. Henkin, A. Joja, Gr. C. Moisil (eds), *Proceedings of the Fourth International Congress for Logic, Methodology and Philosophy of Science*, Bucharest, 1971, Amsterdam, Elsevier, 225-250.

[10] Prawitz, D. (2015). Explaining Deductive Inference. In H. Wansing (ed), *Dag Prawitz on Proofs and Meaning*, Cham, Springer, 65-100.

[11] Sandqvist, T. (2015). Base-Extension Semantics for Intuitionistic Sentential Logic, *Logic Journal of the GPL*, 23 (5), 719-731.

[12] Schreoder-Heister, P. (2006). Validity Concepts in Proof-Theoretic Semantics, *Synthese*, 148, 525-571.

[13] Schroeder-Heister, P. (2018). Proof-theoretic Semantics. In E. N. Zalta (ed), *The Stanford Encyclopedia of Philosophy*.

[14] Schroeder-Heister, P. (2024). Prawitz's Completeness Conjecture: a Reassessment, *Theoria*, forthcoming.

[15] Stafford, W. (2021). Proof-Theoretic Semantics and Inquisitive Logic, *Journal of Philosophical Logic*, 50, 1199-1229.

[16] Stafford, W., Nascimento, V. (2023). Following all the Rules: Intuitionistic Completeness for Generalised Proof-Theoretic Validity, *Analysis*.
[9] Prawitz, D. (1973). Towards a Foundation of a General Proof Theory. In P. Suppes, L. Henkin, A. Joja, Gr. C. Moisil (eds), *Proceedings of the Fourth International Congress for Logic, Methodology and Philosophy of Science*, Bucharest, 1971, Amsterdam, Elsevier, 225-250.

[10] Prawitz, D. (2015). Explaining Deductive Inference. In H. Wansing (ed), *Dag Prawitz on Proofs and Meaning*, Cham, Springer, 65-100.

[11] Sandqvist, T. (2015). Base-Extension Semantics for Intuitionistic Sentential Logic, *Logic Journal of the GPL*, 23 (5), 719-731.

[12] Schreoder-Heister, P. (2006). Validity Concepts in Proof-Theoretic Semantics, *Synthese*, 148, 525-571.

[13] Schroeder-Heister, P. (2018). Proof-theoretic Semantics. In E. N. Zalta (ed), *The Stanford Encyclopedia of Philosophy*.

[14] Schroeder-Heister, P. (2024). Prawitz's Completeness Conjecture: a Reassessment, *Theoria*, forthcoming.

[15] Stafford, W. (2021). Proof-Theoretic Semantics and Inquisitive Logic, *Journal of Philosophical Logic*, 50, 1199-1229.

[16] Stafford, W., Nascimento, V. (2023). Following all the Rules: Intuitionistic Completeness for Generalised Proof-Theoretic Validity, *Analysis*.