Coarsening Natural Deduction Proofs I: Finding Perfect Proofs

Abstract

1 Introduction

When we formalize an argument and provide a proof to demonstrate its validity, oftentimes redundancies, irrelevancies, and unnecessary detours creep into the proof. For instance, we may not find the simplest or most direct proof. Or we may come up with a proof that contains unnecessary detours in the sense, familiar to proof theorists, of having maximal sentence occurrences.

It can also happen, when formalizing an argument, that the original argument itself contains irrelevancies or is unnecessarily weak. For instance, the argument may have contained irrelevant premises or it may have a weaker conclusion than the premises warranted.

Either of these situations is suboptimal from a logical perspective. While there may be practical reasons to be satisfied with a proof that contains irrelevancies or detours—for instance, because it was the easiest to find and it serves your purposes—the simplest and most direct proof has a distinguished standing from a proof-theoretical point of view. Similarly, there may be rhetorical or dialectical reasons to provide a proof for a weaker argument even when a stronger argument is available, but from a logical point of view we generally want to prove the strongest result possible. We can ask, then, whether it is in general possible to avoid these logically suboptimal situations, and if so how.

This leads to the guiding question of this paper: given a natural deduction proof, is there a way to systematically transform it into a proof that contains no irrelevancies and in which the argument proved to be valid is as strong as possible? In brief, the answer is yes, though it will depend to some extent on whether we are interested in classical or intuitionistic validity and exactly how we define a proof with no irrelevancies. With this guiding question and its intuitive motivation on the table, I turn now to making it precise, so that it admits of a definitive answer.

1.1 Making the Question Precise

In what follows I will use the convention that |$\varPhi ,\varPsi ,...$| are metavariables ranging over sets of formulas, |$\phi ,\psi ,...$| are metavariables ranging over formulas, and |$A,B,...$| are metavariables ranging over atoms.

Instead of arguments, I will talk of sequents. A sequent, as I will understand it here, is an ordered pair |$\varDelta : \varPhi $| of sets of sentences in a given language. Since I will be working in a natural deduction setting, and natural deduction proofs have at most one conclusion, |$\varPhi $| will be at most a singleton. The absurdity symbol |$\bot $| is treated merely as a punctuation device in proofs, not a formula itself; hence a natural deduction proof of |$\bot $| from |$\varDelta $| is really a proof of the zero-conclusion sequent |$\varDelta :\emptyset $|⁠. We say |$\varDelta ^{\prime}:\varPhi ^{\prime}$| is a subsequent of |$\varDelta :\varPhi $| iff |$\varDelta ^{\prime}\subseteq \varDelta $| and |$\varPhi ^{\prime}\subseteq \varPhi $|⁠; if either of these inclusions is proper, then |$\varDelta ^{\prime}:\varPhi ^{\prime}$| is a proper subsequent.

I will be concerned with both classical validity and intuitionistic validity. As usual, |$\varDelta : \varPhi $| is valid when every interpretation that makes every member of |$\varDelta $| true also makes at least one member of |$\varPhi $| true. The difference between classical validity and intuitionistic validity is a matter of what an interpretation is. In the classical case an interpretation can be taken to be a truth-assignment using the familiar truth-tables. In the intuitionistic case, interpretations are given in terms of Kripke models (or something equivalent, such as Heyting algebras). I will assume the reader is familiar with Kripke models for intuitionistic logic and their basic features; see [23, Ch. 2] for a standard reference.

With these preliminary remarks in place, we can now offer a precise definition of what counts as a proof with no irrelevancies or detours. In fact, there are two precisifications of this notion that I will study. The first is based on the idea of perfect validity:

The basic idea is that if any element of the sequent were irrelevant, then it could be omitted without loss. Since no premise or conclusion can be omitted from a perfectly valid sequent without rendering it invalid, no element of the sequent is irrelevant. A perfect proof, then, is a proof of a sequent with no irrelevancies, and moreover it does not contain any detours through subproofs with irrelevancies.

The second way to precisify the idea of a proof with no irrelevancies or detours is based on the notion of gaunt validity. Introducing this requires an auxiliary definition:

A coarsening |$\varDelta ^{\prime}:\varPhi ^{\prime}$| of |$\varDelta :\varPhi $| is trivial just in case the mapping |$\sigma $| that gives |$\sigma \varDelta ^{\prime}=\varDelta $| and |$\sigma \varPhi ^{\prime}=\varPhi $| is a one-one mapping of atoms to atoms. Thus a trivial coarsening is a mere relettering. Note that if |$\sigma $| maps all the atoms in |$\varDelta ^{\prime}$| to other atoms it will be considered non-trivial provided it is not one-one.

The idea behind gaunt validity is to ask not only whether a premise or conclusion is needed for the validity of a sequent, but whether all of the internal logical structure of a premise or conclusion is needed for its validity.

The guiding question of this paper now admits of two precise versions: (1) Can any natural deduction proof be systematically transformed into a perfect proof that is appropriately related to the original proof? (2) Can any natural deduction proof be systematically transformed into a gaunt proof that is appropriately related to the original proof?

1.2 Outine of the Paper and Main Results

In Section 2, I will present the natural deduction systems for core logic and classical core logic, which will be the main tools I use to study perfect and gaunt validity. To a first approximation, classical core logic can be thought of as subtracting ex falso quodlibet from classical logic and adding disjunctive syllogism. This is a way of achieving the minimal revision of classical logic that does not make the so-called Lewis Paradox |$A,\neg A: B$| provable. Core logic bears the analogous relation to intuitionistic logic as classical core logic does to classical logic.

