2
$\begingroup$

The curry howard isomorphism states that proofs in intuitionist logic can be represented as terms, and theorems as types.

However, I'm wondering: if we add the classical logical axioms like LEM (and the axiom of choice?), is it then possible to do all classical proofs in type theory?

Or are only theorems that are provable from intuitionist logic, provable in type theory?

$\endgroup$
5
  • $\begingroup$ "Type theory" is not a single thing, but a loosely-related family of foundational proposals. Your answer might well be different between them. Are you talking about Russell-Whitehead PM? Church's simple types? Martin-Löf type theory? Homotopy type theory? $\endgroup$
    – hmakholm left over Monica
    Jul 14, 2018 at 17:45
  • $\begingroup$ @HenningMakholm, I am talking about type theory in general, and in particular proof-assistants. So an answer to my question could be: "It is possible in type theory X because of reason Y, but not in type theory Z because of reason W" $\endgroup$
    – user56834
    Jul 14, 2018 at 18:07
  • $\begingroup$ For an exposition on curry howard for classical logic, see homepages.inf.ed.ac.uk/wadler/papers/dual/dual.pdf $\endgroup$
    – spaceisdarkgreen
    Jul 14, 2018 at 18:08
  • $\begingroup$ Actually, now that I think of it, I am primarily interested in the answer with respect to dependent type theory based on the CoC, as used in the proof assistant Lean or Coq $\endgroup$
    – user56834
    Jul 14, 2018 at 18:09
  • $\begingroup$ @spaceisdarkgreen, thanks! $\endgroup$
    – user56834
    Jul 14, 2018 at 18:09

1 Answer 1

Reset to default
2
$\begingroup$

With both LEM and a type theoretic analogue of the Axiom of Choice, you do end up with a system at least as strong as ZFC. A Coq development demonstrating this is here, created by the author of Sets in types, types in sets. That paper actually claims even more, namely that ZFC+$n$ inaccessible cardinals is encodable into the Calculus of Inductive Constructions (plus the above axioms) with $n+1$ universes. It also goes the other way and encodes CIC with $n$ universes into ZFC + $n$ inaccessible cardinals.

The Coq development actually proves all of the axioms of ZFC except replacement and choice without assuming any axioms (not even LEM). That is, it shows that Coq can encode an intuitionistic variant $Z$ and classical $Z$ if you do include LEM, though CIC(+LEM) is likely quite a bit stronger than $Z$ due to its higher order features. If we assume a type theoretic Axiom of Choice but not LEM, we can prove the Axiom Schema of Collection which is equivalent to the Axiom Schema of Replacement when we add LEM.

$\endgroup$
2
  • $\begingroup$ Thank you. Does this also mean that it is practically doable to write working mathematician's proofs into Coq, without changing the outline of the proof? $\endgroup$
    – user56834
    Jul 15, 2018 at 2:45
  • $\begingroup$ I would say it's about as practically doable to convert an informal proof to Coq as it is to Mizar, say. How practical that is is up for debate. Most informal proofs aren't too tied to a foundational system and rarely are they really plumbing the depths of ZFC. Formalizing an informal proof into Coq is going to maintain the high level structure because Coq is designed to capture typical patterns of reasoning. Sometimes you'll need to assume extra stuff, but that's no different than ZFC. That you can achieve the power of ZFC by adding a few axioms is largely irrelevant. $\endgroup$
    – Derek Elkins left SE
    Jul 15, 2018 at 3:41

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.