セマンティクスを経由しないでという意味が分かりづらかったので説明します

３つの公理スキーマ
（Ａ１） Ｂ⇒（Ｃ⇒Ｂ）
（Ａ２） （Ｂ⇒（Ｃ⇒Ｄ））⇒（（Ｂ⇒Ｃ）⇒（Ｂ⇒Ｄ））
（Ａ３） （¬Ｃ⇒¬Ｂ）⇒（（¬Ｃ⇒Ｂ）⇒Ｃ）
とＭＰからなる公理系から出発すると、Deduction定理などを経由して完全系定理を示すことができて
この公理系はトートロジーの集合と一致することが示せます

一方、ルカシーヴィッツの公理系
（Ｌ１） （¬Ｂ⇒Ｂ）⇒Ｂ
（Ｌ２） Ｂ⇒（¬Ｂ⇒Ｃ）
（Ｌ３） （Ｂ⇒Ｃ）⇒（（Ｃ⇒Ｄ）⇒（Ｂ⇒Ｄ））
も同等の性質を持つ公理系らしいので、完全性定理の証明ができるはずですが
導くのにヒラメキが必要そうで、自分では証明を構成できていません

自分の第一の動機は、ルカシーヴィッツの公理系を出発点にした
完全性定理の証明を見つけたいので、コンピュータを援用したいという動機です

そして、一般の公理系は、適当に３つの公理スキーマを指定して考えることができるので、
適当に３つの公理スキーマが与えられたときに、それが完全性定理を満足するかを
ヒラメキなして自動的に判断するアルゴリズムが必要だろう、というのが第２の動機です

よろしくお願いします