An example of an adaptive proof

Here’s an example that might help to see how the machinery described in the previous post works. Let’s take LLL to be CLuN (the positive part of classical logic plus the excluded middle). We can construct an adaptive logic where the constituents of Ω are all substitution instances of (∃)(ϕ ∧¬ ϕ), and we quite naturally obtain CL (classical logic) as the upper limit logic.

Take the adaptive logic thus obtained and consider the example where ourpremise set is:
Before we get to our adaptive proof, observe three facts:

In the proof we first write down the premises:

1.	p ∨ q	Prem	∅
2.	¬p	Prem	∅
3.	r	Prem	∅
4.	¬r	Prem	∅
5.	r ∨ s	Prem	∅

Since p∧¬p is an abnormality and q ∨ (p∧¬p) LLL-follows from lines 1 and 2, we can apply Rc to lines 1 and 2 and conclude q, relying on the normal behavior of p ∧¬p:

6.	q	Rc: 1, 2	{p ∧¬p}

Similarly, s ∨ (r ∧¬r) is LLL-derivable from lines 4 and 5, and hence:

7.	s	Rc: 4, 5	{r ∧¬r}

However, we are faced with the following difficulty: Prem₃ is clearly problematic. Our input data inform us that r doesn’t behave normally. In fact, according to our premises, both r and ¬r are true. But then, should we really conclude that s is true just because r ∨ s is true? The usual rationale behind the disjunctive syllogism (ϕ ∨ ψ,¬ϕ ⊢ ψ) is this: ϕ ∨ ψ tells us that at least one of the involved sentences is true; ¬ϕ, however, tells us that ϕ is false and hence it cannot be true. Therefore, the only option is that it is ψ that is true and its truth accounts for the truth of ϕ ∨ ψ. On the paraconsistent approach, however, a formula and its negation can be both true: the claim that ¬ϕ is true doesn’t entail the claim that ϕ cannot be true. For this reason, when both r and ¬r are true, the disjunctive syllogism applied to ¬r, r ∨ s might fail. For even if s is still (only) false, r ∨ s will still be true in virtue of r being true. Hence, our premise set LLL-proves an abnormality: r ∧¬r.

8.	r ∧¬r	RU: 3, 4	∅

This also shows that r ∧¬r is not an abnormality on whose falsehood we can rely: it is actually derivable from our premises. But this, according to our marking regulations requires us to cancel any conclusion that relied on the normal behavior of r ∧¬r, which (in our case) means that we have to withdraw line 8 (which I mark by putting ‘⋎’ besides a line):

7.	s	Rc: 4, 5	{r ∧¬r}	⋎
8.	r ∧¬r	RU: 3, 4	∅

So, as things stand, the only line with s as its formula has been canceled. It might be the case, however, that a formula actually is AL-derivable from a set of premises even though it is a formula of a marked line. The fact that ϕ is a formula in a marked line only means that the way it is introduced in that line is unreliable. This doesn’t have to mean that ϕ is not AL-derivable from the premises in general. Is it the case with s? A moment of consideration should convince us that it isn’t. From these premises, there is no other sensible way we could introduce s without relying on the normal behavior of r ∧¬r.

If we were simply reasoning in CLuN we also wouldn’t be allowed to introduce line 7 either, because we wouldn’t be allowed to use disjunctive syllogism in general. In our AL, however, we can still keep line 7 as long as the abnormality on which it depends is not CLuN-derived from our premises. That is, q is finally derivable if no possible extension of our proof derives on ∅ a minimal Dab-formula Dab(Δ) with (p ∧¬p) in Δ such that for no Δ′⊆ Δ, where (p ∧¬p) is not in Δ′, Dab(Δ′) is LLL-derivable from the premises. Luckily, the question whether these formulas are CLuN-derivable from Prem₃ is decidable (as long as we stay on the level of propositional logic). Hence we can consider q to be finally derived, even though s is not derivable.