Contraction-free sequent calculi for geometric theories with an application to Barr's theorem

 Geometric theories are presented as contraction- and cut-free systems of sequent calculi with mathematical rules following a prescribed rule-scheme that extends the scheme given in Negri and von Plato (1998). Examples include cut-free calculi for Robinson arithmetic and real closed fields. As an immediate consequence of cut elimination, it is shown that if a geometric implication is classically derivable from a geometric theory then it is intuitionistically derivable. Received: 18 April 2001 / Published online: 10 October 2002 Mathematics Subject Classification (2000): 03F05, 18C10, 18B15 Key words or phrases: Cut elimination – Geometric theories – Barr's theorem