User:Ans/propositional calculus
w:Propositional_calculus#Example_1._Simple_axiom_system <-- axiom แค่ 3 อันข้างล่าง มันใช้ derive logic rule/theory อื่นๆ ได้อีกเยอะแยะเลยเหรอ?, ไม่อยากจะเชื่อเลย.
หลังจากใคร่ครวญมาหลายวัน ก็ทำให้นึกออกว่า, จริงๆ ลำพังเพียง truth table ของ if then operator (->), ก็จัดเป็น axiom ที่เพียงพอจะ derive rule อื่นๆ ได้หมด. ทีนี้ axiom 3 อันใน ตย. นั้น, คงเป็น axiom ที่แสดงให้เห็นว่า if then operator มี truth table ยังไง. คือมี truth table information เป็นนัยยะที่แฝงอยู่ใน axiom 3 อันนั้นอยู่. นั่นคือ truth table ของ if then จะเป็นแบบอื่นไปไม่ได้เลย, ถ้าจะทำให้ axiom 3 อันนั้นเป็นจริง. --Ans (discuss • contribs) 10:59, 30 December 2019 (UTC)
แต่พอ check อย่างละเอียดแล้ว, พบว่าแค่ axiom 1 กับ 3 กับ modus ponen rule ก็ครอบคลุม truth table ของทั้ง if then และ negation แล้ว --Ans (discuss • contribs) 12:18, 7 January 2020 (UTC)
ข้างล่างนี้คือ perl script เพื่อตรวจสอบ truth table ที่เป็นไปได้ทั้งหมด, ว่าแบบไหนที่ทำให้ axiom 1 กับ 2 เป็นจริงบ้าง. column แรกคือค่า truth table แบบต่างๆ, column สองคือค่าความจริงที่เป็นไปได้ทั้งหมดของ axiom. บรรทัดไหนที่ column 2 เป็น 1 ทั้งหมดแสดงว่า axiom เป็นจริงทุกกรณีสำหรับ truth table ของบรรทัดนั้น.
ubuntu@ubuntu:~$ perl -e 'for (glob("{0,1}{0,1}{0,1}{0,1}")) {@a=split""; sub p{return $a[$_[0]*2+$_[1]];} print"$_ "; for (glob("{0,1}{0,1}")) {($p,$q)=split"";print p($p,p($q,$p))} print"\n" }'
0000 0000
0001 0001
0010 0011
0011 0011
0100 0000
0101 0011
0110 0101
0111 0111
1000 0100
1001 0101
1010 0011
1011 0011
1100 1100
1101 1111
1110 1101
1111 1111
ubuntu@ubuntu:~$ perl -e 'for (glob("{0,1}{0,1}{0,1}{0,1}")) {@a=split""; sub p{return $a[$_[0]*2+$_[1]];} print"$_ "; for (glob("{0,1}{0,1}{0,1}")) {($p,$q,$r)=split"";print p(p($p,p($q,$r)),p(p($p,$q),p($p,$r)))} print"\n" }'
0000 00000000
0001 00000001
0010 00001001
0011 00001111
0100 00000000
0101 01010101
0110 00001111
0111 01111111
1000 10000000
1001 00001111
1010 10101010
1011 01101111
1100 00001111
1101 11111111
1110 11111110
1111 11111111
--Ans (talk) 12:58, 5 February 2020 (UTC)
axiom 3, axiom 2, axiom 1, modus ponen, p->p
$ perl -e 'for (glob("{0,1}{0,1}{0,1}{0,1}{0,1}{0,1}")) {@a=split""; sub p{return $a[$_[0]*2+$_[1]];} sub n{return $a[4+$_[0]];} print"$_ "; for (glob("{0,1}{0,1}")) {($p,$q)=split"";print p(p(n($p),n($q)),p($q,$p))} print"\n" }' | LC_ALL=C sort -k2
000000 0000
000001 0000
000010 0000
000011 0000
000100 0000
000110 0000
001000 0000
001010 0000
001011 0000
001100 0000
010010 0000
011001 0000
011010 0000
100000 0000
110000 0000
000101 0001
000111 0001
111000 0001
111001 0001
001001 0010
010000 0010
010001 0010
010011 0010
001101 0011
010100 0011
010101 0011
010110 0011
010111 0011
101000 0011
101001 0011
101010 0011
101011 0011
110001 0011
011000 0110
011011 0110
100010 0110
011100 0111
011101 0111
100001 0111
100011 0111
100100 1001
100111 1001
111010 1001
101101 1011
110100 1011
110101 1011
110111 1011
001110 1100
110010 1100
001111 1111
011110 1111
011111 1111
100101 1111
100110 1111
101100 1111
101110 1111
101111 1111
110011 1111
110110 1111
111011 1111
111100 1111
111101 1111
111110 1111
111111 1111
$ perl -e 'for (glob("{0,1}{0,1}{0,1}{0,1}")) {@a=split""; sub p{return $a[$_[0]*2+$_[1]];} print"$_ "; for (glob("{0,1}{0,1}{0,1}")) {($p,$q,$r)=split"";print p(p($p,p($q,$r)),p(p($p,$q),p($p,$r)))} print"\n" }' | LC_ALL=C sort -k2
0000 00000000
0100 00000000
0001 00000001
0010 00001001
0011 00001111
0110 00001111
1001 00001111
1100 00001111
0101 01010101
1011 01101111
0111 01111111
1000 10000000
1010 10101010
1110 11111110
1101 11111111
1111 11111111
$ perl -e 'for (glob("{0,1}{0,1}{0,1}{0,1}")) {@a=split""; sub p{return $a[$_[0]*2+$_[1]];} print"$_ "; for (glob("{0,1}{0,1}")) {($p,$q)=split"";print p($p,p($q,$p))} print"\n" }' | LC_ALL=C sort -k2
0000 0000
0100 0000
0001 0001
0010 0011
0011 0011
0101 0011
1010 0011
1011 0011
1000 0100
0110 0101
1001 0101
0111 0111
1100 1100
1110 1101
1101 1111
1111 1111
$ perl -e 'for (glob("{0,1}{0,1}{0,1}{0,1}")) {@a=split""; sub p{return $a[$_[0]*2+$_[1]];} print"$_ "; for (glob("{0,1}{0,1}")) {($p,$q)=split"";print $p&&p($p,$q)?$q:1} print"\n" }' | LC_ALL=C sort -k2
0010 1101
0011 1101
0110 1101
0111 1101
1010 1101
1011 1101
1110 1101
1111 1101
0000 1111
0001 1111
0100 1111
0101 1111
1000 1111
1001 1111
1100 1111
1101 1111
$ perl -e 'for (glob("{0,1}{0,1}{0,1}{0,1}")) {@a=split""; sub p{return $a[$_[0]*2+$_[1]];} print"$_ "; for (glob("{0,1}")) {($p,$q)=split"";print p($p,$p)} print"\n" }' | LC_ALL=C sort -k2
0000 00
0010 00
0100 00
0110 00
0001 01
0011 01
0101 01
0111 01
1000 10
1010 10
1100 10
1110 10
1001 11
1011 11
1101 11
1111 11