doc-src/Logics/ZF.tex
 changeset 461 170de0c52a9b parent 349 0ddc495e8b83 child 498 689e2bd78c19
equal inserted replaced
460:5d91bd2db00a 461:170de0c52a9b
   656 \begin{figure}
   656 \begin{figure}
   657 \begin{ttbox}
   657 \begin{ttbox}
   658 \tdx{the_equality}     [| P(a);  !!x. P(x) ==> x=a |] ==> (THE x. P(x)) = a
   658 \tdx{the_equality}     [| P(a);  !!x. P(x) ==> x=a |] ==> (THE x. P(x)) = a
   659 \tdx{theI}             EX! x. P(x) ==> P(THE x. P(x))
   659 \tdx{theI}             EX! x. P(x) ==> P(THE x. P(x))
   660
   660
   661 \tdx{if_P}             P ==> if(P,a,b) = a
   661 \tdx{if_P}              P ==> if(P,a,b) = a
   662 \tdx{if_not_P}        ~P ==> if(P,a,b) = b
   662 \tdx{if_not_P}         ~P ==> if(P,a,b) = b
   663
   663
   664 \tdx{mem_anti_sym}     [| a:b;  b:a |] ==> P
   664 \tdx{mem_asym}         [| a:b;  b:a |] ==> P
   665 \tdx{mem_anti_refl}    a:a ==> P
   665 \tdx{mem_irrefl}       a:a ==> P
   666 \end{ttbox}
   666 \end{ttbox}
   667 \caption{Descriptions; non-circularity} \label{zf-the}
   667 \caption{Descriptions; non-circularity} \label{zf-the}
   668 \end{figure}
   668 \end{figure}
   669
   669
   670
   670
   690 because of the two occurrences of~$\Var{P}$.  However,
   690 because of the two occurrences of~$\Var{P}$.  However,
   691 \tdx{the_equality} does not have this problem and the files contain
   691 \tdx{the_equality} does not have this problem and the files contain
   692 many examples of its use.
   692 many examples of its use.
   693
   693
   694 Finally, the impossibility of having both $a\in b$ and $b\in a$
   694 Finally, the impossibility of having both $a\in b$ and $b\in a$
   695 (\tdx{mem_anti_sym}) is proved by applying the Axiom of Foundation to
   695 (\tdx{mem_asym}) is proved by applying the Axiom of Foundation to
   696 the set $\{a,b\}$.  The impossibility of $a\in a$ is a trivial consequence.
   696 the set $\{a,b\}$.  The impossibility of $a\in a$ is a trivial consequence.
   697
   697
   698 See the file {\tt ZF/upair.ML} for full proofs of the rules discussed in
   698 See the file {\tt ZF/upair.ML} for full proofs of the rules discussed in
   699 this section.
   699 this section.
   700
   700
  1054 \begin{figure}
  1054 \begin{figure}
  1055 \begin{ttbox}
  1055 \begin{ttbox}
  1056 \tdx{QPair_def}       <a;b> == a+b
  1056 \tdx{QPair_def}       <a;b> == a+b
  1057 \tdx{qsplit_def}      qsplit(c,p)  == THE y. EX a b. p=<a;b> & y=c(a,b)
  1057 \tdx{qsplit_def}      qsplit(c,p)  == THE y. EX a b. p=<a;b> & y=c(a,b)
  1058 \tdx{qfsplit_def}     qfsplit(R,z) == EX x y. z=<x;y> & R(x,y)
  1058 \tdx{qfsplit_def}     qfsplit(R,z) == EX x y. z=<x;y> & R(x,y)
  1059 \tdx{qconverse_def}   qconverse(r) == {z. w:r, EX x y. w=<x;y> & z=<y;x>}
  1059 \tdx{qconverse_def}   qconverse(r) == \{z. w:r, EX x y. w=<x;y> & z=<y;x>\}
  1060 \tdx{QSigma_def}      QSigma(A,B)  ==  UN x:A. UN y:B(x). {<x;y>}
  1060 \tdx{QSigma_def}      QSigma(A,B)  == UN x:A. UN y:B(x). \{<x;y>\}
  1061
  1061
  1062 \tdx{qsum_def}        A <+> B      == (\{0\} <*> A) Un (\{1\} <*> B)
  1062 \tdx{qsum_def}        A <+> B      == (\{0\} <*> A) Un (\{1\} <*> B)
  1063 \tdx{QInl_def}        QInl(a)      == <0;a>
  1063 \tdx{QInl_def}        QInl(a)      == <0;a>
  1064 \tdx{QInr_def}        QInr(b)      == <1;b>
  1064 \tdx{QInr_def}        QInr(b)      == <1;b>
  1065 \tdx{qcase_def}       qcase(c,d)   == qsplit(\%y z. cond(y, d(z), c(z)))
  1065 \tdx{qcase_def}       qcase(c,d)   == qsplit(\%y z. cond(y, d(z), c(z)))
  1081 \begin{figure}
  1081 \begin{figure}
  1082 \begin{ttbox}
  1082 \begin{ttbox}
  1083 \tdx{bnd_mono_def}   bnd_mono(D,h) ==
  1083 \tdx{bnd_mono_def}   bnd_mono(D,h) ==
  1084                  h(D)<=D & (ALL W X. W<=X --> X<=D --> h(W) <= h(X))
  1084                  h(D)<=D & (ALL W X. W<=X --> X<=D --> h(W) <= h(X))
  1085
  1085
  1086 \tdx{lfp_def}        lfp(D,h) == Inter({X: Pow(D). h(X) <= X})
  1086 \tdx{lfp_def}        lfp(D,h) == Inter(\{X: Pow(D). h(X) <= X\})
  1087 \tdx{gfp_def}        gfp(D,h) == Union({X: Pow(D). X <= h(X)})
  1087 \tdx{gfp_def}        gfp(D,h) == Union(\{X: Pow(D). X <= h(X)\})
  1088
  1088
  1089
  1089
  1090 \tdx{lfp_lowerbound} [| h(A) <= A;  A<=D |] ==> lfp(D,h) <= A
  1090 \tdx{lfp_lowerbound} [| h(A) <= A;  A<=D |] ==> lfp(D,h) <= A
  1091
  1091
  1092 \tdx{lfp_subset}     lfp(D,h) <= D
  1092 \tdx{lfp_subset}     lfp(D,h) <= D