------------------------------------------------------------------------
Subject:  Non-Constructive Existence Proof by Cases
------------------------------------------------------------------------

After today's lecture in which I presented a non-constructive existence
proof by cases of the proposition that there are irrational numbers x,y
such that x sup y is rational (see Rosen, p. 91, Ex. 11), a student
asked if it could be formalized.  Here's one such formalization, using
the relatively *informal* methods that Rosen presents:

Notation:  To represent "x raised to the nth power" in this type font,
           I will write "x sup n".  So, e.g., 4 sup 2 = 16.

           To represent "square root of n" in this type font,
           I will write "sqrt(n)".  So, e.g., sqrt(16) = 4 (or -4).	


Syntax & Semantics:  Q(x) = x is a rational number (i.e., a fraction)

Theorem:	ExEy[-Q(x) ^ -Q(y) ^ Q(x sup y)]

proof:

 1.  -Q(sqrt(2))                             : lemma from arithmetic
                                               (or earlier proof;
                                                see Rosen pp.80-81,Ex.10)
 
 2.  Q(sqrt(2) sup sqrt(2))                  : assumption
 
 3.  -Q(sqrt(2)) ^ -Q(sqrt(2)) ^ Q(sqrt(2) sup sqrt(2)) 
                                             : From 1,1,2, by Conjunction

: Notice that here I'm conjoining *3* propositions,
: two of which are the same.
 
 4.  ExEy[-Q(x) ^ -Q(y) ^ Q(x sup y)]        : From 3, by EG
                                               (applied twice)
 
 5.  Q(sqrt(2) sup sqrt(2)) -> ExEy[-Q(x) ^ -Q(y) ^ Q(x sup y)]
                                             : From 2-4 by Direct Proof

: i.e., the assumption in line 2 implies the proposition in line 4,
: so we can write it as a conditional proposition whose antecedent
: is the proposition in line 2 and whose consequent is the proposition
: in line 4.
 
 6.  -Q(sqrt(2) sup sqrt(2))                 : assumption
 
 7.  (sqrt(2) sup sqrt(2)) sup sqrt(2) = 2   : lemma from arithmetic
 
 8.  Q((sqrt(2) sup sqrt(2)) sup sqrt(2))    : From 7,
                                               by lemma from arithmetic
                                               (or by def of Q)
 
 9.  -Q(sqrt(2)) ^ -Q(sqrt(2) sup sqrt(2)) 
                 ^ Q((sqrt(2) sup sqrt(2)) sup sqrt(2))
                                             : From 1,6,8 by Conjunction

10.  ExEy[-Q(x) ^ -Q(y) ^ Q(x sup y)]        : From 9, by EG
                                               (applied twice)

11.  -Q(sqrt(2) sup sqrt(2)) -> ExEy[-Q(x) ^ -Q(y) ^ Q(x sup y)]
                                             : From 6-10 by Direct Proof

12.  (Q(sqrt(2) sup sqrt(2)) v -Q(sqrt(2) sup sqrt(2)))
                                     -> ExEy[-Q(x) ^ -Q(y) ^ Q(x sup y)]
                                             : From 5,11, by Pf by Cases

13.  Q(sqrt(2) sup sqrt(2)) v -Q(sqrt(2) sup sqrt(2))
                                             : tautology

14.  ExEy[-Q(x) ^ -Q(y) ^ Q(x sup y)]        : From 12,13, by MP

QED!