[TYPES] non-constuctive proofs

[Thorsten Altenkirch]

Thank you all. This teaches me to think properly before asking a  
question.

Alternatively, I have to tell my mail client not to accept any mails  
on Friday evenings... :-)

Thorsten (with a red face)

On 22 Aug 2009, at 04:35, prakash wrote:

> Suppose log_2 3 = n/m where n,m are positive integers with no common  
> factors.  Then m * log_2 3 = n so log_2 3^m = n hence 2^n = 3^m.
> This is impossible as one side is even and the other is odd.  I  
> think this is easier than the sqrt(2) proof.


On 22 Aug 2009, at 00:29, Thorsten Altenkirch wrote:

> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list 
>  ]
>
>> By the way, I  reveal the a= sqrt{2}  and b = log_2 9 trick on page
>> 51 of my notes!
>
> Thanks to both of you. However, we may have learned at School how to
> prove that sqrt{2} is irrational. Is there an easy proof that log_2 9
> is?
>
> Cheers,
> Thorsten
>
> This message has been checked for viruses but the contents of an  
> attachment
> may still contain software viruses, which could damage your computer  
> system:
> you are advised to perform your own checks. Email communications  
> with the
> University of Nottingham may be monitored as permitted by UK  
> legislation.
>


This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.