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].

For the entire collection see [Zbl 0870.00024].

##### MSC:

03F05 | Cut-elimination and normal-form theorems |

03B15 | Higher-order logic; type theory (MSC2010) |