On Dummett's Pragmatist Justification Procedure

TL;DR

This paper demonstrates that propositional intuitionistic logic can be fully justified through an adaptation of Dummett's pragmatist procedure, enabling derivations from assumptions based on pragmatic justification.

Contribution

It introduces a novel adaptation of Dummett's pragmatist justification for propositional intuitionistic logic, establishing its completeness.

Findings

Propositional intuitionistic logic is complete with respect to the adapted pragmatist procedure.

A method to derive natural deduction proofs from pragmatist justification is provided.

The approach bridges pragmatic justification and formal proof systems.

Abstract

I show that propositional intuitionistic logic is complete with respect to an adaptation of Dummett's pragmatist justification procedure. In particular, given a pragmatist justification of an argument, I show how to obtain a natural deduction derivation of the conclusion of the argument from, at most, the same assumptions.

Equations

$$\begin{array}[]{p{0.2\textwidth}p{0.2\textwidth}p{0.2\textwidth}p{0.2\textwidth}}$A\to{B}B[A]$&&$B\lx@proof@logical@and AA\to{B}$&\end{array}$$

$$\begin{array}[]{p{0.2\textwidth}p{0.2\textwidth}p{0.2\textwidth}p{0.2\textwidth}}$A\wedge{B}\lx@proof@logical@and AB$&&$AA\wedge{B}$&$BA\wedge{B}$\end{array}$$

$$\begin{array}[]{p{0.2\textwidth}p{0.2\textwidth}p{0.2\textwidth}p{0.2\textwidth}}$A\vee{B}A$&$A\vee{B}B$&$C\lx@proof@logical@and A\vee{B}C[A]C[B]$&\end{array}$$

$$A\perp$$

$$\cdots \text{lx@proof@logical@and}\cdots \text{lx@proof@logical@and}\cdots \cdots \cdots \text{lx@proof@logical@and}\cdots \text{lx@proof@logical@and}\cdots ▽▽\cdots \text{lx@proof@logical@and}\cdots ▽▽$$

$$C\text{lx@proof@logical@and}G,\Gamma \Delta$$

$$AA\wedge B\text{lx@proof@logical@and}G,\Gamma \Delta$$

$$B\text{lx@proof@logical@and}A\to B\text{lx@proof@logical@and}G,\Gamma {\Delta }_{\ast }A$$

$$C\perp \text{lx@proof@logical@and}G,\Gamma \Delta$$

$$C\text{lx@proof@logical@and}A\vee B\text{lx@proof@logical@and}G,\Gamma {\Delta }_{\ast }C\text{lx@proof@logical@and}A\to C[A]C\text{lx@proof@logical@and}B\to C[B]$$

$$C\perp \Gamma ,{\Delta }_{\ast }$$

$$C\lx@proof@logical@and A/B\to{C}\framebox{$A/B\Gamma,\Delta_{*}$}$$

$$C\text{lx@proof@logical@and}\cdots \Gamma ,{\Delta }_{\ast }C\text{lx@proof@logical@and}A/B\to CA/B\Gamma ,{\Delta }_{\ast }C\perp \Gamma ,{\Delta }_{\ast }$$

$$B\text{lx@proof@logical@and}A\to BA\text{lx@proof@logical@and}(A\to B)\to ((C\to C)\to A)A\to B$$

$$B\text{lx@proof@logical@and}A\to BA\text{lx@proof@logical@and}(C\to C)\to A\text{lx@proof@logical@and}(A\to B)\to ((C\to C)\to A)A\to BC\to C[C]$$

$$\perp \text{lx@proof@logical@and}\neg (A\vee \neg A)A\vee \neg A\neg (A\vee \neg A)$$

$$\perp \text{lx@proof@logical@and}\neg (A\vee \neg A)A\vee \neg A\neg A\perp \text{lx@proof@logical@and}\neg (A\vee \neg A)A\vee \neg A{A}^{(1)}$$

$$B\text{lx@proof@logical@and}A\to BA$$

$$C\text{lx@proof@logical@and}A\vee BC\text{lx@proof@logical@and}A\to C[A]C\text{lx@proof@logical@and}B\to C[B]$$

$$(A\to B)\wedge (A\to C)A\to (B\wedge C)$$

$$\begin{array}[]{p{0.6\textwidth}p{0.3\textwidth}}$B\lx@proof@logical@and A\mathbin{\to}B(A\mathbin{\to}B)\mathbin{\wedge}(A\mathbin{\to}C)A\mathbin{\to}(B\mathbin{\wedge}C)A$&$C\lx@proof@logical@and A\mathbin{\to}C(A\mathbin{\to}B)\mathbin{\wedge}(A\mathbin{\to}C)A\mathbin{\to}(B\mathbin{\wedge}C)A$\end{array}$$

$$\begin{array}[]{p{0.6\textwidth}p{0.3\textwidth}}$BB\mathbin{\wedge}C\lx@proof@logical@and A\mathbin{\to}(B\mathbin{\wedge}C)A$&$CB\mathbin{\wedge}C\lx@proof@logical@and A\mathbin{\to}(B\mathbin{\wedge}C)A$\end{array}$$

$$\neg \neg (\neg A\vee B)A\to \neg \neg B$$

$$\perp \text{lx@proof@logical@and}\neg \neg (\neg A\vee B)A\to \neg \neg B\neg (\neg A\vee B)$$

$$\perp \text{lx@proof@logical@and}\neg (\neg A\vee B)\neg A\vee B$$

$$\bot\lx@proof@logical@and\lnot{}(\lnot{A}\mathbin{\vee}B)\framebox{ $\lnot{A}\mathbin{\vee}B\lx@proof@logical@and A\mathbin{\to}\lnot\lnot{B}\lnot{}(\lnot{A}\mathbin{\vee}B)$}$$

$$C\text{lx@proof@logical@and}\neg A\vee B\text{lx@proof@logical@and}A\to \neg \neg B\neg (\neg A\vee B)C\text{lx@proof@logical@and}\neg A\to C[\neg A]C\text{lx@proof@logical@and}B\to C[B]$$

$$C\lx@proof@logical@and\lnot{A}\mathbin{\to}C\framebox{ $\lnot{A}\lx@proof@logical@and A\mathbin{\to}\lnot\lnot{B}\lnot{}(\lnot{A}\mathbin{\vee}B)$}$$

$$\perp \text{lx@proof@logical@and}\neg A\text{lx@proof@logical@and}A\to \neg \neg B\neg (\neg A\vee B)A$$

$$\bot\lx@proof@logical@and\lnot\lnot{B}\lx@proof@logical@and A\mathbin{\to}\lnot\lnot{B}A\framebox{ $\lnot{B}\lnot{}(\lnot{A}\mathbin{\vee}B)$}$$

