[FOM] "Hidden" contradictons; and Core Logic

[Neil Tennant]

It is not just classical logic that has arbitrary propositions allegedly following from a contradiction, no matter how 'minor' or 'isolated' the latter might, intuitively, be; so too has intuitionistic logic. The issue is whether the inference 'A, not-A; therefore B' is correct. Both the classicist and the intuitionist think it is.

The relevantist does not. But the relevantist still wishes to recognize contradictions whenever they crop up. So the relevantist still needs the inference 'A, not-A; therefore #', where # is the absurdity symbol.  The absurdity symbol also, of course, features in the statement of the rule of (constructive) reductio ad absurdum, or negation-introduction (in the natural deduction setting):

      --(i)
      A
       :
       :

      #
    _____(i)
    not-A


which the relevantist regards as correct, provided only that the assumption A is really relevant to the conclusion # in the subordinate proof.

With # thus admitted on to the scene, the relevantist absolutely must avoid the rule Ex Falso Quodlibet:

    #
   __

    B

otherwise the unwanted inference 'A, not-A; therefore B' will be derivable. (The relevantist is committed to being a paraconsistentist.)

The relevantist who is serious about providing a logical system that can accommodate mathematical reasoning must allow as correct the inference known as Disjunctive Syllogism, since it is used all over the place in both constructive and classical mathematics:

      A or B       not-A
     ______________

                 B


All this is with reference to natural deduction, which uses introduction and elimination rules.

In the sequent-calculus setting, the 'right' rules for logical operators correspond to Introduction rules of natural deduction, and their 'left' rules correspond to Elimination rules.


In the sequent setting, the (unwanted) natural deduction rule EFQ becomes Thinning on the Right.
So Thinning on the Right must be disallowed by the relevantist.
So too must Thinning on the Left, since its use can make any 'assumption' appear to be 'relevant' to the conclusion.

So Thinning (tout court) must be disallowed by the relevantist.

Now, the Cut rule will allow two relevant (and constructive) proofs to be strung together to deliver the dreaded inference 
'A, not-A; therefore B': To see this, take the relevantist's proofs of the two inferences

           A  =>A or B               A or B, not-A => B


and cut away 'A or B'.


So Cut must be disallowed by the relevantist.

What is left? Answer: only the structural rule of Reflexivity:

        A => A

(since sequent proofs have to get started!) and the right- and left-logical rules, suitably formulated so as to ensure relevance of premises to conclusions.

The resulting system is Core Logic.

Core Logic can also be classicized, by appending the classical Rule of Dilemma.

Core Logic allows for Cut to be *admissible*, in the following epistemically gainful sense, which will often allow one to find a proof of a stronger result than had been expected:

     There is an effective operation * such that: 

     given any Core proof P1 of the sequent X=>{A}, and Core proof P2 of the sequent A,Y=>{B}, 

     P1*P2 is a Core proof of (some subsequent of) X,Y=>{B}.

Consider the notorious 'proof' of Lewis's First Paradox 'A, not-A, therefore B', which involved a proof P1 of the sequent {A} => {A or B} and a proof P2 of the sequent {A or B, not-A} => {B}. In this case, the admissibility result for Core Logic tells one that there is a Core proof of some subsequent of the sequent {A, not-A} => {B}'. Indeed there is. It is the obvious proof of the sequent 'A,not-A => { }', with empty succedent.

Some Corollaries of the admissibility of Cut in the form just stated:

1. Core Logic suffices for constructive mathematics.
2. Classicized Core logic suffices for classical mathematics.
3. All logical consequences of satisfiable sets of premises are Core-deducible from them.
4. All inconsistent sets are Core-provably inconsistent (so Core logic suffices for the hypothetico-deductive method in science).
5. All logical truths are Core-theorems.
One can also show that Core Logic is the inviolable core of logic, in the sense that none of its rules can be given up, on pain of not being able to carry out the reasoning that is required for rational belief-revision. The case is made in my book Changes of Mind: An Essay on Rational Belief Revision ((http://ukcatalogue.oup.com/product/9780199655755.do).
 
Neil Tennant