Preservation of the equivalence of proofs under reduction of the formula depth

S. V. Solov'ev

Zapiski Nauchnykh Seminarov POMI, Studies in constructive mathematics and mathematical logic. Part VIII, Tome 88 (1979), pp. 197-208

Résumé

The derivability of a sequent is the invariant of the following transformation decreasing the formula depth of the sequent. If $S$ is a sequent and $\Phi[F]$ is any $S$-formula then we replace $\Phi[F]$ by $\Phi[p]$ and add a new formula $\Psi$ into antecedent of $S$. If $F$ is positive in $S$ then $\Psi=F\supset p$ and $\Psi=p\supset F$ otherwise, where $p$ is a new propositional variable. We prove that a natural extension of this transformation to derivations is univalent, i.e. two derivations are equivalent (i.e. have the same normal form) if and only if the transformed ones are equivalent. We call sequent $S$ the "$R$-sequent" if and only if the succedent of $S$ is a variable and antecedent formulas of $S$ are of the form $b$, $b\$, $b\supset c$, $(b\supset c)\supset d$, $(b\)\supset d$, $b\supset(c\)$ where $b,c,d$ – are variables. By an iteration of transformation described above a sequent $S$ can be transformed into $R$-sequent $S$. This result permits us to restrict consideration to $R$-sequents in proofs of many theorems. By an iteration of transformation described above a sequent $S$ can be transformed into $R$-sequent $S'$.This result permits us to restrict consideration to $R$-sequents in proofs of many theorems. From the point of wiev of the category theory (cf. [1], [2]) our transformation is an univalent functor $\mathfrak{A}\colon\mathbb C\to\mathbb C$ where $\mathbb C$, is a free cartesian closed category.