Full text

Section 1 Introduction

Proof-theoretic definitions of validity can be considered as loosely inspired by Wittgenstein’s ideas relating meaning and use. They attempt to explain of the concept of logical validity in terms of the deductive use of the logical constants, as expressed by inference rules. In this context, Gentzen’s investigations into deduction, particularly his calculus of natural deduction, are often used as a starting point for explaining the meaning of the logical constants on the basis of rules governing their use.

In the standard natural deduction calculus [6, 10], the deductive use of a logical constant is governed by its introduction and elimination rules. Thus, from a semantic perspective where meaning is explained on the basis of use, the introduction and elimination rules express the canonical manner in which a sentence with a logical constant as main operator is used in a deductive argument: the introduction rules express the canonical use of the sentence as a conclusion, the elimination rules express the canonical use of the sentence as an assumption. Along these lines, Dummett [2, 3] proposed that the analysis of the deductive meaning of a logical constant into introduction and elimination rules accounts for two distinct aspects of its use. Roughly speaking, the introduction rules show how to establish a sentence, or to warrant its assertion; they stand for the verificationist aspect. On the other hand, the elimination rules show what consequences can be extracted from a sentence, or what difference accepting it makes to our practice; they stand for the pragmatist aspect.

Accordingly, in a verificationist approach to proof-theoretic semantics, valid arguments are defined on the basis of introductions rules. The main idea is that an argument is valid if, whenever we can obtain the assumptions in a canonical manner, we can also obtain the conclusion in a canonical manner. In a pragmatist approach, on the other hand, valid arguments are defined on the basis of elimination rules. The main idea is that any consequence that can be drawn in a canonical manner from the conclusion can also be drawn in a canonical manner from the assumptions.

Prawitz [11, 16] and Dummett [2, 3] conjectured that proof-theoretic approaches to logical semantics would result in an intuitionistic, or constructive, notion of validity. Due to bias towards the verificationist point of view, proof-theoretic definitions of validity have often been approached via introduction rules [11, 13, 14, 16, 19]. Unfortunately, with respect to their adequacy to intuitionistic logic, verificationist proposals ran into some problems [17, 18, 9, 8, 7].

However, as suggested by some remarks of Gentzen [6], the introduction and elimination rules for a logical constant are harmoniously related, such that one could extract, in some sense, the elimination rules from the introduction rules and vice versa. The harmony between introduction and elimination rules suggests that the elimination rules could just as well provide a basis upon which to develop a proof-theoretic definition of validity.

The pragmatist proof-theoretic approach to validity, the one based on elimination rules, has received comparatively less attention [3, 15, 22]. In this paper, I show that propositional intuitionistic logic is complete with respect to an adaptation of Dummett’s pragmatist proof-theoretic definition of validity. I adapt Dummett’s definitions lightly in order to avoid problems and objections but otherwise stay as closely as possible to the original framework.

Section 2 Preliminaries

This section explains the basic notions and terminology. It also recalls and restates results and definitions that will be needed later.

2.1 Terminology and notation

I borrow most of the terminology from Dummett [3] himself. A noteworthy difference is the use of the term “assumption” in place of Dummett’s term “initial premiss”. I included this subsection in the interest of self-containment, but it can be safely skipped if you are already familiar with the notation and typographical conventions used in natural deduction.

The language.

We consider a propositional language with infinitely many propositional variables (atomic sentences) and the propositional logical constants: $\to$ (implication), $\vee$ (disjunction), $\wedge$ (conjunction) and $\bot$ (absurdity). The complex sentences of the language are formed from atomic sentences by means of composition with the logical constants in the usual way. Latin letters ($A$, $B$, $C$ etc.) are used to stand for arbitrary sentences of the language and Greek letters ($\Gamma$ and $\Delta$) to stand for finite collections of sentences. Subscripts are used whenever it is necessary or convenient. The degree of a sentence is the number of logical constants that occur in it.

Arguments and derivations.

Formally, arguments can be considered as trees of sentence occurrences (designated with $\Pi$, possibly with subscripts). They are constructed from top to bottom, from the leaves to the root, by inferences. These inferences lead from one or more sentences, the premisses, to a single sentence, the consequence. In an argument, each premiss of an inference is either a leaf of the tree or the consequence of a previous inference. Thus, argument trees are formal representations of the process of argumentation, or reasoning, with some leaves acting as assumptions and the root acting as the conclusion of the argument. Any occurrence of a sentence in an argument determine, in the obvious way, a subargument with that sentence as conclusion.111As a limiting case, a single sentence occurrence is an argument with that sentence acting as both assumption and conclusion. A path in an argument is a sequence of sentence occurrences such that each sentence in the path is an immediate inferential consequence of the previous one.222Again, as a limiting case, a single sentence occurrence measures an empty path from that sentence occurrence to itself. Every leaf in an argument is initially an assumption, albeit assumptions can be discharged by inferences.333An axiom or logical theorem $A$ can be considered the result of an inference from leaf $A$ to conclusion $A$ that discards the leaf occurrence of $A$. After an assumption is discharged by an inference, the argument, starting from the consequence of that inference, does not depend any more on the assumption. The discharge of assumptions are indicated using square brackets with numeric indices used to pinpoint the particular inference discharging the assumption. Whenever it is clear from context, the numeric indices are left implicit. I write $\langle\Gamma,A\rangle$ to denote an argument from assumptions $\Gamma$ (those that remained undischarged throughout the argument) to conclusion $A$ without paying attention to the argumentation process that goes from $\Gamma$ to $A$. Also, for the sake of simplicity, I often talk about sentences when I actually mean occurrences of sentences in an argument, and similarly with respect to inference rules and the particular inferences resulting from their application.

Propositional intuitionistic logic is characterised by the standard system of natural deduction [6, 10]. The inference rules for the propositional connectives are symmetrically distributed between introduction (I) and elimination (E) rules.

[TABLE]

[TABLE]

[TABLE]

Negation ($\lnot$) can be defined as usual in terms of implication and absurdity. The rule for the absurdity logical constant $\bot$ can be considered an elimination rule.

[TABLE]

Natural deduction derivations are a particular subclass of arguments in which every inference is in accordance with one of the inference rules above.

2.2 Elimination rules and related notions

In an elimination rule for a logical constant, exactly one premiss of the rule is required to have that constant as main logical operator. This premiss is called the major premiss, and all others, if there are any others, are called minor premisses.

In an elimination rule, a minor premiss is vertical if the same sentence figures as both minor premiss and consequence of the rule, otherwise it is called horizontal. An elimination rule is a vertical rule if at least one of its minor premisses is vertical and it allows the discharge of assumptions in the subarguments for its vertical minor premisses. We can and shall assume that every application of vertical elimination rules do in fact discharge the assumptions as indicated by the rule.444Otherwise, the application of the elimination rule would be superfluous [10, p. 49–50]. This is in line with Dummett [3, p. 283]. Elimination rules which are not vertical are called reductive.

