∀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".



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


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.

enter image description here

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.


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/

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.