In Section 3, I will elaborate the historical background and conceptual motivation for our key notions of perfect validity and gaunt validity. This will include their relation to the concept of relevance, their connection to core logic and classical core logic, and the relation to the main results proved in this paper.

Sections 4 and 5 contain the technical contributions of this paper. The main result below is that for every proof |$\varPi $| of the sequent |$\varDelta :\varPhi $| in classical core logic or core logic there is respectively a classical core proof or core proof |$\varPi ^{\prime}$| of a perfectly valid sequent |$\varDelta ^{\prime}:\varPhi ^{\prime}$| such that for some uniform substitution |$\sigma $|⁠, |$\sigma \varDelta ^{\prime}$| and |$\sigma \varPhi ^{\prime}$| are trivially equivalent to |$ \varDelta $| and |$\varPhi $|⁠, respectively (in a sense made precise below).

Finally, in Section 6, I remark on the relation of these results to Tennant’s soundness conjecture for core logic.

In the sequel to this paper I will show how, in the case of core logic, by adapting the methods of this paper we can find a proof |$\varPi ^{\prime}$| of a gauntly valid coarsening |$\varDelta ^{\prime}:\varPhi ^{\prime}$| that is similarly related to |$\varDelta :\varPhi $|⁠. This latter result is unique to core logic, as there are gauntly valid sequents in classical logic which do not have gaunt natural deduction proofs.

2 Classical Core Logic

Classical core logic has the following rules of natural deduction. The vertical dots indicate the possible occurrence of further proofwork, and where these are missing it is understood that the node in question must be a leaf-node in the prooftree. In particular, major premises of eliminations (MPEs) are not allowed to have any proofwork above them. Also, vacuous discharge is not allowed in any of the rules: the premises to be discharged must really have been used.

• Here either |$\phi $|⁠, |$\psi $|⁠, or both may occur as premises in the rightmost subproof.

• Here either |$\theta $| or |$\bot $| may occur as the conclusion of each subproof. If one or both subproofs end in |$\theta $|⁠, then the conclusion of the rule is |$\theta $|⁠, and if both subproofs end in |$\bot $|⁠, then the conclusion of the rule is |$\bot $|⁠.

Core logic is the constructive system that results from omitting the rule |$CR$|⁠.

The notion of a subproof will be essential for what follows:

A proof of a sequent |$\varDelta :\phi $| is a proof with conclusion |$\phi $| whose undischarged premises are exactly the members of |$\varDelta $|⁠. A proof of |$\varDelta :\emptyset $| is a proof with conclusion |$\bot $| whose undischarged premises are exactly the members of |$\varDelta $|⁠. Note that, while a sequent is just a formal object which may be valid or invalid, |$\varDelta \vdash \phi $| is an assertion that there is a proof of |$\phi $| whose premises are among |$\varDelta $|⁠.

3 Background

3.1 Perfect Validity

While the notion of perfect validity is of obvious logical interest for any logician, it was first isolated in connection with relevance logic and the problem of analyzing the concept of entailment. The basic idea, as it was originally put by von Wright [25], Geach [6], Smiley [12], and perhaps most clearly enunciated by Geach in [7], was that |$\phi $| entails |$\psi $| if it is possible to come to know |$\psi $| by a deduction from |$\phi $| whose validity did not turn on |$\psi $| being logically true or on |$\phi $| being logically false.³ The definitions of Geach, von Wright, and Smiley only applied to single-premise entailment, but a natural way to generalize this idea to multiple-premise deductions is to add the requirement that in coming to know |$\psi $| by deduction from |$\phi _{1},...,\phi _{n}$| one must use all the |$\phi $|’s. This leads us to the idea of a sequent |$\phi _{1},...,\phi _{n}:\psi $| being valid and having no valid proper subsequents, or in other words, being perfectly valid. Finally, Geach and von Wright were particularly interested in deduction; and since deduction is arguably a formal matter, it should be closed under substitution. Thus, they thought that entailments should also be closed under substitution. Later on, Burgess [5] would coin a term for sequents that are obtained from perfectly valid sequents by substitution:⁴

A different, though related, route to perfect validity is offered by the explication of relevance in [3]. In that paper, I aimed to identify a robust notion of relevance. The goal was not to develop a system of ‘relevance logic’ as an alternative to classical logic, however, but rather to study the notion of relevance in the context of classical logic. The basic idea was that relevance is a relation between sentences and sequents: a sentence is relevant to a sequent if it contributes to the validity of that sequent. I then argued that this standard of relevance is best exemplified by the perfectly valid sequents, since every sentence in the sequent is essential for the validity of the sequent: remove any sentence from a perfectly valid sequent and you are left with an invalid sequent.⁵

Where von Wright, Geach, Smiley, and I arrived at the notion of perfect validity by conceptual analysis or explication, Tennant approaches it from a more top-down methodology. In the early programmatic work [14], he argued that a theory of entailment must account for ordinary deductive reasoning, and in [15] and [16] he developed a proof system that arguably does so. This is an early version of what would he would come to call classical core logic.⁶ Specifically, Tennant argues that all entailments should have normalizable natural deduction proofs, that the entailment relation should be transitive at least when the premises are consistent, and that entailment should be preserved under uniform substitution. On this basis, he defined entailment to be perfectibility: |$\varDelta $| entails |$\phi $| iff |$\varDelta :\phi $| is perfectible. While Tennant has refined his system in various ways over the years, the main properties established in these early works continue to hold for the up to date system of classical core logic. The main properties of (classical) core logic are as follows; the results for classical core logic were established in [15] and the results for core logic were established in [17].

The analogue of Theorem 2 for core logic remains open, however, and is Tennant’s soundness conjecture for core logic:

