Fermat は Diophantus『算術』の問2-8「平方数を二つの平方数に分けよ」に対して次のような注釈を与えました。
これは中世ラテン語なので少し読みにくいのですが、文字に起こすと次の通りです。
Cvbum autem in duos cubos, aut quadratoquadratum in duos quadratoquadratos & generaliter nullam in infinitum vltra quadratum poteſtatem in duos eiuſdem nominis fas eſt diuidere cuius rei demonſtrationem mirabilem ſane detexi. Hanc marginis exiguitas non caperet.
直訳すると次の通りになるはずです。
一方で、立方数を二つの立方数に、また四乗数を二つの四乗数に、そして一般に、平方を超えて無限に至る冪を同名の二つに分けることができないのが天理であり、このことの{真に驚くべき証明を私は発見した/驚くべき証明を私は本当に発見した}。これを余白の狭さが捕まえない。
一般的には現代的に分かりやすく意訳されていると思いますが、中世の数学は中世らしく訳しておくのが良いでしょう。これを解釈すると
となるはずです。
実は、とある友人に、上の論理式と次の論理式が本当に同値になるのかと質問されたのがこの記事を書いたきっかけです。
よく聞いてみると、対偶を取って
となるところまでは良いけど、これと2番目の論理式が同値なのかは怪しいということでした。この疑問は非常に正当なものであって、実際、この変形は直観論理においては成り立ちません。一方で、古典論理においてはすべての論理式がそれと等価な冠頭標準形を持つということも事実として知っておくと色々迷わなくて済みます。この場合は、論理式 に , , が自由変項として含まれていないので、存在量化子をこのように全称量化子にして冠頭に持ってくることができるというわけです。冠頭標準形の理論は数理論理学においてそれなりに大事な概念で、少し推し進めると Skolem 標準形や完全性定理などと繋がりがあるものなので押さえておいても損はないかなと思います。