I'd really like your help proving:
1)⊢∃x(AvB)→(∃xAv∃xB)
2)⊢(∃xAv∃xB)→∃x(AvB)
Our proof system contains next Hilbert's axioms:
1.A→(B→A)
2.(A→B)→((A→(B→X))→(A→X))
3.(A&B)→A
4.(A&B)→B
5.(A→B)→((A→X)→(A→(B&X)))
6.A→(AvB)
7.A→(BvA)
8.(A→X)→((B→X)→((AvB)→X))
9.(A→B)→((A→¬B)→¬A)
10.¬¬A→A
And other two axioms: ∀xA→A{t/x}, A{t/x}→∃xA where t is free for assignment instead of x in A.
Finally theres the MP rules:
1.From A,A→B we conclude B
2.From A→B we conclude A→∀xB, where x not included in the set of variables A free
3.From A→B we conclude ∃xA→B, where x not included in the set of variables A free
I tried couple of different ways but didn't come with any smart result.
About the first formula :
a) $A \rightarrow \exists x A$ --- 2nd Axiom for quantifiers
b) $\exists x A \rightarrow ( \exists x A \lor \exists x B )$ --- from your 6)
c) $ [ \exists x A \rightarrow ( \exists x A \lor \exists x B ) ] \rightarrow [ A \rightarrow ( \exists x A \rightarrow ( \exists x A \lor \exists x B ) ) ] $ --- from your 1)
d) $ A \rightarrow ( \exists x A \rightarrow ( \exists x A \lor \exists x B ) ) $ --- from b) and c) by MP
e) $ A \rightarrow ( \exists x A \lor \exists x B ) $ --- from a) and d) using your 2) by MP twice
In the same way, you can get :
f) $ B \rightarrow ( \exists x A \lor \exists x B ) $ --- using your 7)
g) $ ( A \lor B ) \rightarrow ( \exists x A \lor \exists x B ) $ --- from e) and f) using your 8) by MP twice
Now you can get :
h) $ \exists x ( A \lor B ) \rightarrow ( \exists x A \lor \exists x B ) $ --- from g) using your rule 3) ( because $x$ is not free in $( \exists x A \lor \exists x B )$ ).
Following a similar approach, you can try with the second formula.