Mechanizing Set Theory: Cardinal Arithmetic and the Axiom of Choice.

Details Mechanizing Set Theory: Cardinal Arithmetic and the Axiom of Choice. Mechanizing Set Theory: Cardinal Arithmetic and the Axiom of Choice.

2001-03-29

arxiv.org/abs/cs/9612104v1

Journal of Automated Reasoning 17 (1996), 291-323

Computer Science

Logic in Computer Science

Scientific paper

Fairly deep results of Zermelo-Frenkel (ZF) set theory have been mechanized using the proof assistant Isabelle. The results concern cardinal arithmetic and the Axiom of Choice (AC). A key result about cardinal multiplication is K*K = K, where K is any infinite cardinal. Proving this result required developing theories of orders, order-isomorphisms, order types, ordinal arithmetic, cardinals, etc.; this covers most of Kunen, Set Theory, Chapter I. Furthermore, we have proved the equivalence of 7 formulations of the Well-ordering Theorem and 20 formulations of AC; this covers the first two chapters of Rubin and Rubin, Equivalents of the Axiom of Choice, and involves highly technical material. The definitions used in the proofs are largely faithful in style to the original mathematics.

Affiliated with

Also associated with

No associations

Rating

Mechanizing Set Theory: Cardinal Arithmetic and the Axiom of Choice. does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with Mechanizing Set Theory: Cardinal Arithmetic and the Axiom of Choice., we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Mechanizing Set Theory: Cardinal Arithmetic and the Axiom of Choice. will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-418200