2.3 Normal derivations

This subsection recollects some results and fixes some terminology regarding normal derivations in propositional intuitionistic logic. The results are restated mainly for your convenience and to avoid confusion resulting from conflicting terminology. For detailed proofs, please resort to Prawitz’s monographs [10, 11].

Definition 2.1**.**

A track555The notion of “track” is obviously a slight adaptation of Prawitz’s notion of “path”. Since the term “path” is already reserved for a different concept, the term “track” is used in order to avoid confusion. in an argument $\Pi$ is a sequence of sentence occurrences $A_{1},\cdots{}A_{n}$ such that:

1. (i)

$A_{1}$ is a leaf in $\Pi$ that is not discharged by an application of a vertical elimination rule 2. (ii)

$A_{i}$, for each $i<n$, is not a horizontal minor premiss of an application of an elimination rule, and either (1) $A_{i}$ is not a major premiss of a vertical rule and $A_{i+1}$ is the sentence immediately below $A$, or (2) $A_{i}$ is a major premiss of a vertical rule and $A_{i+1}$ is the assumption discharged by the respective application of the rule 3. (iii)

$A_{n}$ is either a horizontal minor premiss or the conclusion of $\Pi$

As a sequence of occurrences of sentences, a track can also be divided into segments; they conflate repeated consecutive occurrences of the same sentence that arise from applications of vertical elimination rules. If the first sentence in a track is an assumption of the argument, the track is open in the argument, otherwise it is closed.

The tracks in an argument can be assigned an order. The lowest order is assigned to tracks whose last sentence occurrence is the conclusion of the argument; they are called main tracks. The order then increases progressively through horizontal minor premisses. The major premiss of the horizontal rule belongs to a parent track which, of course, can have other children tracks sharing an immediately higher order than their parents. The last sentence occurrence in a track determines a subargument, or subderivation, whose order is the order of the track. The progeny relationship between tracks can be naturally extended to cover them.

Theorem 2.1**.**

Let $\tau$ be a track in a normal intuitionistic derivation and let $\sigma_{1}\cdots\sigma_{n}$ be the corresponding sequence of segments in $\tau$. Then there is a segment $\sigma_{i}$, called the base segment in $\tau$, which separates two (possibly empty) parts of $\tau$, called the analytic part and the synthetic part of $\tau$, such that:

1. (i)

for each $\sigma_{j}$ in the analytic part, $\sigma_{j}$ is a major premiss of an elimination rule and the sentence occurring in $\sigma_{j+1}$ is a subsentence of the one occurring in $\sigma_{j}$ 2. (ii)

the base segment $\sigma_{i}$ is a premiss of an introduction rule or of $\bot$E, provided $i\neq{n}$ 3. (iii)

for each $\sigma_{j}$ in the synthetic part, except the last one, $\sigma_{j}$ is a premiss of an introduction rule and the sentence occurring in $\sigma_{j}$ is a subsentence of the one occurring in $\sigma_{j+1}$

Definition 2.2**.**

The subsentences of a sentence $A$ are classified as positive or negative as follows:

• •

$A$ is a positive subsentence of $A$

• •

if $B\wedge{C}$ or $B\vee{C}$ are positive (resp. negative) subsentences of $A$, then $B$ and $C$ are positive (resp. negative) subsentences of $A$

• •

if $B\to{C}$ is a positive (resp. negative) subsentence of $A$, then $B$ is a negative (resp. positive) subsentence of $A$ and $C$ is a positive (resp. negative) subsentence of $A$

Definition 2.3**.**

A sentence $A$ is an assumption component (resp. conclusion component) of an argument $\langle\Gamma,G\rangle$ when $A$ is a positive (resp. negative) subsentence of some assumption in $\Gamma$, or a negative (resp. positive) subsentence of the conclusion $G$.

The notions defined above can be naturally extended to cover segments, whereby a segment $\sigma_{j}$ is a subsegment of a segment $\sigma_{i}$ if the sentence occurring in $\sigma_{j}$ is a subsentence of the sentence occurring in $\sigma_{i}$.

Theorem 2.2**.**

Let $\sigma_{1}\cdots{\sigma_{n}}$ be a track in a normal derivation of $G$ from $\Gamma$. It holds that:

1. (i)

every segment occurring in the analytic part is an assumption component of $\langle\Gamma,G\rangle$ and subsegment of $\sigma_{1}$ 2. (ii)

the base segment $\sigma_{i}$ is an assumption component of $\langle\Gamma,G\rangle$ and a subsegment of $\sigma_{1}$; also, if different from $\bot$, $\sigma_{i}$ is a conclusion component of $\langle\Gamma,G\rangle$ and a subsegment of $\sigma_{n}$ 3. (iii)

every segment occurring in the synthetic part is a conclusion component of $\langle\Gamma,G\rangle$ and a subsegment of $\sigma_{n}$

2.3 below provides a complexity measure for normal derivations that decreases on the order of the tracks. This complexity measure is later employed in 3.6 and 3.7.

Definition 2.4**.**

A negative assumption (resp. conclusion) component of an argument $\langle\Gamma,G\rangle$ is a negative subsentence of $G$ (resp. some sentence in $\Gamma$). Analogously, a positive conclusion (resp. assumption) component of an argument $\langle\Gamma,G\rangle$ is a positive subsentence of $G$ (resp. some sentence in $\Gamma$).

The negative and positive partitions introduced in 2.4 make out the components in 2.3. The assumption and conclusion components afford a coarse summary of the sentences occurring in the elimination and introduction parts of tracks in a normal derivation on the basis of its assumptions and conclusion. Their partition into negative and positive constituents yields a somewhat finer distinction.

Definition 2.5**.**

A distinctive assumption (resp. conclusion) component of an argument is either a negative assumption (resp. conclusion) component or an assumption (resp. the conclusion).

The distinctive assumption components correspond intuitively to first sentences (leaves) of tracks. They are either assumptions or, possibly, leaves discharged by applications of $\to$I and, consequently, negative subsentences of the conclusion. The negative assumption components represent, in a sense, a potential discharge. Whether an actual leaf was discharged would depend on the particular derivation.

The distinctive conclusion components correspond intuitively to last sentences (roots) of tracks. They include the conclusion of main tracks and, possibly, conclusions of their descendant tracks. More precisely, provided a parent track is open, the conclusion of a child track is a negative subsentence of its assumption.

Definition 2.6** (Dershowitz and Manna [1]).**

