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

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.