zbMATH — the first resource for mathematics

Proof normalization for a first-order formulation of higher-order logic. (English) Zbl 0905.03036
Gunter, Elsa L. (ed.) et al., Theorem proving in higher order logics. 10th international conference, TPHOLs ’97. Murray Hill, NJ, USA. August 19–22, 1997. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1275, 105-119 (1997).
Summary: We define a notion of cut and a proof normalization process for a class of theories, including all equational theories and a first-order formulation of higher-order logic. Proof normalization terminates for all equational theories. We show that the proof of termination of normalization for the usual formulation of higher-order logic can be adapted to a proof of termination of normalization for its first-order formulation. The “hard part” of the proof, that cannot be carried out in higher-order logic itself, i.e. the normalization of the system $$F_\omega$$, is left unchanged. Thus, from the point of view of proof normalization, defining higher-order logic as a different logic or as a first-order theory does not matter. This result also explains a relation between the normalization of propositions and the normalization of proofs in equational theories and in higher-order logic: normalizing of propositions does not eliminate cuts, but it transforms them.
For the entire collection see [Zbl 0870.00024].

MSC:
 03F05 Cut-elimination and normal-form theorems 03B15 Higher-order logic; type theory (MSC2010)
ETPS