[FOM] truth preservation of Gentzen rules?

[Randall Holmes]

Dear all,

It is possible to simulate a version of the Gentzen calculus using
completely equational calculations (I've done this in my theorem
proving work).  A proof of a sentence in this implementation is a computation
in an equational version of first-order logic leading to the
conclusion that it is equal to the True.  This seems about as
"truth-preserving" as one can get.

There are some fiddly points:  "new" variables are bound variables
in the term representing the sequent proof (making it clear why they
can't appear outside their scope).  The quantifier rules have to
keep certain terms around which are discarded in the usual formalization:
for example, an existential (Ex.P(x)) on the right is not replaced with
P(t) (for an arbitrary term) but with P(t), (Ex.P(x)) (because (Ex.P(x))
is equivalent to "P(t) or (Ex.P(x))", and commas on the right of a sequent
are read as disjunction).

Details available on request (and fairly easy to work out on one's
own).

--Randall Holmes