The degree of a collection of sentences $\Delta_{j}$ is lower than the degree of a collection of sentences $\Delta_{i}$ ($\Delta_{j}<\Delta_{i}$) if, and only if, $\Delta_{j}$ results from $\Delta_{i}$ by replacing one or more sentences with a finite collection of sentences of lower degree.

Lemma 2.1**.**

In a normal derivation, the degree of the collection of distinctive conclusion components never increases on the order of subderivations. In particular, if a parent track is closed, then the collection of distinctive conclusion components of the child subderivation has lower degree.

Proof.

Consider derivations $\Pi_{i}$ and $\Pi_{j}$, where $\Pi_{j}$ is a child of $\Pi_{i}$. I show that any distinctive conclusion component of $\Pi_{j}$ is either itself a distinctive conclusion component of $\Pi_{i}$, or is replaced in $\Pi_{i}$ with a distinctive conclusion component of higher degree. By 2.5, a distinctive conclusion component of $\Pi_{j}$ is either the conclusion of $\Pi_{j}$ or a negative conclusion component of $\Pi_{j}$. First, consider the negative conclusion components of $\Pi_{j}$. By 2.4, they also belong to the distinctive conclusion components of $\Pi_{i}$, unless the corresponding assumption was discharged. In that case, by 2.1, either ($\to$I) the conclusion of $\Pi_{i}$ has higher degree, or ($\vee$E) it is a negative subsentence of some assumption in $\Pi_{i}$ and, consequently, a negative conclusion component of $\Pi_{i}$. Now consider the conclusion of $\Pi_{j}$. Take a parent track $\tau$ in $\Pi_{i}$. Suppose that $\tau$ is open and $A$ is its assumption. By 2.2, it is a negative subsentence of $A$ and, by 2.5, also a distinctive conclusion component of $\Pi_{i}$. Finally, suppose that $\tau$ is closed and its leaf $A$ was discharged. Then, by 2.1, the conclusion of $\Pi_{i}$ has higher degree than the conclusion of $\Pi_{j}$. ∎

Definition 2.7**.**

Let $\Delta_{\Gamma}$ (resp. $\Delta_{G}$) stand for the collection of distinctive assumption (resp. conclusion) components of a normal derivation from $\Gamma$ to $G$. Consider sequences of subderivations $\langle\Gamma_{0},G_{0}\rangle\cdots\langle\Gamma_{n},G_{n}\rangle$ where each element stands for a child subderivation of the previous one ($\langle\Gamma_{0},G_{0}\rangle$ being the main derivation). The derivations in the sequence are measured for their complexity as follows:

• •

if $\Delta_{G_{j}}<\Delta_{G_{i}}$ then $\langle\Gamma_{j},G_{j}\rangle\prec\langle\Gamma_{i},G_{i}\rangle$

• •

if $\Delta_{G_{j}}=\Delta_{G_{i}}$ then

• –

if $\Delta_{\Gamma_{j}}<\Delta_{\Gamma_{i}}$ then $\langle\Gamma_{j},G_{j}\rangle\prec\langle\Gamma_{i},G_{i}\rangle$

• –

if $\Delta_{\Gamma_{j}}\geq\Delta_{\Gamma_{i}}$ then $\langle\Gamma_{j},G_{j}\rangle\succeq\langle\Gamma_{i},G_{i}\rangle$

Theorem 2.3**.**

For any derivable argument, there is a normal derivation where the complexity decreases on the order of subderivations.

Proof.

I describe a method to shorten normal derivations by removing redundancies (loops). Consider a normal derivation where a subderivation $\Pi_{j}$ has equal or higher complexity than its parent subderivation $\Pi_{i}$. By 2.1, a parent track is open. Let $A_{i}$ be its assumption. Now, there is also an open track in $\Pi_{j}$ where another occurrence $A_{j}$ of the same sentence is an analytic assumption, because otherwise $\Pi_{j}$ would already have lower complexity than $\Pi_{i}$. Let $\Pi_{k}$ be the descendant subderivation for the minor premiss of $A_{j}$. Replace $\Pi_{j}$ with $\Pi_{k}$. Because $\Pi_{j}$ has at least the same complexity as $\Pi_{i}$, any negative assumption components of $\Pi_{j}$ is also a negative assumption component of $\Pi_{i}$. Therefore, any discharge of assumptions of $\Pi_{k}$ can be transferred from $\Pi_{j}$ to $\Pi_{i}$. This shortening process can be iterated until the resulting child of $\Pi_{i}$ has lower complexity. ∎

Section 3 Proof-theoretic validity

The proof-theoretic justification procedures proposed by Dummett [3] consist of definitions of validity for arguments based on canonical inference rules for the logical constants. These inference rules fix the meaning of the logical constants by expressing their canonical deductive use. They are, in Dummett’s terminology, self-justifying.

In contrast with common practice [11, 12, 19, 22], Dummett’s definitions are not based on semantic clauses for particular logical constants. Instead, he assumes that self-justifying rules are given. These self-justifying rules are introduction rules in the context of the verificationist procedure, and elimination rules in the context of the pragmatist procedure. In both procedures, the definitions are stated irrespective of the particular constants or rules provided. Dummett’s approach is thus more general and could, in principle, be applied to any logic.666For technical reasons, the approach would certainly be restricted at the outset to logics with nice proof-theoretic properties (normalisation, subformula property and etc.), however there is no intrinsic technical limitation that confines it to intuitionistic logic or some specific formulation thereof. For our particular case, the self-justifying rules are the standard elimination rules of propositional intuitionistic logic: $\wedge$E, $\to$E, $\vee$E and $\bot$E.

From a pragmatist perspective, a canonical argument start from open (usually complex) assumptions and, through applications of elimination rules, arrive at an atomic conclusion. Dummett also admits basic rules (or boundary rules) to determine deducibility among atomic sentences. In canonical arguments, these basic rules can be applied to an atomic conclusion in order to obtain further atomic consequences.

However, since our main concern is with logical validity, I leave basic rules out of the picture and adapt Dummett’s definitions accordingly, for the sake of simplicity.777Dummett [3, p. 273] explicitly stated the irrelevance of basic rules, or boundary rules, as he called them, to logical validity. Furthermore, by reflection on the pragmatist definition of validity (3.8), it is easy to see that any basic rule in the complementation can be transferred to the valid canonical argument required, thus making no difference to which complex arguments are actually validated. I also adapt the definitions to the propositional case.

Definition 3.1**.**

A sentence occurrence in an argument is principal if every sentence (inclusive) in the path down to the conclusion (exclusive) is a major premiss of an elimination rule.888As a limiting case, in an argument consisting of a single occurrence of a sentence $A$, acting both as assumption and conclusion, $A$ is principal, since the empty path from $A$ to $A$ satisfies the definition.

