3

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

4

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
| improve this answer | |
0

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

enter image description here

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

| improve this answer | |

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.