diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-08-01 09:27:26 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-08-01 09:27:26 +0000 |
| commit | d846ae7e7e0a0e9e4e4343f1a4a3efb08a25d40b (patch) | |
| tree | 0349ff096406c23b98917b2985c8f43e0a205905 /theories/Logic/ChoiceFacts.v | |
| parent | 44074272d177ff5828a3027e26121681aad952ae (diff) | |
Commentaires coqdoc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6001 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Logic/ChoiceFacts.v')
| -rw-r--r-- | theories/Logic/ChoiceFacts.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/theories/Logic/ChoiceFacts.v b/theories/Logic/ChoiceFacts.v index 933761612..f7a38cd02 100644 --- a/theories/Logic/ChoiceFacts.v +++ b/theories/Logic/ChoiceFacts.v @@ -8,12 +8,12 @@ (*i $Id$ i*) -(* We show that the functional formulation of the axiom of Choice +(** We show that the functional formulation of the axiom of Choice (usual formulation in type theory) is equivalent to its relational formulation (only formulation of set theory) + the axiom of (parametric) definite description (aka axiom of unique choice) *) -(* This shows that the axiom of choice can be assumed (under its +(** This shows that the axiom of choice can be assumed (under its relational formulation) without known inconsistency with classical logic, though definite description conflicts with classical logic *) @@ -80,7 +80,7 @@ intro H; split; intros [H H0]; exact (description_rel_choice_imp_funct_choice H0 H). Qed. -(* We show that the guarded relational formulation of the axiom of Choice +(** We show that the guarded relational formulation of the axiom of Choice comes from the non guarded formulation in presence either of the independance of premises or proof-irrelevance *) |