Definition 3.2**.**

An argument is proper if at least one of its assumptions is principal.

The concept of proper argument is an essential component in the pragmatist notion of validity because proper arguments are built from the principal assumption by application of elimination rules. Arguments that do not follow this pattern are improper. The path from the principal assumption to the conclusion is the principal path.

The notion of canonical argument to be introduced later (3.4) is based primarily on the notion of a proper argument. Even in proper arguments, however, the subargument for minor premisses of elimination rules may depend on auxiliary assumptions that arrive at the conclusion through improper means, i. e., through a path that is not solely composed of major premisses of elimination. These kind of improper subarguments for minor premisses of elimination are called critical subarguments (3.5).

3.1 Canonical arguments and critical subarguments

The following definitions are adapted from Dummett’s original definitions as explained in 3.2. The core ideas, however, are preserved.

Definition 3.3**.**

A sentence occurrence is placid if no sentence down the path to the conclusion is a horizontal minor premiss.

Definition 3.4**.**

A canonical argument has the following properties:

1. (i)

it is proper; 2. (ii)

the subargument for any placid vertical minor premiss of an elimination rule is proper.

Definition 3.5**.**

A critical subargument of a canonical argument is a non-canonical subargument whose conclusion is a horizontal minor premiss of an elimination rule.

In subarguments for minor premisses, the notion of canonicity deals with vertical and horizontal minor premisses differently. The subarguments for vertical minor premisses are considered independent auxiliary arguments and are thus required to be proper themselves. Ideally, the subarguments for horizontal minor premisses would also be proper (and canonical). However, in general, it is not possible to place any restrictions on the form of the subarguments for horizontal minor premisses: when not already canonical, those subarguments are critical, which means that the validity of the whole canonical argument would depend on their validity (3.6).

Remark 3.1*.*

The inference steps in canonical arguments consist primarily of applications of elimination rules: there is a principal path (which is composed of eliminations) and subarguments for minor premisses which are themselves either proper (again with a principal path composed of eliminations) or critical. Thus, a canonical argument has the general form

[TABLE]

where the inference steps are applications of elimination rules except for the critical subarguments (represented with “$\bigtriangledown{}{}$” above), because the definitions impose no restrictions on their inference steps. If we were to ignore the critical subarguments, what remained could be called the proper fraction of the canonical argument and the corresponding sentence occurrences be called proper occurrences. In the proper fraction, in addition to the principal assumption, all other assumptions are principal assumptions of proper subarguments. In the context of canonical arguments, they are called, collectively, proper leaves, or proper assumptions, when undischarged throughout the argument.

Lemma 3.1**.**

The conclusion of a canonical argument is always a subsentence of some assumption, provided there is no proper occurrence of $\bot$.

Proof.

Let $\Pi$ be a canonical argument with no proper occurrence of $\bot$. By 3.4, $\Pi$ is proper and, by 3.2 and 3.1, it has a principal path of major premisses of applications of elimination rules from an assumption to the conclusion. In the principal path, the consequences of applications of $\wedge$E and $\to$E are subsentences of their respective major premisses. The interesting cases are applications of vertical rules ($\vee$E) since they figure a consequence which is not required to be a subsentence of the major premiss. By 3.4, the subarguments for minor premisses of vertical rules are proper. By 3.2 and 3.1, each vertical subargument has a path of eliminations from a proper leaf to the conclusion of the subargument. Now, if the proper leaf of a subargument for a vertical minor premiss was discharged by the corresponding application of $\vee$E, then the conclusion is, by induction hypothesis, a subsentence of its major premiss and hence a subsentence of the principal assumption. Otherwise, if the proper leaf was not discharged, then it is actually a proper assumption of the canonical argument and the conclusion is, by induction hypothesis, a subsentence of this assumption. ∎

Remark 3.2*.*

It would perhaps be useful to make a parallel between the definitions above and concepts familiar from normalisation for intuitionistic natural deduction (2.3). For instance, notice that clause (ii) of 3.4 ensures that the segments in main tracks of canonical arguments are all major premisses of applications of elimination rules (except the last one). In main tracks of canonical arguments, the major premisses of vertical rules are followed by the corresponding discharged assumption, which (if not the last segment in the track) is also a major premiss of an elimination rule. As a result, the first sentence in a main track is a proper assumption and the last sentence (the conclusion of the canonical argument) is a subsentence of this assumption, provided $\bot$ does not occur in the main track. The first sentence in a main track, however, can be distinct from the principal assumption of the canonical argument, because assumptions discharged by vertical rules need not be principal in the proper subargument for a minor premiss. The tracks to whom the principal assumption belongs may be called principal tracks. By 2.1, in normal derivations with empty synthetic parts, the main tracks are all principal tracks and the derivations are, therefore, canonical arguments.

Definition 3.6**.**

A canonical argument is valid if all its critical subarguments are valid and of lower complexity.

Definition 3.7**.**

A complementation of an argument $\langle\Gamma,G\rangle$ is the result of replacing $G$ by a valid canonical argument with the following properties:999Dummett’s original definition has a special clause for when the conclusion $G$ is an atomic sentence. His clause is subsumed here by canonical arguments consisting of a single occurrence of $G$ (3.1).

1. (i)

it has $G$ as principal assumption 2. (ii)

it has an atomic conclusion 3. (iii)

it has at most the same complexity

Definition 3.8**.**

An argument is valid if there is an effective method to transform any complementation of it into a valid canonical argument for the same conclusion from, at most, the same assumptions.

3.6, 3.7 and 3.8 should always be considered together since they define notions in terms of each other. For instance, the notion of valid canonical argument in 3.6 is defined in terms of the notion of valid argument which is itself only defined in 3.8.

The process of complementation consists basically in the application of elimination rules to the conclusion of the argument until we reach an atomic sentence. During complementation, the application of elimination rules figuring minor premisses can introduce auxiliary assumptions. Thus, the valid canonical argument required by 3.8 can depend on additional assumptions introduced by complementation.

Theorem 3.1** (Completeness of Intuitionistic Logic).**

If an argument $\langle\Gamma,G\rangle$ is valid, then there is a natural deduction derivation of $G$ from $\Gamma$ in intuitionistic logic.

Proof.

Suppose $\langle\Gamma,G\rangle$ is valid. By 3.8, for any complementation $\Pi_{c}$, we have a valid canonical argument $\Pi_{v}$ with, at most, the same assumptions and the same conclusion. By 3.7, the complementations are obtained by replacing $G$ with a valid canonical argument that has $G$ as principal assumption. By 3.2, there is a principal path in $\Pi_{c}$ from $G$ to the atomic conclusion $C$ which consists solely of applications of elimination rules. Furthermore, there can be auxiliary assumptions $\Delta$ in the subarguments for minor premisses of elimination rules in the principal path.

