doc-src/Logics/logics.toc
 author lcp Tue May 03 18:38:28 1994 +0200 (1994-05-03) changeset 359 b5a2e9503a7a parent 136 a9015b16a0e5 child 465 d4bf81734dfe permissions -rw-r--r--
final Springer version
 lcp@359 ` 1` ```\contentsline {chapter}{\numberline {1}Basic Concepts}{1} ``` lcp@359 ` 2` ```\contentsline {section}{\numberline {1.1}Syntax definitions}{2} ``` lcp@104 ` 3` ```\contentsline {section}{\numberline {1.2}Proof procedures}{3} ``` lcp@359 ` 4` ```\contentsline {chapter}{\numberline {2}First-Order Logic}{4} ``` lcp@104 ` 5` ```\contentsline {section}{\numberline {2.1}Syntax and rules of inference}{4} ``` lcp@104 ` 6` ```\contentsline {section}{\numberline {2.2}Generic packages}{8} ``` lcp@104 ` 7` ```\contentsline {section}{\numberline {2.3}Intuitionistic proof procedures}{8} ``` lcp@104 ` 8` ```\contentsline {section}{\numberline {2.4}Classical proof procedures}{10} ``` lcp@104 ` 9` ```\contentsline {section}{\numberline {2.5}An intuitionistic example}{11} ``` lcp@104 ` 10` ```\contentsline {section}{\numberline {2.6}An example of intuitionistic negation}{12} ``` lcp@104 ` 11` ```\contentsline {section}{\numberline {2.7}A classical example}{14} ``` lcp@359 ` 12` ```\contentsline {section}{\numberline {2.8}Derived rules and the classical tactics}{15} ``` lcp@359 ` 13` ```\contentsline {subsection}{Deriving the introduction rule}{16} ``` lcp@104 ` 14` ```\contentsline {subsection}{Deriving the elimination rule}{17} ``` lcp@359 ` 15` ```\contentsline {subsection}{Using the derived rules}{17} ``` lcp@359 ` 16` ```\contentsline {subsection}{Derived rules versus definitions}{19} ``` lcp@359 ` 17` ```\contentsline {chapter}{\numberline {3}Zermelo-Fraenkel Set Theory}{22} ``` lcp@359 ` 18` ```\contentsline {section}{\numberline {3.1}Which version of axiomatic set theory?}{22} ``` lcp@359 ` 19` ```\contentsline {section}{\numberline {3.2}The syntax of set theory}{23} ``` lcp@359 ` 20` ```\contentsline {section}{\numberline {3.3}Binding operators}{25} ``` lcp@359 ` 21` ```\contentsline {section}{\numberline {3.4}The Zermelo-Fraenkel axioms}{27} ``` lcp@359 ` 22` ```\contentsline {section}{\numberline {3.5}From basic lemmas to function spaces}{30} ``` lcp@359 ` 23` ```\contentsline {subsection}{Fundamental lemmas}{30} ``` lcp@359 ` 24` ```\contentsline {subsection}{Unordered pairs and finite sets}{32} ``` lcp@359 ` 25` ```\contentsline {subsection}{Subset and lattice properties}{32} ``` lcp@359 ` 26` ```\contentsline {subsection}{Ordered pairs}{36} ``` lcp@359 ` 27` ```\contentsline {subsection}{Relations}{36} ``` lcp@359 ` 28` ```\contentsline {subsection}{Functions}{37} ``` lcp@359 ` 29` ```\contentsline {section}{\numberline {3.6}Further developments}{38} ``` lcp@359 ` 30` ```\contentsline {section}{\numberline {3.7}Simplification rules}{47} ``` lcp@359 ` 31` ```\contentsline {section}{\numberline {3.8}The examples directory}{47} ``` lcp@359 ` 32` ```\contentsline {section}{\numberline {3.9}A proof about powersets}{48} ``` lcp@359 ` 33` ```\contentsline {section}{\numberline {3.10}Monotonicity of the union operator}{51} ``` lcp@359 ` 34` ```\contentsline {section}{\numberline {3.11}Low-level reasoning about functions}{52} ``` lcp@359 ` 35` ```\contentsline {chapter}{\numberline {4}Higher-Order Logic}{55} ``` lcp@359 ` 36` ```\contentsline {section}{\numberline {4.1}Syntax}{55} ``` lcp@359 ` 37` ```\contentsline {subsection}{Types}{57} ``` lcp@359 ` 38` ```\contentsline {subsection}{Binders}{58} ``` lcp@359 ` 39` ```\contentsline {subsection}{The {\ptt let} and {\ptt case} constructions}{58} ``` lcp@359 ` 40` ```\contentsline {section}{\numberline {4.2}Rules of inference}{58} ``` lcp@359 ` 41` ```\contentsline {section}{\numberline {4.3}A formulation of set theory}{60} ``` lcp@359 ` 42` ```\contentsline {subsection}{Syntax of set theory}{65} ``` lcp@359 ` 43` ```\contentsline {subsection}{Axioms and rules of set theory}{69} ``` lcp@359 ` 44` ```\contentsline {section}{\numberline {4.4}Generic packages and classical reasoning}{71} ``` lcp@359 ` 45` ```\contentsline {section}{\numberline {4.5}Types}{73} ``` lcp@359 ` 46` ```\contentsline {subsection}{Product and sum types}{73} ``` lcp@359 ` 47` ```\contentsline {subsection}{The type of natural numbers, {\ptt nat}}{73} ``` lcp@359 ` 48` ```\contentsline {subsection}{The type constructor for lists, {\ptt list}}{76} ``` lcp@359 ` 49` ```\contentsline {subsection}{The type constructor for lazy lists, {\ptt llist}}{76} ``` lcp@359 ` 50` ```\contentsline {section}{\numberline {4.6}The examples directories}{79} ``` lcp@359 ` 51` ```\contentsline {section}{\numberline {4.7}Example: Cantor's Theorem}{80} ``` lcp@359 ` 52` ```\contentsline {chapter}{\numberline {5}First-Order Sequent Calculus}{82} ``` lcp@359 ` 53` ```\contentsline {section}{\numberline {5.1}Unification for lists}{82} ``` lcp@359 ` 54` ```\contentsline {section}{\numberline {5.2}Syntax and rules of inference}{84} ``` lcp@359 ` 55` ```\contentsline {section}{\numberline {5.3}Tactics for the cut rule}{86} ``` lcp@359 ` 56` ```\contentsline {section}{\numberline {5.4}Tactics for sequents}{87} ``` lcp@359 ` 57` ```\contentsline {section}{\numberline {5.5}Packaging sequent rules}{88} ``` lcp@359 ` 58` ```\contentsline {section}{\numberline {5.6}Proof procedures}{88} ``` lcp@359 ` 59` ```\contentsline {subsection}{Method A}{89} ``` lcp@359 ` 60` ```\contentsline {subsection}{Method B}{89} ``` lcp@359 ` 61` ```\contentsline {section}{\numberline {5.7}A simple example of classical reasoning}{90} ``` lcp@359 ` 62` ```\contentsline {section}{\numberline {5.8}A more complex proof}{91} ``` lcp@359 ` 63` ```\contentsline {chapter}{\numberline {6}Constructive Type Theory}{93} ``` lcp@359 ` 64` ```\contentsline {section}{\numberline {6.1}Syntax}{95} ``` lcp@359 ` 65` ```\contentsline {section}{\numberline {6.2}Rules of inference}{95} ``` lcp@359 ` 66` ```\contentsline {section}{\numberline {6.3}Rule lists}{101} ``` lcp@359 ` 67` ```\contentsline {section}{\numberline {6.4}Tactics for subgoal reordering}{101} ``` lcp@359 ` 68` ```\contentsline {section}{\numberline {6.5}Rewriting tactics}{102} ``` lcp@359 ` 69` ```\contentsline {section}{\numberline {6.6}Tactics for logical reasoning}{103} ``` lcp@359 ` 70` ```\contentsline {section}{\numberline {6.7}A theory of arithmetic}{105} ``` lcp@359 ` 71` ```\contentsline {section}{\numberline {6.8}The examples directory}{105} ``` lcp@359 ` 72` ```\contentsline {section}{\numberline {6.9}Example: type inference}{105} ``` lcp@359 ` 73` ```\contentsline {section}{\numberline {6.10}An example of logical reasoning}{107} ``` lcp@359 ` 74` ```\contentsline {section}{\numberline {6.11}Example: deriving a currying functional}{110} ``` lcp@359 ` 75` ```\contentsline {section}{\numberline {6.12}Example: proving the Axiom of Choice}{111} ```