Coarsening natural deduction proofs II: finding gaunt proofs

Abstract

This paper is the second part of a series exploring how, given a proof, we can inductively transform it into a proof that contains no irrelevancies and is as strong as possible. In the prequel paper, I defined a weaker and a stronger notion of what counts as a proof with no irrelevancies, calling them perfect proofs and gaunt proofs, respectively. There, I showed how proofs in core logic and classical core logic can be transformed into perfect proofs. In this paper I study gaunt proofs. I show how proofs in core logic can be inductively transformed into gaunt core proofs, but that this property fails for the natural deduction system of classical core logic.

Issue Section:

Articles

1 Introduction

This paper and its prequel, [2], address this guiding question: 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? I introduced two precisifications of when an argument is as strong as possible, each with an associated definition of a proof that contains no irrelevancies, calling them respectively perfectly valid sequents and perfect proofs, and gauntly valid sequents and gaunt proofs. The prequel paper showed how any classical or constructive proof can be inductively transformed into a perfect proof by a method I called coarsening of proofs. In this paper I will adapt the method of coarsening to show how a constructive proof can be transformed into a gaunt proof. I show by example, however, that this feature does not hold of classical logic, as there are classically valid sequents with no gauntly valid natural deduction proofs.

I will present and discuss the key definitions below, but for more thorough background, including references and precedents, I refer the reader to the prequel paper.

2 Preliminaries

I present the key technical definitions and discuss their philosophical motivation before presenting the rules of core logic, which I use as the tool for studying intuitionistic natural deductions.

2.1 Technical definitions

In what follows I will use the convention that $Φ, Ψ, . . .$ are metavariables ranging over sets of formulas, $ϕ, ψ, . . .$ are metavariables ranging over formulas, and $A, B, . . .$ are metavariables ranging over atoms.

A sequent, as I will understand it here, is an ordered pair $Δ : Φ$ 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, $Φ$ will be at most a singleton. The absurdity symbol $⊥$ is treated merely as a punctuation device in proofs, not a formula itself; hence, a natural deduction proof of $⊥$ from $Δ$ is really a proof of the zero-conclusion sequent $Δ : \emptyset$ ⁠. We say $Δ^{'} : Φ^{'}$ is a subsequent of $Δ : Φ$ iff $Δ^{'} \subseteq Δ$ and $Φ^{'} \subseteq Φ$ ⁠; if either of these inclusions is proper, then $Δ^{'} : Φ^{'}$ is a proper subsequent.

I will be primarily concerned with intuitionistic validity. As usual, $Δ : Φ$ is valid if every Kripke model that makes every member of $Δ$ true at every world also makes at least one member of $Φ$ true at every world.

Let us now recall the two definitions of what counts as a proof with no irrelevancies or detours.

Definition 1

(Perfect validity; perfect proofs).

A sequent $Δ : Φ$ is perfectly valid iff it is valid but has no proper subsequent that is valid. A proof $Π$ is a perfect proof iff every subproof, including $Π$ itself, is a proof of a perfectly valid sequent.

The second way to precisify the idea of a proof with no irrelevancies or detours is based on the notion of gaunt validity, which in turn requires an auxiliary definition:

Definition 2

(Coarsening).

A sequent $Δ^{'} : Φ^{'}$ is a coarsening of $Δ : Φ$ iff there is a uniform substitution $σ$ (that is, a mapping from atoms to formulas) such that $σ (Δ^{'}) = Δ$ and $σ (Φ^{'}) = Φ$ ⁠.

