1

When I prove this: -∃x.P(x) ⊢ ∀x.-P(x) [True]

I did it like that: ∀x.-P(x) ⊢ ∀x.-P(x) because (negative ∃) -∃x.P(x) becomes ∀x.-P(x) so that we can say that it's true.

However, I didn't understand how I can prove something like those:

1) ∃x.∀y.P(x, y) ⊢ ∀y.∃x.P(x, y)

2) ∀xy.[¬(P(x) → Q(x, y))] ⊢ ¬∃yx.[¬(P(y) ∧ ¬Q(y, x))]

Improve this question
2
  • 1
    Since you already understand how to prove -∃x.P(x) ⊢ ∀x.-P(x), then the 2) exercise is a recursive application of it with further implication conversion to disjunction by its definition. 1) exercise is intuitively true for any conceivable model, but to rigorously prove it you need to invoke proof by contradiction first and then use ∃,∀-elim rules to instantiate both its antecedent and consequent to finally arrive at ⊥...
    – Double Knot
    Jan 16, 2022 at 21:45
  • 1
    Thank you for your answer! I figured it out.
    – bladeavis
    Jan 22, 2022 at 17:04

0

Reset to default

You must log in to answer this question.

Browse other questions tagged .