14 \contentsline {subsection}{Deriving the elimination rule}{17} |
14 \contentsline {subsection}{Deriving the elimination rule}{17} |
15 \contentsline {subsection}{Using the derived rules}{18} |
15 \contentsline {subsection}{Using the derived rules}{18} |
16 \contentsline {subsection}{Derived rules versus definitions}{20} |
16 \contentsline {subsection}{Derived rules versus definitions}{20} |
17 \contentsline {chapter}{\numberline {3}Zermelo-Fraenkel set theory}{23} |
17 \contentsline {chapter}{\numberline {3}Zermelo-Fraenkel set theory}{23} |
18 \contentsline {section}{\numberline {3.1}Which version of axiomatic set theory?}{23} |
18 \contentsline {section}{\numberline {3.1}Which version of axiomatic set theory?}{23} |
19 \contentsline {section}{\numberline {3.2}The syntax of set theory}{25} |
19 \contentsline {section}{\numberline {3.2}The syntax of set theory}{24} |
20 \contentsline {section}{\numberline {3.3}Binding operators}{25} |
20 \contentsline {section}{\numberline {3.3}Binding operators}{26} |
21 \contentsline {section}{\numberline {3.4}The Zermelo-Fraenkel axioms}{28} |
21 \contentsline {section}{\numberline {3.4}The Zermelo-Fraenkel axioms}{28} |
22 \contentsline {section}{\numberline {3.5}From basic lemmas to function spaces}{33} |
22 \contentsline {section}{\numberline {3.5}From basic lemmas to function spaces}{33} |
23 \contentsline {subsection}{Fundamental lemmas}{33} |
23 \contentsline {subsection}{Fundamental lemmas}{34} |
24 \contentsline {subsection}{Unordered pairs and finite sets}{36} |
24 \contentsline {subsection}{Unordered pairs and finite sets}{34} |
25 \contentsline {subsection}{Subset and lattice properties}{36} |
25 \contentsline {subsection}{Subset and lattice properties}{37} |
26 \contentsline {subsection}{Ordered pairs}{37} |
26 \contentsline {subsection}{Ordered pairs}{37} |
27 \contentsline {subsection}{Relations}{37} |
27 \contentsline {subsection}{Relations}{37} |
28 \contentsline {subsection}{Functions}{40} |
28 \contentsline {subsection}{Functions}{38} |
29 \contentsline {section}{\numberline {3.6}Further developments}{40} |
29 \contentsline {section}{\numberline {3.6}Further developments}{41} |
30 \contentsline {section}{\numberline {3.7}Simplification rules}{47} |
30 \contentsline {section}{\numberline {3.7}Simplification rules}{49} |
31 \contentsline {section}{\numberline {3.8}The examples directory}{48} |
31 \contentsline {section}{\numberline {3.8}The examples directory}{49} |
32 \contentsline {section}{\numberline {3.9}A proof about powersets}{49} |
32 \contentsline {section}{\numberline {3.9}A proof about powersets}{52} |
33 \contentsline {section}{\numberline {3.10}Monotonicity of the union operator}{51} |
33 \contentsline {section}{\numberline {3.10}Monotonicity of the union operator}{54} |
34 \contentsline {section}{\numberline {3.11}Low-level reasoning about functions}{52} |
34 \contentsline {section}{\numberline {3.11}Low-level reasoning about functions}{55} |
35 \contentsline {chapter}{\numberline {4}Higher-order logic}{55} |
35 \contentsline {chapter}{\numberline {4}Higher-order logic}{58} |
36 \contentsline {section}{\numberline {4.1}Syntax}{55} |
36 \contentsline {section}{\numberline {4.1}Syntax}{58} |
37 \contentsline {subsection}{Types}{55} |
37 \contentsline {subsection}{Types}{58} |
38 \contentsline {subsection}{Binders}{58} |
38 \contentsline {subsection}{Binders}{61} |
39 \contentsline {section}{\numberline {4.2}Rules of inference}{58} |
39 \contentsline {section}{\numberline {4.2}Rules of inference}{61} |
40 \contentsline {section}{\numberline {4.3}Generic packages}{62} |
40 \contentsline {section}{\numberline {4.3}Generic packages}{65} |
41 \contentsline {section}{\numberline {4.4}A formulation of set theory}{63} |
41 \contentsline {section}{\numberline {4.4}A formulation of set theory}{66} |
42 \contentsline {subsection}{Syntax of set theory}{63} |
42 \contentsline {subsection}{Syntax of set theory}{66} |
43 \contentsline {subsection}{Axioms and rules of set theory}{69} |
43 \contentsline {subsection}{Axioms and rules of set theory}{72} |
44 \contentsline {subsection}{Derived rules for sets}{69} |
44 \contentsline {subsection}{Derived rules for sets}{72} |
45 \contentsline {section}{\numberline {4.5}Types}{69} |
45 \contentsline {section}{\numberline {4.5}Types}{72} |
46 \contentsline {subsection}{Product and sum types}{74} |
46 \contentsline {subsection}{Product and sum types}{77} |
47 \contentsline {subsection}{The type of natural numbers, $nat$}{74} |
47 \contentsline {subsection}{The type of natural numbers, $nat$}{77} |
48 \contentsline {subsection}{The type constructor for lists, $\alpha \pcomma list$}{74} |
48 \contentsline {subsection}{The type constructor for lists, $\alpha \pcomma list$}{77} |
49 \contentsline {subsection}{The type constructor for lazy lists, $\alpha \pcomma llist$}{78} |
49 \contentsline {subsection}{The type constructor for lazy lists, $\alpha \pcomma llist$}{81} |
50 \contentsline {section}{\numberline {4.6}Classical proof procedures}{78} |
50 \contentsline {section}{\numberline {4.6}Classical proof procedures}{81} |
51 \contentsline {section}{\numberline {4.7}The examples directory}{78} |
51 \contentsline {section}{\numberline {4.7}The examples directories}{81} |
52 \contentsline {section}{\numberline {4.8}Example: deriving the conjunction rules}{79} |
52 \contentsline {section}{\numberline {4.8}Example: deriving the conjunction rules}{82} |
53 \contentsline {subsection}{The introduction rule}{79} |
53 \contentsline {subsection}{The introduction rule}{82} |
54 \contentsline {subsection}{The elimination rule}{80} |
54 \contentsline {subsection}{The elimination rule}{83} |
55 \contentsline {section}{\numberline {4.9}Example: Cantor's Theorem}{81} |
55 \contentsline {section}{\numberline {4.9}Example: Cantor's Theorem}{84} |
56 \contentsline {chapter}{\numberline {5}First-order sequent calculus}{83} |
56 \contentsline {chapter}{\numberline {5}First-order sequent calculus}{87} |
57 \contentsline {section}{\numberline {5.1}Unification for lists}{83} |
57 \contentsline {section}{\numberline {5.1}Unification for lists}{87} |
58 \contentsline {section}{\numberline {5.2}Syntax and rules of inference}{84} |
58 \contentsline {section}{\numberline {5.2}Syntax and rules of inference}{88} |
59 \contentsline {section}{\numberline {5.3}Tactics for the cut rule}{84} |
59 \contentsline {section}{\numberline {5.3}Tactics for the cut rule}{88} |
60 \contentsline {section}{\numberline {5.4}Tactics for sequents}{88} |
60 \contentsline {section}{\numberline {5.4}Tactics for sequents}{93} |
61 \contentsline {section}{\numberline {5.5}Packaging sequent rules}{89} |
61 \contentsline {section}{\numberline {5.5}Packaging sequent rules}{93} |
62 \contentsline {section}{\numberline {5.6}Proof procedures}{89} |
62 \contentsline {section}{\numberline {5.6}Proof procedures}{94} |
63 \contentsline {subsection}{Method A}{90} |
63 \contentsline {subsection}{Method A}{95} |
64 \contentsline {subsection}{Method B}{90} |
64 \contentsline {subsection}{Method B}{95} |
65 \contentsline {section}{\numberline {5.7}A simple example of classical reasoning}{91} |
65 \contentsline {section}{\numberline {5.7}A simple example of classical reasoning}{95} |
66 \contentsline {section}{\numberline {5.8}A more complex proof}{92} |
66 \contentsline {section}{\numberline {5.8}A more complex proof}{97} |
67 \contentsline {chapter}{\numberline {6}Constructive Type Theory}{95} |
67 \contentsline {chapter}{\numberline {6}Constructive Type Theory}{99} |
68 \contentsline {section}{\numberline {6.1}Syntax}{96} |
68 \contentsline {section}{\numberline {6.1}Syntax}{100} |
69 \contentsline {section}{\numberline {6.2}Rules of inference}{96} |
69 \contentsline {section}{\numberline {6.2}Rules of inference}{100} |
70 \contentsline {section}{\numberline {6.3}Rule lists}{101} |
70 \contentsline {section}{\numberline {6.3}Rule lists}{105} |
71 \contentsline {section}{\numberline {6.4}Tactics for subgoal reordering}{104} |
71 \contentsline {section}{\numberline {6.4}Tactics for subgoal reordering}{108} |
72 \contentsline {section}{\numberline {6.5}Rewriting tactics}{105} |
72 \contentsline {section}{\numberline {6.5}Rewriting tactics}{109} |
73 \contentsline {section}{\numberline {6.6}Tactics for logical reasoning}{105} |
73 \contentsline {section}{\numberline {6.6}Tactics for logical reasoning}{109} |
74 \contentsline {section}{\numberline {6.7}A theory of arithmetic}{106} |
74 \contentsline {section}{\numberline {6.7}A theory of arithmetic}{110} |
75 \contentsline {section}{\numberline {6.8}The examples directory}{106} |
75 \contentsline {section}{\numberline {6.8}The examples directory}{110} |
76 \contentsline {section}{\numberline {6.9}Example: type inference}{108} |
76 \contentsline {section}{\numberline {6.9}Example: type inference}{112} |
77 \contentsline {section}{\numberline {6.10}An example of logical reasoning}{109} |
77 \contentsline {section}{\numberline {6.10}An example of logical reasoning}{113} |
78 \contentsline {section}{\numberline {6.11}Example: deriving a currying functional}{112} |
78 \contentsline {section}{\numberline {6.11}Example: deriving a currying functional}{116} |
79 \contentsline {section}{\numberline {6.12}Example: proving the Axiom of Choice}{113} |
79 \contentsline {section}{\numberline {6.12}Example: proving the Axiom of Choice}{117} |
80 \contentsline {chapter}{\numberline {7}Defining Logics}{118} |
80 \contentsline {chapter}{\numberline {7}Defining Logics}{121} |
81 \contentsline {section}{\numberline {7.1}Precedence grammars}{118} |
81 \contentsline {section}{\numberline {7.1}Precedence grammars}{121} |
82 \contentsline {section}{\numberline {7.2}Basic syntax}{119} |
82 \contentsline {section}{\numberline {7.2}Basic syntax}{122} |
83 \contentsline {subsection}{Logical types and default syntax}{120} |
83 \contentsline {subsection}{Logical types and default syntax}{123} |
84 \contentsline {subsection}{Lexical matters *}{121} |
84 \contentsline {subsection}{Lexical matters *}{124} |
85 \contentsline {subsection}{Inspecting syntax *}{121} |
85 \contentsline {subsection}{Inspecting syntax *}{124} |
86 \contentsline {section}{\numberline {7.3}Abstract syntax trees}{123} |
86 \contentsline {section}{\numberline {7.3}Abstract syntax trees}{126} |
87 \contentsline {subsection}{Parse trees to asts}{125} |
87 \contentsline {subsection}{Parse trees to asts}{128} |
88 \contentsline {subsection}{Asts to terms *}{126} |
88 \contentsline {subsection}{Asts to terms *}{129} |
89 \contentsline {subsection}{Printing of terms *}{126} |
89 \contentsline {subsection}{Printing of terms *}{129} |
90 \contentsline {section}{\numberline {7.4}Mixfix declarations}{128} |
90 \contentsline {section}{\numberline {7.4}Mixfix declarations}{130} |
91 \contentsline {subsection}{Infixes}{130} |
91 \contentsline {subsection}{Infixes}{133} |
92 \contentsline {subsection}{Binders}{130} |
92 \contentsline {subsection}{Binders}{133} |
93 \contentsline {section}{\numberline {7.5}Syntactic translations (macros)}{131} |
93 \contentsline {section}{\numberline {7.5}Syntactic translations (macros)}{134} |
94 \contentsline {subsection}{Specifying macros}{132} |
94 \contentsline {subsection}{Specifying macros}{135} |
95 \contentsline {subsection}{Applying rules}{133} |
95 \contentsline {subsection}{Applying rules}{136} |
96 \contentsline {subsection}{Rewriting strategy}{135} |
96 \contentsline {subsection}{Rewriting strategy}{138} |
97 \contentsline {subsection}{More examples}{135} |
97 \contentsline {subsection}{More examples}{138} |
98 \contentsline {section}{\numberline {7.6}Translation functions *}{138} |
98 \contentsline {section}{\numberline {7.6}Translation functions *}{141} |
99 \contentsline {subsection}{A simple example *}{139} |
99 \contentsline {subsection}{A simple example *}{142} |
100 \contentsline {section}{\numberline {7.7}Example: some minimal logics}{140} |
100 \contentsline {section}{\numberline {7.7}Example: some minimal logics}{143} |