[FOM] The basics of Core Logic

[Neil Tennant]

Harvey Friedman has suggested that I write to the fom list to spell out the basics of Core Logic, and especially the result of Thinning-Elimination, for the benefit of members who have not read any of my publications on it. 
 
It is easiest to proceed in terms of the sequent calculus, although everything I say here has its immediate natural-deduction analogue. 

A sequent X:Y consists of a set X and a set Y (of sentences). X is called the antecedent, and Y is called the succedent, of the sequent X:Y.  Succedents are either empty or singletons. For any non-empty succedent we shall just write the sentence concerned, instead of its singleton. 
       
Since underlining is difficult in ascii, readers are to imagine the underlinings for themselves. I shall space the premise sequents and the conclusion sequent of any rule so that it is easy to imagine this. In ascii we shall use Ex for the existential quantifier, and (x) for the universal quantifier.

Our notational conventions are very important for an understanding of what is allowed in Core Logic, and what is not. 
'X,Y' denotes the union of X with Y. 
When an antecedent of a sequent is written 'X,A', this means that the sentence A is in the antecedent, and X is the set (possibly empty) of the other sentences in the antecedent. 
And of course X,A is the union of X with the singleton of A.  
When a sequent is written 'Z:', with nothing explicitly mentioned on the right, then the succedent is empty. 

We have only one structural rule in Core Logic, the rule of initial sequents, for arbitrary sentences A:       

A:A 

Core Logic has NO Cut rule.
Core Logic has NO Thinning rules.

The right- and left-rules for the logical operators are carefully stated for Core Logic in slightly different forms than are found in Gentzen. The reason for these differences is that in Core Logic we are making do without Thinning and without Cut. 

The following are the right- and left-rules for the logical operators in Core Logic. Note that every one of them, as stated, is derivable in Gentzen's sequent calculus LJ for intuitionistic logic. (To be sure, one might need to use Thinning in order to derive some of them in LJ. My point is just that the intuitionistic logician cannot object to any of the basic rules of Core Logic.) Remember that a succedent rendered as a set (usually: as Y or as Z) may be empty, and is at most a singleton. If we write a succedent as a sentence (usually: as B or as C), then this means that the succedent is the singleton of that sentence.

X,A :                         
X : ~A                        

X:A
X,~A:
_________________________

X:A       Y:B                    
  X,Y:A&B    
  
X,A,B:Y   (At least one of A, B in the antecedent, and neither one in X.)
X,A&B:Y
_________________________

  X:A
X:AvB

  X:B
X:AvB

X,A:C     Y,B:C
   X,Y,AvB:C
   
X,A:C     Y,B:
   X,Y,AvB:C
   
X,A:     Y,B:C
   X,Y,AvB:C
   
X,A:     Y,B:
   X,Y,AvB:
_________________________

 X,A:B
X:A->B

  X:B            (A not in X)
X:A->B

  X,A:
X:A->B

X:A      Y,B:Z
 X,Y,A->B:Z
_________________________

  X:Ft
X:ExFx

X,Fa:Y        (parameter a not in concluding sequent)
X,ExFx:Y

_________________________

  X:Fa           (parameter a not in concluding sequent)
X:(x)Fx

X,Ft1,...,Ftn:Y
   X,(x)Fx:Y

_________________________

Gentzen's sequent proofs could of course contain both cuts and thinnings. He proved his so-called Hauptsatz, or Cut-Elimination Theorem, for his sequent calculus LJ: every sequent proof in LJ of X:Y can be transformed into a cut-free sequent proof in LJ of X:Y.  His proof relied heavily on the availability of Thinning, so that antecedents and/or succedents could be 'topped up' so as to get them into the required form for the application of his left- and right-rules. This was needed in order to obtain X:Y as the sequent proved by the cut-free proof resulting from the transformation.

This raises the simple question: Why not extend Gentzen's Hauptsatz so as to get rid not only of cuts but also of thinnings? In order to carry this through, only one insight is needed: the resulting (cut-free, thinning-free) CORE proof P might not be a proof of the original sequent X:Y; BUT, in such a case, P is a core proof of SOME SUBSEQUENT OF X:Y---having which is every bit as good as (when not better than) having a thinning-filled proof of X:Y itself.

Thinning-Elimination Theorem:  Any Cut-free proof of X:Y in the Gentzen calculus LJ can be converted into a Core proof of some subsequent of X:Y.

The proof of Thinning-Elimination on already Cut-free proofs proceeds by a straightforward induction on the complexity of Cut-free proofs in Gentzen's system LJ. In all cases of the inductive step, the reader will find that the rules stated above accommodate every possibility that might be served up by applying the Inductive Hypothesis to the immediate subproofs for the application of any rule.

(This result, for natural deduction, was first established in my paper 'Intuitionistic Mathematics Does Not Need Ex Falso Quodlibet', Topoi 13, 1994, pp. 127-133.  In that paper, Core Logic was called IR, for 'Intuitionistic Relevant' Logic.)

The extension of Thinning-Elimination to Gentzen's classical system LK is reasonably straightforward. One just has to bear in mind that Classical Core Logic uses the single-conclusion rule of Dilemma, whereas in LK one is allowed sequents with multiple succedents. 

The interested reader will find more about Core Logic, and the 'epistemically gainful' admissibility of Cut for it, in my paper 'Cut for Core Logic', Review of Symbolic Logic,  5, no.3, 2012, pp. 450-479.  DOI: http://dx.doi.org/10.1017/S1755020311000360