summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

doc-src/Logics/ZF.tex

changeset 713 | b470cc6326aa |

parent 595 | 96c87d5bb015 |

child 1449 | 25a7ddf9c080 |

equal
deleted
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 |