Consider the argument

∀x∀y((S(x,a)∧ S(a,y))→S(x,y)), ∀x¬S(x,x) ├ ∀x(S(x,a)→¬S(a,x))

My approach to formally proving this was to first eliminate ∀x and use x0 as the free variable. Then afterwards eliminate ∀y and use x0 as the free variable again.

  1. ∀x∀y((S(x,a)∧ S(a,y))→S(x,y)) - Premise
  2. ∀x¬S(x,x) - Premise

-- assumption block 1 --


  1. ¬S(x0,x0) - ∀x e 2
  2. ∀y((S(x0,a)∧S(a,y))→S(x0,y)) - ∀x e 1
  3. (S(x0,a)∧S(a,x0))→S(x0,x0) - ∀y e 4
  4. ¬(S(x0,a)∧S(a,x0)) - MT 5, 3

-- assumption block 2 --

  1. S(x0,a) - assumption

x. ¬S(a,x0) - ?

-- end assumption block 2 --

x + 1. S(x0,a)→¬S(a,x0)

-- end assumption block 1 --

x + 2. ∀x(S(x,a)→¬S(a,x)) ∀x i 3 - x + 1

The issue I'm having, assuming the rest of the proof is on the right track, is how to get from step 7 to step x? In other words, how does one prove ¬(P∧Q) ⊦ P→¬Q?

  • If you are not forced to use natural ded rules, MY in step 6 is Ok; after step 7 you must add another assumption : 8) S(a,x0) and then make the conjunction of 7 and 8, contradicting thus 6) ¬(S(x0,a)∧ S(a,x0)). Form this, reductio and so on ... Sep 6, 2015 at 12:04
  • Thank you. I ended up using your suggestion from the comment as I am allowed to use MT. Sep 6, 2015 at 12:22

2 Answers 2


I'll suggest this approach, using Natura Deduction (see : Ian Chiswell & Wilfrid Hodges, Mathematical Logic (2007)) :

1) ∀x∀y((S(x,a)∧ S(a,y))→S(x,y)) --- premise

2) ∀x¬S(x,x) --- premise

3) ¬S(x,x) --- from 2) by ∀-elimination

4) S(x,a) --- assumed [a]

5) S(a,x) --- assumed [b]

6) S(x,a) ∧ S(a,x) --- from 4) and 5) by ∧-introduction

7) S(x,a)∧ S(a,x) → S(x,x) --- from 1) by ∀-elimination twice

8) S(x,x) --- from 6) and 7) by →-elimination (modus ponens)

9) contradiction with 3) and 8) and thus by RAA (reductio ad absurdum) applied with 5) :

10) ¬S(x,a) --- discharging [b]

11) S(a,x) → ¬S(x,a) --- from 4) and 10) by →-introduction, discharging [a]

Now, the ausiliary assumptions [a] and [b] have been discharged, and we are left with the premises 1) and 2) where x is not free; thus, we can apply ∀-introduction, concluding with :

∀x(S(x,a) → ¬S(a,x)).


The question is: The issue I'm having, assuming the rest of the proof is on the right track, is how to get from step 7 to step x? In other words, how does one prove ¬(P∧Q) ⊦ P→¬Q?

The following proof uses the first seven steps and obtains the final result.

enter image description here

Note that in this proof the name "c" corresponds to the OP's "x0".

The first seven lines are the same as the OP. On line 7 the assumption, "Sca", is made with the goal of reaching "¬Sac" so the conditional can be introduced and then with universal introduction (AI) the proof can be completed.

To see how this proof gets there, note the use of the De Morgan rule (DeM) on line 8 to change line 6 from a conjunction (∧) to a disjunction (∨). With the disjunction, I consider cases intending each case to give me "¬Sac".

In the first case, assuming "¬Sca" and reach a contradiction. That contradiction is not what I want, but having a contradiction and using the explosion rule (X) I can put anything, in particular, "¬Sac", on line 11. So, I let that case give me "¬Sac". For the second case, I already have "¬Sac" so there is nothing to do.

This allows me to eliminate the disjunction on line 13.

On line 14 I introduce the desired conditional.

For more information about these rules see forall x: Calgary Remix.


Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/

P. D. Magnus, Tim Button with additions by J. Robert Loftis remixed and revised by Aaron Thomas-Bolduc, Richard Zach, forallx Calgary Remix: An Introduction to Formal Logic, Winter 2018. http://forallx.openlogicproject.org/

You must log in to answer this question.

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