9
$\begingroup$

I am playing with impredicative type theories (CC and UTT). I am not quite familiar with the distinction between $\textsf{Prop}$ and $\textsf{Type}$ as it is not available in MLTT. Here is my question.

Let $\Gamma$ be a valid context and let $A:\textsf{Prop}$, $D:\textsf{Type}$ and $B:D\rightarrow\textsf{Prop}$. My question can be divided into two parts:

  1. By the above definitions, $A\rightarrow\Sigma x:D.B(x)$ is a well-formed type. Is it possible that $A\rightarrow\Sigma x:D.B(x)$ is not a theorem in an empty context but is a theorem in context $\Gamma$?
  2. If $A\rightarrow\Sigma x:D.B(x)$ is not a theorem in an empty context but is a theorem in context $\Gamma$, then what amounts to a proof object of $A\rightarrow\Sigma x:D.B(x)$ in $\Gamma$?

Thanks!

$\endgroup$
1
$\begingroup$

$\newcommand{\Prop}{\mathsf{Prop}}$

If we take $P : \Prop$ to be some independent proposition, then we can take: $$A = ⊤\\D = 2\\B(0) = ¬P\\B(1) = P$$

Then a derivation of $$⊢ ⊤ → Σb:2. B(b)$$ is deciding $P$. If no non-constructive principles are assumed, presumably there is no such derivation. However there is an easy derivation of $$P ⊢ ⊤ → Σb:2.B(b)$$ In the sort of theories you're talking about, constructions in $\Prop$ aren't really very different from those in $\mathsf{Type}$, aside from rules for equality and possible restrictions on eliminators and the like. So a proof term could just look like:

$$p:P ⊢ λt. (1, p) : ⊤ → Σb:2.B(b)$$

I.E. propositional implication and $∀$ are proved by functions, $∧$ and $∃$ by pairs, and $∨$ by terms that look like they belong to a disjoint union, but values of a proposition are considered equal even if they are not syntactically identical, and e.g. you may not be able to do case analysis on an $∨$ value to produce a value of $A : \mathsf{Type}$.

Edit: perhaps I should mention, the bits about how $\Prop$ behaves differently are mostly unrelated to impredicativity, and are instead related to how people think propositions should be different from other types. The possible exception is that impredicative $Σ$ types are inconsistent unless you place restrictions on the way they are eliminated. However, I'm not sure the restrictions I mentioned above are the ones necessary to fix that problem.

$\endgroup$
3
  • $\begingroup$ Hi, a quick question. What do you mean by requiring $D=2$? Or you mean $D$ is $\textsf{Bool}$? Because I see later you mention 0 and 1. Thanks! $\endgroup$ – Samuel Jan 14 at 10:52
  • $\begingroup$ Yeah, I mean the type with two values. Could be $\mathsf{Bool}$, $\mathsf{true}$ and $\mathsf{false}$, too. $\endgroup$ – Dan Doel Jan 14 at 14:55
  • $\begingroup$ I see. Thank you! $\endgroup$ – Samuel Jan 14 at 16:00

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.