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


2 Answers 2


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, 2014 at 18:36
  • care to help me out on another?
    – John
    Aug 30, 2014 at 18:44
  • @John (There's a button marked ^ for any answers on the site you find useful and clear.)
    – AndrewC
    Aug 31, 2014 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/

You must log in to answer this question.

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