finitism, epsilon calculus

**scubasteve123** · March 24th 2010, 05:37 PM

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)

**emakarov** · March 25th 2010, 04:08 AM

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$ .

Thread: finitism, epsilon calculus

LinkBack

Thread Tools

Display

finitism, epsilon calculus

Similar Math Help Forum Discussions

Solving Delta Epsilon Proof (Given Epsilon)

Epsilon-N

One more epsilon ?

Advanced Calculus - Epsilon-Neighborhoods

calculus help on Limits and epsilon delta

Search Tags