[TYPES] non-constuctive proofs

[Stephane Lengrand]

Incidentally, this is the very reason why keyboards are imperfectly 
tuned, i.e. well-tempered.

If you want a scale that is closed under composition and that contains 
the fifth, you end up looking at the group (of musical intervals) 
generated by the ratio 3, identifying all notes that only differ by 
octaves (i.e. whose frequency ratio is a power of 2).
Since 3^n is never a power of 2, you never get back to a note you 
already have, and the group is infinite, which is a pain for a 
keyboard-instrument.
(However, with n=12, you get pretty close to a power of 2, and you can 
spread the error uniformly over the 12 elements of the group, i.e. the 
12 well-tempered intervals.)

Stephane

Thorsten Altenkirch wrote:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>
> 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.
>
>