[TABLE]

By 3.8, the valid canonical argument $\Pi_{v}$ have $C$ as conclusion and, at most, $\Gamma,\Delta$ as assumptions. We use $\Pi_{v}$ as base and assume that we already have a natural deduction derivation $\Pi_{d}$ for $C$ from $\Gamma,\Delta$ obtained by recursive application of the procedure described here to the critical subarguments of $\Pi_{v}$.101010Recall that a canonical argument is mostly already a natural deduction derivation, except for the critical subarguments (3.1). The termination of the recursive application of the procedure to the critical subarguments of $\Pi_{v}$ is warranted by the complexity restrictions on critical subarguments (3.6). 4.2 illustrates the recursive nature of the definitions. Then, we go through the applications of elimination rules in the principal path and construct, through a process of inversion, a natural deduction derivation of $G$ from $\Gamma$ alone. Starting with $C$, we obtain a natural deduction derivation for each principal sentence in the principal path until we reach $G$ (at which point we would have either discarded or discharged the auxiliary assumptions $\Delta$). Since 3.8 ensures a valid canonical argument $\Pi_{v}$ for any complementation $\Pi_{c}$, we are free to consider those complementations that are more convenient for the construction of our natural deduction derivation. We proceed case by case, where each case shows the derivation of the major premiss on the basis of derivations of the principal sentences that came before (ordered from $C$ to $G$). For the cases of $\vee$E and $\to$E, which introduce auxiliary assumptions, I show how these assumptions can be either discarded ($\vee$E) or discharged ($\to$E). That is, for each occurrence of $\vee$E and $\to$E in the principal path of $\Pi_{c}$, I show how to obtain a derivation from only $\Gamma,\Delta_{*}$, where $\Delta_{*}$ stands for the auxiliary assumptions except those assumptions that are being introduced at that particular inference step. As a result, after going through all sentences in the principal path, we obtain a derivation of $G$ which depends solely on $\Gamma$.

• ($\wedge$E)

Consider complementations by both elimination rules for conjunction

[TABLE]

From the derivations of $A$ and $B$, the conjunction $A\wedge{B}$ is derived by $\wedge$I.

• ($\to$E)

Consider a complementation where the minor premiss $A$ is assumed.

[TABLE]

From a derivation of $B$ from $\Gamma,\Delta$, we apply $\to$I to obtain $A\to{B}$, discharging $A$.

• ($\bot$E)

Consider a complementation where $C$ is an atomic sentence which does not occur as a subsentence in either $\Gamma$ or $\Delta$. As a result, $\bot$E is the last rule applied. I show that $\Pi_{d}$ contain a derivation of $\bot$ which depends, at most, on $\Gamma,\Delta$.

[TABLE]

By 3.2, $\Pi_{d}$ has a principal path from one of the assumptions $\Gamma,\Delta$ to $C$. Since $C$ is not a subsentence of the principal assumption, it could only have been obtained by either $\bot$E or, possibly, a sequence of one or more applications of $\vee$E.111111The cases where there is an application of $\bot$E with a complex consequence containing $C$ and then further eliminations arriving at $C$ are easily subsumed under the case where the corresponding application of $\bot$E has $C$ directly as a consequence. In the first case, we already have a derivation of $\bot$ from $\Gamma,\Delta$. In the second case, by 3.4, the subarguments for vertical premisses of $\vee$E are proper and hence have a principal path to $C$. We work our way up applications of $\vee$E until we reach an application of a reductive elimination rule. The reductive elimination rule in question can only be $\bot$E (3.1). We permute its application down the sequence of applications of $\vee$E and thus obtain a derivation of $\bot$ from, at most, $\Gamma{},\Delta$.

• ($\vee$E)

Consider a complementation of the form below, where $A\to{C}$ and $B\to{C}$ are assumed and $C$ is atomic and does not occur as a subsentence in either $\Gamma$, $A$, $B$ or auxiliary assumptions $\Delta_{*}$ (where $\Delta_{*}$ does not contain $A\to{C}$ and $B\to{C}$).

[TABLE]

In the derivation $\Pi_{d}$, the conclusion $C$ could have been obtained:

1. (a)

by $\bot$E.

[TABLE]

It is easy to derive $A\vee{B}$ instead by the same rule. 2. (b)

by $\to$E from either $A\to{C}$ or, respectively, $B\to{C}$ as principal assumption.

[TABLE]

In either case, we obtain a derivation of $A\vee{B}$ from the subderivation of the horizontal minor premiss by $\vee$I. 3. (c)

by a sequence of one or more applications of $\vee$E.

[TABLE]

We then consider main tracks in $\Pi_{d}$ (3.2) and replace each occurrence of $C$ in the segment by $A\vee{B}$ in accordance with the previous cases (a) and (b).

The resulting derivation of $A\vee{B}$ abstains from assumptions $A\to{C}$ and $B\to{C}$. Any doubts can be dispelled by putting the derivation into normal form (2.1).∎

Theorem 3.2** (Soundness of Intuitionistic Logic).**

If there is a natural deduction derivation of $G$ from $\Gamma$, then the argument $\langle\Gamma,G\rangle$ is valid.

Proof.

Let $\Pi_{d}$ be a normal derivation of $G$ from $\Gamma$. Now, suppose $\Pi_{c}$ is a complementation of $\Pi_{d}$ from $\Gamma{},\Delta$ to conclusion $C$. I show how to obtain a valid canonical argument from $\Gamma{},\Delta$ to $C$. By 3.2, $G$ is the first of a (possibly empty) sequence of major premisses of applications of elimination rules and, by 2.1, the last of a (possibly empty) sequence of immediate premisses of applications of introduction rules. By induction on the degree of $G$, we perform reductions until we obtain a deduction $\Pi_{v}$ of $C$ from $\Gamma{},\Delta$. By 3.2 and induction hypotheses on its critical subarguments, $\Pi_{v}$ is a valid canonical argument for $C$ from $\Gamma{},\Delta$. ∎

3.2 Prawitz’s objection

There are subtle issues involved in the treatment of critical subarguments and Dummett was not able to get his definitions completely right. In particular, problems emerge when we consider a counterexample pointed out by Prawitz [15, endnote 15]:

