Given a term t : ∀x.∃y.(¬(x = 0) ⇒ x = S(y)) in Martin-Lof's type theory, what's the value of w(t(0)), where w is the operator that extracts the witness of a term of existential type?

  • $\begingroup$ I think you mean $\neg(x=0)$. $\endgroup$ Commented Nov 29, 2010 at 21:41
  • $\begingroup$ Yes, Mark, thanks for pointing out that, fixed. $\endgroup$
    – day
    Commented Nov 29, 2010 at 22:16

2 Answers 2


Any value. It depends upon which $t$ you are given. A term of type $\exists y.(\neg(0 = 0) \Rightarrow 0 = S(y))$ is a pair of an int $y$ and a function that takes a proof of $\neg(0=0)$ and gives you a proof of $0 = S(y)$. You can use a term of type $\neg(0 = 0)$ and type $0 = 0$ (from reflexivity) to derive a term of any type you want. This includes a term of type $0 = S(0)$, $0 = S(1)$, $\ldots$. So, you can make $y$ any integer you want.


To demonstrate Mark's answer, consider the following proof t of your statement, written in Coq. In the proof we assume that a parameter k of type nat is given. We use k as the value of y in case x = 0:

Parameter k : nat.

Theorem t : forall x : nat, { y : nat | x <> 0 -> x = S y}.
  induction x.
  exists k; tauto.
  induction x.
  exists 0; auto.
  destruct IHx as [z G].
  exists (S z).
  intro H.
  elim G; auto.

We can prove that t 0 is equal to k:

Theorem A: projT1 (t 0) = k.

The protT1 is there because t 0 is not just a natural number, but actually a natural number with a proof that 0 <> 0 -> 0 = S y and projT1 throws away the proof.

The extracted Ocaml code for t, obtained with the command Extraction k is

(** val t : nat -> nat **)

let rec t = function
  | O -> k
  | S n0 -> (match n0 with
              | O -> O
              | S n1 -> S (t n0))

Again we can see t 0 is equal to k, which was an aribtrarily assumed parameter.

  • $\begingroup$ Thanks for the example in Coq, Andrej, it clarifies more. $\endgroup$
    – day
    Commented Dec 17, 2010 at 16:35

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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