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

Question

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?

Answer 1

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.

Answer 2

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.