doc-src/Logics/ZF.tex
 changeset 713 b470cc6326aa parent 595 96c87d5bb015 child 1449 25a7ddf9c080
equal inserted replaced
712:1f5800d2c366 713:b470cc6326aa
   133 Figure~\ref{zf-trans} presents the syntax translations.  Finally,
   133 Figure~\ref{zf-trans} presents the syntax translations.  Finally,
   134 Figure~\ref{zf-syntax} presents the full grammar for set theory, including
   134 Figure~\ref{zf-syntax} presents the full grammar for set theory, including
   135 the constructs of \FOL.
   135 the constructs of \FOL.
   136
   136
   137 Set theory does not use polymorphism.  All terms in {\ZF} have
   137 Set theory does not use polymorphism.  All terms in {\ZF} have
   138 type~\tydx{i}, which is the type of individuals and lies in class~{\tt
   138 type~\tydx{i}, which is the type of individuals and has class~{\tt
   139   logic}.  The type of first-order formulae, remember, is~{\tt o}.
   139   term}.  The type of first-order formulae, remember, is~{\tt o}.
   140
   140
   141 Infix operators include binary union and intersection ($A\union B$ and
   141 Infix operators include binary union and intersection ($A\union B$ and
   142 $A\inter B$), set difference ($A-B$), and the subset and membership
   142 $A\inter B$), set difference ($A-B$), and the subset and membership
   143 relations.  Note that $a$\verb|~:|$b$ is translated to $\neg(a\in b)$.  The
   143 relations.  Note that $a$\verb|~:|$b$ is translated to $\neg(a\in b)$.  The
   144 union and intersection operators ($\bigcup A$ and $\bigcap A$) form the
   144 union and intersection operators ($\bigcup A$ and $\bigcap A$) form the