# What happens if we try to extract a witness but it actually does not exist from a term of existential type?

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?

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

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}.
Proof.
induction x.
exists k; tauto.
induction x.
exists 0; auto.
destruct IHx as [z G].
exists (S z).
intro H.
elim G; auto.
Defined.


We can prove that t 0 is equal to k:

Theorem A: projT1 (t 0) = k.
Proof.
auto.
Qed.


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.

• Thanks for the example in Coq, Andrej, it clarifies more. – day Dec 17 '10 at 16:35