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 $\displaystyle \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 $\displaystyle \equiv$ means "syntactically equal". Therefore, we need to prove $\displaystyle [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, $\displaystyle \epsilon x.\,A\lor B$ must return the same answer in both occurrences; if $\displaystyle \epsilon x.\,A\lor B$ returned some random witness of $\displaystyle A\lor B$ every time it is called, the formula we need is not necessarily true. In other words, $\displaystyle \epsilon$ is deterministic, just like regular functional symbols.

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

So, from $\displaystyle A(\epsilon x.\,A)$ we conclude $\displaystyle 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 $\displaystyle (A\lor B)(\epsilon x.\,A\lor B)$. This is possible using the axiom about $\displaystyle \epsilon$.