- 当直医のスレ Part23 [無断転載禁止]©2ch.net
310 ：卵の名無しさん (ﾜｯﾁｮｲ a3ab-W16a)[sage]：2017/08/14(月) 07:10:45.91 ID:e8So+UKW0 - Amazonの書評に釣られてhttps://www.amazon.co.jp/dp/4790703975現代論理学 単行本 ? 1991/5 安井 邦夫 (著)を数日前から読み始めた。
ルカシェヴィッツによる命題論理公理系 System of axioms 1930
■３．転換規則（推論規則）の制定
代入法則：Modus Ponens：(S1)，(S1→S2)├ S2
■４．公理の制定
p → (q → p)，
(p → (q → r)) → ((p → q) → (p → r))，
(¬p → ¬q) → (q → p)
を題材に無矛盾性・独立性・完全性が論じられているのだが、なんせ公理が自明とは言いがたい。代入法則はまあ自明で納得できるが。
含意（→ならば）と否定（¬でない）だけが公理が定義されているのは簡素でいいのだが、この公理からp→pの証明は骨が折れる。
上記、公理と代入法則をRに計算させて真理表で検証してみた。
library('gtools')
pm2=permutations(2,2,v=c(T,F),re=TRUE) ; pm2
pm3=permutations(2,3,v=c(T,F),re=TRUE) ; pm3
imply <- function(x,y) !x || y
# L1 : A->(B->A)
f <- function(A,B) imply(A,imply(B,A))
f1 <- function(pm) f(pm[1],pm[2])
for(i in 1:4) print(f1(pm2[i,]))
# L2 : (A->(B->C))->((A->B)->(A->C))
f <- function(A,B,C) imply(imply(A,imply(B,C)),imply(imply(A,B),imply(A,C)))
f1 <- function(pm) f(pm[1],pm[2],pm[3])
for(i in 1:8) print(f1(pm3[i,]))
続きとその結果はここ
http://egg.2ch.net/test/read.cgi/hosp/1428282054/899-901
|