doc-src/Logics/ZF.tex
 changeset 498 689e2bd78c19 parent 461 170de0c52a9b child 595 96c87d5bb015
equal inserted replaced
497:990d2573efa6 498:689e2bd78c19
   124 {\tt FOL} with additional syntax for finite sets, ordered pairs,
   124 {\tt FOL} with additional syntax for finite sets, ordered pairs,
   125 comprehension, general union/intersection, general sums/products, and
   125 comprehension, general union/intersection, general sums/products, and
   126 bounded quantifiers.  In most other respects, Isabelle implements precisely
   126 bounded quantifiers.  In most other respects, Isabelle implements precisely
   127 Zermelo-Fraenkel set theory.
   127 Zermelo-Fraenkel set theory.
   128
   128
   129 Figure~\ref{zf-constanus} lists the constants and infixes of~\ZF, while
   129 Figure~\ref{zf-constants} lists the constants and infixes of~\ZF, while
   130 Figure~\ref{zf-trans} presents the syntax translations.  Finally,
   130 Figure~\ref{zf-trans} presents the syntax translations.  Finally,
   131 Figure~\ref{zf-syntax} presents the full grammar for set theory, including
   131 Figure~\ref{zf-syntax} presents the full grammar for set theory, including
   132 the constructs of \FOL.
   132 the constructs of \FOL.
   133
   133
   134 Set theory does not use polymorphism.  All terms in {\ZF} have
   134 Set theory does not use polymorphism.  All terms in {\ZF} have
   345 \tdx{Bex_def}            Bex(A,P)  == EX x. x:A & P(x)
   345 \tdx{Bex_def}            Bex(A,P)  == EX x. x:A & P(x)
   346
   346
   347 \tdx{subset_def}         A <= B  == ALL x:A. x:B
   347 \tdx{subset_def}         A <= B  == ALL x:A. x:B
   348 \tdx{extension}          A = B  <->  A <= B & B <= A
   348 \tdx{extension}          A = B  <->  A <= B & B <= A
   349
   349
   350 \tdx{union_iff}          A : Union(C) <-> (EX B:C. A:B)
   350 \tdx{Union_iff}          A : Union(C) <-> (EX B:C. A:B)
   351 \tdx{power_set}          A : Pow(B) <-> A <= B
   351 \tdx{Pow_iff}            A : Pow(B) <-> A <= B
   352 \tdx{foundation}         A=0 | (EX x:A. ALL y:x. ~ y:A)
   352 \tdx{foundation}         A=0 | (EX x:A. ALL y:x. ~ y:A)
   353
   353
   354 \tdx{replacement}        (ALL x:A. ALL y z. P(x,y) & P(x,z) --> y=z) ==>
   354 \tdx{replacement}        (ALL x:A. ALL y z. P(x,y) & P(x,z) --> y=z) ==>
   355                    b : PrimReplace(A,P) <-> (EX x:A. P(x,b))
   355                    b : PrimReplace(A,P) <-> (EX x:A. P(x,b))
   356 \subcaption{The Zermelo-Fraenkel Axioms}
   356 \subcaption{The Zermelo-Fraenkel Axioms}
   617 \tdx{IntD2}        c : A Int B ==> c : B
   617 \tdx{IntD2}        c : A Int B ==> c : B
   618 \tdx{IntE}         [| c : A Int B;  [| c:A; c:B |] ==> P |] ==> P
   618 \tdx{IntE}         [| c : A Int B;  [| c:A; c:B |] ==> P |] ==> P
   619
   619
   620 \tdx{DiffI}        [| c : A;  ~ c : B |] ==> c : A - B
   620 \tdx{DiffI}        [| c : A;  ~ c : B |] ==> c : A - B
   621 \tdx{DiffD1}       c : A - B ==> c : A
   621 \tdx{DiffD1}       c : A - B ==> c : A
   622 \tdx{DiffD2}       [| c : A - B;  c : B |] ==> P
   622 \tdx{DiffD2}       c : A - B ==> c ~: B
   623 \tdx{DiffE}        [| c : A - B;  [| c:A; ~ c:B |] ==> P |] ==> P
   623 \tdx{DiffE}        [| c : A - B;  [| c:A; ~ c:B |] ==> P |] ==> P
   624 \end{ttbox}
   624 \end{ttbox}
   625 \caption{Union, intersection, difference} \label{zf-Un}
   625 \caption{Union, intersection, difference} \label{zf-Un}
   626 \end{figure}
   626 \end{figure}
   627
   627