3.2 Gaunt Validity

The notion of gaunt validity has less history than perfect validity. It was first isolated in print by Tennant in [20, Ch. 11], though it is prefigured in Quine’s Maxim of Shallow Analysis: “expose no more logical structure than seems useful for the deduction or other inquiry at hand.”⁷ Part of Tennant’s motivation derives from the circuitous nature of proofs such as:

Alternatively, we can modify the ideas from [3] to motivate studying gaunt validity. As mentioned above, the core idea in that paper was that relevance meant contributing to the validity of a sequent. That paper was focused on the question of whether a premise is relevant to a sequent, but we can equally ask whether the internal structure of a premise is relevant in the sense of contributing to the validity of a sequent. If a complex formula could just as well be an atom without affecting the validity of a sequent, then the internal logical complexity of that formula does not really contribute anything to the validity of the sequent.⁹ For instance, say |$\phi ,\phi \rightarrow \psi :\psi $| is perfectly valid; then even if |$\phi $| and |$\psi $| are highly complex sentences, their internal complexity is not essential to the validity of this sequent. We could coarsen |$\phi $| and |$\psi $| to atoms, revealing the bare logically necessary structure of this sequent: |$A, A\rightarrow B:B$|⁠. Just as perfectly valid sequents epitomize the ideal of a sequent in which every member contributes something to its validity, gauntly valid sequents epitomize the ideal of a sequent in which every iota of logical structure is needed for its validity.

3.3 Relation to the present work

The results in Section 4 on classical core logic are closely related to the work of [16] (stated as Theorem  2 above). I will improve on that work in a few regards, however. A small difference is that Tennant omitted the connective |$\rightarrow $| from his language, and it was not until [18] that he settled on a particular set of rules for the arrow. I will consider the full language |$\lbrace \neg ,\wedge ,\vee ,\rightarrow \rbrace $| in what follows. More significantly, while Tennant established that every provable sequent is a substitution instance of perfectly valid sequent, I will consider properties not only of provable sequents, but of proofs as wholes, showing that every proof can be coarsened to a perfect proof. Tennant’s approach also turned on his use of a multi-conclusion sequent calculus, while I will focus on natural deduction proofs, limiting us to a single conclusion. (Natural deduction and sequent calculi are each of interest in their own right, so this is a mere difference from [16] rather than an improvement per se.) Finally, and this is the most novel aspect of the current paper, I will build on the results about perfect validity and classical core logic to establish entirely new results in §5 about perfect proofs in core logic. The sequel paper will push these results about core logic even further, showing how core proofs can be transformed into gaunt core proofs.

The present work is thus a contribution to Tennant’s program of studying (classical) core logic. It is also a contribution to the program initiated in [3] of studying perfect validity within the context of classical logic. The provable sequents of classical core logic are a proper subset of the provable sequents of classical logic; but as noted above, whenever |$\varDelta : \varPhi $| is provable in classical logic there is some subsequent |$\varDelta ^{\prime}:\varPhi ^{\prime}$| provable in classical core logic. Hence classical core logic includes every classically perfectly valid sequent, and we can use classical core logic as a tool for studying perfect validity within classical logic.

4 Coarsening Classical Core Proofs

In this section I address the guiding question of this paper as it applies to classical logic, and for this section a proof will refer to a proof in classical core logic unless otherwise stated. The main result will be that a classical core proof of |$\varDelta :\varPhi $| can be transformed into a perfect proof of a sequent |$\varDelta ^{\prime}:\varPhi ^{\prime}$| which is trivially equivalent to |$\varDelta :\varPhi $| in the following sense.

The definition of a c-variant is primarily technical rather than philosophical in nature, being motivated by its usefulness in the proof of Theorem 3. The philosophical significance of c-variants, however, is that a formula is trivially equivalent to its c-variants. Determining whether |$\phi $| and |$\psi $| are c-variants is neither conceptually nor computationally demanding. And although applying the notion of synonymy to logical formulas is notoriously vexed, it would not be absurd to offer being c-variants as a surrogate for synonymy in propositional logic.¹⁰

I begin with a lemma which will be used in proving the main theorem.

Proof.

Induction on the height of |$\varPi $|⁠, defined as the length of the longest branch in |$\varPi $|⁠. In the basis case we have the trivial proof of |$\phi $| from the premise |$\phi $|⁠. Take as |$\varPi ^{\prime}$| the trivial proof of |$A$| from |$A$|⁠, with |$\sigma : A \mapsto \phi $|⁠.

For the induction step, I proceed according to the last rule applied in |$\varPi $|⁠. I will begin with the cases where the last rule is an I-rule.

First, assume the last rule applied in |$\varPi $| is |$\wedge $|I, so |$\varPi $| is of the form:

By i.h. we have perfect proofs:

And we have the two substitutions |$\sigma _{1}$| and |$\sigma _{2}$| such that |$\sigma _{i}\varDelta _{i}^{\prime}=\varDelta _{i}$| and |$\sigma _{1}\psi ^{\prime}$| is a c-variant of |$\psi $| and |$\sigma _{2}\theta ^{\prime}$| is a c-variant of |$\theta $|⁠. Without loss of generality we can assume that |$\varPi _{1}^{\prime}$| and |$\varPi _{2}^{\prime}$| are atom-disjoint, since we can always reletter if need be. Then putting |$\sigma :=\sigma _{1}\cup \sigma _{2}$|⁠, and taking |$\varPi ^{\prime}$| to be the following proof will provide our result.

Second, assume the last rule applied in |$\varPi $| is |$\vee $|I, so |$\varPi $| is:

