diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/faq/FAQ.tex | 7 | ||||
| -rw-r--r-- | doc/faq/axioms.fig | 141 |
2 files changed, 102 insertions, 46 deletions
diff --git a/doc/faq/FAQ.tex b/doc/faq/FAQ.tex index 7355838a5d..46351e23df 100644 --- a/doc/faq/FAQ.tex +++ b/doc/faq/FAQ.tex @@ -478,8 +478,9 @@ equations have to be treated by hand or using specialised tactics. \Question{What axioms can be safely added to {\Coq}?} There are a few typical useful axioms that are independent from the -Calculus of Inductive Constructions and that can be safely added to -{\Coq}. These axioms are stated in the directory {\tt Logic} of the +Calculus of Inductive Constructions and that are considered consistent with +the theory of {\Coq}. +Most of these axioms are stated in the directory {\tt Logic} of the standard library of {\Coq}. The most interesting ones are \begin{itemize} @@ -487,6 +488,8 @@ standard library of {\Coq}. The most interesting ones are \item Proof-irrelevance: $\forall A:Prop \forall p_1 p_2:A, p_1=p_2$ \item Unicity of equality proofs (or equivalently Streicher's axiom $K$): $\forall A \forall x y:A \forall p_1 p_2:x=y, p_1=p_2$ +\item Hilbert's $\epsilon$ operator: if $A \neq \emptyset$, then there is $\epsilon_P$ such that $\exists x P(x) \rightarrow P(\epsilon_P)$ +\item Church's $\iota$ operator: if $A \neq \emptyset$, then there is $\iota_P$ such that $\exists! x P(x) \rightarrow P(\iota_P)$ \item The axiom of unique choice: $\forall x \exists! y R(x,y) \rightarrow \exists f \forall x R(x,f(x))$ \item The functional axiom of choice: $\forall x \exists y R(x,y) \rightarrow \exists f \forall x R(x,f(x))$ \item Extensionality of predicates: $\forall P Q:A\rightarrow Prop, (\forall x, P(x) \leftrightarrow Q(x)) \rightarrow P=Q$ diff --git a/doc/faq/axioms.fig b/doc/faq/axioms.fig index f07759302f..78e448865f 100644 --- a/doc/faq/axioms.fig +++ b/doc/faq/axioms.fig @@ -7,78 +7,131 @@ Letter Single -2 1200 2 -5 1 0 1 0 7 50 -1 -1 0.000 0 0 0 1 3600.000 6750.000 3600 6900 3450 6750 3600 6600 +5 1 0 1 0 7 50 -1 -1 0.000 0 1 1 0 14032.500 7222.500 4725 3825 4425 4800 4200 6000 1 1 1.00 60.00 120.00 -5 1 0 1 0 7 50 -1 -1 0.000 0 0 0 1 3600.000 6450.000 3600 6600 3450 6450 3600 6300 +5 1 0 1 0 7 50 -1 -1 0.000 0 0 0 1 3600.000 8925.000 3600 9075 3450 8925 3600 8775 1 1 1.00 60.00 120.00 -5 1 0 1 0 7 50 -1 -1 0.000 0 0 1 1 3600.000 6150.000 3600 6300 3450 6150 3600 6000 +5 1 0 1 0 7 50 -1 -1 0.000 0 0 0 1 3600.000 8625.000 3600 8775 3450 8625 3600 8475 1 1 1.00 60.00 120.00 +5 1 0 1 0 7 50 -1 -1 0.000 0 0 1 1 3600.000 8325.000 3600 8475 3450 8325 3600 8175 1 1 1.00 60.00 120.00 -5 1 0 1 0 7 50 -1 -1 0.000 0 0 1 1 3600.000 6450.000 3600 6600 3450 6450 3600 6300 1 1 1.00 60.00 120.00 +5 1 0 1 0 7 50 -1 -1 0.000 0 0 1 1 3600.000 8625.000 3600 8775 3450 8625 3600 8475 1 1 1.00 60.00 120.00 -5 1 0 1 0 7 50 -1 -1 0.000 0 0 1 1 3600.000 6750.000 3600 6900 3450 6750 3600 6600 1 1 1.00 60.00 120.00 +5 1 0 1 0 7 50 -1 -1 0.000 0 0 1 1 3600.000 8925.000 3600 9075 3450 8925 3600 8775 1 1 1.00 60.00 120.00 -5 1 0 1 0 7 50 -1 -1 0.000 0 0 1 1 3600.000 7050.000 3600 7200 3450 7050 3600 6900 1 1 1.00 60.00 120.00 +5 1 0 1 0 7 50 -1 -1 0.000 0 0 1 1 3600.000 9225.000 3600 9375 3450 9225 3600 9075 1 1 1.00 60.00 120.00 -5 1 0 1 0 7 50 -1 -1 0.000 0 1 1 0 14032.500 5272.500 4725 1875 4425 2850 4200 4050 1 1 1.00 60.00 120.00 -2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 +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 - 4200 5175 4200 5775 +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 - 7050 5175 4575 5775 + 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 - 4200 4275 4200 4875 + 7725 3900 7200 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 - 4950 4275 7125 4875 -2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2 + 7200 6225 7200 7050 +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 - 7725 1950 7200 4050 + 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 - 4350 3075 7350 1950 + 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 + 3375 3225 3375 3600 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 - 7200 4275 7200 4875 -2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 0 0 2 - 3075 1875 3975 1875 + 3373 1950 3376 2250 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 - 5550 3675 5550 4050 + 3375 2625 3375 3000 2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 0 0 2 - 4575 4050 6450 4050 -2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 1 2 + 2175 3600 3750 3600 +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 2475 2475 2475 +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 + 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 - 3525 1875 3525 2250 + 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 - 2325 1875 2250 3975 + 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 + 3075 1725 2025 1725 +2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 0 0 4 + 8025 5925 8250 5925 9000 4950 9150 4950 +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 + 8625 5400 8250 3900 +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 + 7050 7350 4575 7950 +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 0 2 + 1 1 1.00 60.00 120.00 + 4714 6255 7039 7080 +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 + 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 - 7800 1275 2100 1275 -4 0 0 50 -1 0 12 0.0000 4 135 1305 6600 5100 Proof-irrelevance\001 -4 0 0 50 -1 0 12 0.0000 4 135 1260 3675 4200 Excluded-middle\001 -4 0 0 50 -1 0 12 0.0000 4 180 1830 6900 1800 Predicate extensionality\001 -4 0 0 50 -1 0 12 0.0000 4 180 1050 3375 3525 (Diaconescu)\001 -4 0 0 50 -1 0 12 0.0000 4 180 1905 4650 3600 Propositional degeneracy\001 -4 0 0 50 -1 0 12 0.0000 4 135 1800 3825 1800 Relational choice axiom\001 -4 0 0 50 -1 0 12 0.0000 4 180 1575 1725 1800 Description principle\001 -4 0 0 50 -1 0 12 0.0000 4 135 1830 2550 2400 Functional choice axiom\001 -4 0 0 50 -1 0 12 0.0000 4 195 2340 3600 5100 Decidability of equality on $A$\001 -4 0 0 50 -1 0 12 0.0000 4 180 2175 4425 4575 (needs Prop-impredicativity)\001 -4 0 0 50 -1 0 12 0.0000 4 180 705 5025 4725 (Berardi)\001 -4 0 0 50 -1 0 12 0.0000 4 180 1620 1500 3075 (if Set impredicative)\001 -4 0 0 50 -1 0 12 0.0000 4 135 1560 1500 4200 Not excluded-middle\001 -4 0 0 50 -1 0 12 0.0000 4 135 1080 3600 6000 Axiom K on A\001 -4 0 0 50 -1 0 12 0.0000 4 180 4800 3600 7200 Invariance by substitution of reflexivity proofs for equality on A\001 -4 0 0 50 -1 0 12 0.0000 4 180 2100 6150 4200 Propositional extensionality\001 -4 0 0 50 -1 0 12 0.0000 4 180 5700 2100 1200 The dependency graph of axioms in the Calculus of Inductive Constructions\001 -4 0 0 50 -1 0 12 0.0000 4 180 3210 3600 6900 Injectivity of equality on sigma-types on A\001 -4 0 0 50 -1 0 12 0.0000 4 180 3735 3600 6300 Uniqueness of reflexivity proofs for equality on A\001 -4 0 0 50 -1 0 12 0.0000 4 180 2670 3600 6600 Uniqueness of equality proofs on A\001 + 4425 4875 7350 3825 +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 |