# Fitch Proof by Contradiction help Hi, I'm pretty new to writing formal proofs and I was wondering if I could get some help solving this question.

I've set up the problem and I was thinking of perhaps proving it by contradiction that WeakPref(b,a)->~StrongPref(b,a) but I was unsure how to proceed. I've gotten this far into the proof now, but I am unsure if what I am doing is wrong as I can no longer use universal instantiations. Similarly, I cannot find the contradiction required for ~(StrongPref(b,a) v StrongPref(a,b)).

The rules of inference are named as they are for a reason.

When feel the need to raise a context to derive a target, determine what rule of introduction you will need to deduce the target. That will tell you what assumption you might need to raise and what conclusion you will need to derive.

• When the target is a conditional, like, Indiff(a,b) → ~(StrongPref(b,a) v StrongPref(a,b)), use conditional introduction. Assume the antecedant and derive the consequent.

• When the target is a negation, like ~(StrongPref(b,a) v StrongPref(a,b)), use negation introduction. Assume the positive and derive a contradiction.

On reaching a target that's not produced by an introduction rule, look to the assumptions (and premises) for rules of elimination to fill in the derivations.

• When you have assumed a disjunction, like StrongPref(b,a) v StrongPref(a,b), use disjunction elimination. Assume each case in succession and derive the same consequence.

I'll leave actually deriving the contradiction to you (but, okay, premises 3 and 4 are most useful).

|  Ɐx Ɐy StrongPref(x,y) ↔ ~WeakPref(y,x)
|  Ɐx Ɐy Indiff(x,y) → WeakPref(y,x) ^ WeakPref(x,y)
|  |_ [a]
|  |  |_ [b]
|  |  |  |_ Indiff(a,b)
|  |  |  |  :
|  |  |  |  |_ StrongPref(b,a) v StrongPref(a,b)
|  |  |  |  |  |_ StrongPref(b,a)
|  |  |  |  |  |  :
|  |  |  |  |  |  #
|  |  |  |  |  +
|  |  |  |  |  |_ StrongPref(a,b)
|  |  |  |  |  |  :
|  |  |  |  |  |  #
|  |  |  |  |  #
|  |  |  |  ~(StrongPref(b,a) v StrongPref(a,b))
|  |  |  Indiff(a,b) → ~(StrongPref(b,a) v StrongPref(a,b))
|  |  :


Edit: the completed proof

:
|  Ɐx Ɐy StrongPref(x,y) ↔ ~WeakPref(y,x)
|_ Ɐx Ɐy Indiff(x,y) → WeakPref(y,x) ^ WeakPref(x,y)
|  |_ [a]                                                   Arbitrary Term
|  |  |_ [b]                                                Arbitrary Term
|  |  |  |_ Indiff(a,b)                                     Assumption
|  |  |  |  Ɐy Indiff(a,y) → WeakPref(y,a) ^ WeakPref(a,y)  Universal Elimination
|  |  |  |  Indiff(a,b) → WeakPref(b,a) ^ WeakPref(a,b)     Universal Elimination
|  |  |  |  WeakPref(b,a) ^ WeakPref(a,b)                   Conditional Elimination
|  |  |  |  WeakPref(b,a)                                   Conjunction Elimination
|  |  |  |  WeakPref(a,b)                                   Conjunction Elimination
|  |  |  |  |_ StrongPref(b,a) v StrongPref(a,b)            Assumption
|  |  |  |  |  |_ StrongPref(b,a)                           Assumption
|  |  |  |  |  |  Ɐy StrongPref(b,y) ↔ ~WeakPref(y,b)       Universal Elimination
|  |  |  |  |  |  StrongPref(b,a) ↔ ~WeakPref(a,b)          Universal Elimination
|  |  |  |  |  |  ~WeakPref(a,b)                            Biconditional Elimination
|  |  |  |  |  |  #                                         Negation Elimination
|  |  |  |  |  +
|  |  |  |  |  |_ StrongPref(a,b)
|  |  |  |  |  |  Ɐy StrongPref(a,y) ↔ ~WeakPref(y,a)       Universal Elimination
|  |  |  |  |  |  StrongPref(a,b) ↔ ~WeakPref(b,a)          Universal Elimination
|  |  |  |  |  |  ~WeakPref(b,a)                            Biconditional Elimination
|  |  |  |  |  |  #                                         Negation Elimination
|  |  |  |  |  #                                            Disjunction Elimination
|  |  |  |  ~(StrongPref(b,a) v StrongPref(a,b))            Negation Introduction
|  |  |  Indiff(a,b) → ~(StrongPref(b,a) v StrongPref(a,b)) Conditional Introduction
|  |  Ɐy Indiff(a,y) → ~(StrongPref(y,a) v StrongPref(a,y)) Universal Introduction
|  Ɐx Ɐy Indiff(x,y) → ~(StrongPref(y,x) v StrongPref(x,y)) Universal Introduction

• Hi there, I've managed to prove one contradiction but I cannot seem to do the other. I would be extremely grateful if you could take another look at my proof (in my edited post). Thank you so much for your help so far! Nov 21 '18 at 9:09
• Looks good, @JohnAbercrombie , but don't use negation introduction after each of the subproofs; just use disjunction elimination after both. Nov 21 '18 at 11:29
• @JohnAbercrombie Like so. Nov 22 '18 at 22:44

Here is a proof using a different proof checker. I also made some substitutions.

• For Indiff I used I.
• For StrongPref I used S.
• For WeakPref I used W.

Of the four premises I only used the third and fourth. Here are the concerns:

I've gotten this far into the proof now, but I am unsure if what I am doing is wrong as I can no longer use universal instantiations. Similarly, I cannot find the contradiction required for ~(StrongPref(b,a) v StrongPref(a,b)).

I ran into a problem with the universal instantiations or introductions also, but I had two separate premises on which I used universal elimination. I did not associate the variables in the universal statements with the same names on these two premises. In other words just because I associated "x" with "a" in the fourth premise does not mean I cannot associate "x" with "b" in the third premise. Similarly for "y". The "x" and "y" are variables and can stand for any names since these are universally quantified variables. Any name can be used.

In particular, to eliminate the universal quantifier of "x" in premise 4, I replaced the variable "x" with the name "a" in line 5. Then I eliminated the universal quantifier of "y" in line 5 by replacing the variable "y" with the name "b". This produced line 6.

However, on line 9 I used universal elimination on premise 3 by replacing "x" with "b" (not "a"). On line 10, I used universal elimination on line 9 and replaced "y" with "a" (not "b").

To introduce the negation on 15, I assumed "Sba" on line 11, eliminated the biconditional on line 12, eliminated the conjunction on line 13, and derived a contradiction on line 14. That contradiction allowed me to derive "¬Sba" on line 15.

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/