“The main fault [with Dummett’s definitions] is that in a complementation of an argument, the minor premise of an implication elimination is only assumed. By not considering complementations where the minor premise is the end of an arbitrary argument (which is not possible to do in Dummett’s definition, proceeding as it does by induction over the degree of arguments), the notion of validity becomes too weak. In particular, it cannot be shown that inferences by modus ponens are valid in general, because given two valid arguments $\Pi$ and $\Sigma$ for $A\to{B}$ and $A$, respectively, there is no guarantee that the result $\Delta$ of combining them in a modus ponens to conclude $B$ is valid. For an actual counterexample, we may let $B$ be atomic, $\Pi$ be simply $A\to{B}$, which is a valid argument for $A\to{B}$ from $A\to{B}$, and $\Sigma$ to be a valid argument for a nonatomic $A$ from some hypotheses of higher degree than that of $A\to{B}$. Then $\Delta$ is canonical argument and is its own complementation, but it is not valid ($\Sigma$ being of the same degree as $\Delta$, nor can one find another valid canonical argument for $B$ from the same hypotheses.”

In his reply to Prawitz, Dummett [4] acknowledges the problem. There are actually two different issues brought to light by Prawitz’s counterexample. In the remainder of this section, I discuss these issues and indicate thereby the adaptations that I incorporated into the original definitions in order to avoid them. The adaptations, although elaborate, are fully in agreement with Dummett’s overall philosophical outlook, particularly with respect to the treatment of assumptions.

3.2.1 Canonical atomism

Dummett [3, pp. 284,285] discussed an example closely related to Prawitz’s counterexample.

[TABLE]

Notice that Dummett’s example is basically an instance of Prawitz’s counterexample: both consist of an argument where major premiss $A\to{B}$ stands as an assumption, and where there is a subargument for minor premiss $A$ from assumptions of higher complexity than $A\to{B}$. In Dummett’s discussion, however, the minor premiss $A$ is atomic. This contrasts with Prawitz’s counterexample where $A$ is complex. The difference is important because, according to Dummett’s original definition (which is divided into clauses), a canonical argument, besides being proper (clause iii), must have an atomic conclusion (clause i). Thus, the first problem revealed by Prawitz’s counterexample is that, for complex $A$, there would be, in general, no canonical way to obtain $A$.

However, there is no conceptually compelling reason why canonical arguments must have atomic conclusions. After all, we should be able to obtain also complex sentences in a canonical manner.121212I suspect that Dummett only imposed the requirement of atomic conclusion on canonical arguments in order to simplify the formulation of his definition of complementation which, in general, should require that the principal path be as long as possible in order to afford a complete analysis of the conclusion. In order to avoid this objection, I removed the requirement of atomic conclusion from Dummett’s original definition of canonical argument and adapted the definition of complementation accordingly (clause (iii) of 3.7).

3.2.2 Stringency of the complexity restriction

When discussing his example (1), Dummett was concerned about improper and, therefore, non-canonical subarguments for minor premisses: if these kind of subarguments could have higher complexity than the principal assumption ($A\to{B}$, in this example), the definition of validity would be in danger of circularity. Dummett then presents a transformation that puts the improper subargument into proper form.

[TABLE]

Both arguments depend on the same assumptions but, in contrast with the original example (1), the transformed argument (2) displays a proper subargument for the minor premiss $A$, since there is a principal path from $(A\to{B})\to{((C\to{C})\to{A})}$ to $A$.

Apparently relying on the strength of this particular transformation alone, Dummett then introduces a narrow notion of validity for canonical arguments which restricts improper arguments for minor premisses to those of strictly lower degree, where the degree of an argument is the highest among the degrees of its assumptions and conclusion.

Although the transformation worked for that particular example, it is inadequate in general, at least if Dummett’s notion of degree of an argument is used as complexity measure. Consider, for instance, the following proper argument:

[TABLE]

The degree of the minor subargument is equal to the degree of the principal assumption $\lnot{(A\vee{\lnot{A}})}$. In fact, $\lnot{(A\vee{\lnot{A}})}$ occurs again as an assumption in the minor subargument. The fact that the minor subargument cannot be put into a proper form becomes clear when we replace it by its normal derivation in intuitionistic logic:

[TABLE]

Dummett’s complexity restriction, as originally formulated, is therefore too stringent. The approach suggested by Prawitz [15] and Schroeder-Heister [22] avoids this problem by dealing primarily with closed proofs, where the conclusion provides the adequate complexity measure, since there are no open assumptions. Their approach thus differs unequivocally from Dummett’s, especially with respect to the treatment of assumptions. Dummett’s core approach was maintained through the adoption of an adequate complexity measure (2.7), one that preserves soundness (2.3), instead of his original notion of degree of an argument.

Section 4 A decision procedure

In order to illustrate the definitions and give some intuition about the construction described in the proof of 3.1, it can be useful to work though some examples. The examples are meant to be an overall intuitive illustration of how the proof-theoretic definitions evaluate the validity of arguments. They are presented in the framework of a decision procedure that can be read off from the definitions.

The idea behind 3.8 is roughly that an argument is valid if, whatever we can obtain canonically from the conclusion, could as well be obtained from the assumptions. A procedure to evaluate validity can therefore be divided into two parts:

The complementation process determines what can be obtained from the conclusion.

The search process looks for a way to obtain the same thing from the assumptions.

Both complementation and search can employ only elimination rules — there are no introduction rules available. In line with 3.2, they are based on a similar method (let us call it analysis) of applying elimination rules to a sentence, taken as major premiss, until an atomic sentence is obtained (clause (ii) of 3.7). Thus, in the complementation process, the conclusion of the argument is analysed, in order to see what atomic conclusions can be obtained (possibly under some additional auxiliary assumptions). In the search process, the assumptions are then analysed (one by one), in order to evaluate whether the same atomic conclusions can be obtained.

In the complementation process, the following simplifications are adopted, without loss of generality, with respect to $\vee$E and $\to$E (in agreement with the corresponding cases in the proof of 3.1):

• ($\to$E)

the minor premiss is assumed.

[TABLE]

Here, $A$ is an additional assumption and will be available to search.

• ($\vee$E)

applications are “flattened” with the help of implication.

[TABLE]

In order to maintain generality, $C$ stands for a sentence that does not occur as a subsentence either in the assumptions or the conclusion. Here, $A\mathbin{\to}{C}$ and $B\mathbin{\to}{C}$ are assumed and will be available to search.

• ($\bot$E)

applications are abstained. The search will then target $\bot$. Notice that these simplifications are limited to the complementation process and do not carry over to the search process where, naturally, applications of $\bot$E are not abstained.

Example 4.1*.*

A definition of validity is expected to provide precise criteria for the validity of arguments and, for our definitions in particular, these criteria are supposed to resort to elimination rules only (without assistance from introduction rules). Consider a simple, but not trivial, argument

[TABLE]

and let us evaluate its validity with respect to our definitions.

First, we investigate what can be obtained canonically from the conclusion by means of complementation:

[TABLE]

There are two complementations, with conclusions $B$ and $C$, respectively, and the assumptions $A\mathbin{\to}(B\mathbin{\wedge}C)$ and $A$. In order to establish validity, we must now find canonical arguments from $A\mathbin{\to}(B\mathbin{\wedge}C)$ and $A$ to $B$, and from $A\mathbin{\to}(B\mathbin{\wedge}C)$ and $A$ to $C$.131313The assumptions of the complementations happen to be the same in this example. In the general case, however, they have to be considered separately, e.g.  each complementation has their own assumptions and conclusion. In order to establish validity, we must then show that the conclusion of the complementation can be obtained from the assumptions of the complementation, for every complementation. The search for these canonical arguments can be done mechanically by analysing the assumptions one by one, where some heuristics could be employed to sort out the most promising candidates. In this example, we have few assumptions and don’t need much heuristics to see that $A\mathbin{\to}(B\mathbin{\wedge}C)$ is the best candidate:

[TABLE]

The procedure is thus revealed to be strong enough to validate, not only the introduction rules on the basis of the elimination rules, but also complex arguments whose derivation would require both eliminations and introduction rules.

Example 4.2*.*

Regarded as a decision algorithm, the procedure for evaluation of validity based on elimination rules is not so straightforward and uncomplicated as 4.1 makes it out to be. In the general case, the procedure may involve recursion and backtracking. The search process can deliver candidates with critical subarguments, which would demand a recursive call to evaluate their legitimacy (3.6). If unsuccessful, the process backtracks and tries out the analysis on a different assumption. Consider, for instance, the argument

[TABLE]

The complementation below stops at the conclusion $\bot$, before an application of $\bot$E, in accordance with the aforementioned simplifications to the complementation process.

[TABLE]

The search process has assumptions $A\to{\lnot\lnot{B}}$ and $\lnot{(\lnot{A}\vee{B})}$ to try out in order to obtain $\bot$. For simplicity of exposition, we heuristically select $\lnot{(\lnot{A}\vee{B})}$, but could as well have unsuccessfully tried $A\to{\lnot\lnot{B}}$ out and backtracked here.

[TABLE]

Now, notice that $\lnot{A}\mathbin{\vee}B$ itself is not available among our assumptions. Therefore we presume that $\lnot{A}\mathbin{\vee}B$ can, in fact, be obtained from the assumptions that are available to us, and recall the procedure recursively on the critical subargument enclosed in a box below.141414Notice that $\lnot{}(\lnot{A}\mathbin{\vee}B)$ appears twice: as major premiss and also as an assumption of the critical subargument. This cannot be avoided in general and is related to the problem of contraction in the search for proofs in the sequent calculus [5].

[TABLE]

In the complementation of our recursive call, we again adhere to aforementioned simplifications and use $C$ as the conclusion of $\vee$E since it does not occur anywhere else.

[TABLE]

In order to obtain our foreign $C$, the search must either (1) obtain $\bot$, and thereby $C$, or (2) obtain one of the disjuncts and thereby obtain $C$ from the corresponding assumption, either $\lnot{A}\mathbin{\to}C$ or $B\mathbin{\to}C$, or yet (3) obtain $C$ by $\vee$E from a disjunctive principal sentence, whereby we may use the disjuncts as additional assumptions on the search for proper subarguments for the respective vertical minor premisses. We examine the second option and choose assumption $\lnot{A}\mathbin{\to}C$. The other one may be discarded.

[TABLE]

Our next recursive step reveals an important aspect of the definitions. Consider the next complementation.

[TABLE]

In the candidate (S3) below, if we were to retain all the assumptions available for the next recursive call, that is, if $A\to{\lnot\lnot{B}}$ and $A$ where both passed as assumptions to the critical subargument enclosed in a box, we would be in danger of running into a vicious circle (a loop): after the complementation (C4) below, the candidate (S2) above could have been considered by the search. Indeed, by 2.7, the argument from $\{A\to{\lnot\lnot{B}},A,\lnot{(\lnot{A}\vee{B})}\}$ to $\lnot{B}$ has higher complexity than the critical subargument in (S2), because its conclusion $\lnot{B}$ has the same degree than $\lnot{A}$ and it has $A$ as an additional assumption. Therefore, for the particular case with $A\to{\lnot\lnot{B}}$ as principal assumption, the search must consider only candidates where $A$ or some other assumptions is left out of the critical subargument, on pain of violating the complexity restriction. As it turns out, we do not need $A\to{\lnot\lnot{B}}$ either.

[TABLE]

More recursion.

[TABLE]

We see the complexity restriction at work again in the candidate offered by the search below (notice that $\lnot{}(\lnot{A}\mathbin{\vee}B)$ is left out of the critical subargument).

[TABLE]

I think that the procedure should be clear enough by now for us to omit the last recursive call.

The construction described in 3.1 can be applied to the canonical arguments produced by complementation and search in order to obtain a derivation.

[TABLE]

The derivation contains four tracks. If we order the tracks from one to four and divide them into their analytic and synthetic parts, they correspond roughly to the complementation and search processes of the procedure: (C1), [(C2), (C3)], (C4) and (C5) (omitted) correspond to the synthetic parts of tracks 1, 2, 3 and 4; (S1), (S3) and (S4) correspond to the analytic parts of tracks 1, 2 and 3 (the analytic part of track 4 is empty). The simplifications adopted with respect to $\vee$E in the complementation process resulted in a dedicated recursive step for applications of $\vee$I in the derivation (in track 2, (C2) and (S2); in track 4, (C5) and (S5)). This seems a reasonable exchange against the achieved separation between the processes and deterministic character of the complementation.

Section 5 Discussion

Dummett’s pragmatist justification procedure rejects a widely accepted dogma of proof-theoretic semantics: the primacy of the categorical over the hypothetical or, as it is also called, the placeholder view of assumptions [20, 21]. According to this view, assumptions are placeholders for closed proofs and thus hypothetical reasoning (reasoning from assumptions) are explained in terms of categorical reasoning (proofs without assumptions). In contrast, the pragmatist proof-theoretic notion of canonical argument considers arguments from assumptions as primary and not to be explained away in terms of closed arguments (proofs).

The prevalence of the placeholder view of assumptions has imparted greater emphasis to assertions in detriment of other speech acts like denial or supposition. In contrast, the approach presented in this paper indicate ways to widen the conceptual arena and thus accommodate interesting alternative points of view.

Acknowledgements.

I received very helpful comments and suggestions from members of the research group “Logik und Sprachtheorie” in Tübingen. I am indebted in particular to Peter Schroeder-Heister, who suggested to me the idea of pragmatist canonical arguments with complex conclusions, and to Luca Tranchini, who read and made comments on early drafts. This work was supported by the Deutscher Akademischer Austauschdienst (DAAD), grant number 91562976.