フィッチ表記

フィッチ記法は、フィッチ図（フレデリック・フィッチにちなんで名付けられた）とも呼ばれ、文論理や述語論理で使用される形式的な証明を構築するための記法システムです。フィッチスタイルの証明では、証明を構成する文のシーケンスを行に配置します。フィッチ記法のユニークな特徴は、各行のインデントの度合いによって、そのステップでどの仮定が有効であるかが伝わることです。

フィッチスタイルの証明の各行は次のいずれかです。

• 仮定または証明のサブ仮定。
• （１）推論規則と（２）その規則を正当化する証明の前の行の引用によって正当化される文。

新しい仮定を導入すると、インデントのレベルが上がり、新しい垂直の「スコープ」バーが始まります。このバーは、仮定が解除されるまで後続の行をインデントし続けます。このメカニズムにより、証明内の任意の行でどの仮定が有効であるかが即座に伝わります。各行で仮定を書き直す必要はありません (シークエント スタイルの証明の場合のように)。

次の例は、Fitch 表記法の主な特徴を示しています。

0 |__ [仮定、PでなければPを望む]
1 | |__ P [仮定、望まないP]
2 | | |__ not P [仮定、還元]
3 | | | 矛盾 [矛盾紹介: 1, 2]
4 | | ない P [否定導入: 2]
  |
5 | |__ Pではない[仮定、Pを望む]
6 | | P [否定除去: 5]
  |
7 | P の場合、P ではない [二条件式の導入: 1 - 4, 5 - 6]

0. 帰無仮定、つまりトートロジーを証明している
1. 最初のサブ証明: 左辺が右辺に従うことを示すために仮定する
2. サブサブ証明: 好きなように仮定してかまいません。ここでは、背理法
を目指します 3. これで矛盾が生じました
4. 矛盾を「引き起こした」ステートメントの前に not を付けることができます
5. 2 番目のサブ証明: 左辺が従うことを示すために右辺を仮定する
6. ステートメントのプレフィックスから偶数の not を削除できる規則を適用します
7. 1 から 4 では、P ならば P ではないことを示し、5 から 6 では、P ならば P ではないことを示し、したがって 7 で双条件を導入できます。ここで、iff はif and only ifを表します。

• 自然演繹

• フィッチ、フレデリック・ブレントン（1952年）。記号論理学入門。ロナルド・プレス社。

• バーカー・プラマー、デイブ、バーワイズ、ジョン、エチェメンディ、ジョン(2011) [1999]。言語、証明、論理(第 2 版)。CSLI 出版。p. 606。ISBN 9781575866321。

• フィッチの認識可能性のパラドックス
• 証明構築のためのオンライン Java アプリケーション 2006-10-02 にWayback Machineでアーカイブされました
• proofmod.mindconnect.cc における Fitch 証明システム (命題および一階) の Web 実装
• Jape 汎用証明支援システム ( Jape を参照)
• LaTeX で Fitch 記法による証明をタイプセットするためのリソース ( LaTeX を参照)
• FitchJS: Fitch 表記法で証明を構築するためのオープンソースの Web アプリ (LaTeX にエクスポート可能)
• フィッチ記法による自然演繹証明エディタおよびチェッカー