2

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?

0

1 Answer 1

2

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.

4
  • How do we get to step 4 from contraposition and axiom 4?
    – Ryan T.
    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 ϕ(β / α)→∃αϕ ?
    – Ryan T.
    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

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .