Logics_ZF/document/ZF.tex

1 \chapter{Zermelo-Fraenkel Set Theory}
304 This is similar to the situation in Constructive Type Theory (set theory
459 Martin-L\"of's Type Theory, and is often easier to use than \cdx{fst}
1036 Theory \thydx{Bool} defines $\{0,1\}$ as a set of booleans, with the usual
1074 Theory \thydx{Sum} defines the disjoint union of two sets, with
1098 Theory \thydx{QPair} defines a notion of ordered pair that admits
1160 complete lattice has a fixedpoint.  Theory \thydx{Fixedpt} proves the
1179 Theory \texttt{Finite} (Figure~\ref{zf-fin}) defines the finite set operator;
1312 Theory \thydx{Univ} defines a `universe' $\isa{univ}(A)$, which is used by
1320 Theory \thydx{QUniv} defines a `universe' $\isa{quniv}(A)$, which is used by
1495 Theory \thydx{Nat} defines the natural numbers and mathematical
1499 Theory \thydx{Arith} develops arithmetic on the natural numbers
1561 Theory \thydx{Int} defines the integers, as equivalence classes of natural
2359   \item Theory \isa{Trancl} defines the transitive closure of a relation
2362   \item Theory \isa{WF} proves the well-founded recursion theorem, using an
2366   \item Theory \isa{Ord} defines the notions of transitive set and ordinal
2372   \item Theory \isa{Epsilon} derives $\varepsilon$-induction and
2382 \item Theory \isa{Rel} defines the basic properties of relations, such as
2385 \item Theory \isa{EquivClass} develops a theory of equivalence
2388 \item Theory \isa{Order} defines partial orderings, total orderings and
2391 \item Theory \isa{OrderArith} defines orderings on sum and product sets.
2395 \item Theory \isa{OrderType} defines order types.  Every wellordering is
2398 \item Theory \isa{Cardinal} defines equipollence and cardinal numbers.
2400 \item Theory \isa{CardinalArith} defines cardinal addition and
2410 \item Theory \isa{AC} asserts the Axiom of Choice and proves some simple
2413 \item Theory \isa{Zorn} proves Hausdorff's Maximal Principle, Zorn's Lemma
2417 \item Theory \isa{Cardinal\_AC} uses AC to prove simplified theorems about
2423 \item Theory \isa{InfDatatype} proves theorems to justify infinitely
2448 \item Theory \isa{Ramsey} proves the finite exponent 2 version of
2452 \item Theory \isa{Integ} develops a theory of the integers as
2455 \item Theory \isa{Primrec} develops some computation theory.  It
2459 \item Theory \isa{Primes} defines the Greatest Common Divisor of two
2462 \item Theory \isa{Bin} defines a datatype for two's complement binary
2466 \item Theory \isa{BT} defines the recursive data structure $\isa{bt}(A)$, labelled binary trees.
2468 \item Theory \isa{Term} defines a recursive data structure for terms
2471 \item Theory \isa{TF} defines primitives for solving mutually
2476 \item Theory \isa{Prop} proves soundness and completeness of
2481 \item Theory \isa{ListN} inductively defines the lists of $n$
2484 \item Theory \isa{Acc} inductively defines the accessible part of a
2487 \item Theory \isa{Comb} defines the datatype of combinators and
2492 \item Theory \isa{LList} defines lazy lists and a coinduction