An Addition to “Cut Elimination in ϵ-Calculi”

✍ Scribed by Mitsuru Yasuhara

• Publisher: John Wiley and Sons
• Year: 1989
• Tongue: English
• Weight: 88 KB
• Volume: 35
• Category: Article
• ISSN: 0044-3050
• DOI: 10.1002/malq.19890350603

✦ Synopsis

A(s) -+ A(&zA(z)),

HE^)

Vz(A(z) ++ B ( z ) ) 4 KIA(%) = ~y B ( y ) . It was pointed out in [3] that HE^) makes this calculus non-conservative over the equality-free part. Namely, some formulas that do not contain equality can be proved only with the help of ( H e 2 ) (cf. also [Z], pp. 83, 84.).

The purpose of this Addition is to give an axiomatization of this equality-free part and to prove the cut-elimination theorem for it.

The obvious candidate for being an axiom is the scheme

HE^)

Indeed, let V be the &-calculus, without equality, with ( H d ) and (H.53); and let %' * be the calculus with equality, HE^) and HE^). Then,

Vz(A(z) c, B ( x ) ) & C ( e z A ( z ) ) -+ C(&yB(y)).

T h e o r e m 1. %?* i s conservative over ??.

This will be a corollary of the cut-elimination theorem, below. Note that, in the Now we switch to the sequent calculus of [3], 5 1, strengthened by the new rule: presence of the usual equality axioms, HE^) and HE^) are inter-deducible.