# Predicate logic proof

I need to prove: ∀xRax → ∀x∃yRyx

My available axioms are:

1. ϕ → (Ψ→ϕ )
2. (ϕ → (Ψ→χ)) → ((ϕ→Ψ) → (ϕ→χ)
3. (~Ψ→~ϕ) → ((~Ψ→ϕ) →Ψ)
4. ∀αϕ→ϕ(β / α)
5. ∀α(ϕ→Ψ) → (ϕ→∀αΨ)

Our rules are modus ponens and universal generalization.

How do I do this?

From Ax.4, by Contraposition and using the abbreviation of ¬∀¬ with we can prove :

ϕ(t / x)→∃xϕ.

Now :

1) ⊢ ∀xRax → Rab --- Ax.4

2) ∀xRax --- premise [a]

3) Rab --- from 1) and 2) by Modus Ponens

4) ⊢ Rab → ∃yRay --- from Ax.4

5) ∃yRay --- from 3) and 4) by Modus Ponens

6) ∀x∃yRxy --- from 5) by Universal Generalization

7) ∀xRax → ∀x∃yRxy --- from 2) and 6) by Deduction Theorem.

• How do we get to step 4 from contraposition and axiom 4? Mar 1, 2017 at 16:05
• @RyanT. - deriving with 1)-3) the necessary tautologies : (p → q) → (¬q → ¬p). Mar 1, 2017 at 16:16
• So we can get: ~ϕ(β / α)→~∀αϕ from contraposition, but how does this lead to ϕ(β / α)→∃αϕ ? Mar 1, 2017 at 16:53
• @RyanT. - NO; you have to consider the axiom ⊢ ∀y¬Ray → ¬Rab, contrapose it to get : ⊢ ¬¬Rab→¬∀y¬Ray and then use Double Negation and the abbreviation to get : ⊢ Rab→∃yRay. Mar 1, 2017 at 16:57