Then let |$\varPi _{1}^{\prime}$| and |$\sigma _{1}$| be as guaranteed by i.h., and let |$A$| be a new atom not occurring in |$\varPi _{1}$|⁠.¹¹ Letting |$\sigma :=\sigma _{1}\cup \lbrace A \mapsto \theta \rbrace $|⁠, we have |$\varPi ^{\prime}$| as follows.

Third, assume the last rule applied in |$\varPi $| is |$\rightarrow $|I. This can take three forms, giving us three subcases. In the first subcase, we have |$\varPi $| of the form:

By i.h. we have a substitution |$\sigma $| and a perfect proof:

Using the same |$\sigma $|⁠, we form the perfect proof |$\varPi ^{\prime}$| by an application of |$\rightarrow $|I:

Note, however, that there may be multiple occurrences of |$\psi $| in |$\varPi _{1}$| that are discharged in |$\varPi $| by the rule |$\rightarrow $|I. And in the process of coarsening |$\varPi _{1}$|⁠, those occurrences might be coarsened to distinct formulas |$\psi _{1}^{\prime},...,\psi _{n}^{\prime}$|⁠, provided only that |$\sigma (\psi _{1}^{\prime}),...,\sigma (\psi _{n}^{\prime})$| are all c-variants of |$\psi $|⁠. If this is the case, then we add |$n-1$| terminal applications of |$\wedge $|E as follows:

Since |$\sigma (\psi _{1}^{\prime}\wedge ...\wedge \psi _{n})^{\prime}$| is still a c-variant of |$\psi $|⁠, this proof meets our conditions.

The other two subcases are similarly straightforward. The only difference is that when |$\rightarrow $|I is applied by refuting |$\psi ^{\prime}$|⁠, then let the conclusion be |$\psi ^{\prime}\rightarrow A$|⁠, for |$A$| a new atom; and when |$\rightarrow $|I is applied by deriving |$\theta ^{\prime}$| without |$\psi ^{\prime}$|⁠, then let the conclusion be |$A\rightarrow \theta ^{\prime}$|⁠.

Fourth, assume the last rule applied in |$\varPi $| is |$\neg $|I. This case is straightforward. The only complication is that, as in the case of |$\rightarrow $|I, the discharged premise |$\psi $| may have been coarsened to several distinct formulas |$\psi _{1}^{\prime},...,\psi _{n}^{\prime}$|⁠. If so, then we repeat the trick from |$\rightarrow $|I of adding |$n-1$| applications of |$\wedge $|E at the end of the proof |$\varPi ^{\prime}$|⁠.

This completes the cases with I-rules. Next, we turn to E-rules. First, assume the last rule applied is |$\wedge $|E, so |$\varPi $| has the following form, with at least one of |$\psi $| and |$\theta $| occurring as premises in the main subproof:

By the i.h. we have some |$\sigma $| and the following perfect proof:

If both |$\psi ^{\prime}$| and |$\theta ^{\prime}$| occur as premises in this proof, then our desired proof |$\varPi ^{\prime}$| is formed by the obvious application of |$\wedge $|E. On the other hand, suppose that |$\psi ^{\prime}$| but not |$\theta ^{\prime}$| is used as a premise in |$\varPi _{1}$|⁠. Then, letting |$A$| be a new atom, we have our proof |$\varPi ^{\prime}$| as follows.

Since we are discharging |$\psi ^{\prime}$| (and also |$\theta ^{\prime}$|⁠, if applicable), we have to consider the possibility that in coarsening |$\varPi _{1}$| to obtain |$\varPi _{1}^{\prime}$|⁠, |$\psi $| was split into several different coarsenings |$\psi _{1}^{\prime},...,\psi _{n}^{\prime}$|⁠. If so, then add instances of |$\wedge $|E to the bottom of |$\varPi _{1}^{\prime}$| as necessary to obtain:

Second, assume the last rule applied is |$\vee $|E, so |$\varPi $| has the form:

By i.h. we have the two perfect proofs, with their corresponding substitutions |$\sigma _{1}$| and |$\sigma _{2}$|⁠:

And we can assume that |$\varPi _{1}^{\prime}$| and |$\varPi _{2}^{\prime}$| are atom-disjoint. As expected we set |$\sigma :=\sigma _{1}\cup \sigma _{2}$|⁠. In either of these proofs |$\varPi _{1}^{\prime}$| and |$\varPi _{2}^{\prime}$|⁠, if |$\psi $| or |$\theta $| have been coarsened to distinct formulas |$\psi _{i}^{\prime}$| or |$\theta _{i}^{\prime}$|⁠, then again use the trick of adding |$\wedge $|E to the bottom of |$\varPi _{1}^{\prime}$| or |$\varPi _{2}^{\prime}$| as necessary. If one or both of these proofs has |$\bot $| as the conclusion, then we can obtain our desired proof |$\varPi ^{\prime}$| by the obvious application of |$\vee $|E with |$\varPi _{1}^{\prime}$| and |$\varPi _{2}^{\prime}$| as subproofs. On the other hand, if neither |$\varPi _{1}^{\prime}$| nor |$\varPi _{2}^{\prime}$| have |$\bot $| as a conclusion, then we take the following proof for |$\varPi ^{\prime}$|⁠.

Now |$\sigma (\chi _{1}^{\prime}\vee \chi _{2}^{\prime})=\sigma _{1}(\chi _{1}^{\prime})\vee \sigma _{2}(\chi _{2}^{\prime})=\chi \vee \chi $|⁠, which is a c-variant of |$\chi $|⁠, as required.

Third, assume the last rule applied is |$\rightarrow $|E, so |$\varPi $| has the following form:

