Formal Proof
Áõ¸í°úÁ¤¿¡¼ ³ªÅ¸³ª´Â ¸ðµç ¸íÁ¦´Â ¾î´À°ÍÀ̳ª ±× Á¤´çÇÑ µµÃâ±Ù°Å °¡ ¸í½ÃµÇ¾î¾ß ÇÑ´Ù. Áï ±× ¾Õ¿¡ ³ª¿Â ¾î¶² ¸íÁ¦·ÎºÎÅÍ ¾î¶² ±ÔÄ¢¿¡ ÀǰÅÇÏ¿© µµÃâµÈ °ÍÀÎÁö¸¦ Ç¥½ÃÇÏ¿©¾ß ÇÑ´Ù. ±× Ç¥½Ã´Â °¢ ¸íÁ¦ ¿À¸¥ÂÊ ³¡¿¡ ¸í½ÃÇÑ´Ù. ÀÌ·± Çü½ÄÀÇ Áõ¸í¹ýÀ» Çü½ÄÀû Áõ¸í (formal proof) ¶ó ÇÑ´Ù.
´ÙÀ½°ú °°Àº Ãß·ÐÀ» Áõ¸íÇØ º¸ÀÚ.
¡Å
I ¡ý¡R
1) [G¡ù(W¡ùI)]¤ý[¡C¡ù(L¡ù¡R)] Pr
2)
L¡ù(G¤ý¡C) Pr
3)
L Pr
°á·Ð 'I ¡ý¡R'¸¦ ¾òÀ¸·Á¸é ¼¼ °¡Áö ¹æ¹ýÀ» »ý°¢ÇØ º¼ ¼ö ÀÖ´Ù.
ù° ±³È¯±ÔÄ¢¿¡ ÀÇÇÏ¿© '¡R¡ùI' ¿¡¼ µµÃâÇÏ´Â ¹ý, µÑ° ºÎ°¡±ÔÄ¢(add) ¿¡ ÀÇÇÑ ¹æ¹ý, ¼Â° CD¿¡ ÀÇÇÑ ¹æ¹ýÀÌ´Ù. ±³È¯±ÔÄ¢¿¡ ÀÇÇÏ·Á ÇÏ´õ¶óµµ ¼±¾ð¸íÁ¦ '¡R¡ýI' ¸¦ ¾ò¾î¾ß Çϸç, ºÎ°¡±ÔÄ¢¿¡ ÀÇÇÏ·Á¸é 'I'¿Í '¡R'¸¦ ºÐ¸®½ÃÄÑ ¾ò¾î¾ß Çϴµ¥ 3°³ÀÇ ÀüÁ¦¿¡¼´Â ¾î·Á¿ï °Í °°´Ù.
CD ¿¡ ÀÇÇÑ ¹æ¹ýÀ» ¸ð»öÇØ º¸ÀÚ. 'I ¡ý¡R'À» CD¿¡ ÀÇÇØ¼ µµÃâÇÏ·Á¸é 'I'¿Í '¡R'À» °¢°¢ ÈİÇÀ¸·Î ÇÏ´Â µÎ °³ÀÇ °¡¾ð¸íÁ¦¿Í ±× Àü°ÇµéÀ» ¼±¾ðÀûÀ¸·Î ±àÁ¤ÇÒ ÇϳªÀÇ ¼±¾ð¸íÁ¦°¡ ¿ä±¸µÈ´Ù. ¿ì¼± 1)¿¡¼ 'W¡ùI' ¿Í 'L¡ù¡R' À» ºÐ¸®ÇØ ³»°í 'W¡ýL' À» µµÃâÇϸé CD°¡ °¡´ÉÇÒ °ÍÀÌ´Ù. 'W¡ùI'¿Í 'L¡ù¡R'Àº 'G'¿Í '¡C'°¡ µµÃâµÇ¸é °¢°¢ Modus Ponens ¿¡ ÀÇÇÏ¿© µµÃâµÈ´Ù. ±×·±µ¥ 2)¿Í 3)¿¡¼ MP¿¡ ÀÇÇÏ¿© 'G¤ý¡C'°¡ µµÃâµÉ ¼ö ÀÖÀ¸¹Ç·Î À̰ÍÀ» Simp Çϸé 'G'¿Í '¡C'¸¦ ¾ò´Â´Ù. ¶Ç 'W¡ýL' Àº 3)¿¡ 'W'¸¦ Add ÇÏ¿© 'L¡ýW' ¸¦ ¾ò°í À̰ÍÀ» Com ÇÏ¸é ¾òÀ» ¼ö ÀÖ´Ù. ÀÌ»óÀÇ Ãß·ÐÀýÂ÷¸¦ ¿ª¼øÀ¸·Î ±âÈ£ÈÇϸé À§ÀÇ Ãß·ÐÀº ´ÙÀ½°ú °°ÀÌ Áõ¸íµÈ´Ù.
¡Å
I ¡ý¡R
1) [G¡ù(W¡ùI)]¤ý[¡C¡ù(L¡ù¡R)] Pr
2)
L¡ù(G¤ý¡C) Pr
3)
L Pr
4)
G¡ù(W¡ùI) 1,
Simp
5) [¡C¡ù(L¡ù¡R)]¤ý[G¡ù(W¡ùI)] 1,
Com
6) ¡C¡ù(L¡ù¡R) 5,
Simp
7) G¤ý¡C 2,
3, MP
8) G 7,
Simp
9) ¡C¤ýG 7,
Com
10) ¡C 9,
Simp
11) W¡ùI 4,
8, MP
12) L¡ù¡R 6,
10, MP
13) L¡ýW 3,
Add
14) W¡ýL 13,
Com
15) ¡Å I ¡ý¡R 11,
12, 14, CD
¸íÁ¦ ¾ÕÀÇ ¼ýÀÚ´Â °¢ ¸íÁ¦¸¦ ±¸º°Çϱâ À§ÇÑ °ÍÀÌ°í ¿À¸¥ÂÊ ³¡¿¡ ÀÖ´Â ¼ýÀÚ´Â ±× ¸íÁ¦°¡ µµÃâµÈ ¿ø¸íÁ¦¸¦ °¡¸®Å°¸ç ±× µÚÀÇ ¾àÀÚ´Â µµÃâÇÒ ¶§ »ç¿ëµÈ Ã߷бÔÄ¢ÀÌ´Ù.