A normalization theorem for set theory.

*(English)*Zbl 0683.03036
J. Symb. Log. 53, No. 3, 673-695 (1988); retraction ibid. 76, No. 3, 1096 (2011).

A normalization theorem for a natural proof system of Zermelo Set Theory is presented. To get around examples of non-normalizability, a new inference rule is added. With this modified definition of “normal”, it is no longer true that the normalization theorem implies consistency of Zermelo Set Theory.

However, the modified notion of normal proof is sufficient to prove the completeness of the cut-free algorithm that searches for a proof of a given formula in set theory. The paper is concluded by comments on this algorithm and its potential use in an automated theorem prover for set theory.

However, the modified notion of normal proof is sufficient to prove the completeness of the cut-free algorithm that searches for a proof of a given formula in set theory. The paper is concluded by comments on this algorithm and its potential use in an automated theorem prover for set theory.

Reviewer: P.Štěpánek

##### MSC:

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

03B35 | Mechanization of proofs and logical operations |

03E30 | Axiomatics of classical set theory and its fragments |

##### Keywords:

normalization theorem for a natural proof system of Zermelo Set Theory; normal proof; cut-free algorithm
Full Text:
DOI

##### References:

[1] | Proceedings of the second Scandinavian logic symposium pp 63– (1971) · Zbl 0219.02001 |

[2] | Natural deduction, a proof-theoretic study (1965) |

[3] | The lambda calculus–its syntax and semantics (1981) · Zbl 0467.03010 |

This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.