By i.h. we have the two perfect proofs, and again we can ensure that they are atom-disjoint:

If |$\theta $| has been coarsened to distinct formulas |$\theta _{i}^{\prime}$|⁠, add steps of |$\wedge $|E to the end of |$\varPi _{2}^{\prime}$|⁠. Now we apply the obvious instance of |$\rightarrow $|-E to obtain a proof of |$\varDelta ^{\prime},\psi ^{\prime}\rightarrow \theta ^{\prime}:\chi ^{\prime}$|⁠. Note that |$\sigma \psi ^{\prime}$| may be a c-variant of |$\psi $|⁠, and that |$\sigma \theta ^{\prime}$| may also be a c-variant of |$\theta $|⁠.

Fourth, assume the last rule applied is |$\neg $|E, so |$\varPi $| has the form:

By i.h. we have the perfect proof:

Note again that |$\sigma \psi ^{\prime}$| might be a c-variant of |$\psi $|⁠. Since |$\varDelta ^{\prime}:\psi ^{\prime}$| is perfectly valid, it follows that |$\varDelta ^{\prime},\neg \psi ^{\prime}:\emptyset $| is also perfectly valid. This is because if there were a valid proper subsequent of the form |$\varDelta _{1}^{\prime},\neg \psi :\emptyset $| or |$\varDelta _{1}^{\prime}:\emptyset $| (with |$\neg \psi \notin \varDelta _{1}^{\prime}$|⁠), then we would have the respective valid sequents |$\varDelta _{1}^{\prime}:\psi $| or |$\varDelta _{1}^{\prime}:\emptyset $|⁠, contradicting the perfect validity of |$\varDelta ^{\prime}:\psi $|⁠. This allows us to form the desired perfect proof |$\varPi $|⁠:

This completes the cases with E-rules. The final case for our induction is when the last rule applied is |$CR$|⁠, so that |$\varPi $| is of the form:

By the i.h. we have a substitution |$\sigma $| and perfect proof of the following form:

In this case the i.h. guarantees that |$\sigma \theta =\neg \psi $|⁠, but it is not immediate that |$\theta $| is of the form |$\neg (\psi ^{\prime})$|⁠. Since we know that |$\neg \psi $| is a substitution instance of |$\theta $|⁠, however, we know that either |$\theta $| is of the form |$\neg (\psi ^{\prime})$| or |$\theta $| is an atom |$A$|⁠. And in the latter case Lemma  1 guarantees that we can substitute |$\neg A$| for |$A$| in |$\varPi _{1}^{\prime}$| and then apply |$CR$| to the result to obtain our desired perfect proof |$\varPi ^{\prime}$| of |$\varDelta ^{\prime}:\psi ^{\prime}$|⁠.

It is also possible, however, that there are multiple instances of the premise |$\neg \psi $| which have been coarsened to distinct formulas |$\psi _{1}^{\prime},...,\psi _{n}^{\prime}$|⁠. In that case, we append a series of |$\vee $|I rules and |$n$| instances of |$CR$| as follows.

Now we can apply an instance of |$CR$| discharging |$\neg (\psi _{1}^{\prime}\vee ...\vee \psi _{n}^{\prime})$|⁠, giving us a proof of |$\psi _{1}^{\prime}\vee ...\vee \psi _{n}^{\prime}$|⁠, which is a c-variant of our original formula |$\psi $|⁠.

Example 4

Let us look at three simple examples of classical core proofs and the perfect proofs that result from applying the coarsening procedure of Theorem 3.

1. Our first example will be the following proof of |$\theta \vee \psi , \psi \rightarrow \theta , \neg \theta :\theta $|  

The process of coarsening this proof will leave the structure of the tree as is, merely replacing the formulas with atoms. Note that the occurrence of |$\theta $| in the main disjunction gets coarsened to a different atom than the occurrence in |$\psi \rightarrow \theta $|⁠:

2. Our second example will be somewhat more complicated. Consider the following proof of the sequent |$\emptyset :(\phi \vee \psi )\rightarrow (\psi \vee \phi )$|⁠.

The coarsening procedure applied to this proof will result in the following proof of the sequent |$\emptyset :(A\vee B)\rightarrow [(C\vee A) \vee (B\vee D)]$|⁠.

In outline, here is how we reach this coarsened proof. We begin at the tops of each of the two main subproofs. We coarsen |$\phi $| to |$A$| and |$\psi $| to |$B$|⁠. Then when we move down to the instance of |$\vee $|I that immediately follows |$A$|⁠, we replace the newly introduced disjunct |$\psi $| with a new atom |$C$|⁠; and similarly at the instance of |$\vee $|I following |$B$| we replace the newly introduced disjunct |$\phi $| with a new atom |$D$|⁠. Then at the subsequent occurrence of |$\vee $|E, the two main subproofs have different conclusions. So, as prescribed by the coarsening procedure for |$\vee $|E in the proof of Theorem 3, we insert an instance of |$\vee $|I so that the two subproofs have the same conclusion, namely |$(C\vee A) \vee (B\vee D)$|⁠. Finally, we apply the terminal application of |$\rightarrow $|I.

Now the substitution that maps |$A\mapsto \phi $|⁠, |$D\mapsto \phi $|⁠, |$B\mapsto \psi $|⁠, and |$C\mapsto \psi $| will give the substitution instance |$(\phi \vee \psi ) \rightarrow [(\psi \vee \phi ) \vee (\psi \vee \phi )]$|⁠, which is a c-variant of |$(\phi \vee \psi )\rightarrow (\psi \vee \phi )$|⁠.

(3) Our third example will involve |$CR$|⁠. Suppose we are given the proof:

