Is it possible to add law of excluded middle to Martin-Löf type theory as an axiom? It seems to me, that it's possible to add it to Coq since Coq has a module for non-constructive reasoning. Also, it seems to be impossible to Agda since it leads to inconsistency. But can we add it to plain MLTT? And why it will/won't work?
$\begingroup$
$\endgroup$
asked Dec 23, 2014 at 22:25
Add a comment
|
3 Answers
$\begingroup$
$\endgroup$
10
Law of excluded middle does not make intuitionistic logic inconsistent; intuitionistic logic is in many regards a subset of classical logic (of course classical logic can't have proof objects and there are other diffrences). In Agda you can use the postulate keyword for such things. The following could be added to your postulates.
$LEM : \{A : Set\} \to A \lor \neg A$
I was doing some proofs out of a book on first order logic where I found it more useful to have double negation elimination than LEM.
$\neg\neg E : \{A : Set\} \to \neg\neg A \to A$
One of course implies the other so take your pick.
edit: One of your previous questions gives some insight here as well. cody made mention of Agda being predicative. Martin Lof type theory is predicative (as well as Agda which is basically MLTT). Agda still has large elimination and adding LEM does not make the logic inconsistent. Martin Lof originally tried to base MLTT off of System-F but its impredicative nature kept getting in the way of such things. This is part of the reason why MLTT is predictive.
-
1$\begingroup$ I found this: plato.stanford.edu/entries/logic-intuitionistic which says "Peano arithmetic PA comes from Heyting arithmetic HA by adding LEM". Which although is exactly what you asked for it is strong evidence that adding LEM to intuitionistic logic just gives something closer to classical logic. $\endgroup$– JakeCommented Dec 24, 2014 at 6:56
-
2$\begingroup$ It might be worth noting that while Agda is Predicative, there is no a priori reason why the logic MLTT should be conservative over Heyting Arithmetic, which does not allow quantifying over functions. It is a non-trivial exercise that it does (see "Constructivism in Mathematics", chaper 10) in the absence of universes. With universes this does not hold. Nevertheless, adding EM to MLTT with universes is consistent (with ZFC), as the "usual" set-theoretic model validates it. I'm not certain the axiom of choice isn't necessary though. $\endgroup$– codyCommented Dec 24, 2014 at 20:51
-
1$\begingroup$ Classical logic can have proof objects. $\endgroup$ Commented Dec 26, 2014 at 20:04
-
4$\begingroup$ MLTT can be interpreted in classical set theory, therefore it is consistent to add excluded middle to it. $\endgroup$ Commented Dec 26, 2014 at 20:04
-
3$\begingroup$ I mean the computational interpretation of classical logic whereby we interpret Perice's law using
callcc. $\endgroup$ Commented Dec 27, 2014 at 1:10
$\begingroup$
$\endgroup$
2
Adding LEM to MLTT is no problem. You simply need to assume a term of type forall P:Prop, P \/ ~ P. In Coq, you can use the LEM as follows:
Require Import Classical_Prop.
Print classic.
-
$\begingroup$ It's about Prop but can we say the same about Set? $\endgroup$ Commented Dec 24, 2014 at 6:33
-
$\begingroup$ If you want it in set, just do
forall T:Set, T + (T -> False). $\endgroup$ Commented Aug 23, 2015 at 17:34
$\begingroup$
$\endgroup$
A term that proves the excluded middle will have type:
$$ em:\forall T:\mathrm{Type},\ T\ +\ (T\rightarrow\bot)$$
In MLTT with universes, this can be seen as a kind of choice function, which picks an element from any non-empty type (or provides a proof of emptyness).
In the "usual" set-theoretic model (where function types are interpreted as the set-theoretic function spaces), $\mathrm{Type}$ is interpreted as some universe of sets, and $em$ can be given by invoking some version of the axiom of choice.
This shows that it is consistent to add such a term to "vanilla" MLTT, as it is validated in the set theoretic model.
In some versions of Agda, the set theoretic model cannot be built, in particular when injectivity of type constructors is assumed, for obvious reasons (such constructors are not necessarily injective in set theory!). And indeed, assuming $em$ is contradictory, as discussed in this fascinating exchange: https://lists.chalmers.se/pipermail/agda/2010/001565.html.
Note that there are weakened versions of $em$ which play more nicely with type theory, in particular those coming from Homotopy Type Theory, where EM is allowed only on "proof-irrelevant" types.
