Multiple universal quantifiers in an argument

Question

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 --

x0

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

-- assumption block 2 --

7. 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?

Answer 1

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)).

Answer 2

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.

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.

---

References

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/