In the coarsening process, the two MPEs |$\neg (A\vee \neg A)$| will get coarsened to distinct formulas, so we have to use the trick of inserting |$\vee $|I rules and we will end up with a proper coarsening of the original sequent |$\emptyset :A\vee \neg A$|⁠. What we get as a result of the coarsening process is:

This concludes our three examples.

One of the interesting consequences of Theorem 3 concerns a slight extension of our natural deduction system for classical core logic. Begin with classical core logic in what is sometimes called a ‘sequent natural deduction’ formulation. The inference rules are exactly the same, with the only difference being that instead of writing a single formula at each node of the prooftree we write a sequent where the left-hand side lists all the premises undischarged at that node of the proof.¹² Thus, for instance, if we have a proof of |$\phi $| relying on open assumptions |$\varDelta $| and a proof of |$\psi $| relying on open assumptions |$\varGamma $|⁠, then in an application of |$\wedge $|I we would write:

This theorem can be pithily summarized as showing that every perfectly valid sequent can be derived without a detour through imperfection. Now, applying a uniform substitution obviously will not in general preserve perfect validity, so the deductive system |$D$| will not prove only perfectly valid sequents. However, in this deductive system, every perfectly valid sequent will have some perfect proof.

5 Perfect Core Proofs

I now want to address the guiding question of this paper to intuitionistic logic. Applying the ideas from above to core logic, I will show how every core proof be transformed into a perfect proof. For this section and the next, unless otherwise stated, a proof will mean a core proof, and validity will mean intuitionistic validity (which is in turn understood in terms of Kripke models).

The aim is to adapt Theorem 3 to show how core proofs can be coarsened into perfect proofs. I begin with a lemma that addresses the difficulties noted in Remark  1.

Proof.

Induction on height of |$\varPi $|⁠. In the basis case, |$\varPi $| is the trivial proof of |$\phi :\phi $|⁠. Moreover, by assumption, |$\phi $| must be an atom |$A$|⁠, and clearly |$A,\neg A:\emptyset $| is perfectly valid.

For the induction step, first consider cases where the last rule applied in |$\varPi $| is an E-rule. It cannot be an application of |$\neg $|E, since we have a proof of |$\phi $|⁠, not |$\bot $|⁠.

Next consider the case of |$\vee $|E. Suppose this application of |$\vee $|E is the uniform conclusion version; the other versions can be treated similarly. Then |$\varPi $| is of the form:

By i.h. |$\varDelta _{1},\psi ,\neg (\phi _{l}\vee \phi _{r}):\emptyset $| and |$\varDelta _{2},\theta ,\neg (\phi _{l}\vee \phi _{r}):\emptyset $| are both perfectly valid.

It will follow that |$\varDelta _{1},\varDelta _{2},\psi \vee \theta ,\neg (\phi _{l}\vee \phi _{r}):\emptyset $| is perfectly valid, too. The basic idea is that, since |$\varDelta _{1},\psi ,\phi _{l}$| and |$\varDelta _{2},\theta ,\phi _{r}$| are atom-disjoint, for any proper subsequent of |$\varDelta _{1},\varDelta _{2},\psi \vee \theta ,\neg (\phi _{l}\vee \phi _{r}):\emptyset $| we can create a countermodel by piecing together countermodels for the corresponding proper subsequents of |$\varDelta _{1},\psi ,\neg \phi _{l}:\emptyset $| and |$\varDelta _{2},\theta ,\neg \phi _{r}:\emptyset $|⁠. In more detail, suppose we have a proper subsequent

$$ \begin{align*} &\varDelta_1^{\prime},\varDelta_2^{\prime}, [\psi\vee\theta], [\neg(\phi_l\vee\phi_r)]:\emptyset,\end{align*}$$

where the brackets indicate that |$\psi \vee \theta $| and |$ \neg (\phi _{l}\vee \phi _{r})$| may or may not occur in this sequent. Now we want to show that this sequent has a countermodel, that is, a Kripke model |$M$| where |$\varDelta _{1}^{\prime},\varDelta _{2}^{\prime}, \psi \vee \theta , \neg (\phi _{l}\vee \phi _{r})$| are all true at the root node. Suppose |$\varDelta _{1}^{\prime}\subset \varDelta _{1}$|⁠. Then we know there is a model |$M_{1}$| where |$\varDelta _{1}^{\prime},\psi , \neg (\phi _{l}\vee \phi _{r})$| are true at the root node, because |$\varDelta _{1},\psi ,\neg (\phi _{l}\vee \phi _{r}):\emptyset $| is perfectly valid. Similarly, we can find a model |$M_{2}$| where |$\varDelta _{2}^{\prime},\neg (\phi _{l}\vee \phi _{r})$| are true at the root node. By the assumption that |$\varDelta _{1},\psi ,\phi _{l}$| and |$\varDelta _{2},\theta ,\phi _{r}$| are atom-disjoint, we can merge these two models into a single model |$M$|⁠, and the result is our desired countermodel in which |$\varDelta _{1}^{\prime},\varDelta _{2}^{\prime}, \psi \vee \theta , \neg (\phi _{l}\vee \phi _{r})$| are all true at the root node. The argument is similar for the possibilities where |$\varDelta _{2}^{\prime}\subset \varDelta _{2}$| or where |$\psi \vee \theta $| or |$\neg (\phi _{l}\vee \phi _{r})$| do not occur in the subsequent in question.

The other cases of E-rules follow similarly by appeal to the induction hypothesis and the condition on main subproofs being atom-disjoint.

Now assume the last rule applied in |$\varPi $| is an I-rule. First, suppose it is |$\wedge $|I, so |$\varPi $| has the form:

