公理系APL
axiomatic system for propositional logic
公理系APL
$ A\rightarrow(B\rightarrow A)
$ (A\rightarrow(B\rightarrow C))\rightarrow((A\rightarrow B)\rightarrow(A\rightarrow C))
$ (\lnot B\rightarrow \lnot A)\rightarrow((\lnot A\rightarrow A)\rightarrow B)
$ Aと$ A\rightarrow Bから$ Bを引き出して良い
定義に論理変数?が含まれる
$ A\rightarrow (B\rightarrow A)という形をした論理式ならすべて当てはまる
公理系APLのproof, theoremの定義
以下の条件を満たす論理式の有限個の列$ B_1,B_2,\cdots,B_nを$ C(=B_n)のAPLにおけるproofという
$ B_iは以下のいずれかである
APLの公理である
先行する$ B_j,B_kから推論規則MPによって引き出された式である
$ Cのproofが存在する時、$ CはAPLのtheoremという
もしくは、$ CはAPLによって証明可能であるという https://gyazo.com/f4de6c3b71d36336e41720a5aa2241bf
proofは条件を満たす論理式の列
theoremは列の最後にある論理式そのもの
ってことやなmrsekut.icon
論理式$ Aが公理系$ Kのtheoremである$ \Rightarrow$ Aはトートロジーである
が成り立つ
論理式$ Aがトートロジーである$ \Rightarrow$ Aは公理系$ Kのtheoremである
が成り立つ