今回の数学エッセーでは, 次の命題について,
簡単な解説を試みます.
もちろん, きちんとした証明は長くなりますので,
文献を紹介するにとどめます.
命題
T は述語論理よりも強い形式的体系, A は T の論理式で,
T の任意のモデルに関して A は真と仮定する.
この時, T の公理の有限列 B_1, ... , B_n が存在し, sequent
B_1 , ... , B_n → A
は LK で provable である.
解説.
A は T の任意のモデルで真だから,
完全性定理により,
A は形式的体系 T 内で証明可能.
(形式的体系や証明可能の意味するところは,
下記の知恵ノートを参照のこと:
(等号) 述語論理, 形式的体系のモデル, ゲーデル数についての解説. - kazz の数学旅行記
)
したがって, A はすでに T の公理の有限個と
述語論理の公理系を用いて証明可能.
よって, 倉田令二郎著 入門数学基礎論
p.31, 定理 1より,
T の公理の有限列
B_1, ... , B_n が存在し, sequent
B_1, ... , B_n → A
が LK で provable となる.
注意として, 上記知恵ノートにおける形式的体系や
証明可能性の定式化によれば,
T の明示的公理に現れる文字は
定数扱いであるので,
倉田令二郎「入門数学基礎論」p.31, 定理 1
において, 自由変数が束縛変数に変わらない
という条件は仮定する必要がない.
文責: Dr. Kazuyoshi Katogi
