diff options
Diffstat (limited to 'doc/faq/axioms.fig')
| -rw-r--r-- | doc/faq/axioms.fig | 100 |
1 files changed, 47 insertions, 53 deletions
diff --git a/doc/faq/axioms.fig b/doc/faq/axioms.fig index 78e448865..963178503 100644 --- a/doc/faq/axioms.fig +++ b/doc/faq/axioms.fig @@ -1,4 +1,4 @@ -#FIG 3.2 +#FIG 3.2 Produced by xfig version 3.2.5c Landscape Center Inches @@ -27,14 +27,6 @@ Single 1 1 1.00 60.00 120.00 5 1 0 1 0 7 50 -1 -1 0.000 0 1 1 0 6309.515 5767.724 4200 3825 3450 5550 3825 7200 1 1 1.00 60.00 120.00 -6 2025 300 7725 525 -2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 0 0 2 - 7725 525 2025 525 -4 0 0 50 -1 0 12 0.0000 4 180 5700 2025 450 The dependency graph of axioms in the Calculus of Inductive Constructions\001 --6 -2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 - 1 1 1.00 60.00 120.00 - 4200 6225 4200 7200 2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 1 1 1.00 60.00 120.00 7725 3900 7200 6000 @@ -45,8 +37,6 @@ Single 1 1 1.00 60.00 120.00 1 1 1.00 60.00 120.00 5550 5625 5550 6000 -2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 0 0 2 - 4575 6000 6450 6000 2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 1 2 1 1 1.00 60.00 120.00 1 1 1.00 60.00 120.00 @@ -68,12 +58,6 @@ Single 3374 1125 3377 1425 2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 1 1 1.00 60.00 120.00 - 1049 1950 1052 2250 -2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 - 1 1 1.00 60.00 120.00 - 1048 1125 1051 1425 -2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 - 1 1 1.00 60.00 120.00 3075 975 1575 975 2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 1 1 1.00 60.00 120.00 @@ -89,49 +73,59 @@ Single 2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 1 1 1.00 60.00 120.00 4200 7500 4200 7950 +2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 1 2 + 1 1 1.00 60.00 120.00 + 1 1 1.00 60.00 120.00 + 1139 2771 1364 3521 +2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 0 0 2 + 4425 4875 7350 3825 2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 1 1 1.00 60.00 120.00 - 4714 6255 7039 7080 + 1048 1125 1051 1425 +2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 + 1 1 1.00 60.00 120.00 + 1049 1950 1052 2250 2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 1 1 1.00 60.00 120.00 1500 3900 2175 6000 -2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 1 2 +2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 0 0 2 + 4575 6000 6450 6000 +2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 1 1 1.00 60.00 120.00 + 4714 6255 7039 7080 +2 1 0 1 -1 7 50 -1 -1 0.000 0 0 -1 1 0 2 1 1 1.00 60.00 120.00 - 1139 2771 1364 3521 -2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 0 0 2 - 4425 4875 7350 3825 + 4200 6225 4200 7200 3 0 0 1 0 7 50 -1 -1 0.000 0 0 0 4 6450 7050 4050 6675 3750 6825 3750 7050 0.000 1.000 1.000 0.000 -4 0 0 50 -1 0 12 0.0000 4 180 1830 6900 3750 Predicate extensionality\001 -4 0 0 50 -1 0 12 0.0000 4 135 1800 3825 3750 Relational choice axiom\001 -4 0 0 50 -1 0 12 0.0000 4 180 2100 6150 6150 Propositional extensionality\001 -4 0 0 50 -1 0 12 0.0000 4 180 1005 450 1050 Operator iota\001 -4 0 0 50 -1 2 12 0.0000 4 135 1020 450 1650 Constructive\001 -4 0 0 50 -1 2 12 0.0000 4 180 1530 450 1875 definite description\001 -4 0 0 50 -1 2 12 0.0000 4 180 2010 9000 5175 Functional extensionality\001 -4 0 0 50 -1 0 12 0.0000 4 180 4740 150 10050 Statements in boldface are the most "interesting" ones for Coq\001 -4 0 0 50 -1 0 12 0.0000 4 180 4800 3600 9375 Invariance by substitution of reflexivity proofs for equality on A\001 -4 0 0 50 -1 0 12 0.0000 4 180 3735 3600 8475 Uniqueness of reflexivity proofs for equality on A\001 -4 0 0 50 -1 0 12 0.0000 4 180 2670 3600 8775 Uniqueness of equality proofs on A\001 -4 0 0 50 -1 0 12 0.0000 4 135 1080 3600 8175 Axiom K on A\001 -4 0 0 50 -1 2 12 0.0000 4 135 1455 6450 7275 Proof-irrelevance\001 -4 0 0 50 -1 2 12 0.0000 4 180 3360 3600 9075 Injectivity of equality on Sigma-types on A\001 -4 0 0 50 -1 0 12 0.0000 4 180 2175 4950 6525 (needs Prop-impredicativity)\001 -4 0 0 50 -1 0 12 0.0000 4 180 705 6000 6750 (Berardi)\001 -4 0 0 50 -1 2 12 0.0000 4 135 1290 3675 6225 Excluded-middle\001 -4 0 0 50 -1 0 12 0.0000 4 180 1905 4950 5550 Propositional degeneracy\001 -4 0 0 50 -1 0 12 0.0000 4 180 1050 3750 5250 (Diaconescu)\001 -4 0 0 50 -1 0 12 0.0000 4 180 2475 3375 7425 Decidability of equality on any A\001 -4 0 0 50 -1 0 12 0.0000 4 180 1620 1275 5025 (if Set impredicative)\001 -4 0 0 50 -1 0 12 0.0000 4 135 1560 1575 6225 Not excluded-middle\001 -4 0 0 50 -1 0 12 0.0000 4 180 1770 450 2625 in propositional context\001 -4 0 0 50 -1 2 12 0.0000 4 135 1020 3150 1650 Constructive\001 -4 0 0 50 -1 2 12 0.0000 4 180 1665 3150 1875 indefinite description\001 -4 0 0 50 -1 0 12 0.0000 4 180 2610 3150 2400 Constructive indefinite description\001 -4 0 0 50 -1 0 12 0.0000 4 180 1770 3150 2625 in propositional context\001 -4 0 0 50 -1 2 12 0.0000 4 135 1935 3150 3150 Functional choice axiom\001 -4 0 0 50 -1 0 12 0.0000 4 135 2100 450 2400 Constructive definite descr.\001 -4 0 0 50 -1 2 12 0.0000 4 180 1845 450 3750 Axiom of unique choice\001 -4 0 0 50 -1 2 12 0.0000 4 180 1365 3150 1050 Operator epsilon\001 +4 0 -1 50 -1 2 12 0.0000 2 135 1440 3675 6225 Excluded-middle\001 +4 0 -1 50 -1 0 12 0.0000 2 180 1065 450 1050 Operator iota\001 +4 0 -1 50 -1 0 12 0.0000 2 180 2850 3150 2400 Constructive indefinite description\001 +4 0 -1 50 -1 0 12 0.0000 2 180 1965 3150 2625 in propositional context\001 +4 0 -1 50 -1 0 12 0.0000 2 135 2235 450 2400 Constructive definite descr.\001 +4 0 -1 50 -1 0 12 0.0000 2 180 1965 450 2625 in propositional context\001 +4 0 -1 50 -1 0 12 0.0000 2 135 1995 3825 3750 Relational choice axiom\001 +4 0 -1 50 -1 0 12 0.0000 2 180 1965 6900 3750 Predicate extensionality\001 +4 0 -1 50 -1 0 12 0.0000 2 180 1710 1275 5025 (if Set impredicative)\001 +4 0 -1 50 -1 0 12 0.0000 2 165 1065 3750 5250 (Diaconescu)\001 +4 0 -1 50 -1 0 12 0.0000 2 180 2070 4950 5550 Propositional degeneracy\001 +4 0 -1 50 -1 0 12 0.0000 2 180 2310 6150 6150 Propositional extensionality\001 +4 0 -1 50 -1 0 12 0.0000 2 180 2325 4950 6525 (needs Prop-impredicativity)\001 +4 0 -1 50 -1 0 12 0.0000 2 165 720 6000 6750 (Berardi)\001 +4 0 -1 50 -1 0 12 0.0000 2 135 1725 1575 6225 Not excluded-middle\001 +4 0 -1 50 -1 0 12 0.0000 2 180 2730 3375 7425 Decidability of equality on any A\001 +4 0 -1 50 -1 0 12 0.0000 2 135 1170 3600 8175 Axiom K on A\001 +4 0 -1 50 -1 0 12 0.0000 2 180 4035 3600 8475 Uniqueness of reflexivity proofs for equality on A\001 +4 0 -1 50 -1 0 12 0.0000 2 180 2865 3600 8775 Uniqueness of equality proofs on A\001 +4 0 -1 50 -1 0 12 0.0000 2 180 5220 3600 9375 Invariance by substitution of reflexivity proofs for equality on A\001 +4 0 -1 50 -1 2 12 0.0000 2 180 2145 9000 5175 Functional extensionality\001 +4 0 -1 50 -1 2 12 0.0000 2 180 3585 3600 9075 Injectivity of equality on Sigma-types on A\001 +4 0 -1 50 -1 2 12 0.0000 2 135 1515 6450 7275 Proof-irrelevance\001 +4 0 -1 50 -1 2 12 0.0000 2 180 1440 3150 1050 Operator epsilon\001 +4 0 -1 50 -1 2 12 0.0000 2 135 1080 3150 1650 Constructive\001 +4 0 -1 50 -1 2 12 0.0000 2 180 1785 3150 1875 indefinite description\001 +4 0 -1 50 -1 2 12 0.0000 2 135 2085 3150 3150 Functional choice axiom\001 +4 0 -1 50 -1 2 12 0.0000 2 135 1080 450 1650 Constructive\001 +4 0 -1 50 -1 2 12 0.0000 2 180 1620 450 1875 definite description\001 +4 0 -1 50 -1 2 12 0.0000 2 180 1980 450 3750 Axiom of unique choice\001 |