19/08/23 20:08:10.05 eq9wFyaJ.net
>>764
>>756は間違いでした。
自分が不用意に括弧を付け足したせいです。
(Isabelleも>>756にはNGを返します)
正しくは以下です。
「任意の自然数xに対して、α -> β -> P x」
α：￢(∀z::nat. (P z -> Q z))
β：(∀z::nat. (P z -> Q z) -> (∀n::nat. P n))
しかしこれだと、βに(∀z::nat. (P z -> Q z))を渡せないので、
コラッツ予想の証明には使えません。