4
$\begingroup$

While studying Coq, I found a few references that impredicative Set might not work well with classical axioms, in particular the axiom of choice.

I'm working on a dependent type system based on the calculus of constructions (with Prop and Set), on which I intend to add Peirce's law on sets, as in the computability side it represents call/cc (capturing/resuming the whole computation).

My question is: is the calculus of constructions* with an impredicative Set, with the excluded middle working on sets (precisely, forall P: Set, ((P -> False) -> P) -> P being of type Set), without the axiom of choice, consistent? I didn't manage to find a reference for that.

(* Would inductive types make any difference, from CoC to CIC?)

$\endgroup$
2
$\begingroup$

I'm not an expert, but my understating was not that it it was inconsistent, but that it implies proof irrelevance. That is, if $s,t:T$ then $s=t$.

This gives many undesirable properties, like having $1=2$, but I'm not sure it actually implies bottom. This answer had similar details.

$\endgroup$
  • $\begingroup$ How are you implementing $1=2$ in the calculus of constructions? In the calculus of inductive constructions, with objects of the inductive type nat, it certainly does imply False (the proof tactic in Coq is discriminate and the proof object is centered around a dependent pattern matching in the type 1=2). $\endgroup$ – Gilles 'SO- stop being evil' Nov 28 '17 at 21:25
  • $\begingroup$ @Giles I should be more clear, my mistake. I think it is contradictory if pattern matching is allowed, since that lets you discriminate between different proofs. I'll update this when I get a chance. $\endgroup$ – jmite Nov 28 '17 at 23:44
  • $\begingroup$ I'm initially designing my type system without inductive types (and pattern matching), but I do intend to add them later. If this changes things (on regard to the excluded middle), that would be useful information as well. $\endgroup$ – paulotorrens Nov 29 '17 at 0:12
  • $\begingroup$ Also, on that post they say "[...] since 2 is a complete lattice [...]", I have no idea what that means. :( $\endgroup$ – paulotorrens Dec 1 '17 at 18:45
  • $\begingroup$ @paulotorrens: $2$ is some type-theoretic version of the two-element set $\{0,1\}$. With the standard (numeric) partial order, this set becomes a lattice which happens to be complete (have suprema and infima of arbitrary subsets). Completeness only holds if some version of the law of excluded middle is available; a constructive substitute which is always complete is the lattice of all subsets of $\{\heartsuit\}$, which contains $\emptyset$ and $\{\heartsuit\}$ (corresponding to $0$ and $1$), but potentially also further elements. $\endgroup$ – Ingo Blechschmidt May 16 '18 at 20:06

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.