By i.h. |$\varDelta _{1},\neg \psi :\emptyset $| and |$\varDelta _{2},\neg \theta :\emptyset $| are perfectly valid. By assumption, |$\varDelta _{1},\psi $| and |$\varDelta _{2},\theta $| are atom-disjoint. Similar to the case of |$\vee $|E above, these two conditions entail that |$\varDelta _{1},\varDelta _{2},\neg \psi \vee \neg \theta :\emptyset $| is perfectly valid. Now suppose for reductio that some subsequent |$\varDelta _{1}^{\prime},\varDelta _{2}^{\prime},\neg (\psi \wedge \theta ):\emptyset $| were perfectly valid. Since |$\neg \psi \vee \neg \theta \vdash \neg (\psi \wedge \theta )$|⁠, it would follow that |$\varDelta _{1}^{\prime},\varDelta _{2}^{\prime},\neg \psi \vee \neg \theta :\emptyset $| is valid, contradicting the perfect validity of |$\varDelta _{1},\varDelta _{2},\neg \psi \vee \neg \theta :\emptyset $|⁠.

Next, assume the last rule applied in |$\varPi $| is |$\vee $|I. Then by i.h. we have a perfectly valid sequent |$\varDelta :\psi $|⁠, and a formula |$\theta $| with entirely new atoms, so |$\varDelta :\psi \vee \theta $| is perfectly valid. Now if some subsequent of |$\varDelta , \neg (\psi \vee \theta ):\emptyset $| were valid, then we could find some subsequent of |$\varDelta ,\neg \psi ,\neg \theta :\emptyset $| that were valid. Since |$\theta $| shares no atoms with |$\varDelta ,\neg \psi $| and is not a tautology, it could be omitted from this valid sequent without loss. So if there were a perfectly valid proper subsequent of |$\varDelta ,\neg \psi ,\neg \theta :\emptyset $|⁠, then |$\neg \theta $| would not be in this sequent. Then we would in fact have a valid proper subsequent of |$\varDelta ,\neg \psi :\emptyset $|⁠, which is impossible.

Next, assume the last rule applied in |$\varPi $| is |$\rightarrow $|I. Begin by assuming that the first form of |$\rightarrow $|I is used, so |$\psi $| is used in a derivation of |$\theta $| and discharged. Since |$\varPi $| is perfect, |$\varDelta :\psi \rightarrow \theta $| is perfectly valid, and by i.h. |$\varDelta ,\psi ,\neg \theta :\emptyset $| is perfectly valid. Now |$\psi \wedge \neg \theta \vdash \neg (\psi \rightarrow \theta )$|⁠, so if a proper subsequent |$\varDelta ^{\prime},\neg (\psi \rightarrow \theta ):\emptyset $| were valid then |$\varDelta ^{\prime},\psi ,\neg \theta :\emptyset $| would be valid too, but that is impossible.

Consider the second form of |$\rightarrow $|I, where |$\psi \rightarrow \theta $| is inferred from a refutation of |$\psi $|⁠. Since |$\varPi $| is perfect, |$\varDelta ,\psi :\emptyset $| is perfectly valid. Thus any proper subset of |$\varDelta ,\psi $| is satisfiable. By assumption, |$\theta $| consists of atoms not occurring elsewhere in |$\varPi $|⁠, and so any subset of |$\varDelta ,\psi ,\neg \theta $| is satisfiable whenever the corresponding subset of |$\varDelta ,\psi $| is. Thus every proper subset of |$\varDelta ,\psi \wedge \neg \theta $| is satisfiable, and hence |$\varDelta ,\neg (\psi \rightarrow \theta ):\emptyset $| is perfectly valid. The third form of |$\rightarrow $|-I is treated similarly.

The final case concerns when the last rule applied in |$\varPi $| is |$\neg $|I. So |$\varPi $| is a perfect proof of |$\varDelta :\neg \phi $|⁠. It follows that |$\varDelta ,\neg \neg \phi :\emptyset $| is also perfectly valid.

This theorem does not show that every core-provable sequent is perfectible, so it does not resolve Tennant’s Soundness Conjecture 1. It does, however, show that every core-provable sequent is trivially equivalent to a perfectible sequent.

6 The Soundness of Core Logic

Given Tennant’s definition of entailment as perfectibility, showing that every sequent provable in core logic is perfectible amounts to showing that core logic is sound for this definition of entailment. This was the Soundness Conjecture 1. Milne [8] offered a counterexample to this conjecture, noting that |$A,B,A\vee B:A\wedge B$| is provable in core logic, but is not perfectible. Milne acknowledges, however, that this counterexample depends essentially on treating sequents as having at most one conclusion. If we allow multiple-conclusion sequents, then |$A,B,A\vee B: A \wedge B$| is a substitution instance of the intuitionistically perfectly valid sequent |$C,D, A\vee B: A\wedge D, C\wedge B$|⁠.

It is true that in Gentzen’s original formulation of the sequent calculi, the intuitionistic system LJ was obtained from the classical system LK by restricting the conclusion set to having at most one member. But this is not an essential restriction, and there exist multiple-conclusion sequent calculi for intuitionistic logic.¹³ Similar to the classical case, multiple conclusions are given a disjunctive reading: |$\varDelta :\phi _{1},...,\phi _{n}$| is valid just in case |$\varDelta :\bigvee _{i} \phi _{i}$| is valid. Recognizing that Gentzen’s restriction to single-conclusion sequents was a technical trick rather than an essential feature of intuitionistic logic, the soundness question for core logic could be posed in terms of multiple-conclusion sequents. Milne even suggested that Tennant’s soundness conjecture might hold when posed in these terms.¹⁴