A coarsening $Δ^{'} : Φ^{'}$ of $Δ : Φ$ is trivial just in case the mapping $σ$ that gives $σ Δ^{'} = Δ$ and $σ Φ^{'} = Φ$ is a one-one mapping of atoms to atoms. Thus, a trivial coarsening is a mere relettering. Note that if $σ$ maps all the atoms in $Δ^{'}$ to other atoms it will be considered non-trivial provided it is not one-one.

Definition 3

(Gaunt validity, gaunt proofs).

A sequent $Δ : Φ$ is gauntly valid iff it is perfectly valid and has no non-trivial coarsening that is perfectly valid. A proof $Π$ is a gaunt proof iff every subproof, including $Π$ itself, is a proof of a gauntly valid sequent.

Remark 1

One might wonder whether the definition of gaunt validity could be simplified so as to require only that $Δ : Φ$ be perfectly valid and have no non-trivial coarsening that is valid (not necessarily perfectly valid).¹ This alternative definition will not do, however, as it would trivialize the notion. If $δ_{1}, . . ., δ_{n} : ϕ / ⊥$ is perfectly valid and $A$ is a new atom, then $δ_{1}, . . ., δ_{n}, A : ϕ / ⊥$ is a valid proper coarsening of the original sequent, as witnessed by the substitution $σ : A \mapsto δ_{n}$ ⁠.

The last technical definition we need is that of a c-variant:

Definition 4

(c-variant).

A formula $ϕ_{c}$ is a contraction-variant of $ϕ$ (or c-variant, for short) iff $ϕ$ can be obtained from $ϕ_{c}$ by successively replacing occurrences of $ψ \lor ψ$ with $ψ$ or replacing occurrences of $ψ \land ψ$ with $ψ$ ⁠.

Example 1

The following are each c-variants of $A \to B$ ⁠:

$A \to (B \lor B)$
$(A \to B) \lor (A \to (B \land B))$
$((A \land A) \to B) \land (A \to B)$ ⁠.

Note that being a c-variant is a transitive relation. Moreover, if

ϕ_{c}

is a c-variant of

ϕ

then

\neg ϕ_{c}

is a c-variant of

\neg ϕ

⁠, and

ϕ_{c} \circ ψ

is a c-variant of

ϕ \circ ψ

⁠, and

ψ \circ ϕ_{c}

is a c-variant of

ψ \circ ϕ

⁠, where

\circ

is any of the binary connectives.

The motivation for the notion of a c-variant is technical rather than philosophical in nature. Despite this, the definition is not devoid of all philosophical significance, since a formula is trivially equivalent to its c-variants, and c-variance could be offered as a reasonable explication of synonymy in propositional logic.

2.2 Philosophical remarks

As mentioned at the beginning, the guiding question behind this paper and its prequel is whether it is possible, given a natural deduction proof, to transform that proof into one which is as strong as possible and which contains no irrelevancies. A natural way to understand relevance in formal logic is based on the idea that a constituent of a sequent is relevant when it contributes something to the validity of that sequent.² This leads to perfect validity and gaunt validity as formal explications of relevance. A perfectly valid sequent is one in which each premise/conclusion not only contributes something to the validity of the sequent, but indeed is essential for the validity of the sequent. The concept of gaunt validity presents itself when we ask not only whether a premise/conclusion contributes to the validity of a sequent, but also whether the internal syntactic structure of a premise/conclusion contributes to the validity of the sequent. For instance, take the sequent $A \land B : A \land B$ ⁠. On the one hand, each premise/conclusion is necessary for this sequent to valid—delete either the premise or conclusion, and the result would be an invalid sequent. On the other hand, the internal syntactic complexity of the premise and conclusion is irrelevant to the validity of the sequent. We could just as well have regarded this as an instance of the valid sequent $C : C$ ⁠. A gauntly valid sequent captures the ideal of relevance insofar as each premise/conclusion and their internal syntactic structure is essential for the validity of the sequent in question.

Given these two formal explications of relevance, then, it is simple to define a proof that contains no irrelevancies. If we work with the explication of relevance as perfect validity, then a proof with no irrelevancies should be a proof that takes no detours through imperfection: every sequent proved as part of the overall proof should be perfectly valid. In other words, every subproof should be a proof of a perfectly valid sequent. Likewise, if we work with the explication of relevance as gaunt validity, then a proof with no irrelevancies should be a proof in which every sequent proved along the way is gauntly valid. Hence, the definitions of perfect proof and gaunt proof.

The resulting definitions of perfect proof and gaunt proof, however, end up being hybrid semantic-syntactic notions, turning as they do on both the syntactic definition of proofhood and the semantic definition of perfect validity. And for gaunt proofs the situation is doubly hybrid. The definition of gaunt validity itself is a hybrid syntactic-semantic notion, involving both the syntactic concept of a coarsening and semantic concept of validity; and then the definition of gaunt proof turns on the syntactic definition of proofhood and the syntactic-semantic hybrid notion of gaunt validity.

Given the overall proof-theoretic orientation, one might wonder why the key concepts need to be given in hybrid syntactic-semantic terms. Wouldn’t it be more natural and elegant to provide a proof-theoretic criterion for a proof with no irrelevancies?³ We could call them syntactically-perfect proofs and syntactically-gaunt proofs, say; and then we could try to prove standard soundness and completeness results of the form: every perfectly valid sequent has a syntactically-perfect proof, and every syntactically-perfect proof is a proof of a perfectly valid sequent (and mutatis mutandis for gaunt in place of perfect). Why not take this route?

This alternate route certainly has some attractions from a proof-theoretic point of view, and it has the potential to yield fruitful results. We can even interpret the results of [2] through this lens. The coarsening of proofs, as applied in that paper, turned on four basic ideas:

Leaf nodes that are not MPEs can be restricted to be atoms.
When an inference such as $\lor$ I introduces a new formula that does appear previously in the proof, that (sub)formula can be coarsened to an atom.
When a rule such as $\to$ E or $\land$ I has parallel subproofs, those subproofs can be relettered to be atom-disjoint.
Aside from CR, every rule that discharges formulas can be restricted to discharging a single instance of each formula.

The method of coarsening involved inductively working downward through a proof-tree to transform an arbitrary (classical) core proof into a (classical) core proof satisfying these conditions, with certain tightly constrained exceptions. (For instance, in the uniform-conclusion version of $\lor$ E, we interpolated a step of $\lor$ I that does not conform with condition 2 as just stated.) But the exceptions are all made precise and the essential point remains that we have a syntactic characterization of proofs that suffices for their being perfect proofs.

So there are two potential methodologies before us. On the first hand, we could begin with a syntactic property of natural deductions and then prove that such deductions are all and only the perfect/gaunt proofs. On the second hand, we can begin with the hybrid semantic-syntactic properties of being a perfect proof or a gaunt proof and then find a method of transforming arbitrary natural deductions into perfect/gaunt proofs. The way that we were able to coarsen proofs in the prequel can be fairly naturally seen as falling under either approach, while the proof-transformational work in the present paper falls more clearly under the second methodology rather than the first.⁴ But irrespective of which methodology we adopt, the definitions of gaunt proof and perfect proof are well-motivated and retain their conceptual significance.

This becomes especially apparent when we consider the first-order case, because no decidable syntactic condition can winnow the proofs down to exactly the perfect proofs.

Proposition 1

Let $L$ be either classical or intuitionistic first-order logic. Then there is no decidable property $P$ such that an $L$ -proof $Π$ has $P$ iff $Π$ is a proof of a perfectly valid sequent.

Proof.

Note that if there were such a property $P$ ⁠, then the perfectly valid sequents of $L$ would be computably enumerable (c.e.). For any formula $ϕ$ ⁠, and $A$ an atom not occurring in $ϕ$ ⁠, the sequent $ϕ : ϕ \lor A$ is perfectly valid iff $ϕ$ is satisfiable. So if the perfectly valid sequents are c.e., then satisfiability is c.e. But since unsatisfiability is also c.e., this contradicts the undecidability of $L$ ⁠.

(It is natural to expect that this result carries over also to gaunt validity. The proof given here, however, does not apply to gaunt validity, since

ϕ : ϕ \lor A

is gauntly valid only if

ϕ

is an atom

B

⁠. For now, the analogous claim about gaunt validity remains a conjecture.)

The decidability of perfect validity in propositional logic allows for the possibility of giving a purely syntactic condition on proofs that coincides with perfect proofhood. But the impossibility of doing so for first-order logic assures us that perfect proofhood (and presumably also gaunt proofhood) cannot be conceptually reduced to a purely syntactic form. We are unavoidably left with the hybrid semantic-syntactic notions of perfect proofhood and gaunt proofhood given above.

2.3 Core logic

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 $ϕ$ ⁠, $ψ$ ⁠, or both may occur as premises in the rightmost subproof.
Here either $θ$ or $⊥$ may occur as the conclusion of each subproof. If one or both subproofs end in $θ$ ⁠, then the conclusion of the rule is $θ$ ⁠, and if both subproofs end in $⊥$ ⁠, then the conclusion of the rule is $⊥$ ⁠.

To obtain classical core logic, we add the rule of classical reductio:

By a straightforward induction on the length of proof, one can establish that core logic has the subformula property.

Theorem 1

If $Π$ is a proof of $Δ : Φ$ in core logic, then every formula occurring in $Π$ is a subformula of some member of $Δ, Φ$ ⁠.

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

Definition 5

(Subproof).

If $Π$ is a prooftree and $n$ is a node in $Π$ ⁠, the subtree of $Π$ above $n$ is a subproof of $Π$ iff $n$ is not a major premise of an elimination (MPE).

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

The use of core logic to study intuitionistic validities is legitimated by the following theorem of Tennant’s.

Theorem 2

If, intuitionistically, $Δ ⊢ Φ$ ⁠, then for some subsets $Δ_{0} \subseteq Δ$ and $Φ_{0} \subseteq Φ$ ⁠, there is a core proof of $Δ_{0} : Φ_{0}$ ⁠. Moreover, there is an algorithm for extracting a core proof of $Δ_{0} : Φ_{0}$ from an intuitionistic proof of $Δ : Φ$ ⁠.

(For a comprehensive survey of core logic, including a proof of this theorem, see [5].) This theorem also entails that every intuitionistically perfectly valid sequent, and hence every intuitionistically gauntly valid sequent, is core provable. Thus, every step in a perfect or gaunt proof will be acceptable by the lights of the core logician. In that sense, perfect or gaunt proofs of intuitionistic validities must themselves be core proofs, whether or not they are explicitly presented in the natural deduction system for core logic. In this paper I do work explicitly in the natural deduction system for core logic.

3 Challenges to Finding Gaunt Coarsenings

As we saw in the prequel, the method of coarsening proofs turns on four simple ideas. First, any leaf node that is not an MPE can be coarsened to an atom, and from there we work our way downward through the proof.

Second, any time a new (sub)formula gets introduced, which does not appear previously in the proof, it can be coarsened to a new atom. For instance, suppose we take a proof $Π$ ⁠:

If we apply the coarsening down through

Π_{0}

to obtain a proof

Π^{'}

Δ^{'} : ϕ^{'}

⁠, then at the step of

\lor

I, we coarsen

ψ

to an atom

B

that does not occur elsewhere in the proof, giving us a the coarsened proof

Π^{'}

Δ^{'} : ϕ^{'} \lor B

⁠.

Third, any parallel subproofs can be relettered to be atom-disjoint. This relettering is then propagated to the conclusion and/or MPE of the rule. For instance, say we have an instance of $\to$ E:

If we have coarsened

Π_{1}

and

Π_{2}

so they are respectively proofs of

Δ^{'} : ϕ^{'}

and

Δ_{2}^{'}, ψ^{'} : θ^{'}

⁠, and we have ensured that these proofs are atom-disjoint, then propagating this coarsening through the

\to

E gives us:

In the prequel, there was one exception to the general rule that parallel subproofs be atom-disjoint, which concerned uniform-conclusion applications of

\lor

E. In that case, if we started with a proof:

Then coarsening

Π_{1}

and

Π_{2}

would give us two atom disjoint proofs of

Δ_{1}^{'}, ϕ^{'} : θ_{1}^{'}

and

Δ_{2}^{'}, ψ^{'} : θ_{2}^{'}

⁠, but where

θ_{1}^{'}

and

θ_{2}^{'}

are distinct because of the assumption of atom-disjointness. In order to apply

\lor

E, then, we would insert a step of

\lor

The result is now a proof of a coarsened c-variant of

θ

⁠.

The fourth and final idea is based on the observation that, when we begin with a proof $Π$ and apply these coarsening procedures downwards from the leaf nodes, we may reach an E-rule that discharges multiple occurrences of $ϕ$ in $Π$ ⁠, but where those occurrences $ϕ$ have now been coarsened to distinct formulas $ϕ_{1}, . . . ., ϕ_{n}$ ⁠. When this arose, we appended $n$ instances of $\land$ E, so that we had a proof with one undischarged assumption $ϕ_{1} \land . . . \land ϕ_{n}$ rather than $n$ distinct undischarged premises $ϕ_{1}, . . ., ϕ_{n}$ ⁠. Then the E-rule in question can be applied discharging the conjunction $ϕ_{1} \land . . . \land ϕ_{n}$ ⁠. For instance, suppose we started with a proof of the form:

In the coarsening procedure, the two instances of

ξ

will get coarsened to distinct formulas

ξ_{1}^{'}

and

ξ_{2}^{'}

⁠, so we cannot discharge them both with the instance of

\land

E on

ξ \land ζ

⁠. In that case, we inserted a new instance of

\land

E as follows (step (ii)):

The result is a proof with the coarsened c-variant

(ξ_{1}^{'} \land ξ_{2}^{'}) \land ζ^{'}

as a premise in place of the original premise

ξ \land ζ

⁠.

These four ideas sufficed to ensure that the coarsening procedures yielded perfect proofs. Several obstacles arise, however, when we try to adapt the method of coarsening to yield gaunt proofs. There are four problems we need to confront. In the remainder of this section I will present the problems and indicate their solutions. Then in the next section I will rigorously present the coarsening procedures that incorporate those solutions and that suffice for finding gaunt proofs.

3.1 Disjunction elimination

The first problem comes from the uniform-conclusion version of $\lor$ E. As we saw above, if an instance of $\lor$ E has two subproofs of $Δ_{1}, ϕ : θ$ and $Δ_{2}, ψ : θ$ ⁠, then these will get coarsened to $Δ_{1}^{'}, ϕ^{'} : θ_{1}^{'}$ and $Δ_{2}^{'}, ψ^{'} : θ_{2}^{'}$ ⁠. Then we inserted an instance of $\lor$ I to obtain proofs of $Δ_{1}^{'}, ϕ^{'} : θ_{1}^{'} \lor θ_{2}^{'}$ and $Δ_{2}^{'}, ψ^{'} : θ_{1}^{'} \lor θ_{2}^{'}$ ⁠. But unless $θ_{2}^{'}$ is a new atom, $Δ_{1}^{'}, ϕ^{'} : θ_{1}^{'} \lor θ_{2}^{'}$ will not be gauntly valid (and likewise for righthand subproof). Thus, the coarsening procedure that sufficed for finding perfect proofs will not suffice for finding gaunt proofs.

The resolution of this problem is simple. We can add a new version of $\lor$ E to the rules of core logic:

Obviously, adding this rule is a trivial modification of the proof system and does not change the logic. Moreover, we can assume that this rule only appears in coarsened proofs; so that when we start with a proof

Π

that we want to coarsen,

Π

does not contain this modified

\lor

rule. Now in coarsening core proofs that have an application of uniform conclusion

\lor

E, we can apply this modified form of

\lor

3.2 Conjunction elimination

Here, the fundamental problem stems from a simple observation:

Proposition 2

If $Δ, ϕ, ψ : Φ$ is gauntly valid, then $Δ, ϕ \land ψ : Φ$ is not gauntly valid.

Proof.

If $Δ, ϕ, ψ : Φ$ is gauntly valid, then $Δ, ϕ \land ψ : Φ$ is obviously valid—and indeed perfectly valid—but it has the perfectly valid proper coarsening $Δ, ϕ \land A, B \land ψ : Φ$ ⁠, where $A$ and $B$ are new atoms.

This problem manifests in two different ways. The first is when a proof has an instance of $\land$ E where both the conjuncts occur as premises in the subproof to be discharged. This is easy to accommodate, however, by including two separate instances of $\land$ -E to discharge the two separate premises.

The second way this problem manifests is when originally a rule $R$ discharged multiple occurrences of the same premise $ξ$ ⁠, but those different occurrences have been coarsened to distinct formulas $ξ_{1}^{'}, . . ., ξ_{n}^{'}$ in the coarsening procedure. As described above, the method for dealing with this was to intercalate $n - 1$ steps of $\land$ E, discharging each $ξ_{i}^{'}$ and resulting in a new premise $ξ_{1}^{'} \land . . . \land ξ_{n}^{'}$ that may be discharged by the rule $R$ ⁠. The problem, of course, is that those instances of $\land$ E will not preserve gauntness. To resolve this problem, we will again need to add generalized versions of the rules of core logic. Specifically, we want to add modified versions of $\neg$ I, $\to$ I, and $\lor$ E, each of which is roughly dual to the modified version of $\lor$ E introduced above.

The modified $\neg$ I will be:⁵

Analogously, the modified

\to

I will be:

And the final modified version of

\lor

E will be:

It is again obvious that this amounts to a trivial modification of the proof system and does not change the logic. As with the modified

\lor

E rule above, we can assume that these modified rules do not appear in the original proofs to which we apply the coarsening procedures.

Remark 2

In the remainder of this paper, unless otherwise explicitly stated, we will be working with proofs in core logic supplemented with the generalized versions of $\lor$ E, $\neg$ I, and $\to$ I just provided. In particular, the coarsening procedures detailed below will never take us outside the space of core proofs.

3.3 Negation rules

When we were only aiming to find perfect proofs, the treatment of negation was trivial. Given a proof with a negation rule in it, it sufficed to take the main subproof, coarsen it, and then apply the same negation rule. But while the negation rules preserved perfect validity, there is no guarantee that they preserve gaunt validity. For instance, $\neg \neg \neg A : \neg A$ is gauntly valid; but an instance of $\neg$ E would give a proof of $\neg \neg \neg A, \neg \neg A : \emptyset$ ⁠, which has the valid proper coarsening $\neg B, B : \emptyset$ ⁠. Conversely, $\neg B, B : \emptyset$ is gauntly valid, but an instance of $\neg$ I would give a proof of $\neg B : \neg B$ ⁠, which has the gauntly valid coarsening $C : C$ ⁠.

Addressing this problem will not require any new rules. As I will explain in the next section (and prove in the sections after that), we can give an analysis of exactly when the negation rules fail to preserve gauntness. This analysis will then also provide a coarsening procedure that applies when the negation rules do not preserve gauntness.

3.4 Circuitous E- and I-rules

The final problem arises from the way that E-rules and I-rules can be combined to create circuitous proofs such as the following two examples (note that the example on the left uses our new, generalized version of $\lor$ E):

This also will not require any new rules, but will simply require some care in how the coarsening procedures are defined. I turn now to that task.

4 Coarsening Procedure for Gaunt Proofs

In this section I present the coarsening procedures which will yield gaunt proofs. As before, in order to coarsen a proof $Π$ we begin at the leaf nodes that are not MPEs, coarsening each such formula to an atom $A$ ⁠, and successively work our way down the proof tree. The remaining steps then show how to inductively coarsen subsequent steps in $Π$ ⁠. The main theorem will then follow by an inductive argument checking that each of these operations preserves gaunt validity.

In that inductive argument, I will often appeal to the following fact without mention.

Proposition 3

If $ϕ^{'}$ is a coarsening of $ϕ$ ⁠, then either $ϕ^{'}$ is an atom, or $ϕ^{'}$ and $ϕ$ have the same main connective.

Several other facts will also be useful.

Proposition 4

If $Δ ⊢ A$ ⁠, then either $Δ ⊢ ⊥$ or $A$ has some occurrence in $Δ$ that is not in the scope of a negation or in the antecedent of a conditional.

Proof.

By induction on the length of proof in core logic, we can show that there is a core proof of $Δ : A$ only if $A$ has some occurrence in $Δ$ that is not in the scope of a negation or the antecedent of a conditional. The basis step of this induction is straightforward. For the induction step, we know that the last rule applied cannot be $\neg$ E or an I-rule, because $A$ is an atom. This leaves only $\land$ E, $\lor$ E, and $\to$ E; each of these cases follows easily from the i.h.

Now by Theorem 2, we know that if $Δ$ is consistent and $Δ ⊢ A$ ⁠, then for some $Δ_{0} \subseteq Δ$ there is a core proof of $Δ_{0} : A$ ⁠.

Proposition 5

If $Δ, ψ \circ B : ϕ$ is perfectly valid, where $\circ$ is any binary connective and $B$ is an atom not occurring elsewhere in the sequent, then a coarsening $Δ^{'}, (ψ \circ B)^{'} : ϕ^{'}$ can be valid only if it is of the form $Δ^{'}, ψ^{'} \circ B : ϕ^{'}$ ⁠. Likewise for a perfectly valid sequent $Δ : ϕ \circ B$ ⁠.

Proof.

Given a perfectly valid sequent $Δ, ψ \circ B : ϕ$ as in the proposition, suppose that $Δ^{'}, (ψ \circ B)^{'} : ϕ^{'}$ is a valid coarsening under the substitution $σ$ ⁠. Suppose for reductio that $(ψ \circ B)^{'}$ is an atom $C$ ⁠. Then $C$ cannot occur elsewhere in $Δ^{'}$ or $ϕ^{'}$ ⁠; for if it did, then there would be an instance of $B$ in $σ (Δ^{'}) = Δ$ or in $σ (ϕ^{'}) = ϕ$ ⁠, and this contradicts the assumption that there are no instances of $B$ in $Δ$ or $ϕ$ ⁠. But if $C$ does not occur elsewhere in the sequent, then $Δ^{'} : ϕ^{'}$ would be valid. Hence taking the substitution under $σ$ would give $Δ : ϕ$ ⁠, which would be valid. This contradicts the assumption that $Δ, ψ \circ B : ϕ$ is perfectly valid.

Finally, as we define the various coarsening procedures, we will want to verify that the following property holds:

Lemma 1

Suppose $Π^{'}$ is a gaunt proof of the sequent $Δ : Φ$ obtained by applying the coarsening procedures to a proof $Π$ ⁠. Then:

Every atom has at most two occurrences in $Δ : Φ$ ⁠.
If $ϕ := ψ \circ θ$ occurs in some member of $Δ$ ⁠, where $\circ$ is any binary connective, then either
- (i) one of $ϕ$ ⁠, $ϕ \to χ$ ⁠, or $\neg ϕ$ occurs in $Π^{'}$ as an MPE; or
- (ii) $ϕ$ is a conjunction $θ_{1}^{'} \land . . . \land θ_{k}^{'}$ ⁠, where the $θ_{i}^{'}$ ’s are all coarsened c-variants of a single formula $θ$ from $Π$ ⁠.
If an undischarged premise $ϕ$ in $Π$ gets coarsened to distinct formulas $ϕ_{1}^{'}, . . ., ϕ_{n}^{'}$ in $Π^{'}$ ⁠, then each $ϕ_{i}^{'}$ and $ϕ_{j}^{'}$ are atom-disjoint.

Proof.

All three claims will follow by induction on the height of $Π$ ⁠. We will check this with each of the coarsening procedures defined below.

In defining the coarsening procedures, we will want to pay special attention to the possibility that a discharged formula $ϕ$ has been coarsened to multiple distinct formulas $ϕ_{1}^{'}, . . ., ϕ_{n}^{'}$ ⁠.

4.1 Disjunction

Suppose the last rule in $Π$ is $\lor$ I, with immediate subproof $Π_{0}$ of $Δ : ϕ$ ⁠. Then we have the coarsened proof $Π_{0}^{'}$ of the gauntly valid sequent $Δ^{'} : ϕ^{'}$ ⁠. Letting $B$ be a new atom not occurring elsewhere in $Π_{0}^{'}$ ⁠, we define the coarsening $Π^{'}$ of $Π$ to be:

Because

B

is a new atom, it is easy to see that

Δ^{'} : ϕ^{'} \lor B

will be gauntly valid, and also that Lemma 1 holds.

Suppose that the last rule in $Π$ is $\lor$ E, with MPE $ϕ \lor ψ$ and two main subproofs $Π_{1}$ of $Δ_{1}, ϕ : θ / ⊥$ and $Π_{2}$ of $Δ_{2}, ψ : θ / ⊥$ ⁠. We have coarsened proofs $Π_{1}^{'}$ and $Π_{2}^{'}$ of, respectively, $Δ_{1}^{'}, ϕ_{1}^{'}, . . ., ϕ_{n}^{'} : θ_{1}^{'} / ⊥$ and $Δ_{2}^{'}, ψ_{1}^{'}, . . ., ψ_{m}^{'} : θ_{2}^{'} / ⊥$ ⁠, where $Π_{1}^{'}$ and $Π_{2}^{'}$ are atom-disjoint.

Now (A) define the coarsening $Π^{'}$ of $Π$ to be:

Unless, (B) the open instances of

ϕ_{n - i + 1}^{'}, . . ., ϕ_{n}^{'}

Π_{1}^{'}

occur as premises in successive

\land

I’s:

(Or likewise for some premises

ψ_{m - j + 1}^{'}, . . ., ψ_{m}^{'}

Π_{2}^{'}

⁠.) In this case we trim these

\land

I’s from

Π_{1}^{'}

to obtain a proof

Π_{1}^{t}

Δ^{'}, ϕ_{1}^{'}, . . ., ϕ_{n - i}^{'}, ϕ_{n - i + 1}^{'} \land . . . \land ϕ_{n}^{'} : θ_{1}^{'} / ⊥

⁠. Let

Π_{1}^{''}

be the coarsening of

Π_{1}^{t}

(and likewise for

Π_{2}^{''}

⁠, if applicable). Note that the conjunction

ϕ_{n - i + 1}^{'} \land . . . \land ϕ_{n}^{'}

will coarsen to an atom

A_{1}

Π_{1}^{''}

⁠. Then define the coarsening

Π^{'}

Π

as displayed in Figure 1:

$The coarsening $\varPi ^{\prime}$ in Case (B) for a proof $\varPi $ that ends in $\vee $E.$

Figure 1.

The coarsening $Π^{'}$ in Case (B) for a proof $Π$ that ends in $\lor$ E.

Open in new tab Download slide

$The proof $\varSigma $ referred to in Remark 3. $I:=\lbrace 1,...,n\rbrace $.$

Figure 2.

The proof $Σ$ referred to in Remark 3. $I := {1, . . ., n}$ ⁠.

Open in new tab Download slide

It is easy to verify that Lemma 1 holds. It is also clear that, whether we are in case (A) or case (B), the resulting sequent will be perfectly valid. It remains to show that the relevant sequent is gauntly valid.

Suppose that the sequent

\begin{aligned} Δ_{1}^{'}, Δ_{2}^{'}, (ϕ_{1}^{'} \land . . . \land ϕ_{n}^{'}) \lor (ψ_{1}^{'} \land . . . \land ψ_{m}^{'}) : θ_{1}^{'} \lor θ_{2}^{'} \end{aligned}

(⋆)

has a valid proper coarsening. Because the two parallel subproofs are atom-disjoint, any valid coarsening of (⁠

⋆

⁠) would induce a proper coarsening of either

\begin{aligned} Δ_{1}^{'}, ϕ_{1}^{'} \land . . . \land ϕ_{n}^{'} : θ_{1}^{'} \end{aligned}

(⋆1)

\begin{aligned} Δ_{2}^{'}, ψ_{1}^{'} \land . . . \land ψ_{m}^{'} : θ_{2}^{'} \end{aligned}

(⋆2)

Focus on (⁠

⋆ 1

⁠); the same argument applies mutatis mutandis to (⁠

⋆ 2

⁠). By hypothesis, we know that

Δ_{1}^{'}, ϕ_{1}^{'}, . . ., ϕ_{n}^{'} : θ_{1}^{'}

is gauntly valid, so any valid proper coarsening of (⁠

⋆ 1

⁠) would have to be of the form:

\begin{aligned} Δ_{1}^{''}, ϕ_{1}^{'} \land . . . \land ϕ_{n - i}^{'} \land A_{1} : θ_{1}^{''} \end{aligned}

(where possibly

i = n

⁠). This in turn requires that

ϕ_{n - i + 1}^{'} \land . . . \land ϕ_{n}^{'}

occurs somewhere else in either

Δ_{1}^{'}

θ_{1}^{'}

⁠. Moreover, by Lemma 1 (1), this is the only other place in

Δ_{1}^{'}, θ_{1}^{'}

where any atom from

ϕ_{n - i + 1}^{'}, . . ., ϕ_{n}^{'}

will have an occurrence. Furthermore, letting

σ : A_{1} \mapsto (B_{1} \land . . . \land B_{i})

⁠, it follows that

\begin{aligned} σ (Δ_{1}^{''}), ϕ_{1}^{'} \land . . . \land ϕ_{n - i}^{'} \land B_{1} \land . . . \land B_{i} : σ (θ_{1}^{''}) \end{aligned}

is valid, and hence so is:

\begin{aligned} σ (Δ_{1}^{''}), ϕ_{1}^{'}, . . ., ϕ_{n - i}^{'}, B_{1}, . . ., B_{i} : σ (θ_{1}^{''}) . \end{aligned}

But this would be a valid proper coarsening of

Δ_{1}^{'}, ϕ_{1}^{'}, . . ., ϕ_{n}^{'} : θ_{1}^{'}

⁠, unless it was a mere releterring. Thus,

ϕ_{n - i + 1}^{'}, . . ., ϕ_{n}^{'}

must all be atoms. It follows that

ϕ_{n - i + 1}^{'}, . . ., ϕ_{n}^{'}

must be premises of

\land

I. They cannot be MPEs if they are atoms. They also cannot be premises of I-rules other than

\land

I, because the conclusion of that I-rule would have to be subformula of

Δ^{'}

⁠, but we know that the only occurrences of any of the atoms in

ϕ_{n - i + 1}^{'} \land . . . \land ϕ_{n}^{'}

are in the occurrences of

ϕ_{n - i + 1}^{'} \land . . . \land ϕ_{n}^{'}

⁠. For the same reason

ϕ_{n - i + 1}^{'}, . . ., ϕ_{n}^{'}

cannot occur as minor premises of

\to

E or

\neg

E. Thus, if there were a valid proper coarsening of (⁠

⋆ 1

⁠), then we would be in Case (B), and the coarsening procedures would have us trim out the unnecessary conjunction

ϕ_{n - i + 1}^{'} \land . . . \land ϕ_{n}^{'}

⁠. This would give a proof of

Δ_{1}^{''}, ϕ_{1}^{'} \land . . . \land ϕ_{n - i}^{'} \land A_{1} : θ_{1}^{''}

⁠, which, after applying the instance of

\lor

E, would yield a proof of

\begin{aligned} Δ_{1}^{''}, Δ_{2}^{'}, (ϕ_{1}^{'} \land . . . \land ϕ_{n - i}^{'} \land A_{1}) \lor (ψ_{1}^{'} \land . . . \land ψ_{m}^{'}) : θ_{1}^{''} \lor θ_{2}^{'} / ⊥ \end{aligned}

as required.

Remark 3

We have noted that the possibility of having a premise $ϕ$ get coarsened to distinct premises $ϕ_{1}, . . ., ϕ_{n}$ requires that we include this modified $\lor$ E rule that discharges multiple premises $ϕ_{1}, . . ., ϕ_{n}$ with an MPE of the form $Θ \lor (ϕ_{1} \land . . . \land ϕ_{n})$ ⁠. Observe, however, that we can assume that this only occurs in one of the subproofs of $\lor$ E. If we have two proofs $Π_{1}$ of $ψ_{1}, . . ., ψ_{m} : θ_{1}$ and $Π_{2}$ of $ϕ_{1}, . . ., ϕ_{n} : θ_{2}$ ⁠, then (when $σ_{2}, . . ., σ_{m}$ are distinct reletterings), we can insert $m$ steps of $\lor$ E to obtain the proof $Σ$ displayed in Figure 2.

Most of the time this will not be necessary, but in the arguments of Section 5 it will be convenient to assume that E-rules only discharge a single premise in certain subproofs.

4.2 Conjunction

Suppose the last rule in $Π$ is $\land$ I, with immediate subproofs $Π_{1}$ of $Δ_{1} : ϕ$ and $Π_{2}$ of $Δ_{2} : ψ$ ⁠. Then we have coarsened proofs $Π_{1}^{'}$ and $Π_{2}^{'}$ of the gauntly valid sequents $Δ_{1}^{'} : ϕ^{'}$ and $Δ_{2}^{'} : ψ^{'}$ ⁠, which we can assume to be atom-disjoint. Define the coarsening $Π^{'}$ to be:

Because

Π_{1}^{'}

and

Π_{2}^{'}

are atom-disjoint, it is easy to see that

Δ_{1}^{'}, Δ_{2}^{'} : ϕ^{'} \land ψ^{'}

will be gauntly valid. It is also easy to check that Lemma 1 holds.

Suppose next that the last rule in $Π$ is $\land$ E, with MPE $ϕ \land ψ$ and main subproof $Π_{0}$ of $Δ, ϕ, ψ : θ$ ⁠. We have the coarsened proof $Π_{0}^{'}$ of $Δ^{'}, ϕ_{1}^{'}, . . ., ϕ_{n}^{'}, ψ_{1}^{'}, . . ., ψ_{m}^{'} : θ^{'}$ ⁠. If $B_{1}, . . ., B_{n + m}$ are new atoms, define the coarsening $Π^{'}$ to be:

The fact that the

B_{i}

’s are new atoms ensures that the result will be gauntly valid, and it is easy to check that Lemma 1 holds.

4.3 Implication

Suppose the last rule in $Π$ is $\to$ I, with conclusion $ϕ \to ψ$ ⁠. Recall this rule can take three forms, according to whether the immediate subproof $Π_{0}$ is of $Δ : ψ$ or $Δ, ϕ : \emptyset$ or $Δ, ϕ : ψ$ ⁠. In the first case we know that there will be a coarsened proof $Π_{0}^{'}$ of $Δ^{'} : ψ^{'}$ ⁠. Then if $B$ is a new atom, define the coarsening $Π^{'}$ to be:

The fact that

B

is a new atom ensures that the resulting sequent is gauntly valid. Lemma 1 continues to hold.

In the second and third cases, we know there will be a coarsened proof

Π_{0}^{'}

of either

\begin{aligned} Δ, ϕ_{1}^{'}, . . ., ϕ_{n}^{'} : ⊥ o r Δ, ϕ_{1}^{'}, . . ., ϕ_{n}^{'} : ψ^{'} . \end{aligned}

Then (A) define

Π^{'}

to be:

Unless, (B) the open instances of

ϕ_{n - i + 1}^{'}, . . ., ϕ_{n}^{'}

Π_{0}^{'}

occur as premises in

\land

-I:

In which case we trim these

\land

I’s from

Π_{0}^{'}

to obtain a proof

Π_{0}^{t}

\begin{aligned} Δ^{'}, ϕ_{1}^{'}, . . ., ϕ_{n - i}^{'}, ϕ_{n - i + 1}^{'} \land . . . \land ϕ_{n}^{'} : ψ^{'} / ⊥ . \end{aligned}

Letting

Π_{0}^{''}

be the coarsening of

Π_{0}^{t}

⁠, we then define the coarsening

Π^{'}

Π

to be:

where the consequent is a new atom

B

if the main subproof has conclusion

⊥

rather than

ψ^{'}

⁠.

Unless, (C) $Π_{0}^{'}$ has the following form, where the conclusion $ψ^{'}$ derives from an instance of $\to$ E with MPE $(ϕ_{1}^{'} \land . . . \land ϕ_{n}^{'}) \to ψ^{'}$ ⁠:

In this case, delete the subproof ending in the topmost instance of

\to

E, and replace it with a leaf-node labelled

(ϕ_{1}^{'} \land . . . \land ϕ_{n}^{'}) \to ψ^{'}

⁠, and propagate this down through the E-rules. Then apply the coarsening procedures to this proof to obtain a proof of

Δ^{''} : A

⁠, where

Δ^{'}

is the image of

Δ^{''}

under the substitution

A \mapsto (ϕ_{1}^{'} \land . . . \land ϕ_{n}^{'}) \to ψ^{'}

⁠. Let this be the coarsening

Π^{'}

Π

⁠.

In sum, in Case (A) we end up with a proof $Π^{'}$ of $Δ^{'} : (ϕ_{1}^{'} \land . . . \land ϕ_{n}^{'}) \to ψ^{'}$ ⁠, where possibly $ψ^{'}$ is a new atom $B$ ⁠; in Case (B) we end up with a proof $Π^{'}$ of $Δ^{''} : (ϕ_{1}^{'} \land . . . \land ϕ_{n - i} \land A^{'}) \to ψ^{'}$ ⁠, with $Δ^{''}$ the pre-image of $Δ^{'}$ under $A \mapsto (ϕ_{n - i + 1}^{'} \land . . . \land ϕ_{n}^{'})$ ⁠; and in Case (C) we end up with a proof $Π^{'}$ of $Δ^{''} : A$ ⁠, with $Δ^{''}$ the pre-image of $Δ^{'}$ under $A \mapsto (ϕ_{1}^{'} \land . . . \land ϕ_{n}^{'}) \to ψ^{'}$ ⁠.

It is easy to see that whichever of these sequents we end up with, it must be perfectly valid. Also, Lemma 1 is easy to verify. It remains to show that the relevant sequent does not have any perfectly valid non-trivial coarsening.

Suppose that

Δ^{'} : (ϕ_{1}^{'} \land . . . \land ϕ_{n}^{'}) \to ψ^{'}

has a valid proper coarsening

Δ^{''} : (ϕ_{1}^{'} \land . . . \land ϕ_{n - 1}^{'} \land A) \to ψ^{'}

⁠. Then I claim that

ϕ_{n - i + 1}^{'}, . . ., ϕ_{n}^{'}

must have occurred as premises in successive

\land

I’s in

Π^{'}

⁠. To this end, note that

ϕ_{n - i + 1}^{'} \land . . . \land ϕ_{n}^{'}

must occur in

Δ^{'}

⁠. And by Lemma 1, we know that there must be exactly one such occurrence of

ϕ_{n - i + 1}^{'} \land . . . \land ϕ_{n}^{'}

Δ^{'}

⁠. Moreover, if

\begin{aligned} (Δ^{'})_{c} : (ϕ_{1}^{'} \land . . . \land ϕ_{n - i}^{'} \land A) \to ψ^{'} \end{aligned}

is valid, then so is

\begin{aligned} (Δ^{'})_{c}, (ϕ_{1}^{'} \land . . . \land ϕ_{n - i}^{'} \land A) : ψ^{'} . \end{aligned}

And thus, letting

σ : A \mapsto (B_{1} \land . . . \land B_{i})

⁠, the following is also valid

\begin{aligned} σ ((Δ^{'})_{c}), ϕ_{1}^{'}, . . ., ϕ_{n - i}^{'}, B_{1}, . . ., B_{i} : ψ^{'} \end{aligned}

But this would be a valid proper coarsening of

Δ^{'}, ϕ_{1}^{'}, . . ., ϕ_{n}^{'} : ψ^{'}

⁠, unless the substitution

B_{j} \mapsto ϕ_{n - i + j}^{'}

were a mere relettering. Thus, we know that each

ϕ_{n - i + j}^{'}

is an atom.

Observe that for $n - i + 1 \leq j \leq n$ ⁠, $ϕ_{j}^{'}$ cannot occur as a minor premise in $\to$ E or $\neg$ E or as a premise in an I-rule other than $\land$ I as above; for such rules would require there to be an occurrence of $ϕ_{j}^{'}$ in $Π^{'}$ other than as a conjunct in $ϕ_{n - i + 1}^{'} \land . . . \land ϕ_{n}^{'}$ ⁠, which we know is impossible. And we know that $ϕ_{j}^{'}$ cannot be an MPE, since we have just noted that they must be atoms.

Thus, if $Δ^{'} : (ϕ_{1}^{'} \land . . . \land ϕ_{n}^{'}) \to ψ^{'}$ has a valid proper coarsening $Δ^{''} : (ϕ_{1}^{'} \land . . . \land ϕ_{n - 1}^{'} \land A) \to ψ^{'}$ ⁠, then Case (B) would have applied, and the relevant coarsening procedure would have given a proof $Π^{'}$ of $Δ^{''} : (ϕ_{1}^{'} \land . . . \land ϕ_{n - 1}^{'} \land A) \to ψ^{'}$ ⁠.

On the other hand, suppose that $Δ^{'} : (ϕ_{1}^{'} \land . . . \land ϕ_{n}^{'}) \to ψ^{'}$ has a valid proper coarsening $Δ^{''} : A$ ⁠. Then we know that $(ϕ_{1}^{'} \land . . . \land ϕ_{n}^{'}) \to ψ^{'}$ must occur in $Δ^{'}$ ⁠; and by Lemma 1(1), there will be no other occurrences in $Δ^{'}$ of any of the atoms from $(ϕ_{1}^{'} \land . . . \land ϕ_{n}^{'}) \to ψ^{'}$ ⁠. Furthermore, by Proposition 4, the instance of $A$ in $Δ^{''}$ ⁠, and hence the instance of $(ϕ_{1}^{'} \land . . . \land ϕ_{n}^{'}) \to ψ^{'}$ in $Δ^{'}$ ⁠, will not be in the scope of a negation or in the antecedent of a conditional. So, by Lemma 1 (2), $(ϕ_{1}^{'} \land . . . \land ϕ_{n}^{'}) \to ψ^{'}$ must occur as an MPE in $Π_{0}^{'}$ ⁠. Now, because there are no other occurrences of any of the atoms in $ψ^{'}$ ⁠, the discharged premise $ψ^{'}$ cannot connect with any other rule in the proof, so it must simply descend via a series of E rules to the main conclusion $ψ^{'}$ of $Π_{0}^{'}$ ⁠.

Observe that if

σ : A \mapsto B \to ψ^{'}

⁠, and if

Δ_{c}^{'}

is the preimage of

Δ^{'}

under

σ

⁠, then we also have that

\begin{aligned} Δ_{c}^{'} : B \to ψ^{'} \end{aligned}

is a valid coarsening of

\begin{aligned} Δ^{'} : (ϕ_{1}^{'} \land . . . \land ϕ_{n}^{'}) \to ψ^{'}, \end{aligned}

albeit not gauntly valid. So the argument from Case (B) above applies again here, entailing that

ϕ_{1}^{'}, . . ., ϕ_{n}^{'}

are all atoms that figure in successive

\land

I’s in

Π_{0}^{'}

⁠. Moreover, the only other member of

Δ^{'}

that this conjunction can connect with in

Π_{0}^{'}

is the MPE

(ϕ_{1}^{'} \land . . . \land ϕ_{n}^{'}) \to ψ^{'}

⁠.

So in $Π_{0}^{'}$ we have $ϕ_{1}^{'}, . . ., ϕ_{n}^{'}$ descending through a series of $\land$ I’s to the minor premise of $\to$ E, with MPE $(ϕ_{1}^{'} \land . . . \land ϕ_{n}^{'}) \to ψ^{'}$ ⁠, and then the discharged consequent $ψ^{'}$ descends via a series of E-rules to the conclusion of $Π_{0}^{'}$ ⁠. In sum, if $Δ^{'} : (ϕ_{1}^{'} \land . . . \land ϕ_{n}^{'}) \to ψ^{'}$ has a valid proper coarsening $Δ^{''} : A$ ⁠, then Case (C) would have applied, and the relevant coarsening procedure would have given a proof $Π^{'}$ of $Δ^{''} : A$ as required.

This completes the treatment of $\to$ I. Now turn to the case where $Π$ ends in $\to$ E with MPE $ϕ \to ψ$ ⁠. Then we have coarsened proofs $Π_{1}^{'}$ and $Π_{2}^{'}$ of, respectively, $Δ_{1}^{'} : ϕ^{'}$ and $Δ_{2}^{'}, ψ_{1}^{'}, . . ., ψ_{n}^{'} : θ^{'}$ ⁠. Let ${Π_{1}^{1}}^{'}, . . ., {Π_{1}^{n}}^{'}$ be $n$ atom-disjoint copies of $Π_{1}^{'}$ ⁠. Define the coarsening $Π^{'}$ to be:

It is easy to verify that Lemma 1 holds. The fact that this is a gaunt proof follows from the fact that all the subproofs are atom-disjoint, which itself is an application of Lemma 1 (3).

4.4 Negation

Suppose the last rule in $Π$ is $\neg$ I with an immediate subproof $Π_{0}$ of $Δ, ϕ : ⊥$ ⁠. We know this subproof will have a coarsening $Π_{0}^{'}$ ⁠. The coarsening procedure will be clearer to explain in two separate cases, according to whether $ϕ$ has been coarsened to a single formula $ϕ^{'}$ or to multiple formulas $ϕ_{1}^{'}, . . ., ϕ_{n}^{'}$ in $Π_{0}^{'}$ ⁠.

Suppose $ϕ$ has been coarsened to a single formula $ϕ^{'}$ in $Π_{0}^{'}$ ⁠. Then if $Δ^{'} : \neg ϕ^{'}$ is gauntly valid, define $Π^{'}$ to be:

On the other hand, if

Δ^{'} : \neg ϕ^{'}

is not gauntly valid, then we can appeal to the following fact. (The proof of this fact is quite involved, and will be provided in Section 5.)

Key fact: If $Σ$ is a gaunt proof of $Δ^{'}, ϕ^{'} : ⊥$ obtained by coarsening, but $Δ^{'} : \neg ϕ^{'}$ is not gauntly valid, then: (1) $ϕ^{'}$ is an atom $A$ ⁠, (2) $Δ^{''} : A$ is gauntly valid, where $Δ^{''}$ is the preimage of $Δ^{'}$ under $A \mapsto \neg A$ ⁠, and (3) by permuting steps in $Σ$ we can obtain a gaunt proof $Σ_{p}$ of $Δ_{c}^{'}, A : ⊥$ such that $Δ_{c}^{'}$ consists of coarsened c-variants of $Δ$ and the final conclusion $⊥$ in $Σ_{p}$ descends via a series of E-rules from an instance of $\neg$ E with $\neg A, A$ as premises.

In other words, $Σ_{p}$ has the form:

Then if

Δ_{c}^{''}

is the result of replacing

\neg A

with

A

⁠, define

Π^{'}

to be the proof of

Δ_{c}^{''} : A

as follows:

By definition, and in light of the fact cited above, it is clear that the result is a gaunt proof. And it is easy to check that Lemma 1 holds.

Consider now the possibility that $ϕ$ was coarsened to $ϕ_{1}^{'}, . . ., ϕ_{n}^{'}$ in $Π_{0}^{'}$ ⁠. Then we can use the modified $\neg$ I rule, so (A) define $Π^{'}$ to be:

Unless (B)

ϕ_{n - i + 1}^{'}, . . ., ϕ_{n}^{'}

occur as premises in successive

\land

I rules above

ϕ_{n - i + 1}^{'} \land . . . \land ϕ_{n}^{'}

⁠. In that case, trim those

\land

I rules so that we have a proof of

Δ^{'}, ϕ_{1}, . . ., ϕ_{n - i}, ϕ_{n - i + 1}^{'} \land . . . \land ϕ_{n}^{'} : ⊥

⁠. Now coarsen that proof, to obtain a proof

Π_{0}^{''}

Δ^{''}, ϕ_{1}, . . ., ϕ_{n - i}, A : ⊥

⁠. Now, if

i = n

⁠, then we have a gaunt proof of

Δ^{''}, A : ⊥

⁠, where

ϕ

has been coarsened to a single formula; so we apply the coarsening procedure from above. But if

i < n

⁠, then

ϕ

has still been coarsened to multiple distinct formulas in

Δ^{''}, ϕ_{1}, . . ., ϕ_{n - i}, A : ⊥

⁠. Then, applying the modified

\neg

I rule, define

Π^{'}

to be:

In either case (A) or (B) is easy to check that Lemma 1 holds. It remains to show that the resulting sequent is gauntly valid. The argument for this is substantively the same as we have seen for the modified

\lor

E and

\to

I rules above: if we suppose that the sequent

Δ^{'} : \neg (ϕ_{1} \land . . . \land ϕ_{n})

had some valid proper coarsening, then that coarsening would have to be of the form

Δ^{''} : \neg (ϕ_{1} \land . . . \land ϕ_{n - i} \land A)

⁠. But that would only be possible if

ϕ_{n - i + 1}, . . ., ϕ_{n}

figured as premises in successive

\land

I’s; in which case we would have applied the coarsening procedure from Case (B), resulting in a proof of the sequent

Δ^{''} : \neg (ϕ_{1} \land . . . \land ϕ_{n - i} \land A)

as required.

Finally, suppose the last rule in $Π$ is $\neg$ E, with immediate subproof $Π_{0}$ of $Δ : ϕ$ ⁠. We have the coarsening $Π_{0}^{'}$ of $Δ^{'} : ϕ^{'}$ ⁠. If $Δ^{'}, \neg ϕ^{'} : ⊥$ is gauntly valid, then define $Π^{'}$ to be:

By assumption, this is a gaunt proof, and clearly Lemma 1 holds.

On the other hand, there are two ways that $Δ^{'}, \neg ϕ^{'} : ⊥$ can fail to be gauntly valid; to accommodate these possibilities we will need to define more complex proof transformations. The full details are relatively involved, so I postpone them until Section 6. For now, I will just illustrate the motivating concepts that lie behind those complicated proof transformations.

The first way that

Δ^{'}, \neg ϕ^{'} : ⊥

can fail to be gauntly valid involves

\to

⁠. For example:

\begin{aligned} \neg \neg (A \to \neg B) : A \to \neg B \end{aligned}

is gauntly valid, but

\begin{aligned} \neg \neg (A \to \neg B), \neg (A \to \neg B) : ⊥ \end{aligned}

is not gauntly valid, since it can be coarsened to

\neg A, A : ⊥

⁠.

The second way that $Δ^{'}, \neg ϕ^{'} : ⊥$ might fail to be gauntly valid is similar, but featuring $\neg$ in place of $\to$ ⁠. We know that $\neg \neg \neg A : \neg A$ is gauntly valid, but $\neg \neg \neg A, \neg \neg A : ⊥$ is not gauntly valid since it can also be coarsened to $\neg A, A : ⊥$ ⁠.

As we will see below in Lemma 9, these two examples illustrate all the possible ways that $\neg$ E can fail to preserve gauntness. More concretely, if we have a gaunt proof of $Δ^{'} : ϕ^{'}$ ⁠, but $Δ^{'}, \neg ϕ^{'} : ⊥$ is not gauntly valid, then there are some atoms $B_{1}, . . ., B_{n + m}$ and a substitution $σ$ such that for $1 \leq i \leq n$ ⁠, $σ : B_{i} \mapsto \neg B_{i}$ and for each $1 \leq i \leq m$ ⁠, there is some $j$ such that $σ : B_{n + i} \mapsto C_{1}^{i} \to (C_{2}^{i} \to . . . (C_{j}^{i} \to \neg B_{n + i}) . . .)$ ⁠, and $Δ^{''}, (\neg ϕ^{'})^{'} : ⊥$ is gauntly valid, where $Δ^{''}$ and $(\neg ϕ^{'})^{'}$ are the respective pre-images of $Δ^{'}$ and $\neg ϕ^{'}$ under $σ$ ⁠.

Now I will illustrate the essential idea behind the necessary proof transformations. We can argue that if $Δ^{'} : ϕ^{'}$ has a gaunt proof $Π$ ⁠, but that $Δ^{'}, \neg ϕ^{'} : ⊥$ is not gauntly valid, then $ϕ$ must have an occurrence of $\neg A$ or $χ := C_{1} \to (. . . \to (C_{j} \to \neg A) . . .)$ ⁠, and that $Π$ must have the form:

(The form of the uppermost proof of

⊥

will depend on

Δ_{1}

and whether

A

χ

is among the premises. Explicit details will be given below.)

If we let $Π_{j}^{'}$ and $Δ_{j}^{'}$ be the result of systematically coarsening $\neg A$ to a new atom $B$ ⁠, the essential idea is to rearrange $Π$ into the following form, which will give us the gaunt proof $Π^{'}$ that we seek.

This sketch of the coarsening procedure elides some important details, but it illustrates the main concept. Once again, the full details will be laid out in Section 6.

4.5 Main theorem

We have now provided all the coarsening procedures and verified that they preserved the property of being a gaunt proof, modulo the outstanding claims about negation. It remains to prove the key fact used in the case of $\neg$ I and to fully describe the coarsening procedure for $\neg$ E. The key fact for $\neg$ I is proved in Section 5, and the complete treatment of $\neg$ E is given in Section 6. Once these are in place, we will have established the main result of this paper:

Theorem 3

If $Π$ is a core proof of $Δ : Φ$ ⁠, then there is a gaunt core proof $Π^{'}$ of $Δ^{'} : Φ^{'}$ and a substitution $σ$ such that $σ Δ^{'}$ consists of c-variants of members of $Δ$ and $σ Φ^{'}$ is a c-variant of $Φ$ ⁠. $Π^{'}$ and $σ$ may be obtained from the coarsening procedures defined above.

In the prequel paper, we saw that we could coarsen both classical and constructive core proofs to obtain perfect core proofs. When it comes to gaunt proofs, however, the method of coarsening only allows us to transform constructive core proofs into gaunt core proofs. The analogous result does not hold for classical core logic. One complication comes from $C R$ ⁠. When coarsening an instance of $C R$ whose discharged assumption $\neg ϕ$ had been coarsened to multiple assumptions $\neg ϕ_{1}^{'}, . . ., \neg ϕ_{n}^{'}$ ⁠, we had to insert a series of $\lor$ -I rules. Those will introduce non-gauntness into the proof in the same way that the intercalated $\land$ I rules introduced non-gauntness. This complication can be avoided by introducing a generalized from of $C R$ that applies to multiple assumptions at once, analogous to the modified $\neg$ I and $\to$ I rules we introduced above. The form of this modified $C R$ rule would be:

This rule is clearly derivable in classical core logic, so adding it to the proof system would not change the deducibility relation.

A separate problem for coarsening classical proofs stems from strictly classical validities involving $\to$ ⁠. It is this problem that proves insurmountable.

Theorem 4

There are classical gaunt validities that do not have gaunt proofs in the natural deduction system of classical core logic.

Proof.

Consider the sequent $\neg A \to B, \neg B : A$ ⁠. It is not difficult to see that any proof of this sequent must have $\neg A \to B$ as an MPE. But then $\neg A$ must be the minor premise, and this would constitute a non-gaunt subproof of $\neg A : \neg A$ ⁠. (It is worth noting that this proof does not depend on the fact that we have used $C R$ as a strictly classical rule; so this limitation to classical core natural deduction still applies when we use another classical negation rule such as Dilemma.)

As an illustration, take an obvious classical core proof of this sequent:

This proof has the non-gaunt subproof of

\neg A

from

\neg A

in the proof of minor premise for

\to

-E.

On the other hand, there is reason to think that this limitation is particular to the natural deduction system of classical core logic. As Pierre Saint-Germier pointed out to me, there is a gaunt proof of $\neg A \to B, \neg B : A$ in a standard sequent calculus, such as Gentzen’s LK:⁶

This raises the question of how robust the limitative result of Theorem 4 is. It shows a limitation to natural deduction. But is there a deductive system for classical logic in which every gaunt validity has a gaunt proof? I will not pursue this question here, but flag the issue for future work.⁷

For our purposes here, all that remains is to prove the facts appealed to in defining the $\neg$ I coarsening procedure and to provide the full details of the proof transformations needed in the coarsening procedure for $\neg$ E.

5 Negation Introduction

In this section I will prove the facts that I had relied on in defining the coarsenings of $\neg$ I. First, we can characterize the sequents applied to which $\neg$ -I fails to preserve gaunt validity.

Lemma 2

If $Δ, ϕ : \emptyset$ is gauntly valid, but $Δ : \neg ϕ$ is not gauntly valid, then $ϕ$ is an atom $A$ and $Δ^{'} : B$ is the gauntly valid coarsening of $Δ : \neg A$ ⁠, where $Δ$ is obtained from $Δ^{'}$ by uniformly replacing $B$ with $\neg A$ ⁠.

Proof.

Assume $Δ : \neg ϕ$ is not gauntly valid, so there exists a substitution $σ$ such that $Δ^{'} : θ$ is a valid proper coarsening of $Δ : \neg ϕ$ under $σ$ ⁠. Suppose $θ$ is of the form $\neg χ$ ⁠. Now, $Δ^{'} : \neg χ$ is valid only if $Δ^{'}, χ : \emptyset$ is valid; but then $Δ^{'}, χ : \emptyset$ would be a valid proper coarsening of $Δ, ϕ : \emptyset$ ⁠, contradicting the gaunt validity of $Δ, ϕ : \emptyset$ ⁠. So the main connective of $θ$ cannot be $\neg$ ⁠, and hence by Proposition 3, $θ$ must be an atom $B$ ⁠.

Let $S$ be the set of atoms other than $B$ that $σ$ changed. Suppose $S$ is non-empty and let $σ^{'}$ agree with $σ$ on $S$ and be the identity map otherwise. Also let $β : B \mapsto \neg ϕ$ and be the identity map otherwise. Without loss of generality, we can assume that $ϕ$ does not contain any of the atoms in $S$ ⁠. Then $Δ = σ^{'} (β (Δ^{'}))$ ⁠. So if $S$ is non-empty, then $β (Δ^{'}), ϕ : \emptyset$ would be a valid, non-trivial coarsening of $Δ, ϕ : \emptyset$ under $σ^{'}$ ⁠, which is impossible.

Now suppose $ϕ$ is not atomic, and break $σ$ down into two substitutions: $σ_{1} : B \mapsto \neg C$ and $σ_{2} : C \mapsto ϕ$ ⁠. Then $σ_{1} Δ^{'}, C : \emptyset$ would be a valid proper coarsening of $Δ, ϕ : \emptyset$ under $σ_{2}$ ⁠, which again is impossible. Hence $ϕ$ must be an atom $A$ ⁠, and $σ : B \mapsto \neg A$ ⁠.

Lemma 2 establishes claims (1) and (2) of the key fact we are trying to prove. The remaining part (3) requires us to provide our method for finding a gaunt proof in those instances where appending an instance of $\neg$ I does not preserve gauntness, which we will do by showing how to appropriately permute rules in the proof. Before providing the necessary proof transformations, we will need several preliminary lemmas. To begin with, I record a simple lemma about when atoms are provable that will be useful later.

Lemma 3

Suppose $Π$ is a gaunt coarsened proof of $Δ, \neg A : Φ$ ⁠, and that $Π_{0}$ is a subproof of $Π$ establishing $Δ_{0}, \neg A : Φ_{0}$ ⁠, but that $Δ_{0}, \neg Φ_{0} ⊬ A$ ⁠. Then $Δ, \neg Φ ⊬ A$ ⁠.

Proof.

Induction on the height of $Π$ ⁠. The basis step is trivial, since any subproof of a one line proof $Π$ would have to be $Π$ itself.

The induction step is mostly straightforward; consider the last rule in $Π$ ⁠.

Case 1: The last rule in $Π$ is $\land$ E. Say the MPE is $ψ \land B$ ⁠, with an immediate subproof of $Δ, ψ, \neg A : ϕ$ ⁠. Then $Δ, ψ \land B, \neg ϕ ⊢ A$ only if $Δ, ψ, \neg ϕ ⊢ A$ ⁠, so the claim follows from the i.h.

Case 2: The last rule in $Π$ is $\land$ I. Say we have two immediate subproofs of $Δ_{1}, \neg A : ϕ_{1}$ and $Δ_{2} : ϕ_{2}$ ⁠. Then $Δ_{1}, Δ_{2}, \neg (ϕ_{1} \land ϕ_{2}) ⊢ A$ only if $Δ_{1}, Δ_{2}, \neg ϕ_{1} \lor \neg ϕ_{2} ⊢ A$ ⁠. Because parallel subproofs will be atom-disjoint, $A$ will only occur in, say, $Δ_{1}, ϕ_{1}$ ⁠. So then, because the two subproofs will be perfect, it follows that $Δ_{1}, Δ_{2}, \neg (ϕ_{1} \land ϕ_{2}) ⊢ A$ only if $Δ_{1}, \neg ϕ_{1} ⊢ A$ ⁠, and the claim follows from the i.h.

Case 3: The last rule in $Π$ is $\lor$ E. This follows from the i.h. by appeal to the fact that parallel subproofs will be atom-disjoint. The argument is substantively similar to the case of $\land$ I.

Case 4: The last rule in $Π$ is $\lor$ I. This follows easily from the i.h. analogous to the case of $\land$ E.

Case 5: The last rule in $Π$ is $\neg$ E. Say the MPE is $\neg ϕ$ ⁠, with immediate subproof of $Δ, \neg A : ϕ$ ⁠. The claim is immediate from the i.h.

Case 6: The last rule in $Π$ is $\neg$ I. Say we have a proof of $Δ, \neg A : \neg (\underset{i}{⋀} ϕ_{i})$ with immediate subproof of $Δ, \neg A, ϕ_{1}, . . ., ϕ_{n} : ⊥$ ⁠. Now, $Δ, \neg \neg (ϕ_{1} \land . . . \land ϕ_{n}) ⊢ A$ only if $Δ, ϕ_{1}, . . ., ϕ_{n} ⊢ A$ ⁠, so the claim follows from the i.h.

Case 7: The last rule in $Π$ is $\to$ E. Say we have MPE $ψ \to θ$ and immediate subproofs of, say, $Δ_{1}, \neg A : ψ$ and $Δ_{2}, θ : Φ$ ⁠. Now, $Δ_{1}, Δ_{2}, ψ \to θ, \neg Φ ⊢ A$ only if $Δ_{1}, Δ_{2}, \neg ψ \lor θ, \neg Φ ⊢ A$ ⁠. And by atom-disjointness, this can only hold if $Δ_{1}, \neg ψ ⊢ A$ ⁠, so the claim follows by the i.h. The argument would be similar if we had assumed $\neg A$ occurred in the main subproof rather than the minor subproof.

Case 8: The last rule in $Π$ is $\to$ I. If we have a conclusion $\underset{i}{⋀} ψ_{i} \to B$ ⁠, with $B$ a new atom, then the argument is similar to the case of $\neg$ I. If the conclusion is $B \to θ$ ⁠, then the argument is similar to $\lor$ I. So suppose the conclusion is $(ψ_{1} \land . . . \land ψ_{n}) \to θ$ ⁠, with immediate subproof of $Δ, \neg A, ψ_{1}, . . ., ψ_{n} : θ$ ⁠. Now, $Δ, \neg ((ψ_{1} \land . . . \land ψ_{n}) \to θ) ⊢ A$ only if $Δ, ψ_{1}, . . ., ψ_{n}, \neg θ ⊢ A$ ⁠, so the claim follows from the i.h.

5.1 Preliminary lemmas

The main goal in this subsection is to show that, when we have a gaunt coarsened proof $Π$ of $Δ, δ : ψ$ ⁠, if $Δ, \neg \neg δ ⊢ ψ$ ⁠, then by permuting rules in $Π$ we can obtain a gaunt proof $Π^{'}$ of $Δ, δ : ψ$ where $δ$ occurs above a $⊥$ ⁠. The proof will consist of three lemmas, beginning with the longest and most involved.

Lemma 4

If $Π$ is a gaunt coarsened proof of $Δ, δ : ψ$ or $Δ, δ, ψ : ⊥$ and respectively either $Δ ⊢ \neg δ \lor ψ$ or $Δ ⊢ \neg δ \lor \neg ψ$ ⁠, then:

some formula $γ_{1} \lor γ_{2}$ occurs somewhere in $Δ$ not in the scope of a negation or the antecedent of a conditional.
$γ_{1} \lor γ_{2}$ must occur as an MPE in $Π$ ⁠.
By permuting rules in $Π$ we can obtain a proof $Π^{'}$ such that for each $δ$ and $ψ$ as in the lemma there is an instance of $\lor$ E such that $Π^{'}$ respectively has one of the following forms:
Moreover, by permuting rules in $Π^{'}$ we can ensure that $Σ_{c}$ consists only of E-rules, and that when there is an $\to$ E, $γ_{a} \lor γ_{b}$ stands above the main subconclusion rather than above the minor premise. So, in particular, if $ψ_{1}, . . ., ψ_{n}$ is the branch below $ψ_{1}$ ⁠, then each $ψ_{j}$ is a main subconclusion of the respective E-rule; and $ψ_{j}$ is either the same as $ψ_{j - 1}$ ⁠, or, if the $j^{t h}$ E-rule applied in this end segment is $\lor$ E with neither subconclusion equal to $⊥$ ⁠, then $ψ_{j}$ will be either $ψ_{j - 1} \lor ξ$ or $ξ \lor ψ_{j - 1}$ ⁠, where $ξ$ is the other main subconclusion of that instance of $\lor$ E. Thus, if $ψ$ was a coarsened c-variant of some formula $χ$ ⁠, then $ψ_{n}$ is also a coarsened c-variant of $χ$ (although $ψ$ and $ψ_{n}$ may not be identical).

Proof.

Claim (1) By induction on the height of a coarsened proof, we know that if there is no formula containing $\lor$ in $Δ$ ⁠, then there is no instance of $\lor$ E in $Π$ ⁠. And it is a classic fact about intuitionistic logic that if $Δ ⊢ ξ \lor ζ$ ⁠, and there is no instance of $\lor$ in $Δ$ not in the scope of a negation or the antecedent of a conditional, then $Δ ⊢ ξ$ or $Δ ⊢ ζ$ ⁠.⁸ So unless there were an instance of $\lor$ in $Δ$ not in the scope of a negation or the antecedent of a conditional, $Δ ⊢ \neg δ \lor ψ$ would entail that either $Δ ⊢ ψ$ or $Δ ⊢ \neg δ$ ⁠. And this would contradict the perfect validity of $Δ, δ : ψ$ ⁠.

Claim (2) This follows from claim (1) by Lemma 1 (2).

Claims (3) & (4) can be proved simultaneously by induction on the height of $Π$ ⁠. The basis case is trivial for both claims, since there is no one-line proof with an instance of $\lor$ E in it.

We now proceed to the inductive step in our proof of Claims (3) and (4). There are 8 cases according to the last rule in $Π$ ⁠.

Case 1: The last rule in $Π$ is $\land$ I. For Claim (3) we are given two immediate subproofs $Π_{1}$ of $Δ_{1}, δ : θ_{1}$ and $Δ_{2} : θ_{2}$ ⁠. Since $Δ_{1}, Δ_{2} ⊢ \neg δ \lor (θ_{1} \land θ_{2})$ ⁠, we also know that $Δ_{1}, Δ_{2} ⊢ \neg δ \lor θ_{1}$ ⁠. And since $Δ_{2}$ is atom-disjoint from $Δ_{1}, δ, θ_{1}$ ⁠, it follows that $Δ_{1} ⊢ \neg δ \lor θ_{1}$ ⁠. Thus, the claim follows by applying the i.h. to $Π_{1}$ ⁠.

For Claim (4), the i.h. gives us a proof of the following general form. (For space and generality in the following arguments I will often not display the MPEs of successive $\lor$ E rules; when I do this I will use double lined inferences with a left-label of $\lor$ E.)

Then when we permute the

\land

I upwards, we get the following, where

Σ_{0}^{i}

are

ξ_{i}

are distinct reletterings of

Σ_{0}

and

ξ

⁠:

Note that if there are multiple

δ

’s satisfying the hypotheses of the lemma, this permutation can be performed simultaneously for all of them.

Case 2: The last rule in $Π$ is $\land$ E. Claim (3) is immediate from the i.h. Claim (4) is trivial in this case.

Case 3: The last rule in $Π$ is $\lor$ I. For Claim (3), $Π$ is a proof of $Δ, δ : θ \lor A$ with an immediate subproof $Π_{1}$ of $Δ, δ : θ$ ⁠. By assumption, $Δ ⊢ \neg δ \lor (θ \lor A)$ ⁠; and since $A$ is a new atom it follows that $Δ ⊢ \neg δ \lor θ$ ⁠. Thus the claim follows from the i.h.

For Claim (4), the permutation is substantively similar to the $\land$ I case. We know that the newly introduced disjunct will be a new atom, so that the subproof ending with $R_{i}$ will have conclusion $(θ_{1} \lor . . . \lor θ_{m}) \lor A$ ⁠. Letting $A_{i}$ be distinct new atoms, permuting the $\lor$ I upwards gives us a new subproof with conclusion $(θ_{1} \lor A_{1}) \lor . . . \lor (θ_{m} \lor A_{m})$ ⁠.

Case 4: The last rule in $Π$ is $\lor$ E. For Claim (3) we have several sub-cases based on whether the main subconclusions are $θ_{i}$ or $⊥$ ⁠.

Subcase 1: $Π$ is a proof of $Δ_{1}, Δ_{2}, δ, (ξ_{1} \land . . . \land ξ_{n}) \lor (ζ_{1} \land . . . \land ζ_{m}) : θ$ with subproofs $Π_{1}$ of $Δ_{1}, δ, ξ_{1}, . . ., ξ_{n} : ⊥$ and $Δ_{2}, ζ_{1}, . . ., ζ_{m} : θ$ ⁠. Then the claim is immediate.

Subcase 2: $Π$ is a proof of $Δ_{1}, Δ_{2}, δ, (ξ_{1} \land . . . \land ξ_{n}) \lor (ζ_{1} \land . . . \land ζ_{m}) : θ$ with subproofs $Π_{1}$ of $Δ_{1}, δ, ξ_{1}, . . ., ξ_{n} : θ$ and $Δ_{2}, ζ_{1}, . . ., ζ_{m} : ⊥$ ⁠. Given that $Δ_{1}, Δ_{2}, (ξ_{1} \land . . . \land ξ_{n}) \lor (ζ_{1} \land . . . \land ζ_{m}) ⊢ \neg δ \lor θ$ ⁠, we also know that $Δ_{1}, Δ_{2}, ξ_{1}, . . ., ξ_{n} ⊢ \neg δ \lor θ$ ⁠, and hence (by the atom-disjointness of the two subproofs) $Δ_{1}, ξ_{1}, . . ., ξ_{n} ⊢ \neg δ \lor θ$ ⁠. Now the claim follows from the i.h.

Subcase 3: $Π$ is a proof of $Δ_{1}, Δ_{2}, δ, (ξ_{1} \land . . . \land ξ_{n}) \lor (ζ_{1} \land . . . \land ζ_{m}) : θ_{1} \lor θ_{2}$ ⁠, with immediate subproofs of $Δ_{1}, δ, ξ_{1}, . . ., ξ_{n} : θ_{1}$ and $Δ_{2}, ζ_{1}, . . ., ζ_{m} : θ_{2}$ ⁠. By assumption, $Δ_{1}, Δ_{2}, δ, (ξ_{1} \land . . . \land ξ_{n}) \lor (ζ_{1} \land . . . \land ζ_{m}) ⊢ \neg δ \lor θ_{1} \lor θ_{2}$ ⁠; then it follows from atom-disjointness that $Δ_{1}, ξ_{1}, . . ., ξ_{n} ⊢ \neg δ \lor θ_{1}$ ⁠, and now the claim follows from the i.h.

Subcase 4: $Π$ is a proof of $Δ_{1}, Δ_{2}, δ, (ξ_{1} \land . . . \land ξ_{n}) \lor (ζ_{1} \land . . . \land ζ_{m}) : ⊥$ with immediate subproofs $Π_{1}$ of $Δ_{1}, δ, ξ_{1}, . . ., ξ_{n} : ⊥$ and $Π_{2}$ of $Δ_{2}, ζ_{1}, . . ., ζ_{m} : ⊥$ ⁠; and for some $θ \in Δ_{1}, Δ_{2}, ⋀ ξ_{i} \lor ⋀ ζ_{i}$ ⁠, we have that $(Δ_{1}, Δ_{2}, ⋀ ξ_{i} \lor ⋀ ζ_{i}) ∖ {θ} ⊢ \neg δ \lor \neg θ$ ⁠. We have two possibilities according to whether $θ$ is $⋀ ξ_{i} \lor ⋀ ζ_{i}$ or is some other premise.

First suppose that $θ$ is $⋀ ξ_{i} \lor ⋀ ζ_{i}$ ⁠. Given that $Δ_{1}, Δ_{2} ⊢ \neg δ \lor \neg (⋀ ξ_{i} \lor ⋀ ζ_{i})$ ⁠, we also have $Δ_{1}, Δ_{2} ⊢ \neg δ \lor \neg ⋀ ξ_{i}$ ⁠, and thus for each $i$ ⁠, we have $Δ_{1}, {ξ_{j}}_{j \neq i} ⊢ \neg δ \lor \neg ξ_{i}$ ⁠. So by the i.h., for each $i$ there is some formula $γ_{a}^{i} \lor γ_{b}^{i}$ such that we can obtain $Π_{1}^{'}$ with the form:

Let

Π_{2}^{i}

be distinct reletterings of

Π_{2}

⁠. Then we can form the proof

Π^{'}

as required the claim by inserting an instance of

\lor

E using the copy

Π_{2}^{i}

for each

ξ_{i}

⁠:

(Note that if there are multiple

δ

’s satisfying the hypotheses of the lemma, this can be done simultaneously for each such

δ

in the prooftree.)

Second, suppose that $θ$ is not $⋀ ξ_{i} \lor ⋀ ζ_{i}$ ⁠. If $θ \in Δ_{2}$ ⁠, then the claim is immediate. On the other hand, if $θ \in Δ_{1}$ ⁠, then as before we know that $Δ_{1} ⊢ \neg δ \lor \neg θ$ ⁠; now the claim follows from the i.h. This completes Claim (3) for this case.

Claim (4) is trivial in this case.

Case 5: The last rule in $Π$ is $\neg$ I. For Claim (3), $Π$ is a proof of $Δ, δ : \neg (θ_{1} \land . . . \land θ_{m})$ with immediate subproof $Π_{1}$ of $Δ, δ, θ_{1}, . . ., θ_{n} : ⊥$ ⁠. By assumption, $Δ ⊢ \neg δ \lor \neg (θ_{1} \land . . . \land θ_{m})$ ⁠, so for each $i$ we have that $Δ, {θ_{j}}_{j \neq i} ⊢ \neg δ \lor \neg θ_{i}$ ⁠. Then by the i.h., for each $i$ there is some $γ_{a}^{i} \lor γ_{b}^{i}$ occurring a proof $Π_{1}^{'}$ of the following form:

And by Claim (4) of the i.h., we know that below each such

γ_{a}^{i} \lor γ_{b}^{i}

there are only E-rules. So for each such

i

⁠, we can insert

\neg

I, giving us a proof of the following general form, satisfying both Claims (3) and (4):

Case 6: The last rule in $Π$ is $\neg$ E. For Claim (3), we have a proof $Π$ of $Δ, δ, \neg ϕ : ⊥$ with immediate subproof $Π_{1}$ of $Δ, δ : ϕ$ ⁠. We need both to show that if $Δ ⊢ \neg δ \lor \neg \neg ϕ$ ⁠, then there is some instance of $\lor$ E such that $\neg ϕ$ can be permuted into subproof while $δ$ occurs above a $⊥$ in the other subproof, and we need to consider the possibility that there other premises $ψ_{i}$ such that $Δ, \neg ϕ ⊢ \neg δ \lor \neg ψ_{i}$ ⁠. We can consider in turn what the last rule in $Π_{1}$ is.

If the last rule in $Π_{1}$ is an E-rule, then we can permute the instance of $\neg$ E above the E-rule; then we need to argue according to Case 2, 4, or 8 as appropriate.
If the last rule in $Π$ is $\land$ I, say with $ϕ := ξ \land ζ$ ⁠, then $Π$ has the form:
First note that, if there is a $ψ_{i}$ as displayed such that $Δ, \neg (ξ \land ζ) ⊢ \neg δ \lor \neg ψ_{i}$ ⁠, then by atom disjointness we would have $Δ_{a}, \neg ξ ⊢ \neg δ \lor \neg ψ_{i}$ ⁠. So Claim (3) as applied to $ψ_{i}$ would then follow by the i.h.; we now have to deal with $\neg (ξ \land ζ)$ and any $ψ_{j}$ that occur in the proof.
First assume that $Δ_{a}, Δ_{b} ⊢ \neg δ \lor \neg \neg (ξ \land ζ)$ ⁠. Then we also know that $Δ_{a}, Δ_{b} ⊢ \neg δ \lor \neg \neg ξ$ and hence (by atom disjointness) $Δ_{a} ⊢ \neg δ \lor \neg \neg ξ$ ⁠. Consider the following proof:
Then we can, by the i.h., permute some E-rules to obtain the following proof of $Δ_{a}, δ, ψ_{i}, \neg ξ : ⊥$ ⁠, where $Δ_{a} := Γ_{a} \cup Γ_{b} \cup {γ_{a} \lor γ_{b}}$ ⁠. Moreover, the i.h. also ensures that $ψ_{i}$ and $δ$ will occur in separate subproofs of some instance of $\lor$ E, which may or may not be the same as the instance $γ_{a} \lor γ_{b}$ displayed here. (Accordingly, $ψ_{i}$ could occur in any of the subproofs below, which is why it is not explicitly displayed).
Thus, by inserting the subproof $Π_{1}^{b}$ ⁠, we can obviously obtain a proof of $Δ_{a}, Δ_{b}, δ, \neg (ξ \land ζ) : ⊥$ as follows:
Then $δ$ and $\neg (ξ \land ζ)$ stand in opposite subproofs of $\lor$ E, as do $δ$ and $ψ_{j}$ (if there are such). And as we noted, the i.h. also guarantees that $δ$ and $ψ_{i}$ will also be in distinct subproofs of $\lor$ E, if there are any $ψ_{i}$ ’s.
On the other hand, suppose that $Δ_{a}, Δ_{b} ⊬ \neg δ \lor \neg \neg (ξ \land ζ)$ ⁠, but that there is some $ψ_{j}$ in $Π_{1}^{b}$ such that $Δ_{a}, Δ_{b}, \neg (ξ \land ζ) ⊢ \neg δ \lor \neg ψ_{j}$ ⁠. I claim that either $Δ_{a} ⊢ \neg δ \lor ξ$ or $Δ_{b} ⊢ \neg ψ_{j} \lor ζ$ ⁠. If not, then we would have a countermodel $M_{a}$ witnessing $Δ_{a} ⊬ \neg δ \lor ξ$ and a countermodel $M_{b}$ witnessing $Δ_{b} ⊬ \neg ψ_{j} \lor ζ$ ⁠; and we could piece them together to create a countermodel $M$ witnessing $Δ_{a}, Δ_{b}, \neg (ξ \land ζ) ⊬ \neg δ \lor \neg ψ_{j}$ ⁠, as follows:⁹
But this contradicts our assumption. So we can suppose, without loss of generality, that $Δ_{b} ⊢ \neg ψ_{j} \lor ζ$ ⁠. Then by the i.h. there is some MPE $γ_{1} \lor γ_{2}$ in $Π_{1}^{b}$ such that we have subproofs of $γ_{1}, ψ_{j}, Γ_{1} : ⊥$ and $γ_{2}, Γ_{2} : ζ$ ⁠. Then we can form the following proof, which has $δ$ and $ψ_{j}$ in separate subproofs of $\lor$ E, as required.
If the last rule in $Π_{1}$ is $\lor$ I, then $ϕ := θ \lor A$ ⁠, where $A$ is a new atom, and $Π_{1}$ has the immediate subproof $Π_{0}$ of $Δ, δ : θ$ ⁠. Then we can consider the proof:
And then we can appeal to the i.h., following the same pattern of argument as when $Π_{1}$ ended with $\land$ I.
If the last rule in $Π_{1}$ is $\neg$ I, then $ϕ$ is $\neg θ$ ⁠, with an immediate subproof $Π_{0}$ of $Δ, δ, θ : ⊥$ ⁠. Suppose $Δ ⊢ \neg δ \lor \neg \neg ϕ$ ⁠; then, since $ϕ := \neg θ$ ⁠, we also have $Δ ⊢ \neg δ \lor \neg θ$ ⁠. Similarly, if there is a $ψ \in Δ$ such that $Δ ∖ {ψ}, \neg ϕ ⊢ \neg δ \lor \neg ψ$ ⁠, then we also have $Δ ∖ {ψ}, θ ⊢ \neg δ \lor \neg ψ$ ⁠. So the claim follows from the i.h., applied to $Π_{0}$ ⁠.
If the last rule in $Π_{1}$ is $\to$ I, there are three possibilities according to the form of $\to$ I used:
The first of these cases is treated similarly to the $\lor$ I case. The second is treated analogously to the $\neg$ I case. For the third case, inserting a $\neg$ E would give a proof of $Δ, δ, ξ, \neg ζ : ⊥$ ⁠. (If there are any formulas $ψ$ such that $Δ, \neg (ξ \to ζ) ⊢ \neg δ \lor \neg ψ$ ⁠, we can apply the i.h. to this shorter proof to establish the claim applied to $ψ$ ⁠.)
Now, if it holds that $Δ ⊢ \neg δ \lor \neg \neg (ξ \to ζ)$ ⁠, it also follows that $Δ, ξ ⊢ \neg δ \lor \neg \neg ζ$ ⁠. It likewise follows that $Δ, \neg ζ ⊢ \neg δ \lor \neg ξ$ ⁠. Hence, by appeal to the i.h., we know that there is a proof $Σ$ of $Δ, δ, ξ, \neg ζ : ⊥$ ⁠, with $\neg ζ$ an MPE, and where $δ$ and $\neg ζ$ and $δ$ and $ξ$ respectively stand in different subproofs of $\lor$ E. Consistent with the i.h., the premises $ξ$ and $\neg ζ$ may or may not occur in the same subproof of $\lor$ E, so that the overall form of $Σ$ may be either of the following (using the convention of suppressing MPEs of $\lor$ E for space):
Finally, we can insert $\to$ I to obtain our desired proofs:

This shows how we can satisfy Claim (3), and we have implicitly also dealt with Claim (4). But to be explicit, for Claim (4) the i.h. gives us a proof of the form:

Then pushing the

\neg

E upwards gives us:

Case 7: The last rule in

Π

\to

I. We have three subcases depending on the version of

\to

I applied.

Subcase 1: We have a proof $Π$ of $Δ, δ : A \to θ$ with an immediate subproof of $Δ, δ : θ$ ⁠. By assumption, $Δ ⊢ \neg δ \lor (A \to θ)$ ⁠. But since $A$ is a new atom, it follows that $Δ ⊢ \neg δ \lor θ$ ⁠, so we get Claim (3) from the i.h., and Claim (4) is substantively similar to the case of $\lor$ I.

Subcase 2: We have a proof $Π$ of $Δ, δ : (ξ_{1} \land . . . \land ξ_{n}) \to A$ with an immediate subproof of $Δ, δ, ξ_{1}, . . ., ξ_{n} : ⊥$ ⁠. By assumption, $Δ ⊢ \neg δ \lor ((ξ_{1} \land . . . \land ξ_{n}) \to A)$ ⁠; and since $A$ is a new atom it also follows that $Δ ⊢ \neg δ \lor \neg (ξ_{1} \land . . . \land ξ_{n})$ ⁠. Now Claim (3) follows by the i.h., arguing similarly to the case of $\neg$ I above. Claim (4) is also substantively similar to the case of $\neg$ I.

Subcase 3: We have a proof $Π$ of $Δ, δ : (ξ_{1} \land . . . \land ξ_{n}) \to θ$ with an immediate subproof $Π_{1}$ of $Δ, δ, ξ_{1}, . . ., ξ_{n} : θ$ ⁠. By assumption, $Δ ⊢ \neg δ \lor ((ξ_{1} \land . . . \land ξ_{n}) \to θ)$ ⁠. This entails $Δ, ξ_{1}, . . ., ξ_{n} ⊢ \neg δ \lor θ$ ⁠. By the i.h., this entails that there is a $\lor$ E where $δ$ stands in one subproof above a $⊥$ while $θ$ is the conclusion of the other subproof.

Furthermore, consider also the proof that is like $Π$ except that applies $\neg$ E to the immediate subproof $Π_{1}$ ⁠:¹⁰

Because we know that

Δ ⊢ \neg δ \lor ((ξ_{1} \land . . . \land ξ_{n}) \to θ)

⁠, it also follows that for each

i

we have

Δ, \neg θ, {ξ_{j}}_{j \neq i} ⊢ \neg δ \lor \neg ξ_{i}

⁠. Thus, by the same argument as in the

\neg

E case above, we can infer that for each

ξ_{i}

there is a

\lor

E, where

ξ_{i}

stands in one subproof and

δ

stands in the other subproof; the conclusion of

ξ_{i}

’s subproof may be either

θ

⊥

⁠.

Now to both finish Claim (3) and also establish Claim (4), we can permute the $\to$ I rule upward according to the following process: (i) if $ξ_{i}$ stands in a subproof $Σ_{j}$ above a formula $θ_{j}$ that is a main subconclusion of $\lor$ E, then infer $ξ_{i} \to θ_{j}$ below that subproof, (ii) if $ξ_{i}$ stands in a subproof that concludes with a $⊥$ as a subconclusion in an instance of $\lor$ E, then we infer $ξ_{i} \to B_{i}$ below that subproof, and (iii) if there is a subproof $Σ_{j}$ above a formula $θ_{j}$ ⁠, which is a main subconclusion of a rule of $\lor$ E, but none of the $ξ_{i}$ ’s occur in $Σ_{j}$ ⁠, then infer $B_{j} \to θ_{j}$ below the subproof $Σ_{j}$ ⁠. For instance, suppose that we were given $Π$ as follows:

Then applying our process for permuting this

\to

I upwards would yield the following proof:

Case 8: The last rule in

Π

\to

E. For Claim (3), we have a proof

Π

Δ, δ, ϕ \to θ : χ

with immediate subproofs

Π_{1}

Δ_{1} : ϕ

and

Π_{2}

Δ_{2}, θ : χ

⁠. Take two subcases, according to whether

δ

occurs as a premise in

Π_{1}

or in

Π_{2}

⁠.

Subcase 1: $δ$ occurs in $Π_{2}$ ⁠. By assumption, $Δ_{1}, Δ_{2}, ϕ \to θ ⊢ \neg δ \lor χ$ ⁠; hence $Δ_{1}, Δ_{2}, θ ⊢ \neg δ \lor χ$ ⁠. By atom-disjointness we have that $Δ_{2}, θ ⊢ \neg δ \lor χ$ ⁠, and then the claim follows from the i.h.

Subcase 2: $δ$ occurs in $Π_{1}$ ⁠. Again we are given that that $Δ_{1}, Δ_{2}, ϕ \to θ ⊢ \neg δ \lor χ$ ⁠. On the one hand, if $Δ_{1} ⊢ \neg δ \lor ϕ$ ⁠, then the claim follows from the i.h. Similarly, if $Δ_{2} ⊢ \neg θ \lor χ$ ⁠, then by the i.h. there is a proof $Π_{2}^{'}$ of the form:

Then we can form the following proof, which satisfies Claim (3):

Now, however, if contrary to the above we have

Δ_{1} ⊬ \neg δ \lor ϕ

and

Δ_{2} ⊬ \neg θ \lor χ

⁠, then there will be a countermodel

M_{1}

such that

M_{1} ⊩ Δ_{1}

and

M_{1} ⊮ \neg δ \lor ϕ

and a countermodel

M_{2}

such that

M_{2} ⊩ Δ_{2}

and

M_{2} ⊮ \neg θ \lor χ

⁠. We can piece these together to make a countermodel

M_{3}

witnessing

Δ_{1}, Δ_{2}, ϕ \to θ ⊬ \neg δ \lor χ

⁠, which is a contradiction. Here is how we construct

M_{3}

⁠.

Start by taking $M_{1}$ and adding to its root node every atom true at the root node of $M_{2}$ ⁠. Now, we know that $M_{2}$ must contain a world $v_{2}$ such that $v ⊩ θ$ ⁠, for otherwise $M_{2} ⊩ \neg θ$ ⁠. For any world $w$ in $M_{1}$ such that $w ⊩ ϕ$ ⁠, make all the sentences true at $v_{2}$ also be true at $w$ ⁠. (This is possible because of atom-disjointness). So $ϕ \to θ$ will be true at the root world. Similarly, if there are any worlds $w_{1}$ from $M_{2}$ such that $w_{1} ⊮ ϕ$ ⁠, then we can simply paste a copy of $M_{2}$ below such $w_{2}$ ⁠. The result will then be our desired $M_{3}$ ⁠. On the other hand, we can assume that if there is no such world $w_{1}$ in $M_{1}$ ⁠, then $Δ_{1} ⊢ \neg \neg ϕ$ ⁠.¹¹ In that case, we know that $Δ_{2}, \neg \neg θ ⊬ χ$ ⁠; for otherwise, we would have $Δ_{1}, Δ_{2}, ϕ \to θ ⊢ χ$ ⁠, which is impossible. Thus we can require $M_{2}$ to be such that $M_{2} ⊩ \neg \neg θ$ ⁠, and then paste a copy of $M_{2}$ above every node $v_{1}$ in $M_{1}$ where $v_{1} ⊩ ϕ$ ⁠. That can then serve as our model $M_{3}$ ⁠.

For Claim (4) if the MPE $γ_{a} \lor γ_{b}$ occurs in the main subproof, the result follows directly from the i.h. So we just need to show how, when the MPE $γ_{a} \lor γ_{b}$ occurs above the minor premise of the relevant $\to$ E, we can permute this instance of $\to$ E upwards. Suppose that in our permutations, the minor premise $ϕ$ has become the coarsened c-variant $ϕ_{1} \lor . . . \lor ϕ_{m}$ ⁠, so the major premise is $(ϕ_{1} \lor . . . \lor ϕ_{m}) \to θ$ ⁠, with $Π^{'}$ taking the following general form:

Then we permute the

\to

E into each of the

Σ_{i}

’s as follows, where each

θ_{i}, Σ_{0}^{i}, χ_{i}

are distinct reletterings of

θ, Σ_{0}, χ

⁠.

In the proof we started with, we had the MPE

(ϕ_{1} \lor . . . \lor ϕ_{m}) \to θ,

which was a coarsened c-variant of

ϕ \to θ

⁠, itself a coarsening of some formula

σ (ϕ \to θ)

⁠. In the new proof that results from this permutation we now have multiple distinct coarsenings

ϕ_{i} \to θ_{i}

as premises. The result is that instead of the simple conclusion

χ

we now have the disjunction

χ_{1} \lor . . . \lor χ_{m,}

which is a c-variant of a coarsening of

σ χ

⁠.

Lemma 5

If $Π$ is a gaunt coarsened proof of $Δ, ϕ_{1} \lor ϕ_{2} : ψ_{1} \lor ψ_{2}$ ⁠, where the last rule is $\lor$ E with MPE $ϕ_{1} \lor ϕ_{2}$ and main subproofs $Π_{i}$ of $Δ_{i}, ϕ_{i} : ψ_{i}$ ⁠, and if $Δ, \neg \neg (ϕ_{1} \lor ϕ_{2}) ⊢ θ_{1} \lor θ_{2}$ ⁠, then either $Δ_{1} ⊢ \neg ϕ_{1} \lor θ_{1}$ or $Δ_{2} ⊢ \neg ϕ_{2} \lor θ_{2}$ ⁠.

Proof.

First, observe that if $Δ_{1}, Δ_{2}, \neg \neg (ϕ_{1} \lor ϕ_{2}) ⊢ θ_{1} \lor θ_{2}$ ⁠, then also both $Δ_{1}, Δ_{2}, \neg \neg ϕ_{1} ⊢ θ_{1} \lor θ_{2}$ and $Δ_{1}, Δ_{2}, \neg \neg ϕ_{2} ⊢ θ_{1} \lor θ_{2}$ ⁠. Thus, by atom-disjointness and the gaunt validity of the subproofs $Π_{1}$ and $Π_{2}$ ⁠, we know that $Δ_{1}, \neg \neg ϕ_{1} ⊢ θ_{1}$ and $Δ_{2}, \neg \neg ϕ_{2} ⊢ θ_{2}$ ⁠.

Now note that if $Δ_{i} ⊢ \neg ϕ_{i} \lor \neg \neg ϕ_{i} \lor θ_{i}$ ⁠, then also $Δ_{i} ⊢ \neg ϕ_{i} \lor θ_{i}$ ⁠. So if $Δ_{i} ⊬ \neg ϕ_{i} \lor θ_{i}$ ⁠, then there would be a Kripke countermodel $M_{i}$ where $M_{i} ⊩ Δ_{i}$ but $M_{i} ⊮ \neg ϕ_{i}$ and $M_{i} ⊮ \neg \neg ϕ_{i}$ and $M_{i} ⊮ θ_{i}$ ⁠.

Suppose that for both $i = 1$ and $i = 2$ we have $Δ_{i} ⊬ \neg ϕ_{i} \lor θ_{i}$ ⁠. So we have two $M_{i}$ ’s with have a root node $w$ at which $Δ_{i}$ is true but none of $\neg ϕ_{i}, \neg \neg ϕ_{i}, θ_{i}$ are true; and $M_{i}$ will have at least one terminal node $v$ at which $ϕ_{i}$ is true and at least one terminal node $u$ at which $\neg ϕ_{i}$ is true. Pictorially, we have the two models:

And because

Δ_{1}, ϕ_{1}, θ_{1}

is atom-disjoint from

Δ_{2}, ϕ_{2}, θ_{2}

⁠, we can merge these two models together to form a countermodel to

Δ_{1}, Δ_{2}, \neg \neg (ϕ_{1} \lor ϕ_{2}) : θ_{1} \lor θ_{2}

⁠.

Thus, if both

Δ_{1} ⊬ \neg ϕ_{1} \lor θ_{1}

and

Δ_{2} ⊬ \neg ϕ_{2} \lor θ_{2}

⁠, then

Δ, \neg \neg (ϕ_{1} \lor ϕ_{2}) ⊬ θ_{1} \lor θ_{2}

⁠.

Remark 4

Note that after applying the coarsening procedures, instances of $\land$ E and $\to$ E will each only discharge a single leaf node. As a result, it is always permissible to assume that proofs obtained by coarsening have $\land$ - and $\to$ E applied as high as possible. This means that, if $ψ \to ϕ$ or $A \land ϕ$ are MPEs discharging $ϕ$ ⁠, then either the main subproof of this rule is the trivial proof of $ϕ : ϕ$ ⁠, or the main subproof of this rule ends in an E-rule with MPE $ϕ$ ⁠.

Lemma 6

If $Π$ is a gaunt coarsened proof of $Δ, δ : ψ / ⊥$ ⁠, and if $Δ, \neg \neg δ ⊢ ψ / ⊥$ ⁠, then by permuting E-rules we can obtain a gaunt proof $Π^{'}$ in which each such $δ$ occurs above a $⊥$ ⁠.

Proof.

We can assume that $\land$ E and $\to$ E are applied as high as possible, as noted in Remark 4. We argue by induction on the height of $Π$ ⁠. The base case is trivial, and the induction step breaks into the obvious 8 cases.

Case 1: The last rule in $Π$ is $\land$ I. In this case, the claim follows directly from the i.h.

Case 2: The last rule in $Π$ is $\land$ E. Given our assumption that any $\land$ E is applied as high as possible, this case follows immediately from the i.h.

Case 3: The last rule in $Π$ is $\lor$ I. This case also follows directly from the i.h.

Case 4: The last rule in $Π$ is $\lor$ E. Suppose $δ$ is not the MPE of the final $\lor$ E, so that $Π$ is a proof of $Δ_{1}, Δ_{2}, δ, \underset{i}{⋀} ξ_{i} \lor \underset{j}{⋀} ζ_{j} : θ_{1} / θ_{1} \lor θ_{2} / θ_{2}$ ⁠, with the two immediate subproofs $Π_{1}$ of $Δ_{1}, ξ_{1}, . . ., ξ_{n}, δ : θ_{1} / ⊥$ and $Π_{2}$ of $Δ_{2}, ζ_{1}, . . ., ζ_{m} : θ_{2} / ⊥$ ⁠. Without loss of generality, we can suppose that neither of these subproofs ends in $⊥$ ⁠, so that the overall conclusion of $Π$ is $θ_{1} \lor θ_{2}$ ⁠. By assumption, we have that $Δ_{1}, Δ_{2}, \underset{i}{⋀} ξ_{i} \lor \underset{j}{⋀} ζ_{j}, \neg \neg δ ⊢ θ_{1} \lor θ_{2}$ ⁠. Then, since $Π_{1}$ and $Π_{2}$ will be atom-disjoint, it follows that $Δ_{1}, ξ_{1}, . . ., ξ_{n}, \neg \neg δ ⊢ θ_{1}$ ⁠. Now the claim follows from the i.h.

On the other hand, suppose that $δ$ is the MPE $(ξ_{1} \land . . . \land ξ_{n}) \lor (ζ_{1} \land . . . \land ζ_{m})$ ⁠. If both subconclusions of the $\lor$ E are $⊥$ ⁠, then the claim is trivial. So assume we have a subproof $Π_{i}$ ending in $θ_{i}$ ⁠.

First suppose that the subproof $Π_{2}$ ends in $θ_{2}$ and the other subproof $Π_{1}$ ends in $⊥$ ⁠, and $ψ := θ_{2}$ ⁠. Moreover, by Remark 3, we can assume that only one premise is discharged in $Π_{2}$ ⁠, so $m = 1$ ⁠. Also, if $Δ_{1}, Δ_{2}, \neg \neg (⋀ ξ_{i} \lor ζ) ⊢ θ_{2}$ ⁠, then $Δ_{2}, \neg \neg ζ ⊢ θ_{2}$ ⁠, so by the i.h., $ζ$ must occur above a $⊥$ ⁠. So the form of the proof must be:

Now we can permute this

\lor

E upwards to obtain the required proof

Π^{'}

in which

ξ \lor \underset{j}{⋀} ζ_{j}

occurs above a

⊥

⁠:

On the other hand, suppose

Π_{1}

ends in

θ_{1}

and

Π_{2}

ends in

θ_{2}

⁠, so

ψ := θ_{1} \lor θ_{2}

⁠. We can again invoke Remark 3 to assume that there is only one

ζ

discharged. And by Lemma 5, we know that either

Δ_{1} ⊢ \neg (\underset{i}{⋀} ξ_{i}) \lor θ_{1}

Δ_{2} ⊢ \neg ζ \lor θ_{2}

⁠. Without loss of generality, let it be the former. (The argument is substantively similar if it were the latter.)

Now we can apply Lemma 4, to find a proof $Π_{1}^{'}$ that has the general form of the following prooftree. For space and generality, I will, as above, omit MPEs of subsequent $\lor$ E’s in $Π_{1}^{'}$ ⁠, putting in their place a left-label of $\lor$ E on a double-lined inference. Also, I will use $Σ_{i}^{0}$ with a superscript for subproofs with one of the $ξ_{i}$ ’s above it (which will therefore have conclusion $⊥$ ⁠) and I will use $Σ_{i}$ ’s with no superscript for subproofs above one of the subconclusions $χ_{i}$ ’s, where $θ_{1} := χ_{1} \lor . . . \lor χ_{k}$ ⁠.

We can also observe that if

Δ_{1}, Δ_{2}, \neg \neg ((ξ_{1} \land . . . \land ξ_{n}) \lor ζ) ⊢ θ_{1} \lor θ_{2}

⁠, then also

Δ_{1}, Δ_{2}, \neg \neg ξ_{1}, . . ., \neg \neg ξ_{n}, \neg \neg ζ ⊢ θ_{1} \lor θ_{2}

⁠. And since

Π_{1}

and

Π_{2}

will be atom-disjoint, we also know that

Δ_{2}, \neg \neg ζ ⊢ θ_{2}

⁠. So by the i.h., we can find a proof

Π_{2}^{'}

Δ_{2}, ζ : θ_{2}

where

ζ

stands above a

⊥

⁠:

Now, for

i = 1, . . ., n

⁠, let

Π_{2}^{2 i - 1}, Π_{2}^{2 i}, ζ_{i}, θ_{i + 1}

n

distinct reletterings of

Π_{2}^{1}, Π_{2}^{2}, ζ, θ_{2}

⁠; then we can form our desired

Π^{'}

as follows:

Here, in place of the single premise

(ξ_{1} \land . . . ξ_{n}) \lor ζ

which is a coarsened c-variant of some premise

ϕ

from the original proof, we will instead have

n

distinct coarsened c-variants

ξ_{1} \lor ζ_{1}, . . ., ξ_{n} \lor ζ_{n}

as premises. Likewise, instead of having as a conclusion

(ξ_{1} \lor . . . \lor ξ_{n}) \lor θ_{2}

where

ξ_{1}, . . ., ξ_{n}, θ

are each coarsened c-variants of some formula

ψ,

which stood as the conclusion of the original proof we were coarsening, we now have a different coarsened c-variant of

ψ

⁠, namely

θ_{2} \lor χ_{1} \lor . . . \lor θ_{n + 1} \lor χ_{k}

(in some order). The resulting sequent proved, however, is still going to be a coarsened c-variant of the sequent proved by the original proof we started coarsening.

Case 5: The last rule in $Π$ is $\to$ I. First, suppose that the first form of $\to$ I is applied, so that $Π$ is a proof of $Δ, δ : (ϕ_{1} \land . . . \land ϕ_{n}) \to θ$ with an immediate subproof $Π_{0}$ of $Δ, δ, ϕ_{1}, . . ., ϕ_{n} : θ$ ⁠. By hypothesis, we know that $Δ, \neg \neg δ ⊢ (ϕ_{1} \land . . . \land ϕ_{n}) \to θ$ ⁠, and hence $Δ, \neg \neg δ, ϕ_{1}, . . ., ϕ_{n} ⊢ θ$ ⁠. Hence, by the i.h., we can permute rules in $Π_{0}$ to obtain a proof $Π_{0}^{'}$ of $Δ, δ, ϕ_{1}, . . ., ϕ_{n} : θ$ in which $δ$ stands above a $⊥$ ⁠. Then appending an instance of $\to$ I will give the desired proof $Π^{'}$ ⁠.

Next, suppose that the second form of $\to$ I is applied, so that $Π$ is a proof of $Δ, δ : (ϕ_{1} \land . . . \land ϕ_{n}) \to A$ ⁠, where $A$ is a new atom, with an immediate subproof $Π_{0}$ of $Δ, δ, ϕ_{1}, . . ., ϕ_{n} : ⊥$ ⁠. The claim is immediate.

Finally, suppose that the third form of $\to$ I is applied, so that $Π$ is a proof of $Δ, δ : A \to θ$ ⁠, where $A$ is a new atom, with an immediate subproof $Π_{0}$ of $Δ, δ : θ$ ⁠. By assumption, $Δ, \neg \neg δ ⊢ A \to θ$ ⁠; given that $A$ is a new atom, it follows that $Δ, \neg \neg δ ⊢ θ$ ⁠. Now the claim follows from the i.h.

Case 6: The last rule in $Π$ is $\to$ E. As with the $\land$ E case above, the claim follows directly from the i.h. given our assumption that $\to$ E’s are applied as high as possible.

Case 7: The last rule in $Π$ is $\neg$ I. $Π$ has an immediate subproof $Π_{0}$ with conclusion $⊥$ ⁠, so every premise in $Π$ stands above a $⊥$ ⁠.

Case 8: The last rule in $Π$ is $\neg$ E. Then the conclusion of $Π$ itself is $⊥$ ⁠, so every premise stands above a $⊥$ ⁠.

5.2 Proof transformations

We can now provide the proof transformations that will establish claim (3) of the key fact used in the coarsening procedure for $\neg$ I from Section 4.4.

Lemma 7

Suppose we have a gaunt proof $Π$ of $Δ, A : \emptyset$ obtained by the coarsening procedures applied to a proof of $Δ_{o}, ϕ : \emptyset$ ⁠, and suppose that $Δ : \neg A$ is not gauntly valid. Then there is a gaunt proof $Π^{'}$ of $Δ_{c}, A : \emptyset$ such that the final conclusion $⊥$ in the proof descends via a series of E-rules from an instance of $\neg$ E with $\neg A$ and $A$ as premises, and where $Δ_{c}$ consists of coarsenings of c-variants of $Δ_{o}$ ⁠.

Proof.

Clearly $A$ cannot stand as an MPE. By Lemma 2, we know that $A$ only occurs in $Δ$ as its negation $\neg A$ ⁠. But by the subformula property, if $A$ were a premise of an I rule or a minor premise of $\to$ E, then $A$ would occur un-negated as a subformula in $Δ$ ⁠. Thus, $A$ must occur in $Π$ in $\neg$ E:

If the final concluding

⊥

Π

descends from this rule, then we are done. Otherwise, there must be a rule lower down in

Π

with a premise

⊥

descending from this application of

\neg

E and a conclusion

θ

other than

⊥

⁠, so the general form of

Π

is:

Here

Θ

is the MPE where

θ_{n}

is the minor premise.

Furthermore, invoking Remark 3, we can assume that if there are any $\lor$ E below this leaf node $A$ ⁠, then there is only one premise discharged in the subproof containing $A$ ⁠.

Now the argument will proceed by an inductive measure on the branch through the prooftree below $\neg A$ ⁠. Say the nodes in this branch are labeled $\neg A, χ_{1}, χ_{2}, . . ., χ_{k}$ (where, by assumption, we know that both $χ_{1}$ and $χ_{k}$ are $⊥$ ⁠). Then make the following definitions:

Let $c$ be the number of pairs $χ_{i}, χ_{i + 1}$ in this branch such that either $χ_{i} = ⊥$ and $χ_{i + 1} \neq ⊥$ or $χ_{i} \neq ⊥$ and $χ_{i + 1} = ⊥$ ⁠. In other words, $c$ is the number of times the branch in the prooftree below $\neg A$ changes from having a $⊥$ to a formula or vice versa.
Let $n$ be the largest number such that for some $j < n$ ⁠, if $i \leq j$ then $χ_{i} = ⊥$ ⁠, and if $j < i \leq n$ then $χ_{i} \neq ⊥$ ⁠. In other words, $n$ is the length of the branch down to the second block of $⊥$ ’s.
Let $b$ be the largest number $i$ such that $χ_{1}, . . . χ_{i}$ are all $⊥$ ⁠.

Thus, for instance, if the branch below

\neg A

⊥, θ_{1}, θ_{2}, θ_{3}, ⊥, ⊥

⁠, then

c

is 2,

n

is 4, and

b

is 1. If the branch below

\neg A

⊥, ⊥, θ_{1}, ⊥, ⊥, ⊥, ψ_{1}, ψ_{2}, ⊥, ⊥

⁠, then

c

is 4,

n

is 3, and

b

is 2. Now the argument proceeds by induction on the lexicographic ordering of the triple

⟨ c, n, b ⟩

⁠.

There are three possibilities for the rule by which $θ_{1}$ is inferred. (1) There is an application of $\neg$ I. (2) There is an application of $\to$ I. (3) There is an application of $\lor$ with one subconclusion $⊥$ and the other subconclusion $θ$ ⁠. This gives us three main cases to deal with.

Main Cases 1 & 2: $θ_{1}$ is either $\neg (δ_{1} \land . . . \land δ_{k})$ or $(δ_{1} \land . . . \land δ_{k}) \to B$ ⁠, discharging the $δ_{i}$ ’s. Letting $Π_{1}$ be the subproof immediately above $θ_{1}$ ⁠, we know that the last rule in $Π_{1}$ is an E rule, so we can consider the four different E rules that may apply.

First, observe that the last rule of $Π_{1}$ cannot be $\neg$ E; if it were, we would have the following proof:

θ_{1} (\neg A)

may be either

\neg A \to B

\neg \neg A

⁠. Either way, this means that if

Δ^{A}

is the coarsening of

Δ

under the substitution

A \mapsto \neg A

⁠, then

Δ^{A} ⊬ A

⁠. In other words,

Δ : \neg A

is gauntly valid, contrary to the assumptions of the lemma.

So let $R_{1}, . . ., R_{m}$ be the $\lor$ E, $\land$ E, and $\to$ E rules applied between the top $\neg A, A$ instance of $\neg$ -E and the introduction of $θ_{1}$ ⁠. We can further assume that each $R_{i}$ discharges the MPE of $R_{i - 1}$ ⁠; as noted before, we can always assume that $\land$ E and $\to$ E are applied as high as possible; and for any instance of $\lor$ E in this series, because it will only discharge one premise $ϕ$ in the subproof with $A$ and the other subproof will have conclusion $⊥$ ⁠, we can push this instance of $\lor$ E upward to occur immediately below the discharged $ϕ$ ⁠.

Thus, letting $χ_{i}$ be the MPE of $R_{i}$ ⁠, the general form of $Π_{1}$ will be:

Here each

\circ

may any of

\land

⁠,

\lor

⁠, or

\to

⁠. Note that when

\circ

\lor

\to

there will be another subproof above the relevant E-rule, which is not displayed above. If

\circ

\to

⁠, there will be a minor subproof with conclusion

ψ_{i}

⁠, and if

\circ

\lor

there will be a parallel subproof with premise

ψ_{i}

and conclusion

⊥

⁠. We may take

Δ_{i}

to the be the set of premises other than

χ_{i - 1}, A

that are open above the

i^{t h}

E-rule.

Now we can observe that none of the discharged formulas $δ_{i}$ can be $χ_{m}$ ⁠, i.e., $ψ_{m} \circ χ_{m - 1}$ ⁠. For if it were, then by the subformula property, $θ_{1}$ will occur as a subformula in some member of $Δ$ ⁠. Note that $\neg A$ occurs in $χ_{m}$ and hence in $θ_{1}$ ⁠. So by Lemma 1, $A$ does not occur in any other member of $Δ$ ⁠. Thus the only occurrence of $A$ in $Δ^{A}$ is in the coarsened $θ_{1}^{A}$ ⁠, and hence either in the scope of a negation or the antecedent of a conditional, according to whether $θ_{1}$ is $\neg ⋀ δ_{i}$ or $⋀ δ_{i} \to B$ ⁠. In short, we would have $Δ^{A} ⊬ A$ ⁠, contrary to the assumptions of the lemma.

Thus, none of the discharged formulas $δ_{1}, . . ., δ_{k}$ can be the MPE $χ_{m}$ ⁠, but must each occur as premises either in the minor subproof of $\to$ E at some rule $R_{i}$ or in the other subproof of $\lor$ E at some $R_{i}$ ⁠. Now we deal with three possibilities: (A) the last such rule $R_{i}$ is not $R_{m}$ ⁠; (B) the last rule $R_{i}$ is $R_{m}$ ⁠, and is $\lor$ E; or (C) the last rule $R_{i}$ is $R_{m}$ and is $\to$ E. In order to finish the treatment of the Main Cases 1 & 2, it will suffice to show how, in each of these subcases (A), (B), and (C), we can find a permutation that reduces the index $⟨ c, n, b ⟩$ ⁠.

Subcase (A): if the last such rule $R_{i}$ is not $R_{m}$ ⁠, then we can permute the inference of $θ_{1}$ above $R_{m}$ to get:

This lowers the index

b

while leaving

c

and

n

unchanged.

Subcase (B): suppose $R_{m}$ is an instance of $\lor$ E with one or more $δ_{i}$ occurring in the other supbroof. So the general form of $Π_{1}$ is:

We can permuting the inference to

θ_{1} (δ_{i})

into this other subproof, and, if applicable, infer

θ (\underset{j \neq i}{⋀} δ_{j})

in the right hand subproof. This gives us the following proof:

If the inference of

θ_{1}

has only been permuted into the lefthand subproof, then both

n

and

b

will be lowered. If the inference of

θ_{1}

has been permuted into both subproofs as displayed above, then

n

will remain unchanged, but we have a lower index

b

⁠.

Subcase (C): the rule $R_{m}$ is $\to$ E and one or more $δ$ ’s stands in the minor subproof. This case is the most involved, and this is where we will have to appeal to the preliminary lemmas proved in the previous subsection. The overall form of $Π$ will be as follows:

Let

δ_{1}, . . ., δ_{l}

be the discharged

δ_{i}

’s which stand in

Π_{m}

(so then

δ_{l + 1}, . . ., δ_{k}

occur in

Δ_{m - 1}

⁠).

Now, consider the result of tweaking the discharges so that in the uppermost

\neg

A

gets discharged and

\neg A

stands as an open premise, and then uniformly propagating this change through the proof. The result is a proof of

Δ^{A}, \neg A : ⊥

⁠. By assumption, we know that

Δ^{A} ⊢ A

⁠; so by Lemma 3, we can lift this entailment up to the subproof ending in

θ_{1}

⁠. In other words, we know that:

\begin{aligned} Δ_{m}, ψ_{m} \to χ_{m - 1}^{A}, Δ_{m - 1}, \neg θ_{1} ⊢ A \end{aligned}

By assumption,

θ_{1}

is either

\neg (δ_{1} \land . . . \land δ_{k})

(δ_{1} \land . . . \land δ_{k}) \to B

⁠, where

B

is a new atom. Either way, it follows that

\begin{aligned} Δ_{m}, ψ_{m} \to χ_{m - 1}^{A}, Δ_{m - 1}, \neg \neg δ_{1}, . . ., \neg \neg δ_{k} ⊢ A \end{aligned}

Recalling that

δ_{l + 1}, . . ., δ_{k}

are in

Δ_{m - 1}

⁠, this gives us:

\begin{aligned} \neg \neg δ_{1}, . . ., \neg \neg δ_{l}, Δ_{m}, ψ_{m} \to χ_{m - 1}^{A}, Δ_{m - 1} ⊢ A \end{aligned}

Note that

Δ_{m - 1}, \neg \neg χ_{m - 1}^{A} ⊬ A

⁠, because the only occurrence of

A

in the premise set is in the scope of a negation in

\neg \neg χ_{m - 1}^{A}

⁠. So there will be a countermodel

M_{1}

witnessing this invalidity. Now if

Δ_{m}, \neg \neg δ_{1}, . . ., \neg \neg δ_{l} ⊬ ψ_{m}

⁠, then we could piece together a countermodel

M

witnessing:

\begin{aligned} \neg \neg δ_{1}, . . ., \neg \neg δ_{l}, Δ_{m}, ψ_{m} \to χ_{m - 1}^{A}, Δ_{m - 1} ⊬ A \end{aligned}

In brief,

M

would look like this:

But since that contradicts our assumptions, we have that

Δ_{m}, \neg \neg δ_{1}, . . ., \neg \neg δ_{l} ⊢ ψ_{m}

⁠.

Now it follows by Lemma 6 that each of $δ_{1}, . . ., δ_{l}$ stands above a $⊥$ in $Π_{m}$ ⁠. Thus, we can divide $Π_{m}$ into several chunks:

Then we might try to rearrange our overall proof as follows, where each

Σ_{1}^{i}

is a relettered copy of

Σ_{1}

⁠:

The result would be a proof with a lower index

c

⁠. This basic idea behind this permutation will ultimately work. However, executing that idea via this naive rearrangement is too quick; if there were rules in

Σ

that discharged premises in

Π_{m}^{2}

⁠, this naive rearrangement would ruin that. Instead, I will show how we can extract proofs

Σ_{1}, . . ., Σ_{l}

and

Σ_{0}

from the original

Σ

to successfully execute this permutation strategy. What we require of

Σ_{i}

and

Σ_{0}

is that, for each subproof above

θ_{j}

Σ

there are corresponding subproofs

Σ_{i}^{j}

and

Σ_{0}^{j}

such that:

(a) If $θ_{j}$ is a coarsened c-variant of a formula $ϕ_{j}$ ⁠, then the conclusion of $Σ_{i}^{j}$ is also a coarsened c-variant of $ϕ_{j}$ ⁠, and
(b) the conclusion of $Σ_{0}^{j}$ is either $⊥$ or is also a coarsened c-variant of $ϕ_{j}$ ⁠.
(c) The premises of $Σ_{i}^{j} \cup Σ_{0}^{j}$ are in many-one correspondence with the premises of $Σ$ ⁠, where corresponding premises are both coarsened c-variants of the same original formula.
(d) The MPEs of E-rules in $Σ_{i}^{j}$ only discharge formulas in $Π_{m}^{i}$ or $Σ_{i}^{j - 1}$ ⁠, and the MPEs of E-rules in $Σ_{0}^{j}$ discharge formulas outside of each $Π_{m}^{i}$ and $Σ_{i}^{j - 1}$

We work inductively down the thread $θ_{1}, . . ., θ_{n}$ to define $Σ_{i}^{j}$ and $Σ_{0}^{j}$ ⁠. We will have $Σ_{i}^{j}$ and $Σ_{0}^{j}$ as the proofs we have defined at the $j^{t h}$ step, and then set $Σ_{i} := Σ_{i}^{n}$ and $Σ_{0} := Σ_{0}^{n}$ ⁠. We start by letting each $Σ_{i}^{1}$ be the one line proof of $θ_{1} (δ_{i})$ from itself. If $l = k$ ⁠, so that there all the discharged $δ_{i}$ ’s occur in $Π_{m}$ ⁠, then let $Σ_{0}^{1}$ be the null proof. On the other hand, if $l < k$ and there are discharged formulas $δ_{l_{1}}, . . ., δ_{k}$ outside $Π_{m}$ ⁠, then let $Σ_{0}^{1}$ be the one line proof of $θ_{1} (\underset{l < i \leq k}{⋀} δ_{i})$ from itself.

Now consider the $j_{1}^{t h}$ rule. There are 8 possibilities.

Case 1: The $j + 1^{t h}$ rule is $\land$ I. We know $θ_{j}$ will be one premise of the rule, let $ϕ$ be the other premise and $Π_{j}$ the corresponding subproof of $ϕ$ ⁠. If $Π_{j}^{1}, . . ., Π_{j}^{l}$ are distinct releterrings of $Π_{j}$ ⁠, let $Σ_{i}^{j + 1}$ result from applying $\land$ I with the two subproofs $Σ_{i}^{j}$ and $Π_{j}^{i}$ ⁠.

For $Σ_{0}^{j + 1}$ ⁠, if the conclusion of $Σ_{0}^{j}$ is $⊥$ ⁠, then let $Σ_{0}^{j + 1}$ just be $Σ_{0}^{j}$ ⁠. If the conclusion of $Σ_{0}^{j}$ is not $⊥$ ⁠, then we know it must be some $ξ_{j}$ which is also a coarsened c-variant of the original target formula. Then take another relettering $Π_{j}^{0}$ and append an instance of $\land$ I with $Π_{j}^{0}$ to obtain the proof $Σ_{0}^{j + 1}$ of $ξ_{j} \land ϕ_{0}$ ⁠.

Case 2: The $j + 1^{t h}$ rule is $\land$ E. If the discharged premise occurs in $Σ_{i}^{j}$ or $Π_{m}^{i}$ ⁠, then append a corresponding $\land$ E to the bottom of $Σ_{i}^{j}$ to obtain $Σ_{i}^{j + 1}$ ⁠. If the discharged premise occurs outside of $Σ_{i}^{j}$ and $Π_{m}^{1}$ ⁠, then let $Σ_{i}^{j + 1}$ be the same as $Σ_{i}^{j}$ ⁠.

If the discharged premise occurs outside of each $Σ_{i}^{j}$ and $Π_{m}^{1}$ ⁠, append a corresponding instance of $\land$ E to the bottom of $Σ_{0}^{j}$ to obtain $Σ_{0}^{j + 1}$ ⁠; otherwise, let $Σ_{0}^{j + 1}$ be $Σ_{0}^{j}$ ⁠.¹²

Case 3: The $j + 1^{t h}$ rule is $\lor$ I. Let $Σ_{i}^{j + 1}$ result from appending the $i^{t h}$ relettering of this $\lor$ I to the bottom of $Σ_{i}^{j}$ ⁠.

For $Σ_{0}^{j + 1}$ ⁠, if the conclusion of $Σ_{0}^{j}$ is $⊥$ ⁠, then let $Σ_{0}^{j + 1}$ just be $Σ_{0}^{j}$ ⁠. If the conclusion of $Σ_{0}^{j}$ is not $⊥$ ⁠, then we know it must be some $ξ_{j}$ as in Claim (b); then let $Σ_{0}^{j + 1}$ be the result of appending a new $\lor$ I to the bottom of $Σ_{0}^{j}$ ⁠.

Case 4: The $j + 1^{t h}$ rule is $\lor$ E. Suppose $ξ \lor (ζ_{1} \land . . . \land ζ_{t})$ is the MPE, with $θ_{j}$ being the left subconclusion. If $ξ$ occurs as a premise in $Π_{m}^{i}$ or $Σ_{i}^{j}$ ⁠,¹³ then append a relettering of the same instance of $\lor$ E to the bottom of $Σ_{i}^{j}$ to obtain $Σ_{i}^{j + 1}$ ⁠.

For $Σ_{0}^{j + 1}$ ⁠, if $ξ$ occurs as a premise outside of each $Σ_{i}^{j}$ and $Π_{m}^{i}$ ⁠, then append a relettering of the same instance of $\lor$ E to the bottom of $Σ_{0}^{j}$ to obtain $Σ_{0}^{j + 1}$ ⁠. If the conclusion of $Σ_{0}^{j}$ had been $ξ_{j}$ as in Claim (b), then we also know that the conclusion of $Σ_{0}^{j + 1}$ will be $ξ_{j + 1}$ satisfying Claim (b). If the conclusion of $Σ_{0}^{j}$ had been $⊥$ ⁠, then the conclusion of $Σ_{0}^{j + 1}$ will either be $⊥$ or $ξ_{j + 1}$ according to whether the right hand subconclusion was $⊥$ or was a coarsened c-variant of the same target formula as $θ_{j}$ ⁠.

Case 5: The $j + 1^{t h}$ rule is $\to$ I. We know that the premise $θ_{j}$ is not $⊥$ ⁠. If this rule does not discharge a premise, or if it does discharge some premise(s) that occur in some $Σ_{i}^{j}$ or $Π_{m}^{i}$ ⁠, then append the same rule to the bottom of $Σ_{i}^{j}$ to obtain $Σ_{i}^{j + 1}$ ⁠. If the rule does discharge a premise, but not one that occurs in either $Σ_{i}^{j}$ or $Π_{m}^{i}$ ⁠, then for $B$ a new atom, append an instance of $\to$ I to the bottom of $Σ_{i}^{j}$ to obtain a the proof $Σ_{i}^{j + 1}$ of $B \to θ_{j}$ ⁠.

For $Σ_{0}^{j + 1}$ ⁠, if the instance of $\to$ I does discharge premise(s) $ζ_{1}, . . ., ζ_{t}$ outside of each $Σ_{i}^{j}$ and $Π_{m}^{i}$ ⁠, then append to the bottom of $Σ_{0}^{j}$ an instance of $\to$ I discharging the same premise(s). This will give either a proof of $(ζ_{1} \land . . . ζ_{t}) \to ξ_{j}$ or $(ζ_{1} \land . . . \land ζ_{t}) \to B$ ⁠, according to whether the conclusion of $Σ_{0}^{j}$ is $ξ_{j}$ or $⊥$ ⁠. On the other hand, suppose the instance of $\to$ I does not discharge any premises outside of each $Σ_{i}^{j}$ and $Π_{m}^{i}$ ⁠. If the conclusion of $Σ_{0}^{j}$ is $ξ_{j}$ ⁠, append an instance of $\to$ I to infer $B \to ξ_{j}$ ⁠, for $B$ a new atom. If the conclusion of $Σ_{0}^{j}$ is $⊥$ ⁠, then simply let $Σ_{0}^{j + 1}$ be the same as $Σ_{0}^{j}$ ⁠.

Case 6: The $j + 1^{t h}$ rule is $\to$ E. We can let $Σ_{i}^{j + 1}$ result from appending the same $\to$ E to the bottom of $Σ_{i}^{j}$ as applicable, similar to the treatment of $\land$ E in Case 2.

For $Σ_{0}^{j + 1}$ ⁠, if $θ_{j}$ was the subconclusion of this $\to$ ⁠, and if the rule discharges a premise outside of each $Σ_{i}^{j}$ and $Π_{m}^{i}$ ⁠, then append to the bottom of $Σ_{0}^{j}$ an instance of $\to$ to obtain $Σ_{0}^{j + 1}$ ⁠. If $θ_{j + 1}$ was the subconclusion of this $\to$ ⁠, and the rule does not discharge a premise outside of each $Σ_{i}^{j}$ and $Π_{m}^{i}$ ⁠, then simply let $Σ_{0}^{j + 1}$ be the same as $Σ_{0}^{j}$ ⁠. On the other hand, if $θ_{j}$ was the minor premise of this rule and the conclusion of $Σ_{0}^{j}$ is $ξ_{j}$ ⁠, then append a relettered instance of the same $\to$ E to the bottom of $Σ_{0}^{j}$ to obtain $Σ_{0}^{j + 1}$ ⁠. And if $θ_{j}$ was the minor premise of this rule but the conclusion of $Σ_{0}^{j}$ is $⊥$ ⁠, then simply let $Σ_{0}^{j + 1}$ be the same as $Σ_{0}^{j}$ ⁠.

Case 7: The $j + 1^{t h}$ rule is $\neg$ I. This is impossible, because we know that $θ_{j}$ is not $⊥$ ⁠.

Case 8: The $j + 1^{t h}$ rule is $\neg$ E. This can only happen at the $n^{t h}$ rule, since none of $θ_{1}, . . ., θ_{n}$ are $⊥$ s. In this case, append an appropriately relettered $\neg$ E to the bottom of $Σ_{i}^{j}$ to obtain $Σ_{i}^{n}$ (i.e., $Σ_{i}$ ⁠). For $Σ_{0}^{n}$ ⁠, if the conclusion of $Σ_{0}^{n - 1}$ is $⊥$ ⁠, let $Σ_{0}^{n}$ be the same as $Σ_{0}^{n - 1}$ ⁠; and if the conclusion of $Σ_{0}^{n - 1}$ is $ξ_{n - 1}$ ⁠, then append the corresponding instance of $\neg$ E to obtain $Σ_{0}^{n}$ ⁠.

This concludes the definition of $Σ_{i}$ and $Σ_{0}$ ⁠. Now form the proof:

We know that either

Σ_{0}^{1}

was the null proof, in which case

θ_{1}

has been removed from

Σ_{0}

⁠, or that

Σ_{0}^{1}

was the one line proof of

θ_{1} (\underset{l < i \leq k}{⋀} δ_{i})

⁠.

If $Σ_{0}^{1}$ was the null proof, then observe that corresponding to each of $θ_{2}, . . ., θ_{n}$ in $Σ$ ⁠, there will either be a $⊥$ or $ξ_{i}$ in $Σ_{0}$ ⁠, possibly with repetitions. So either: (i) we have reduced the index $c$ in this new proof (if each of $θ_{1}, . . ., θ_{n}$ correspond to $⊥$ s), or we have reduced $n$ (since, even if each $θ_{2}, . . ., θ_{n}$ correspond to formulas $ξ_{1}, . . ., ξ_{n}$ ⁠, the initial occurrence of $θ_{1}$ has been removed and permuted up the proof).

On the other hand, if $Σ_{0}^{1}$ was the one line proof of $θ_{1} (\underset{l < i \leq k}{⋀} δ_{i})$ ⁠, then $c$ and $b$ will remain unchanged and $n$ may have decreased but at any rate will not have increased. But we are now back in Subcase (A) and can apply the permutation from Subcase (A) described above.

This completes the treatment of Main Cases 1 & 2.

Main Case 3: $Π$ has the following general form (recall that we have invoked Remark 3 to assume that any $\lor$ E only discharges a single premise in the subproof with $A$ ⁠):

Let

R_{1}, R_{2}, . . .

be the rules below the

θ

premise in

Π_{3}

⁠. Let

R_{n}

be the first of these rules that is either an I-rule or a

\neg

E or an

\to

E with

θ_{i}

as the minor premise. We know that there must be some such rule, because otherwise there would never be another

⊥

below

θ_{1}

⁠. Provided

R_{n}

is not an instance of

\to

I that discharges either an assumption

δ

from

Δ_{1}

or the MPE

ξ_{1} \lor ⋀ ξ_{2}^{i}

to infer respectively

δ \to θ_{i}

(ξ_{1} \lor ⋀ ξ_{2}^{i}) \to θ_{i}

⁠, we can permute

R_{n}

up above

\lor

E, so that we have the following:¹⁴

R_{n}

has conclusion

θ_{1}^{'} \neq ⊥

⁠, then this gives a proof with smaller index

n

while

c

and

b

are unchanged. On the other hand, if

R_{n}

has conclusion

⊥

(for instance, if it were an instance of

\neg

E with minor premise

θ_{1}

⁠), then the index

c

will have decreased by 2.

As just noted, this permutation works unless (A) $R_{n}$ discharges a premise $δ \in Δ_{1}$ in $\to$ I to infer $δ \to θ^{'}$ or (B) $R_{n}$ discharges $ξ_{1} \lor ⋀ ξ_{2}^{i}$ to infer $(ξ_{1} \lor ⋀ ξ_{2}^{i}) \to θ_{i}$ ⁠.

Subcase (A): In this case we permute $R_{n}$ above the instance of $\lor$ E into both subproofs. In the left subproof we use the version of $\to$ I that refutes the antecedent, and in right subproof we use the version of $\to$ I that derives the consequent without use of the antecedent. This gives the following proof:

Now the conclusion of the

\lor

-E is a c-variant of

δ \to θ^{'}

⁠, and this gets propagated down through the rest of the proof. The indices

c

⁠,

n

⁠, and

b

are all unchanged; but the proof now falls under Main Case 2.

Subcase (B): Here, the argument again gets complicated, but the main ideas are similar to the treatment of the Subcase (C) from the Main Cases (1) & (2) above. To begin with, note that $\neg A$ cannot occur in $ξ_{1} \lor ⋀ ξ_{2}^{i}$ ⁠, because otherwise we would have an occurrence of $\neg A$ in the antecedent of the conditional $(ξ_{1} \lor ⋀ ξ_{2}^{i}) \to θ_{i}$ ⁠; and then the coarsening $Δ^{A}$ that replaced $\neg A$ with $A$ would have $A$ in the antecedent of a conditional, and hence $Δ^{A} ⊬ A$ ⁠. So $ξ_{1} \lor ⋀ ξ_{2}^{i}$ is not an ancestor of the MPE $\neg A$ at the top of the prooftree.

As before, we know the general form of the proof will have a $\neg$ E with premises $\neg A$ and $A$ followed by a series of $m$ elimination rules, with the first MPE $χ_{1}$ discharging $\neg A$ ⁠, and $χ_{i}$ discharging $χ_{i - 1}$ ⁠. Since $ξ_{1} \lor ξ_{2}$ cannot be one of these $χ_{i}$ ’s, we know that $ξ_{1}$ must be occur as a premise either (i) in the $ψ_{m}$ subproof of $\lor$ E where the MPE is $χ_{m - 1} \lor ψ_{m}$ or (ii) in a minor subproof of $\to$ E, with MPE $ψ_{m} \to χ_{m - 1}$ ⁠.

Take first the possibility (i) that

ξ_{1}

occurs above an

\lor

E. We can assume that the

ξ_{1} \lor ξ_{2}

occurrence of

\lor

E is applied as high as possible, so that the general form of the proof will be

Now by permuting the

ξ_{1} \lor ⋀ ξ_{2}^{i}

premise upwards we get the following proof, which has a lower index

n

and

b

while

c

is unchanged:

Take now the possibility (ii) that

ξ_{1}

occurs in a minor subproof of

ψ_{m}

in a

\to

E with MPE

ψ_{m} \to χ_{m - 1}

⁠. Then the general form of proof will be:

Now, by Lemma 3, where

Δ_{m - 1}

is the set of premises above the rule with MPE

χ_{m - 1}

⁠, we know that:

\begin{aligned} \neg ((ξ_{1} \lor ⋀ ξ_{2}^{i}) \to θ_{1}), Γ_{2}, Δ_{m}, Δ_{m - 1}, ψ_{m} \to χ_{m - 1}^{A} ⊢ A \end{aligned}

And since

\neg \neg ξ_{1}, \neg θ ⊢ \neg ((ξ_{1} \lor ⋀ ξ_{2}^{i}) \to θ)

⁠, this gives us:

\begin{aligned} \neg \neg ξ_{1}, \neg θ, Δ_{m}, Δ_{m - 1}, ψ_{m} \to χ_{m - 1}^{A} ⊢ A \end{aligned}

So by atom-disjointness:

\begin{aligned} \neg \neg ξ_{1}, Δ_{m}, Δ_{m - 1}, ψ_{m} \to χ_{m - 1}^{A} ⊢ A \end{aligned}

And then, by an argument similar to that from Subcase (C) above, it follows that

\begin{aligned} \neg \neg ξ_{1}, Δ_{m - 1} ⊢ ψ_{m} \end{aligned}

So by Lemma 6,

ξ_{1}

must occur above a

⊥

somewhere in

Π_{1}

⁠:

With this in hand, I claim that we can inductively extract two proofs

Σ_{1}

and

Σ_{2}

from

Σ,

which allow us to form the following proof:

The inductive definition of

Σ_{1}

and

Σ_{2}

here is similar to the definition of the proofs

Σ_{i}

and

Σ_{0}

from before, so I will omit the details. The most important thing to note is that, where

Σ

had a premise

θ_{1}

⁠, this has been replaced by a

⊥

Σ_{2}

⁠. And because of this,

Σ_{2}

occurs immediately below the

\to

E. So as a result, both

n

and

b

will have been decreased while the index

c

is unchanged. This completes the treatment of Subcase (B), and thus of Main Case 3 and the proof.

6 Negation Elimination

I turn now to the treatment of proofs that end in $\neg$ -E. Similar to above, the first task is to characterize when the result of adding $\neg$ -E to a proof might not preserve gauntness. We will want to pay particular attention to the structure of the proof in question. The asymmetry between premises and conclusions in intuitionistic logic makes the treatment of $\neg$ -E importantly different from the treatment of $\neg$ -I. An application of $\neg$ -E can require coarsening not only literals but also more complex formulas. For instance, while both $\neg \neg \neg A : \neg A$ and $\neg \neg (A \to \neg B) : A \to \neg B$ are gauntly valid, an application of $\neg$ -E would respectively give proofs of $\neg \neg \neg A, \neg \neg A : \emptyset$ and $\neg \neg (A \to \neg B), \neg (A \to \neg B) : \emptyset$ ⁠. Neither of these sequents are gauntly valid, since they can both be coarsened to $\neg C, C : \emptyset$ ⁠.

Lemma 8

Suppose that $Π$ is a coarsened gaunt proof of $Δ : (ψ_{1} \land . . . \land ψ_{k}) \to θ$ ⁠, where $(ψ_{1} \land . . . \land ψ_{k}) \to θ$ is obtained via the form of $\to$ -I that derives $θ$ and discharges $ψ_{1}, . . ., ψ_{k}$ ⁠, but that $Δ, \neg ((ψ_{1} \land . . . \land ψ_{k}) \to θ) : \emptyset$ has the valid coarsening $Δ^{'}, \neg A : \emptyset$ ⁠. Then $k = 1$ and $ψ_{1} \to θ$ is of the form $A_{1} \to (A_{2} \to (. . . \to (A_{n} \to \neg B) . . .)$ ⁠.

Proof.

The general form of $Π$ will be as follows:

First we want to show that

k = 1

and

ψ_{1}

must be an atom

A_{1}

⁠. Since

Π

is gaunt and we have a subproof of

Δ_{0}, Δ_{1}, Δ_{2}^{d}, ψ_{1}, . . ., ψ_{k} : θ

⁠, this sequent will be gauntly valid. Because the overall sequent has the valid coarsening

Δ^{'}, \neg A : ⊥

⁠, we know that

\underset{i}{⋀} ψ_{i} \to θ

must occur in

Δ

⁠. Further, we know from Lemma 1 that the only occurrence of the

ψ_{i}

’s, or of any atoms in the

ψ_{i}

’s, in

Δ_{0}, Δ_{1}, Δ_{2}^{d}

will be in this form

⋀ ψ_{i} \to θ

⁠. Let

Δ_{0}^{'}, Δ_{1}^{'}, {Δ_{2}^{d}}^{'}

be the result of coarsening

ψ_{1} \land . . . \land ψ_{k}

to a new atom

A

⁠. Then, if

M

is any model that makes

ψ_{1} \land . . . \land ψ_{k}

true at exactly the same worlds

w

as those where this atom

A

is true, then

M

will also assign

Δ_{0}, Δ_{1}, Δ_{2}^{d}

the same value as

Δ_{0}^{'}, Δ_{1}^{'}, {Δ_{2}^{d}}^{'}

⁠; so any countermodel witnessing

Δ_{0}^{'}, Δ_{1}^{'}, {Δ_{2}^{d}}^{'}, A ⊬ θ

would also be a countermodel witnessing

Δ_{0}, Δ_{1}, Δ_{2}^{d}, ψ_{1} \land . . . \land ψ_{k} ⊬ θ

⁠. In other words, if

Δ_{0}, Δ_{1}, Δ_{2}^{d}, ψ_{1} \land . . . \land ψ_{k} ⊢ θ

⁠, then

Δ_{0}^{'}, Δ_{1}^{'}, {Δ_{2}^{d}}^{'}, A ⊢ θ

⁠. Thus,

Δ_{0}^{'}, Δ_{1}^{'}, {Δ_{2}^{d}}^{'} : A \to θ

would be a valid proper coarsening of

Δ_{0}, Δ_{1}, Δ_{2}^{d} : ψ_{1} \land . . . \land ψ_{k} \to θ

unless

ψ_{1} \land . . . \land ψ_{k}

was an atom

A_{1}

⁠.

Now, work up from the root of $Π$ until you find the place where $θ$ is first introduced. For brevity, let $Γ$ be the set of undischarged premises above this inference, and note that $ψ \to θ$ must occur in some member of $Γ$ ⁠. Otherwise, $ψ \to θ$ would have to occur as an MPE with either $ψ \to θ$ as the main subconclusion or $θ$ as the main subconclusion and a $\to$ I inferring $ψ \to θ$ lower down the prooof; either way this contradicts the assumption that $Π$ was obtained by coarsening.

A priori, the rule that introduces $θ$ could be either an I-rule, or the modified $\lor$ E rule, or $θ$ could be a leafnode. But we know that $θ$ cannot be introduced by $\land$ I or the modified $\lor$ E because the two parallel subproofs have to be atom-disjoint, and that would be impossible because we know that $ψ \to θ$ occurs in $Γ$ ⁠. Likewise, it cannot be $\lor$ I, because one disjunct would be a new atom. If $θ$ descended from a leafnode, it would have to be as the main subconclusion of an E-rule; moreover, because $θ$ can only occur in the context of $A_{1} \to θ$ ⁠, this rule would have to be $\to$ E, with minor premise $A_{1}$ ⁠. But in that case the coarsening procedure for $\to$ I would have led not to $Δ : ψ \to θ$ ⁠, but to some coarsening $Δ_{C} : C$ ⁠. (Refer to Case (C) in the coarsening procedure for $\to$ I in Section 4.3.) So the rule that introduces $θ$ can only be $\neg$ I or $\to$ I.

Suppose first that $θ$ is $\neg χ$ ⁠, obtained by $\neg$ I, so we have a gaunt subproof of $Γ, ψ, χ : \emptyset$ ⁠. We know that $Γ, \neg (ψ \to \neg χ) : \emptyset$ has a valid coarsening $Γ^{'}, \neg A : \emptyset$ ⁠. Hence, $Γ^{'} [A / ψ \to \neg B], \neg (ψ \to \neg B) : \emptyset$ is valid. Thus $Γ^{'} [A / ψ \to \neg B], ψ, \neg \neg B : \emptyset$ is valid and, hence, so is $Γ^{'} [A / ψ \to \neg B], ψ, B : \emptyset$ ⁠. But this would be a proper coarsening of $Γ, ψ, χ : \emptyset$ ⁠, unless $χ$ was an atom.

On the other hand, suppose $θ$ is obtained by $\to$ I. Then neither the antecedent nor consequent can be a new atom, so it must be $χ \to ξ$ ⁠, obtained by deriving $ξ$ and discharging $χ$ ⁠. So we have a gaunt proof of $Γ, ψ, χ : ξ$ ⁠. We also know that $Γ, \neg (ψ \to (χ \to ξ)) : \emptyset$ can be coarsened to $Γ^{'}, \neg A : \emptyset$ ⁠. Now, as a substitution instance, it follows that $Γ^{'} [A / ψ \to B], \neg (ψ \to B) : \emptyset$ is valid, and hence that $Γ^{'} [A / ψ \to B], ψ, \neg B : \emptyset$ is valid. But this is a valid coarsening of $Γ, ψ, \neg (χ \to ξ) : \emptyset$ ⁠. Now we iterate the argument as applies to the conclusion $ξ$ in the subproof.

Corollary 1

Suppose $Π$ is as in the previous lemma. Then the following proof $Π_{1}$ occurs as a subproof somewhere at the top of $Π$ ⁠:

The open occurrence of

A_{1} \to (A_{2} \to . . . (A_{n} \to \neg B) . . .)

will be discharged somewhere in

Π

⁠. And (possibly after permuting some E-rules) the bottom

n + 1

steps of

Π

are as follows, with each inference respectively discharging

B, A_{n}, . . ., A_{1}

from

Π_{1}

⁠:

Proof.

In light of Lemma 8 and the assumptions of the claim, it follows that $Π$ will end with a series of $\to$ -I’s, possibly interspersed with E-rules, of which the formulas $A_{i} \to (. . . \to \neg B)$ are the main subconclusions. Since these formulas are all main subconclusions, and the discharges of the $\to$ -I’s and the E-rules will not conflict, the E-rules can be permuted upward to precede the $\to$ -I’s.

We know by Lemma 1 that each $A_{i}$ only occurs in the premise set $Δ$ as $A_{i} \to (A_{i + 1} \to . . .)$ ⁠. And by the proof of Lemma 8 we know that $Π$ has a subproof of $⊥$ with open premises $A_{1}, . . ., A_{n}, B$ ⁠. Moreover, $A_{1}, . . ., A_{n}$ must figure as minor premises for $\to$ -E; otherwise, they would occur as subformulas in a context other than $A_{1} \to (A_{2} \to . . . (A_{n} \to \neg B))$ ⁠.

Putting these facts together, we know that each $A_{i}$ will stand undischarged as the minor premise of $\to$ -E, which determines the form of $Π_{1}$ until the we get to main subproof of $A_{n} \to \neg B$ ⁠. The discharged premise $\neg B$ must connect with another occurrence of $B$ ⁠. But we know that $B$ must occur as an undischarged premise, and that there are no other instances of $B$ in $Δ$ aside from $A_{1} \to (. . . \to A_{n} \to \neg B)$ ⁠, the only rule that can be applied in this subproof is an instance of $\neg$ -E where the minor premise $B$ is undischarged in $Π$ ⁠.

One more technical lemma is needed before we can put all the pieces together to define our coarsening procedure for negation elimination.

Lemma 9

Suppose $Π$ is a gaunt coarsened proof of $Δ : ϕ$ ⁠, but that $Δ, \neg ϕ : \emptyset$ can be coarsened to the valid sequent $Δ^{'}, (\neg ϕ)^{'} : \emptyset$ under the substitution $σ$ ⁠. Then:

If $B_{1}, . . ., B_{m}$ are the atoms changed by $σ$ ⁠, then $B_{1}, . ., B_{m}$ occur either in $(\neg ϕ)^{'}$ or in some $ψ^{'}$ ⁠, where $ψ$ occurs as the minor premise of $\to$ -E in $Π$ ⁠; and
$σ (B_{i})$ will either be a formula $χ_{i}$ or $\neg χ_{i}$ ⁠, with the latter case only when $\neg χ_{i} = \neg ϕ$ ⁠, and where $χ_{i}$ is one of the following forms:
- (a) $χ_{i}$ is $\neg A_{i}$ and the occurrence of $\neg A_{i}$ in $ϕ$ or $ψ$ descends from an application of $\neg$ -I in $Π$ ⁠; or
- (b) $χ_{i}$ is of the form $C_{1} \to (C_{2} \to . . . (C_{n} \to \neg D))$ or $\neg (C_{1} \to (C_{2} \to . . . (C_{n} \to \neg D)))$ ⁠, and the occurrence of $χ_{i}$ in $ϕ$ or $ψ$ descends from a subproof of the form specified in Corollary 1.

Proof.

Both claims can be proved simultaneously by induction on the height of $Π$ ⁠. The basis step is trivial. For the induction step, we have the obvious series of cases.

Case 1: The last rule in $Π$ cannot be $\neg$ -E, by the hypotheses of the lemma.

Case 2: Suppose we have a gaunt coarsened proof of $Δ : \neg (θ_{1} \land . . . \land θ_{k})$ where the last rule is $\neg$ -I. Now, $Δ : \neg (θ_{1} \land . . . \land θ_{k})$ is valid iff $Δ, \neg \neg (θ_{1} \land . . . \land θ_{k}) : \emptyset$ is valid. So if $Δ, \neg \neg (θ_{1} \land . . . \land θ_{k}) : \emptyset$ is not gauntly valid, it must be that there is a coarsening $Δ^{'}, A : \emptyset$ or $Δ^{'}, \neg A : \emptyset$ ⁠. First, I want to show that $A$ is the only atom changed by $σ$ ⁠. Let $S = {C_{1}, . . ., C_{k}}$ be the set of atoms other than $A$ changed by $σ$ ⁠, and let $Δ_{S}$ be the image of $Δ^{'}$ under $σ ↾ {A}$ ⁠. Evidently $Δ_{S}, \neg \neg (θ_{1} \land . . . \land θ_{k}) : \emptyset$ is valid, hence so is $Δ_{S} : \neg (θ_{1} \land . . . \land θ_{k})$ ⁠. But if $S$ were non-empty, this would be a valid proper coarsening of $Δ : \neg (θ_{1} \land . . . \land θ_{k})$ ⁠, contradicting the fact that $Π$ is gaunt.

Now I would like to argue that $(θ_{1} \land . . . \land θ_{k})$ must be an atom (and so $k = 1$ ⁠). Let $σ : A \mapsto \neg_{i} (θ_{1} \land . . . \land θ_{k})$ ⁠, where $i \in {1, 2}$ ⁠, so that $σ (Δ^{'}) = Δ$ ⁠. Obviously we can decompose $σ$ into $σ_{1} : A \mapsto \neg_{i} B$ and $σ_{2} : B \mapsto (θ_{1} \land . . . \land θ_{k})$ ⁠. Clearly $σ_{1} (Δ^{'}), \neg \neg B : \emptyset$ is valid, hence $σ_{1} (Δ^{'}) : \neg B$ is valid, which would be a valid coarsening of $Δ : \neg ϕ$ under $σ_{2}$ ⁠. So $σ_{2}$ must be a mere relettering, and hence $k = 1$ and $(θ_{1} \land . . . \land θ_{k})$ is an atom.

Case 3: suppose that the last rule is $\to$ -I. First consider the form where $ψ$ is derived from $θ_{1}, . . ., θ_{k}$ ⁠, and then the $θ_{i}$ ’s are discharged to infer $(θ_{1} \land . . . \land θ_{k}) \to ψ$ ⁠. If there is a coarsening of the form $Δ^{'}, \neg_{i} A : \emptyset$ ⁠, where $i \in {0, 1}$ ⁠, then the fact that $σ (A)$ has the required form follows from Corollary 1. Concerning any other atoms $B$ that are changed by $σ$ ⁠, note that if we have a valid coarsening $Δ^{'}, \neg_{i} A : \emptyset$ ⁠, then we also have a valid coarsening of the form $Δ^{'}, \neg (θ_{1} \land . . . \land θ_{k})^{'} \to ψ^{'}) : \emptyset$ ⁠. In this case, $Δ^{'}, (θ_{1} \land . . . \land θ_{k})^{'}, \neg ψ^{'} : \emptyset$ would also be valid, and the claim follows by the i.h.

On the other hand, suppose that $Δ : (θ_{1} \land . . . \land θ_{k}) \to B$ is deduced from a subproof of $Δ, θ_{1}, . . ., θ_{k} : \emptyset$ ⁠. Since $B$ is a new atom, a coarsening of $Δ, \neg ((θ_{1} \land . . . \land θ_{k}) \to B) : \emptyset$ would have to be of the form $Δ^{'}, \neg ((θ_{1} \land . . . \land θ_{k})^{'} \to B) : \emptyset$ ⁠. But, since $B$ is a new atom, this can be valid only if $Δ^{'} ⊢ \neg (θ_{1} \land . . . \land θ_{k})^{'}$ ⁠. Now consider the various forms the coarsened formula $(θ_{1} \land . . . \land θ_{k})^{'}$ might take. Let $σ$ be substitution under which this coarsening is obtained.

Suppose there is some $i < k$ such that $(θ_{1} \land . . . \land θ_{k})^{'}$ is of the form $θ_{1}^{'} \land . . . \land θ_{i - 1}^{'} \land C$ ⁠, so that $σ : C \mapsto θ_{i} \land . . . \land θ_{k}$ ⁠.¹⁵ Then $θ_{i}, . . ., θ_{k}$ must be atoms $A_{i}$ ⁠, for otherwise we could decompose $σ$ into two non-trivial substitutions $σ_{1} : C \mapsto A_{i} \land . . . \land A_{k}$ and $σ_{2} : A_{i} \mapsto θ_{i}$ ⁠. In that case, $σ_{1} (Δ^{'}) : (θ_{1}^{'} \land . . . \land θ_{i - 1}^{'} \land A_{i} \land . . . \land A_{k}) \to B)$ would be a valid proper coarsening of $Δ : (θ_{1} \land . . . \land θ_{k}) \to B$ ⁠, which is impossible. So we know that $θ_{i}, . . ., θ_{k}$ are all atoms $A_{i}, . . ., A_{k}$ ⁠, and furthermore the conjunction $A_{i} \land . . . \land A_{k}$ must occur in $Δ$ ⁠. By Proposition 1, then, we know that this will be the only place in $Δ$ that $A_{i}, . . ., A_{k}$ can appear. Thus, by the subformula property, $A_{i}, . . ., A_{k}$ can only occur in $Π$ in a series of $\land$ I rules. But this is impossible, since it would conflict with Case (B) of the coarsening procedure for $\to$ I.
On the other hand, if there is no such $i$ ⁠, then the coarsening $(θ_{1} \land . . . \land θ_{k})^{'}$ will be of the form $θ_{1}^{'} \land . . . \land θ_{k}^{'}$ ⁠. But then we would have that $Δ^{'} ⊢ \neg (θ_{1}^{'} \land . . . \land θ_{k}^{'})$ ⁠; hence $Δ^{'}, θ_{1}^{'}, . . ., θ_{k}^{'} : \emptyset$ would be a valid proper coarsening of $Δ, θ_{1}, . . ., θ_{k} : \emptyset$ ⁠, which is impossible.

This completes the treatment of the second form of

\to

For the third form, suppose $Δ : B \to ψ$ is deduced from a subproof of $Δ : ψ$ ⁠. Since $B$ is a new atom, a coarsening of $Δ, \neg (B \to ψ) : \emptyset$ would have to be of the form $Δ^{'}, \neg (B \to ψ^{'}) : \emptyset$ ⁠. Then because $B$ is a new atom, this is valid only if $Δ^{'}, \neg ψ^{'} : \emptyset$ is valid, and we apply the i.h.

Case 4: Suppose now that the last rule is $\to$ -E, so we have a proof:

Suppose there is a valid proper coarsening

Δ_{1}^{'}, Δ_{2}^{'}, (ψ \to θ)^{'}, (\neg ϕ)^{'} : \emptyset

⁠. Since

Π_{1}

and

Π_{2}

will be atom-disjoint, this coarsening must be of the form

Δ_{1}^{'}, Δ_{2}^{'}, ψ^{'} \to θ^{'}, (\neg ϕ)^{'} : \emptyset

⁠. Now,

Δ_{1}^{'}

and

ψ^{'}

will only be properly coarsened if

Δ_{1}^{'}, \neg ψ^{'} : \emptyset

is valid; otherwise, we could piece together models of

Δ_{1}^{'}, \neg ψ^{'}

and

Δ_{2}^{'}, (\neg ϕ)^{'}

to create a countermodel to

Δ_{1}^{'}, Δ_{2}^{'}, ψ^{'} \to θ^{'}, (\neg ϕ)^{'} : \emptyset

⁠. Thus,

Δ_{1}^{'}

and

ψ^{'}

are proper coarsenings only if

Δ_{1}^{'}, \neg ψ^{'} : \emptyset

is a valid proper coarsening of

Δ_{1}, \neg ψ : \emptyset

⁠. So we may apply the i.h. to

Π_{1}

⁠. Furthermore, because

Δ_{1}, ψ

is atom-disjoint from

Δ_{2}, θ, ϕ

⁠, we know that

Δ_{2}^{'}, θ^{'}, (\neg ϕ)^{'} : \emptyset

must be valid, so we may also apply the i.h. to

Π_{2}

⁠.

Case 5: suppose the last rule in $Π$ is $\land$ -I, so we have:

Since

Π_{1}

and

Π_{2}

are atom-disjoint,

ψ \land θ

cannot be among the premises of

Δ

⁠. So if

Δ, \neg (ψ \land θ) : \emptyset

had a valid coarsening, it would have to be of the form

Δ^{'}, \neg (ψ^{'} \land θ^{'}) : \emptyset

⁠. Without loss of generality, we can suppose we have a valid coarsening of the form

Δ_{1}^{'}, Δ_{2}, \neg (ψ^{'} \land θ) : \emptyset

⁠, with

ψ^{'}

a coarsening of

ψ

⁠. Evidently, then,

Δ_{1}^{'}, \neg ψ^{'} : \emptyset

is valid and is a proper coarsening of

Δ_{1}, \neg ψ : \emptyset

⁠. The claim then follows from the i.h.

Case 6: suppose the last rule in $Π$ is $\land$ -E, so we have:

Since

Π

is obtained by coarsening, we know that

C

is a new atom. Thus a coarsening

Δ^{'}, (ψ \land C)^{'}, \neg ϕ^{'} : \emptyset

would induce a similar coarsening

Δ^{'}, ψ^{'}, \neg ϕ^{'} : \emptyset

⁠. Then the claim follows from the i.h.

Case 7: suppose the last rule in $Π$ is $\lor$ -I. Since this is a coarsened proof, the newly introduced disjunct will be a new atom. So any coarsening of $Δ, \neg (ψ \lor C) : \emptyset$ will induce a corresponding coarsening of $Δ, \neg ψ : \emptyset$ ⁠, and the claim follows from the i.h.

Case 8: suppose the last rule in $Π$ is $\lor$ -E, so we have a proof of $Δ, (ψ_{1} \land . . . \land ψ_{k}) \lor (θ_{1} \land . . . \land θ_{l}) : ϕ$ ⁠. The case of uniform $⊥$ conclusion does not apply. If the subproof $Π_{2}$ below the $θ_{i}$ ’s has conclusion $⊥$ ⁠, and we have a conclusion $ϕ$ descending from the $ψ_{i}$ ’s in subproof $Π_{1}$ ⁠, then, since the two subproofs will be atom-disjoint, any coarsening $Δ_{1}^{'}, Δ_{2}^{'}, ((ψ_{1} \land . . . \land ψ_{k}) \lor (θ_{1} \land . . . \land θ_{l}))^{'}, \neg ϕ^{'} : \emptyset$ would correspond to a coarsening $Δ_{1}^{'}, (ψ_{1} \land . . . \land ψ_{k})^{'}, (\neg ϕ)^{'} : \emptyset$ or $Δ_{2}^{'}, (θ_{1} \land . . . \land θ_{l})^{'} : \emptyset$ ⁠. Take each of the two subproofs in turn:

Focus on $Π_{2}$ ⁠. If $(θ_{1} \land . . . \land θ_{l})^{'}$ were a non-trivial coarsening, then we would have $Δ_{1}^{'} ⊢ \neg (θ_{1} \land . . . \land θ_{l})^{'}$ ⁠. But the same argument as we used in the second form of $\to$ I shows that this is impossible. So a proper $Δ_{2}^{'}, (θ_{1} \land . . . \land θ_{l})^{'} : \emptyset$ would have to take the form $Δ_{2}^{'}, (θ_{1}^{'} \land . . . \land θ_{l}^{'}) : \emptyset$ ⁠; but this conflicts with the assumption that $Δ_{2}, θ_{1}, . . ., θ_{l} : \emptyset$ is gauntly valid.
Now consider $Π_{1}$ ⁠. The argument is largely similar: suppose that we have $Δ_{1}^{'}, (ψ_{1} \land . . . \land ψ_{k})^{'}, (\neg ϕ)^{'} : \emptyset$ ⁠. Now, if the coarsening of $(ψ_{1} \land . . . \land ψ_{k})^{'}$ is of the form $ψ_{1}^{'} \land . . . \land ψ_{k}^{'}$ ⁠, then the claim follows by the i.h. On the other hand, suppose that the coarsening of $(ψ_{1} \land . . . \land ψ_{k})^{'}$ is of the form $ψ_{1}^{'} \land . . . \land ψ_{i - 1}^{'} \land C$ ⁠, with $C \mapsto ψ_{i} \land . . . \land ψ_{k}$ ⁠. Then, arguing as above, we know that $ψ_{i}, . . ., ψ_{k}$ must be atoms $A_{i}, . . ., A_{k}$ ⁠; and the conjunction $A_{i} \land . . . \land A_{k}$ must occur somewhere else in $Δ_{1}, ϕ$ ⁠; and thus the only way that $A_{i}, . . ., A_{k}$ can figure in the proof $Π$ is as premises in successive $\land$ I’s. But that is ruled out by Case (B) of the coarsening procedure for $\lor$ E. So a valid proper coarsening $Δ_{1}^{'}, (ψ_{1} \land . . . \land ψ_{k})^{'}, (\neg ϕ)^{'} : ⊥$ would have to be of the form $Δ_{1}^{'}, (ψ_{1}^{'} \land . . . \land ψ_{k}^{'}), (\neg ϕ)^{'} : ⊥$ ⁠. This obviously gives us a valid proper coarsening $Δ_{1}^{'}, ψ_{1}^{'}, . . ., ψ_{k}^{'}, (\neg ϕ)^{'} : ⊥$ ⁠, and so the claim follows by the i.h.

On the other hand, suppose neither conclusion is

⊥

⁠, so we have a proof of the following form, using the modified

\lor

-E rule:

Again,

Π_{1}

and

Π_{2}

are atom-disjoint, so in the sequent

Δ, (ψ_{1} \land . . . \land ψ_{k}) \lor (θ_{1} \land . . . \land θ_{l}) : ϕ_{1} \lor ϕ_{2}

⁠, neither

(ψ_{1} \land . . . \land ψ_{k}) \lor (θ_{1} \land . . . \land θ_{l})

nor

ϕ_{1} \lor ϕ_{2}

can be coarsened to an atom

B

⁠. As a result, any coarsening of this sequent will induce coarsenings of

Δ_{1}, (ψ_{1} \land . . . \land ψ_{k}) : ϕ_{1}

and

Δ_{2}, (θ_{1} \land . . . \land θ_{l}) : ϕ_{2}

⁠, and we argue like we did for

Π_{1}

just above.

And now we can show how to find gaunt proofs that end in $\neg$ -E:

Lemma 10

Suppose that there is a gaunt coarsened proof $Π$ of $Δ : ϕ$ ⁠, but that $Δ, \neg ϕ : \emptyset$ has a valid proper coarsening $Δ^{'}, (\neg ϕ)^{'} : \emptyset$ ⁠. Then by permuting rules in $Π$ ⁠, we can obtain a gaunt coarsened proof $Π^{'}$ of $Δ_{c}^{'}, \neg ϕ_{c}^{'} : \emptyset$ ⁠, which is also a coarsened c-variant of the original target sequent.

Proof.

If $σ$ is the substitution under which $Δ, \neg ϕ : ⊥$ gets coarsened, and $B_{1}, . . ., B_{n}$ are the atoms changed by $σ$ ⁠, then we know from Lemma 9 that each $σ (B_{i})$ will either be $\neg A$ or $C_{1}^{i} \to (C_{2}^{i} \to . . . \to \neg D^{i})$ ⁠, or, in the case where $σ (B_{i}) = \neg ϕ$ ⁠, this will either be $\neg \neg A_{i}$ or $\neg (C_{1}^{i} \to (C_{2}^{i} \to . . . \to \neg D^{i})$ ⁠. We also know from Lemma 9 that each $σ (B_{i})$ will either occur in $ϕ^{'}$ or in the minor premise of some $\to$ E in $Π$ ⁠. In either case, then, if $ψ^{'}$ is a formula in which some $B$ occurs, then there will be some (not necessarily proper) subproof $Π_{0}$ of $Π$ such that $Π_{0}$ is a gaunt coarsened proof of $Δ_{0} : ψ$ but $Δ_{0}, \neg ψ$ is not gauntly valid. $Π_{0}$ is of course either $Π$ itself, in which case $ψ$ is just $ϕ$ ⁠, or is a minor subproof above an instance of $\to$ E, in which case $ψ$ is the minor premise.

We already know from Corollary 1 what general form $Π_{0}$ will take when there is some $χ := C_{1} \to (C_{2} \to . . . \to \neg B)$ occurring in $ψ$ ⁠. We can also observe the general form $Π_{0}$ must have when there is some $\neg A$ in $ψ$ ⁠. From Lemma 9, we know that $\neg A$ descends from an instance of $\neg$ -I. So $A$ occurs as a leaf-node somewhere in $Π$ ⁠. Now, if this leaf-node were a premise in an I-rule or a minor premise of $\to$ -E, then conclusion of that I-rule or the MPE of $\to$ -E would be a formula $A \circ ξ$ ⁠, which would then be a subformula in $Δ$ ⁠. But if $\neg A$ gets coarsened to $A$ in $Δ^{'}$ ⁠, then every occurrence of $A$ in $Δ$ must be immediately in the scope of a negation. So the leaf-node occurrence of $A$ must be a minor premise for $\neg$ E. Thus, $Π_{0}$ must have the following form:

We can observe that in either case, for formulas

\neg A_{i}

χ_{i}

⁠,

Π_{0}

must fit the following general pattern:

If the top left leaf-node is

A

⁠, then it is a minor premise in

\neg

E, and the major premise

\neg A

is discharged somewhere in

Π_{1}

⁠;

A

itself is discharged in the

\neg

I at the bottom of

Π_{1}

⁠. If the top left leaf-node is

χ

⁠, then the

⊥

comes from a series of

\to

E rules as indicated in Corollary 1,

χ

will be discharged somewhere in

Π_{1}

⁠, and the

χ

occurring at the conclusion of

Π_{1}

is obtained by a series of

\to

I’s.

So we have two key chunks in the overall proof: there is the $Π_{1}$ portion, which takes us from one $⊥$ to another $⊥$ ⁠, and then there is the $Π_{2}$ portion, which takes us from $\neg A / χ$ to $ψ (\neg A / χ)$ ⁠. I will show how we can systematically find corresponding $Σ_{1}$ and $Σ_{2}$ such that the following is a gaunt coarsened proof as required by the lemma:

I argue by induction on the height of

Π

⁠.

For the basis step, $Π_{2}$ may be a trivial one line proof, but we know that $Π_{1}$ must have at least one inference rule because it must discharge $\neg A$ (or $χ$ ⁠, although in that case $Π_{2}$ could not be the trivial one-line proof). The rule discharging $\neg A$ could be either $\neg$ I or $\to$ I, and the next rule introducing the $⊥$ could be either $\neg$ E or $\to$ E. This gives us four shortest possible proofs $Π$ ⁠. If the last rule is $\neg$ E, we have the two possibilities:

And if the last rule is

\to

E, then we have these two possibilities (where the main subproof of

Γ, θ : ⊥

may be any gaunt coarsened proof of height

\leq 3

⁠):

In the first case, the coarsening of

\neg \neg \neg A, \neg \neg A : \emptyset

would be

\neg A, A : \emptyset

⁠. To obtain our proof of this sequent, we let

Σ_{1}

be the trivial proof, and let

Σ_{2}

be:

In the second case, the coarsening of

\neg (\neg A \to B), \neg \neg A : \emptyset

would be

\neg (A \to B), \neg A : \emptyset

⁠. To obtain our proof of this sequent, we again let

Σ_{1}

be the trivial proof, and let

Σ_{2}

be:

In the third case, the coarsening of

Γ, \neg \neg A \to θ, \neg \neg A : ⊥

will be

Γ, A \to θ, A : ⊥

⁠. So we let

Σ_{1}

be the trivial proof and let

Σ_{2}

be:

Finally, in the fourth case, the coarsening of

Γ, (\neg A \to C) \to θ, \neg \neg A : ⊥

will be

Γ, (A \to C) \to θ, \neg A : ⊥

⁠. So we again let

Σ_{1}

be the trivial proof, and let

Σ_{2}

be:

This completes the four cases of the basis step.

For the induction step, we can consider the obvious series of cases according to the last rule applied in $Π$ ⁠. I will begin with the E-rules. A remark on the notation used below: $ψ (\neg A_{i} / χ_{i})$ will refer to a formula $ψ$ that has a specified subformula either $\neg A_{i}$ or $χ_{i}$ ⁠; then $ψ (B_{i})$ will refer to the result of replacing the specified occurrence of $\neg A_{i}$ or $χ_{i}$ with the atom $B_{i}$ ⁠.

Case 1: Suppose the the last rule applied in $Π_{2}$ is $\land$ E, so $Π$ is a proof of $Δ, θ \land C : ψ (\neg A_{i} / χ_{i})$ —where $C$ is a new atom—with an immediate subproof of $Δ, θ : ψ (A_{i} / χ_{i})$ ⁠. Then by the i.h. we have proofs $Σ_{1}, Σ_{2}$ that give the following gaunt coarsened proof, where $θ^{'}$ may occur as a premise in either $Σ_{1}$ or $Σ_{2}$ (but not both):

Appending an instance of

\land

E discharging

θ^{'}

to the bottom of

Σ_{1}

will then give us the required proofs.

Case 2: suppose the last rule in $Π$ is $\to$ E, so we have:

If there is a valid coarsening of the form

Δ^{L}, ψ \to θ^{'}, {Δ^{R}}^{'}, (\neg ϕ)^{'} : \emptyset

⁠, then the claim follows directly from the i.h., similar to the case of

\land

E. On the other hand, suppose the coarsening also affects

Δ^{L}

⁠, so we have a gauntly valid sequent

{Δ^{L}}^{'}, ψ^{'} \to θ^{'}, {Δ^{R}}^{'}, (\neg ϕ)^{'} : \emptyset

⁠. It follows that

{Δ^{L}}^{'} ⊢ \neg \neg ψ^{'}

⁠, for otherwise we could find a model

M

{Δ^{L}}^{'}, \neg ψ^{'}

⁠, which we could then merge with a model of

{Δ^{R}}^{'}, (\neg ϕ)^{'}

to create a countermodel to our overall coarsened sequent. So, while

Δ^{L} : ψ

was gauntly valid,

Δ^{L}, \neg ψ : \emptyset

has the valid proper coarsening

{Δ^{L}}^{'}, \neg ψ^{'} : \emptyset

⁠. That is, both

Π^{L}

and

Π^{R}

satisfy the assumptions of the lemma. By the i.h. we know we have proofs as follows:

With these we can form the following proof of our target sequent

{Δ^{L}}^{'}, ψ^{'} \to θ^{'}, {Δ^{R}}^{'}, (\neg ϕ)^{'} : \emptyset

⁠.

To see that this is gaunt, consider the subproof above an arbitrary node in

Σ_{1}^{L}

⁠. For brevity, let

Δ_{L}

be the undischarged premises above this node other than

{Δ^{R}}^{'}

\neg ϕ^{'}

⁠.¹⁶ Then the subproof is a proof of

{Δ^{R}}^{'}, Δ_{L}, \neg ϕ^{'}, ψ^{'} \to θ^{'} : ξ

⁠. Note that in the proof from the i.h. there is a corresponding subproof proof of

Δ_{L}, \neg ψ^{'} : ξ

⁠. Now consider a coarsening

Δ_{L}^{'}, {Δ^{R}}^{'}, \neg ϕ^{'}, ψ^{''} \to θ^{'} : ξ^{'}

⁠; we want to show that it is invalid. Because the proof from the i.h. was gaunt, we know that

Δ_{L}^{'}, \neg ψ^{''} : ξ^{'}

is invalid, so there is a countermodel

M_{1}

⁠. Similarly,

{Δ^{R}}^{'}, \neg ϕ^{'} : \emptyset

is invalid, so there is a countermodel

M_{2}

⁠. And by atom-disjointness, we can merge these two models together to create a countermodel to

Δ_{L}^{'}, {Δ^{R}}^{'}, \neg ϕ^{'}, ψ^{''} \to θ^{'} : ξ^{'}

⁠.

Case 3: suppose the last rule applied in $Π_{2}$ is $\lor$ E. This will have two subcases, according to whether or not one of the subconclusions is $⊥$ ⁠. On the one hand, if one of the subconclusions is $⊥$ ⁠, then $Π$ is:

We can apply the i.h. to the left subproof to get a proof of the required form of

Δ_{1}^{'}, Δ_{2}^{'}, θ_{1}^{'}, . . ., θ_{k}^{'}, \neg ψ (B_{i}) : \emptyset

⁠. Then appending a terminal application of

\lor

E will give the proof of

Δ^{'}, (θ_{1}^{'} \land . . . \land θ_{k}^{'}) \lor (ξ_{1} \land . . . \land ξ_{l}), \neg ψ (A_{i}) : \emptyset

of the form that we seek.

On the other hand, suppose that

Π

ends with an instance of

\lor

E where neither of the subconclusions are

⊥

⁠. Then

Π

is of the following form (where each

θ_{j}

may occur as a premise in either

Π_{1}

Π_{2}

⁠):

By the i.h. we can find

Σ_{1}

and

Σ_{2}

such that the following is a gaunt coarsened proof:

From this we can then construct the following proof, where

C

is a new atom:

Concerning

Π_{3}

⁠, assume for simplicity and without loss of generality that

Δ_{3}, ξ, \neg ψ_{2} : \emptyset

is gaunt. (If not, we could deal with it in a similar fashion to the left subproof.) Then, we can form the following proof, where

D

is another new atom.

This is a proof, in the required form, of

\begin{aligned} Δ^{'}, (θ_{1}^{'} \land . . . \land θ_{k}^{'}) \lor (ξ_{1} \land . . . \land ξ_{l}), \neg (ψ_{1} (B_{i}) \lor C), \neg (D \lor ψ_{2}) : \emptyset, \end{aligned}

which is a coarsened c-variant of our original target sequent, as desired.

Case 4: the final E-rule to consider is $\neg$ E. But since the conclusion of $Π$ is a formula, not $⊥$ ⁠, we know that $Π$ cannot end in $\neg$ E. I turn now to the cases where the last rule in $Π$ is an I-rule.

Case 5: suppose the last rule in $Π$ is $\land$ I, with conclusion $ψ_{1} (\neg A_{i} / χ_{i}) \land ψ_{2}$ and subproofs $Π^{L}$ of $Δ^{L} : ψ_{1}$ and $Π^{R}$ of $Δ^{R} : ψ_{2}$ ⁠. Now we need to consider two subcases, according to whether (i) $Δ^{R}, \neg ψ_{2} : \emptyset$ is gaunt or, (ii) it is not. For (i), if it is gaunt, then we can form the following proof, where $Σ_{1}^{L}$ and $Σ_{2}^{L}$ are guaranteed to exist by the i.h.

To see that this proof is gaunt, consider the subproof above some arbitrary node in

Σ_{1}^{L}

labeled with, say,

ξ

⁠. Let

Δ_{L}

be the undischarged premises of this subproof other that those in

Δ^{R}

⁠. Then the subproof in question is a proof of

Δ^{R}, Δ_{L}, \neg (ψ_{1} (B) \land ψ_{2}) : ξ

⁠. Suppose that

Δ^{R}, ψ_{2}

⁠, were coarsened to

{Δ^{R}}^{'}, ψ_{2}^{'}

⁠. Since

Δ^{R}, \neg ψ_{2} : \emptyset

is gauntly valid, we know that there is model

M_{1}

{Δ^{R}}^{'}, \neg ψ_{2}^{'}

⁠. Now, by the i.h.,

Δ_{L}, \neg ψ_{1} (B) : ξ

is gauntly valid, so there will be a model

M_{2}

that witnesses

Δ_{L} ⊬ ξ

⁠. And because the

Δ_{L}

and

Δ^{R}

are atom-disjoint, we can combine

M_{1}

and

M_{2}

into a single model that is a counterexample to

{Δ^{R}}^{'}, Δ_{L}, \neg (ψ_{1} (B) \land ψ_{2}^{'}) : ξ

⁠. The argument is similar if

Δ_{L}, \neg ψ_{1} (B) : ξ

were coarsened.

On the other hand, in subcase (ii) there are some formulas $A_{j} / χ_{j}$ to be coarsened in $Π_{2}$ ⁠. Then we form the following proof, where again all of $Σ_{1}^{L}, Σ_{2}^{L}, Σ_{1}^{R}, Σ_{2}^{R}$ exist by the i.h.

We know this is gaunt by an argument similar to above: take an arbitrary subproof above some node

ξ

in, say,

Σ_{1}^{R}

⁠, and let

Δ_{R}

be the set of undischarged premises in this subproof other than those in

Δ^{L}

⁠. Consider a coarsening of

Δ_{R}^{'}, \neg ψ_{2} (B_{j})^{'} : ξ^{'}

⁠. By the i.h., this will be invalid and hence have a countermodel

M_{1}

⁠. Likewise, we know

Δ^{L}, \neg ψ_{1} (B_{i}) : \emptyset

is gauntly valid, so

Δ^{L} : \emptyset

will have a countermodel

M_{2}

⁠. And since

Δ^{L}

and

Δ_{R}

are atom-disjoint, we can merge

M_{1}

and

M_{2}

into a single model

M

which is a countermodel to

Δ^{L}, Δ_{R}^{'}, \neg (ψ_{1} (B_{i}) \land ψ_{2} (B_{j})^{'}) : ξ^{'}

⁠.

Case 6: suppose the last rule in $Π$ is $\lor$ I. Then $ψ$ will be of the form $ψ_{1} \lor C$ ⁠, where $C$ is a new atom, and by the i.h. we have the following proof:

From which we can obtain our desired proof by inserting an instance of

\lor

Case 7: suppose the last rule in $Π$ is $\to$ I. First, suppose $θ (\neg A_{i} / χ_{i}) \to C$ is derived by refuting $θ (\neg A_{i} / χ_{i})$ ⁠. Then, as observed in the proof of Lemma 9, $Δ, \neg (θ \to C) : \emptyset$ is gauntly valid, so there is nothing to show.

Second, suppose that $C \to ξ (\neg A_{i} / χ_{i})$ is inferred by deriving $ξ (\neg A_{i} / χ_{i})$ and $C$ is a new atom. This case is similar to $\lor$ I above: given $Σ_{2}$ with conclusion $ξ (B_{i})$ ⁠, we then append an instance of $\to$ I to infer $C \to ξ (B_{i})$ ⁠, and this can then be the minor premise in $\neg$ E with major premise $\neg (C \to χ (B_{i}))$ ⁠.

Third, consider the possibility that $θ \to ξ$ is inferred by deriving $ξ$ from $θ$ ⁠. There are two possibilities: either (i) $θ \to ξ$ is $C_{1} \to (C_{2} \to . . . \to \neg D)$ and gets coarsened to an atom $B$ ⁠, or (ii) not.

Consider case (i), so by Corollary 1, we have the following proof:

Take the leaf-node occurrence of

C_{1} \to (C_{2} \to . . . \to \neg D)

⁠. Clearly, the next step below this

\to

E must discharge the formula

C_{1} \to (C_{2} \to . . . \to \neg D)

(after all, in Corollary 1, the only other open premises are ones that must be discharged later in the proof). Suppose this formula is discharged by any rule other than

\neg

I. Then there will be an occurrence of

C_{1} \to (C_{2} \to . . . \to \neg D)

Δ

that is not immediately within the scope of a negation; and thus, the coarsening of

Δ, \neg (C_{1} \to (C_{2} \to . . . \to \neg D) : \emptyset

will be

Δ^{'}, \neg B : \emptyset

⁠. We can form the required gaunt proof of this as follows, where

Π_{0}^{'}

is the result of propagating the replacement of

B

in place of

C_{1} \to (C_{2} \to . . . \to \neg D)

⁠.

On the other hand, if

Δ, \neg (C_{1} \to (C_{2} \to . . . \to \neg D)) : \emptyset

coarsens to

Δ^{'}, B : \emptyset

⁠, then the leafnode occurrence of

C_{1} \to (C_{2} \to . . . \to \neg B)

must be discharged by

\neg

I, so

Π_{0}

could be represented in more detail as:

From this we obtain the gaunt proof of

Δ^{'}, B : \emptyset

as follows, where

Π_{0}^{'}

is the result of propagating

B

in place of

\neg (C_{1} \to (C_{2} \to . . . \to \neg D))

⁠:

This is our proof

Σ_{2}

⁠, and

Σ_{1}

is the trivial proof.

Now take case (ii), where $(θ_{1} \land . . . \land θ_{k}) \to ξ$ is inferred from a proof of $ξ$ with the $θ_{j}$ ’s as open premises. Then $Π$ is of the following form, where each $θ_{j}$ may occur in either $Π_{1}$ or $Π_{2}$ (but not both):

Note that if

Δ, \neg (θ \to ξ) : \emptyset

is valid, then so is

Δ, θ, \neg ξ : \emptyset

⁠. So if the former has a valid coarsening, then so does the latter.¹⁷ Thus, we may apply the i.h. to find a proof of the following form, where again each

θ_{j}^{'}

may occur in either

Σ_{1}

Σ_{2}

⁠, but not both:

Now it is possible that all the

θ_{j}^{'}

’s are in

Σ_{1}

⁠, it is possible that all the

θ_{j}^{'}

’s are in

Σ_{2}

⁠, and it is possible that some

θ_{j}^{'}

’s occur in each of

Σ_{1}

and

Σ_{2}

⁠. Assume we are in the third case; the first two can be dealt with similarly. Let

J

be an index set for the

θ_{j}^{'}

’s in

Σ_{2}

and

K

an index set for the

θ_{j}^{'}

’s in

Σ_{1}

⁠. Then we can form the our desired proof as follows, where

C

is a new atom:

This is a proof of

Δ^{'}, \neg (\underset{K}{⋀} θ_{j}^{'} \to C), \neg (\underset{J}{⋀} θ_{j}^{'} \to χ (B_{i})) : \emptyset

⁠, which is a c-variant of our target sequent

Δ^{'}, \neg (θ (B_{i}) \to χ (B_{i})) : \emptyset

⁠, as desired.

Case 8: Finally, suppose that the last rule in $Π$ is $\neg$ I. So $Π$ is a proof of $Δ : \neg (θ_{1} \land . . . \land θ_{k})$ ⁠, with the immediate subproof $Δ, θ_{1}, . . ., θ_{k} : \emptyset$ ⁠. If $Δ, \neg \neg (θ_{1} \land . . . \land θ_{k}) : \emptyset$ is not gauntly valid, then from Lemma 9, we know that $k = 1$ and $θ$ is an atom. It also follows that the coarsening must be of the form $Δ^{'}, \neg_{i} B : \emptyset$ ⁠, with $i = 0$ or $i = 1$ ⁠. So $Π$ will be:

Now the coarsening

Δ^{'}

will be obtained either by deleting 2 negations from

A

or only 1 negation. If 2, then obviously the occurrence of

A

Δ

must be preceded by two negations. Thus, the premise

\neg A

at the top left must be discharged by inferring

\neg \neg A

\neg

I. Otherwise, the descendant of that leafnode

\neg A

would be a formula with an occurrence of

A

preceded by only one negation. So

Π

Now take

Π_{0}

and replace the node

\neg \neg A

A

⁠, and propagate this downward through the prooftree. This gives us a proof:

We may take this as our proof

Σ_{2}

⁠, with

Σ_{1}

being the trivial proof.

On the other hand, suppose $Δ^{'}, \neg A : \emptyset$ is gauntly valid, where $Δ^{'}$ is obtained by deleting one negation from in front of $A$ ⁠. Let $Π_{0}^{'}$ be the result of uniformly replacing every instance of $\neg A$ in $Π_{0}$ with $A$ ⁠. (We know that every instance of $A$ in $Π_{0}$ is a descendant or ancestor of the top left $\neg A$ ⁠, so every occurrence of $A$ in $Π_{0}$ will have at least one negation, and hence this deletion will preserve proofhood.) Then, by tweaking the discharges, we have the following proof:

Again, we may take this as our proof

Σ_{2}

⁠, with

Σ_{1}

being the trivial proof.

7 Conclusion

This paper and its prequel 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 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. The prequel paper showed how to coarsen both classical and constructive natural deduction proofs to obtain perfect proofs.

In this paper we have seen how to coarsen constructive proofs, so that from a core proof of $Δ : Φ$ we can find not just a perfect proof but also a gaunt proof of some $Δ^{'} : Φ^{'}$ which is a coarsening of a c-variant of $Δ : Φ$ ⁠. This result does not carry over to classical natural deduction proofs because of how negation can figure in premises of strictly classical rules, such as reductio ad absurdum or dilemma. An outstanding issue to explore, then, is how to extend the method of coarsening to sequent proofs, in which classicality can be achieved by the use of multiple conclusions rather than by logical inference rules. Does this difference between natural deduction and sequent calculi allow us to find a method of transforming an arbitrary sequent proof into a gaunt proof?

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, and Peter Verdée. Thanks especially to the anonymous referees whose comments have improved both the exposition and technical arguments of this paper.

Footnotes

Thanks to an anonymous referee for raising this question.

This idea is developed more carefully in [1] and [3].

I am indebted to a referee for raising this question and suggesting the following line of reply.

This is because Lemma 5 and its application in Case 4 of the proof of Lemma 6 guarantees that certain transformations are possible, but does not provide an independent syntactic characterization of when to apply those transformations.

In general, I will assume that multiple conjunctions associate to the right, so that $ϕ_{1} \land . . . \land ϕ_{n}$ abbreviates $ϕ_{1} \land (ϕ_{2} \land (. . . \land (ϕ_{n - 1} \land ϕ_{n}) . . .)$ ⁠.

Note that this remark does not apply to the sequent calculus [5] provides for classical core logic. Tennant’s system only allows for single conclusions, not multiple conclusions. As a result, sequent proofs are isomorphic to natural deduction proofs, and results about natural deduction carry over immediately to the sequent calculus.

This question is partly addressed in [3], where I use a multi-conclusion sequent calculus to show that any classical gauntly valid sequent has a gaunt proof. That argument uses a bottom-up proof search, however, rather than a top-down coarsening procedure. It remains a further matter to study coarsening in a sequent calculus setting. An important feature of coarsening, as used in this paper, is that it provides a method for starting with any valid sequent and finding a gaunt proof of a coarsening of that sequent. The proof search method used in [3], by contrast, produces a gaunt proof of any gauntly valid sequent, but terminates unsuccessfully when given a sequent that is valid but not gauntly valid.

See Corollary 6 of Chapter IV in [4].

Given a countermodel to $Δ_{a} ⊬ \neg δ \lor ξ$ ⁠, we know that $δ$ cannot be true at the root node, since then $ξ$ would have to be true as well; but there must be at least one terminal node where $δ$ is true. There must also be at least one terminal node where $ξ$ is true, since otherwise $\neg ξ$ and hence $\neg δ$ would be true at the root node. Likewise for a countermodel to $Δ_{b} ⊬ \neg ψ_{j} \lor ζ$ ⁠. And by atom-disjointness we can make these terminal nodes combine in the way pictured.

Note this proof is the same height as $Π$ ⁠.

For if $Δ_{1} ⊬ \neg \neg ϕ$ ⁠, we could require $M_{1}$ to have a terminal world $w$ where $w ⊮ ϕ$ ⁠.

Note that it is possible for the discharged premise to occur both inside some $Σ_{i}^{j}$ and $Π_{m}^{1}$ and outside each $Σ_{i}^{j}$ and $Π_{m}^{1}$ ⁠. Despite the fact that the instance of $\land$ E in the original proof will only discharge one formula, we may have introduced multiple reletterings of that premise in the inductive definitions of $Σ_{i}^{j}$ and $Σ_{0}^{j}$ ⁠. If so, we will now have multiple relettered versions of the MPE for this instance of $\land$ E.

Or if some relettering corresponding to $ξ$ so occurs—a qualification I will henceforth omit.

It is possible that there are other $\lor$ E rules among $R_{1}, . . ., R_{n - 1}$ ⁠, in which case we also permute a copy of $R_{n}$ into their respective subproofs as appropriate. This permutation would be similar to the process for proving Lemma 6(4).

Recall that conjunctions and disjunctions are assumed to associate to the right.

Thus, $Δ_{L}$ will include ${Δ_{2}^{L}}^{'}$ as well as the subset of ${Δ_{1}^{L}}^{'}$ whose members occur as premises in this subproof and the set of premises that are undischarged in this subproof but which get discharged lower down in $Σ_{1}^{L}$ ⁠.

This is how we know that the $\neg A_{i}$ ’s and $χ_{i}$ ’s must occur in $ξ$ as displayed in the prooftree.

References

[1]

Brauer

Relevance for the classical logician

Review of Symbolic Logic

436

–

457

2020

Google Scholar

Crossref

WorldCat

[2]

Brauer

Coarsening natural deduction proofs i: finding perfect proofs

Journal of Logic and Computation

2024

Google Scholar

OpenURL Placeholder Text

WorldCat

[3]

Brauer

A hierarchy of relevance properties

. In

New Directions in Relevant Logic

Tedder

Sedlar

and

Standefer

, eds.

Springer

forthcoming

[4]

Prawitz

Natural Deduction: A Proof-Theoretical Study

Dover

2006

Originally published in 1965

Google Scholar

Google Preview

OpenURL Placeholder Text

WorldCat

[5]

Tennant

Core Logic

Oxford University Press

2017

This is an Open Access article distributed under the terms of the Creative Commons Attribution License (https://creativecommons.org/licenses/by/4.0/), which permits unrestricted reuse, distribution, and reproduction in any medium, provided the original work is properly cited.

Download all slides

Month:	Total Views:
February 2024	70
March 2024	40
April 2024	34
May 2024	30
June 2024	21
July 2024	11
August 2024	6
September 2024	9
October 2024	10
November 2024	9
December 2024	3
January 2025	7
February 2025	16
March 2025	48
April 2025	27

Article Contents

Coarsening natural deduction proofs II: finding gaunt proofs

Abstract

1 Introduction

2 Preliminaries

2.1 Technical definitions

2.2 Philosophical remarks

2.3 Core logic

3 Challenges to Finding Gaunt Coarsenings

3.1 Disjunction elimination

3.2 Conjunction elimination

3.3 Negation rules

3.4 Circuitous E- and I-rules

4 Coarsening Procedure for Gaunt Proofs

4.1 Disjunction

4.2 Conjunction

4.3 Implication

4.4 Negation

4.5 Main theorem

5 Negation Introduction

5.1 Preliminary lemmas

5.2 Proof transformations

6 Negation Elimination

7 Conclusion

Funding

Acknowledgements

Footnotes

References

Citations

Views

Altmetric

Email alerts

Citing articles via

Latest

Most Read

Most Cited

Article Contents

Coarsening natural deduction proofs II: finding gaunt proofs

Abstract

1 Introduction

2 Preliminaries

2.1 Technical definitions

2.2 Philosophical remarks

2.3 Core logic

3 Challenges to Finding Gaunt Coarsenings

3.1 Disjunction elimination

3.2 Conjunction elimination

3.3 Negation rules

3.4 Circuitous E- and I-rules

4 Coarsening Procedure for Gaunt Proofs

4.1 Disjunction

4.2 Conjunction

4.3 Implication

4.4 Negation

4.5 Main theorem

5 Negation Introduction

5.1 Preliminary lemmas

5.2 Proof transformations

6 Negation Elimination

7 Conclusion

Funding

Acknowledgements

Footnotes

References

Citations

Views

Altmetric

Email alerts

Citing articles via

Latest

Most Read

Most Cited

This Feature Is Available To Subscribers Only