Loading article…
フィッチ記法（フレデリック・フィッチにちなんで名付けられたフィッチ図とも呼ばれる）は、命題論理と一階述語論理における自然演繹証明を、仮定、推論、およびその範囲を明示的に示す構造化された行ごとの形式で表現する方法である。これは1930年代にフレデリック・ブレントン・フィッチによって考案され、後に彼の教科書『記号論理学』（1952年）によって普及した。[ 1 ]フィッチ記法は、従属仮定の範囲を示すためにインデントやボックスを使用することで知られており、形式論理を教えるための最も教育的にアクセスしやすいシステムの1つとなっている。
フィッチは、1934年にプリンストン大学でアロンゾ・チャーチの指導の下、博士課程の研究の一環として自然演繹の体系を開発した。彼の手法は、仮定を部分導出の中で開始し、含意や否定を証明するときのように後で解除できる従属証明という重要な概念を導入した。彼の体系は当初未発表の形で流通していたが、学部教育で広く使用された著書『記号論理学』[ 1 ]を通じて広く知られるようになった。
後にパトリック・サップス[ 2 ]やEJレモン[ 3 ]といった論理学者や教育者がフィッチのシステムを改良した。彼らはインデントを縦棒に置き換えるなど図式的な変更を加えたが、フィッチ式の自然演繹の根底にある構造はそのまま残された。これらのバリエーションは、フィッチのオリジナルの記法に基づいているものの、しばしばサップス＝レモン形式と呼ばれる。
フィッチ記法では、証明は番号付きの行のシーケンスとして表され、各行には以下が含まれます。
フィッチ式証明の各行は、以下のいずれかです。
新しい仮定を導入すると、インデントのレベルが上がり、新しい垂直方向の「スコープ」バーが開始されます。このバーは、仮定が解除されるまで、後続の行をインデントし続けます。この仕組みにより、証明内の任意の行でどの仮定が有効であるかが即座に伝わり、仮定を各行に書き直す必要がなくなります（シーケント形式の証明とは異なります）。
以下の例は、フィッチ記法の主な特徴を示しています。
0 |__ [仮定、Pでない場合はPであるべき] 1 | |__ P [仮定、Pではないことを望む] 2 | | |__ Pではない [仮定、簡略化のため] 3 | | | 矛盾 [矛盾の導入: 1、2] 4 | | 非P [否定導入: 2] | 5 | |__ Pではない [仮定、Pを望む] 6 | | P [否定除去: 5] | 7 | P かつ P でない場合に限る [双条件導入: 1 - 4、5 - 6]
フィッチ記法は、論理学の教科書や教育現場で広く用いられている。また、いくつかの証明支援ツールの基盤にもなっている。その構造化されたスタイルは、大学学部教育における形式論理学の標準的な教授法となっている。