How would one go about proving the following statement in predicate logic?

Question

I need to prove this: ⊢(∀x)((Fx→Gx)∨(Gx→Fx)) Not entirely sure how I'd go about this.

Answer 1

You can prove it by assuming a negated instance and proving a contradiction:

{1}      1.   ~((Fa → Ga) ∨ (Ga → Fa))            Assum.
{1}      2.   ~(Fa → Ga) & ~(Ga → Fa)             1 DM
{1}      3.   ~(Fa → Ga)                          2 &E
{1}      4.   ~(~Fa ∨ Ga)                         3 MI
{1}      5.   Fa & ~Ga                            4 DM
{1}      6.   Fa                                  5 &E
{1}      7.   ~(Ga → Fa)                          2 &E
{1}      8.   ~(~Ga ∨ Fa)                         7 MI                        
{1}      9.   Ga & ~Fa                            8 DM
{1}      10.  ~Fa                                 9 &E
{1}      11.  Fa & ~Fa                            6,10 &I
-        12.  ~~((Fa → Ga) ∨ (Ga → Fa))           1,11 RAA
-        13.  (Fa → Ga) ∨ (Ga → Fa)               12 DNE
-        14.  ∀x[(Fx → Gx) ∨ (Gx → Fx)]           13 UI

Here's another version that doesn't rely on identities such as DeMorgan's law:

{1}      1.   ~((Fa → Ga) ∨ (Ga → Fa))            Assum.
{2}      2.   Fa → Ga                             Assum.
{2}      3.   (Fa → Ga) ∨ (Ga → Fa)               2 ∨I
{1,2}    4.   ⊥                                   1,3 &I
{1}      5.   ~(Fa → Ga)                          2,4 RAA
{6}      6.   Ga → Fa                             Assum.
{6}      7.   (Fa → Ga) ∨ (Ga → Fa)               6 ∨I
{1,6}    8.   ⊥                                   1,7 &I
{1}      9.   ~(Ga → Fa)                          6,8 RAA
{10}     10.  Fa                                  Assum.
{11}     11.  Ga                                  Assum.
{10,11}  12.  Fa & Ga                             Assum.
{10,11}  13.  Ga                                  12 &E
{11}     14.  Fa → Ga                             10,13 CP
{1,11}   15.  ⊥                                   5,14 RAA
{1}      16.  ~Ga                                 10,15 RAA
{17}     17.  ~Fa                                 Assum.
{1,17}   18.  ~Fa & ~Ga                           16,17 &I
{1,17}   19.  ~Ga                                 18 &E
{1}      20.  ~Fa → ~Ga                           17,19 CP
{11}     21.  ~~Ga                                11 DNI
{1,11}   22.  ~~Fa                                20,21 MT
{1,11}   23.  Fa                                  22 DNE
{1}      24.  Ga → Fa                             11,23 CP
{1}      25.  ⊥                                   9,24 &I
-        26.  ~~((Fa → Ga) ∨ (Ga → Fa))           1,25 RAA
-        27.  (Fa → Ga) ∨ (Ga → Fa)               26 DNE
-        28.  ∀x[(Fx → Gx) ∨ (Gx → Fx)]           27 UI

Answer 2

The following proof uses the law of the excluded middle (LEM) rather than reductio ad absurdum (RAA) used by user3017.

Since the conclusion is a disjunction without premises and "Gx" is in both disjuncts, I tried to construct a proof from the tautology "Ga ∨ ¬Ga".

In each case I used conditional introduction (→I) on lines 4 and 10. Then I used disjunction introduction (∨I) to get the same result for both cases on lines 5 and 11.

In the first case I used reiteration (R) to copy line 1 to line 3.

In the second case I used explosion (X) to get the desired consequent (Fa) on line 9.

Getting the same result for both cases allowed me to close the subproofs for these cases using the law of the excluded middle (LEM) on line 11.

On line 12 I introduced a universal quantifier to complete the proof.

More information on these rules can be found in 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