In the natural deduction setting that I have been working in, we do not have multiple conclusions. But we can still capture the same insight by rephrasing the soundness conjecture to state: if there is a core proof of |$\varDelta :\phi $|⁠, then there is an intuitionistically perfectly valid sequent |$\varDelta _{0}:\phi _{1},...,\phi _{n}$| and a substitution |$\sigma $| such that |$\sigma \varDelta _{0}=\varDelta $| and |$\sigma \phi _{1}=...=\sigma \phi _{n}=\phi $|⁠. While this claim does not follow from what I have proved here, there is a sense in which Theorem  5 is intimately related to this soundness claim.

If a multiple-conclusion sequent |$\varDelta :\varPhi $| is perfectly valid, and has a single-conclusion substitution instance |$\varDelta ^{\prime}:\phi $| under the substitution |$\sigma $|⁠, this is because |$\sigma $| maps every member of |$\varPhi $| to the same formula |$\phi $|⁠. This effect turns on treating sequents as pairs of sets of formulas rather than pairs of multisets of formulas. If sequents are pairs of multisets, then to get from |$\sigma \varDelta :\sigma \varPhi $| to |$\varDelta ^{\prime}:\phi $| would require finitely many applications of the contraction rule. Analogously, if |$\varDelta _{0}:\phi _{1},...,\phi _{n}$| is perfectly valid, and we have a natural deduction proof of |$\varDelta _{0}:\phi _{1}\vee ...\vee \phi _{n}$|⁠, then applying the substitution |$\sigma $| will give us a natural deduction proof of |$\varDelta :\phi \vee ...\vee \phi $|⁠. ‘Contracting’ this terminal self-disjunction would be the equivalent in the natural deduction setting of applying the structural rule of contraction in the multiset sequent setting.

Theorem 5 gives us a similar way to obtain a core-provable sequent from a perfectible sequent by contracting self-disjunctions and self-conjunctions. That theorem requires a slightly more liberal understanding of what counts as the natural deduction analogue of the structural rule of contraction in the sequent calculus. The structural rule of contraction allows us to eliminate duplicate occurrences of premises or conclusions from a sequent. The straightforward analogy would be to regard |$\varDelta ,\psi :\phi $| and |$\varDelta , \psi \wedge \psi :\phi $| or |$\varDelta ,\psi :\phi \vee \phi $| as equivalent from the standpoint of natural deduction.¹⁵ In other words, I am suggesting that if every core provable sequent could be obtained from a perfectible sequent by contracting outermost self-conjunctions in the premise set and contracting outermost self-disjunctions in the conclusion, that could naturally be seen as providing a positive solution to the soundness problem for core logic.

What Theorem 5 shows, on the other hand, is that every core provable sequent can be obtained from a perfectible sequent by contracting not-necessarily-outermost self-conjunctions and self-disjunctions in both the premises and the conclusion. The relation to the soundness question is clear and suggestive. But we do not have a direct answer to the soundness question per se.

7 Conclusion

This paper began with the guiding question of whether, given a natural deduction proof, there is a way to systematically transform it into a proof that contains no irrelevancies and which in which the argument proved to be valid is as strong as possible. I offered two different definitions of when a proof contains no irrelevancies: the first is when we have a perfect proof and the second is when we have a gaunt proof. I dealt with perfect proofs in this paper and the sequel paper deals with gaunt proofs.

In order to transform an arbitrary core or classical core proof into a perfect proof, I developed the idea of working top-down through a proof to gradually coarsen it into a perfect proof. This method of coarsening is based on four essential ideas:

1. Leaf nodes that are not MPEs can be coarsened to atoms, and this coarsening is then propagated down the prooftree.

2. When an inference such as |$\vee $|I introduces a new formula that does appear previously in the proof, that (sub)formula can be coarsened to an atom.

3. When a rule such as |$\rightarrow $|E or |$\wedge $|I has parallel subproofs, those subproofs can be relettered to be atom-disjoint.

4. When we reach an E-rule |$R$| that discharges multiple instances of a formula |$\phi $|⁠, if those instances have been coarsened to distinct formulas |$\phi _{1}^{\prime},...,\phi _{n}^{\prime}$|⁠, then we interpolate |$n$| instances of |$\wedge $|E, so that in the coarsened proof we have rule |$R$| discharging |$\phi _{1}^{\prime}\wedge ...\wedge \phi _{n}^{\prime}$|⁠; or, if |$R$| is an instance of |$CR$|⁠, we interpolate |$n$|  |$\vee $|I’s to discharge |$\neg (\phi _{1}^{\prime}\vee ...\vee \phi _{n}^{\prime})$|⁠.

By implementing these four ideas, we saw that a core or classical core proof of |$\varDelta :\varPhi $| can always be coarsened to a perfect proof of |$\varDelta ^{\prime}:\varPhi ^{\prime}$|⁠, where |$\varDelta ^{\prime}:\varPhi ^{\prime}$| is coarsening of a c-variant of |$\varDelta :\varPhi $|⁠. In the case of core proofs, as I explained, this result is closely related to Tennant’s Soundness Conjecture  1 for core logic; while it does not solve the conjecture, perhaps it is not unreasonable to describe it as a partial solution.

Funding

This work was partly supported by an Early Career Scheme grant from the Research Grants Council of Hong Kong SAR, China, project number 23606822.

Acknowledgements

Thanks are due to Neil Tennant for sharing his unpublished work on gaunt validity, and to Pierre Saint-Germier, Neil Tennant, Pilar Torrés Villalonga, Peter Verdée, and especially several anonymous referees for comments that greatly improved the exposition of this paper.

Footnotes

References