By the sequent calculus with equality we mean Gentzen’s systems LJ and LK, with the ∀ ⇒ and ⇒ ∃ rules restricted to individual parameters, enriched by the reflexivity axioms ⇒ t = t, for t an arbitrary term, and the multiple right congruence rule: Γ ⇒ F{x1/r1,...,xn/rn} Γ ⇒ r1 = s1 ...Γ ⇒ rn = sn Γ ⇒ F{x1/s1,...,xn/sn} for r1, . . . sn arbitrary terms. We show that for both systems, every deriv- able sequent has a cut-free derivation in which occur only terms and atomic formulae other than equalities, that are renamings of terms and atomic formulae occurring in the sequent itself. That is instrumental in the proof theoretic analysis of the logic of par- tial terms, where ”existence”, namely defineteness, of a term t is expressed by ∃x(x = t), for x not occurring in t.
The Subterm Property for the Sequent Calculus with Equality
PARLAMENTO, Franco;
2012-01-01
Abstract
By the sequent calculus with equality we mean Gentzen’s systems LJ and LK, with the ∀ ⇒ and ⇒ ∃ rules restricted to individual parameters, enriched by the reflexivity axioms ⇒ t = t, for t an arbitrary term, and the multiple right congruence rule: Γ ⇒ F{x1/r1,...,xn/rn} Γ ⇒ r1 = s1 ...Γ ⇒ rn = sn Γ ⇒ F{x1/s1,...,xn/sn} for r1, . . . sn arbitrary terms. We show that for both systems, every deriv- able sequent has a cut-free derivation in which occur only terms and atomic formulae other than equalities, that are renamings of terms and atomic formulae occurring in the sequent itself. That is instrumental in the proof theoretic analysis of the logic of par- tial terms, where ”existence”, namely defineteness, of a term t is expressed by ∃x(x = t), for x not occurring in t.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
