# Thread: finitism, epsilon calculus

1. ## finitism, epsilon calculus

prove that (∃x A(x) v ∃x B(x)) ----> x ( A(x) v B(x))

using epsilon calculus.

Im using that ∃x A(x) is the same as A(εx A)

2. Wow, this must be one of the most advanced questions in this section. I am not a specialist on epsilon-calculus, but I'll give it a try.

So $\exists x.\,A\lor B\equiv(A\lor B)(\epsilon x.\,A\lor B)\equiv A(\epsilon x.\,A\lor B)\lor B(\epsilon x.\,A\lor B)$, where $\equiv$ means "syntactically equal". Therefore, we need to prove $[A(\epsilon x.\,A)\lor B(\epsilon x.\,B)]\to[A(\epsilon x.\,A\lor B)\lor B(\epsilon x.\,A\lor B)]$. Note that semantically, $\epsilon x.\,A\lor B$ must return the same answer in both occurrences; if $\epsilon x.\,A\lor B$ returned some random witness of $A\lor B$ every time it is called, the formula we need is not necessarily true. In other words, $\epsilon$ is deterministic, just like regular functional symbols.

The structure of the proof is probably similar to that of the proof with $\exists$. I.e., we consider two cases: $\exists x.\,A(x)$ and $\exists x.\,B(x)$. In the first case we take the witness $x_0$ of $A$ and conclude $A(x_0)\lor B(x_0)$, and therefore $\exists x.\,A(x)\lor B(x)$. The second case is similar.

So, from $A(\epsilon x.\,A)$ we conclude $A(\epsilon x.\,A)\lor B(\epsilon x.\,A)\equiv (A\lor B)(\epsilon x.\,A)$. Next, according to the plan, we need to derive $(A\lor B)(\epsilon x.\,A\lor B)$. This is possible using the axiom about $\epsilon$.