diff options
| author | Hugo Herbelin | 2019-10-14 12:54:31 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2019-10-14 12:59:16 +0200 |
| commit | a8166315acaa63252f5753b71ad26d126873bbe4 (patch) | |
| tree | b49ff8f219829b364bb85e2428c9e0a55b224b94 | |
| parent | 1d3c90de94e1c05d42aba704a80ab1135bdc058f (diff) | |
Weak excluded-middle: adding a reference.
| -rw-r--r-- | theories/Logic/ClassicalFacts.v | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/theories/Logic/ClassicalFacts.v b/theories/Logic/ClassicalFacts.v index 98dcd0d122..9ba3db6eff 100644 --- a/theories/Logic/ClassicalFacts.v +++ b/theories/Logic/ClassicalFacts.v @@ -523,11 +523,15 @@ End Weak_proof_irrelevance_CCI. (** ** Weak excluded-middle *) (** The weak classical logic based on [~~A \/ ~A] is referred to with - name KC in [[ChagrovZakharyaschev97]] + name KC in [[ChagrovZakharyaschev97]]. See [[SorbiTerwijn11]] for + a short survey. [[ChagrovZakharyaschev97]] Alexander Chagrov and Michael Zakharyaschev, "Modal Logic", Clarendon Press, 1997. -*) + + [[SorbiTerwijn11]] Andrea Sorbi and Sebastiaan A. Terwijn, + "Generalizations of the weak law of the excluded-middle", Notre + Dame J. Formal Logic, vol 56(2), pp 321-331, 2015. *) Definition weak_excluded_middle := forall A:Prop, ~~A \/ ~A. |