# help with deductive proof

∀x (Fx ∨ x=c), ¬Fb ∧ Gb |- ¬Fa → Ga

So far I don't understand how to switch variables around to prove the result. I've got a subproof set up assuming "¬Fa" in order to derive "Ga".

In that proof I reached "F(b) ∨ b = c" and tried to use an or-elimination, but I couldn't get past "b = c".

Help!!

We need first-order logic with equality.

We have :

1) ∀x (Fx ∨ x=c)

2) ¬Fb ∧ Gb

3) ¬Fa → Ga

and we want to derive 3) from 1) and 2).

I think that the "trick" is to rewrite 1) as :

a) ∀x (¬Fx → x=c)

b) ¬Fb --- from 2) by ∧-elim

c) ¬Fb → b=c --- from a) by ∀-elim

d) b=c --- from b) and c) by →-elim (modus ponens)

e) ¬Fa --- assumed

f) ¬Fa → a=c --- from a) by ∀-elim

g) a=c --- from e) and f) by →-elim (modus ponens)

h) a=b --- from d) and g) and laws of equality

i) Gb --- from 2) by ∧-elim

j) Ga --- from h) and i) and laws of equality

k) ¬Fa → Ga --- form e) and j) by →-intro, "discharging" assumption e).

Note

The above "trick" can be avoided using Disjunctive Syllogism : form P and ¬P ∨ Q, infer Q.

• Ahh yes, I didn't see it that way because our system doesn't allow plain rewriting like that. I would need a proof to get to a→c from ¬avc. I did however manage to solve it using V elimination twice. once for the ~Fa assumption and again for me b = c assumption but I also did another ∀-elim to get a = c and go from there. – John Aug 30 '14 at 18:36
• care to help me out on another? – John Aug 30 '14 at 18:44
• @John (There's a button marked ^ for any answers on the site you find useful and clear.) – AndrewC Aug 31 '14 at 9:24

Here is a proof using disjunctive syllogism (DS) that Mauro ALLEGRANZA suggested as an alternative. The two premises are in lines 1 and 2. In lines 3 and 4 I use conjunction elimination (∧E) to separate the two parts of the conjunction onto separate lines.

On line 5, I used universal elimination (∀E) naming "x" as "b".

On line 6 I used disjunctive syllogism (DS) noting that since Fb is contradicted by line 3, the other side of the disjunction (b = c) must be the case.

With this setup I assume the antecedent of the desired conditional (¬Fa) and universal elimination again, replacing "x" with "a" this time.

Again disjunctive syllogism allows me to access "a = c".

On lines 10 and 11 I use equality elimination to first get "Gc" from "Gb" and "b = c" and then what I want for the consequent of the conditional "Ga" from "Gc" and "a = c". At that point I can introduction the conditional (→I) which completes the proof.

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/