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