命題論理の演繹における健全性・完全性に関する現時点での見解
導出原理によるトートロジー・矛盾判定に関して、サイト運営者の方が内容を修正されました。
私の方も以下の記事を非公開にしました。
「導出原理」で恒真性は判定できるのか？
トートロジー・矛盾に対するイメージのずれ？（導出原理で恒真・恒偽を判定できるのか）
こちらの内容に勘違いの部分がありました。すみません。
たとえば
(Ａ∨￢Ｃ)∧(Ｂ∨￢Ｄ)∧(￢Ａ∨￢Ｂ)∧(Ｃ∨Ｄ)
〜> (￢Ｃ∨￢Ｂ)∧(Ｂ∨Ｃ)
〜> ￢Ｂ∧Ｂ⇒Ｆ
ではなくて、
(Ａ∨￢Ｃ)∧(Ｂ∨￢Ｄ)∧(￢Ａ∨￢Ｂ)∧(Ｃ∨Ｄ)
〜> (￢Ｃ∨￢Ｂ)∧(Ｂ∨Ｃ)
〜> ￢Ｂ∨Ｂ（⇒T?）
とするべきでした。これでは”反例”とは言えないように思えます。
上記参照ページの内容をもう少し吟味して、導出原理に関して自分なりにあれこれ考えてみようと思います。
例えば（証明で用いられている）”対偶”とは何か、対偶は常に”正しい”ものであるのか、対偶が成立する前提条件というものがあるのではないか。
＊＊＊＊＊＊＊＊＊＊＊＊＊
ここまで命題論理の自然演繹の健全性・完全性についてあれこれ考えてきました。
私は人工論理としての命題論理（における演繹）の健全性・完全性が成り立つと考えられているその”仕組み”を明らかにしたいと考えています。それは”証明”ではなく、証明が成り立つ背景（あるいは設定）を明らかにするということでもあります。
現時点での見解は以下のとおりです。
１．健全性に関しては疑念が残る。命題論理の自然演繹からはトートロジーではない命題式が導かれうる。健全性はおのずから導かれる原理ではなく、トートロジーとならない証明は考えない・除外するという論理学という学問界隈における”空気感”で成立しているように感じられる。要するに健全性は原理ではなく約束事でしかない。
２．完全性については、→、∧、∨という論理記号の性質により、前提（たとえばAとB）とA→B、A∧B、A∨Bとの関連付けによりトートロジーが成立するようになっている。そしてそれぞれの関係はEx falso quodibetか背理法を用いれば証明できるようになっている。とりあえず矛盾させてしまえば証明できる、というふうに。
ではEx falso quodibetが成立する根拠は・・・と考えてみれば、そのトートロジー性、条件法（→）の真理値設定しかないように思えます。つまりトートロジー性により根拠づけられた推論規則によるトートロジーの演繹、という循環性が見て取れます。
・・・２については説明が足りないので意味がよくわからないかもしれませんが、これから具体的に検証していきたいと思います。
＊＊＊＊＊＊＊＊＊＊＊＊＊＊
公理系APLやウカシェビッチの公理系に基づく演繹の健全性に関しても循環論理が入り込んでいます。
下記のような公理系APL(axiomatic system for propositional logic)・・・
A1 A→(B→A)
A2 (A→(B→C))→((A→B)→(A→C))
A3 (￢B→￢A)→((￢B→A)→B)
R1 MP
・・・あるいはウカシェビッチの公理系（＋MP）において、ＡやＢ、Ｃにどんな命題式を代入しても良い、とする根拠がそもそもＡ１、Ａ２、Ａ３の論理式全体でトートロジーが維持されることだからです。
よく考えてみてください。トートロジー云々の根拠なしに上記の式のＡやＢ、Ｃにどんな論理式を代入しても良いという根拠づけなどできるでしょうか？ そもそも論理式の”形式”だけで代入の根拠が獲得できるでしょうか？ 無意味な記号の羅列だけで、そこに何の意味を見出すこともできないはずです。
つまり上記の公理系の正当性はトートロジーを根拠に成立している、さらに言えば条件法（→）の真理値設定が根拠になっているのです。ＡＰＬの公理系やウカシェビッチの公理系の”健全性”とは、前提そのものなのです。前提そのものを証明の結果とする循環論理に陥っているのだと言えるでしょう。