2005/10/12

根本から勘違いしている可能性があるけど、

|- T ( x=y <-> y=x ) (ただしT はTheorem)
∵ |- T ( x=y -> x=x -> y=y -> y=x )

この理屈が成立するには、p を T における述語として、 |- T ( p3xxy -> y), |- T ( p3yxy -> x ) となるp3 が必要だと思うんだけど、これって自明なの?(少なくとも僕にとってはムズカシイ。) 「式中に1度しか出現しかない元を抽出できる」、さらには「式中である性質を持つ元だけを抽出できる」なんて、直感的には定理になるとは思えないんだけどねえ。

No comments :