symbolic logic กับ classical logic มันคืออะไรกัน แตกต่างกันยังไงนะ

โพสนี้อยู่ในหมวด เรียนรู้ logic programming + argumentation นะคะ

จริงๆตอนแรกอยากจะตั้งชื่อโพสวันนี้ว่าบันทึกบทสนทนาเวลาเบื่อๆ ของชาว logic แต่ก็เกรงใจกลัวว่าเดี๋ยวอาจจะเข้าใจผิดได้ว่า เอ... ทำไมต้องเป็นชาว logic ถึงจะคุยอะไรแบบนี้ แต่จริงๆเจตนาเราคือ อยากจะล้อเล่นน่ะค่ะ  เนื่องจากว่า  วันนี้อาจารย์เราเกิดความรู้สึกเบื่อๆ อยู่ในภาวะไม่มีอะไรทำ พอดีคุยโทรฯกันเรื่องงาน เราก็เลยแก้เบื่ออาจารย์ด้วยการถามคำถามไปซะเลย  ฮ่าๆๆๆ

เพราะเราอยากจะรู้(โดยไม่ต้องไปอ่านเองตั้งมากมาย) ว่า symbolic logic กับ classical logic มันต่างกันยังไงนะ 

เพื่อป้องกันไม่ให้ตัวเองลืม และเพื่อเป็นการแลกเปลี่ยนความรู้กันกับผู้อ่าน เราก็เลยคิดว่า ควรจะบันทึกบทสนทนาแก้เบื่อวันนี้ไว้ในบล็อกดีกว่า :)

เอาล่ะ เข้าเรื่องเลยนะคะ มาเริ่มที่คำแรกก่อน symbolic logic  ผู้อ่านบางท่านอาจจะเคยได้ยินคำนี้ และอาจจะเคยอ่านหนังสือที่เราแนะนำไปแล้วด้วย

แล้วสงสัยกันไหมคะ ว่าคำๆนี้ สื่อถึงอะไร

สั้นๆเลยก็คือ symbolic logic เนี่ย คือ logic ที่เราสามารถนำเสนอมันได้ด้วย symbol ค่ะ ซึ่งถ้าเรามองดู logic ประเภทต่างๆที่เราเคยเห็นผ่านหูผ่านตากันมา มันก็มีแต่ logic ที่แทนค่าด้วย symbol กันทั้งนั้น

ยกตัวอย่างเช่น propositional logic , first order logic , second order logic, description logic , modal logic, logic programming, etc. ลอจิกต่างๆเหล่านี้ เวลาเรา represent มัน เราก็ใช้ symbol นำเสนอ ใช่ไหมคะ

อย่าง propositional logic เราก็ใช้ ตัวอักษร อย่างเช่น p, q อะไรต่างๆ แทน proposition แต่ละอัน ตัว logical connection ก็ แทนด้วย symbol อย่างพวก and, or, implication อะไรทำนองนี้

แน่นอนว่า first order logic ก็ไม่ต่างกันมาก เพราะคล้ายกับ propositional logic ที่เพิ่ม quantifier ขึ้นมา

ดังนั้น ถ้าให้นิยามโดยไอเดียแล้ว symbolic logic คือ การ reasoning  ที่เรานำเสนอมันด้วย symbol ต่างๆ นั่นเอง


ต่อมา เราก็มาดู อีกคำนึงที่มักจะได้ยินกันบ่อยๆ รวมถึงในหลายๆโพสที่เราเคยเขียนไว้ก่อนหน้าด้วย
แล้ว classical logic คืออะไรกัน

คำจำกัดความของคำนี้ก็อาจจะเป็นที่ถกเถียงได้นะคะ  เราเองไม่ได้หาหลักฐานยืนยัน แต่ว่าขอยืนยันด้วยความเห็นของผู้เชี่ยวชาญด้านนี้(ซึ่งก็คืออาจารย์นั่นเอง)  ถ้าผู้อ่านท่านใดมีความคิดเห็นต่าง อยากจะหาข้อสรุปกันเราก็ยินดีค่ะ

ก่อนอื่น เราต้องย้อนไปที่คำว่า monotonic reasoning ก่อนค่ะ หวังว่าคงจะยังจำความหมายคำนี้ได้นะคะ
คือว่า classical logic เนี่ย จะมีลักษณะของ monotonic reasoning ค่ะ แต่ว่า.... ไม่ได้หมายความว่า logic ที่มีลักษณะเป็น monotonic reasoning จะถูกจัดเป็น classical logic เสมอไป

รายละเอียดเรื่อง monotonic reasoning หาอ่านได้จากโพสนี้ค่ะ

ตรงนี้เราจะขอขยายความให้ว่า ยกตัวอย่างเช่น description logic(ไม่นับ extension ของมันก่อนนะคะ)  มีลักษณะเป็น monotonic reasoning แต่ว่า มันไม่ได้ถูกนับเป็น classical logic

เพราะว่า... เดิมทีคำว่า classical logic เนี่ยใช้เรียก logic ที่นัก logician เป็นคนคิดกัน เมื่อ 20-30 ปีก่อนมาแล้ว ทีนี้ ตอนหลังๆ อย่าง description logic ก็ถึงจะคลอดออกมาใช้กันในวงการนักคอมพิวเตอร์


ซึ่ง logic หลายๆตัว ในช่วงหลังๆ ก็จะมี extension ของมัน ซึ่งจากลักษณะเดิม ที่เป็น monotonic reasoning เขาก็ปรับให้ extension มันกลายเป็น non-monotonic reasoning อย่างเช่น description logic เป็นต้น

ดังนั้น เพื่อความเข้าใจง่ายๆ เราก็จะขอสรุปว่า classical logic หมายถึง logic สมัยเก่า 20-30 ปีที่แล้ว ที่มีลักษณะเป็น monotonic reasoning ค่ะ

หวังว่า จะช่วยคลายความสงสัยให้กับหลายๆคน รวมถึงตัวเราเองด้วยนะคะ
จบบทสนทนาวันเบื่อๆ กันแค่นี้นะคะ (เป็นโพสเกี่ยวกับลอจิก ที่สั้นที่สุดแล้ว ฮ่าๆๆ)


ถ้าหากโพสนี้มีข้อผิดพลาดประการใด เราขอรับผิดชอบแต่ผู้เดียวนะคะ เพราะเราเกรงว่า สิ่งที่บันทึก เราอาจจะจำผิดพลาด จากบทสนทนาจริงๆได้ เพราะบันทึกจากความจำและที่เราคิดว่าเราเข้าใจค่ะ

ขอให้สนุกกับลอจิกนะคะ :)

มาเรียน Logic for Computer Science (4 -- Propositional Logic vs First-Order Logic)

สำหรับใครที่เพิ่งเข้ามาหน้านี้ แนะนำว่าให้อ่าน ที่นี่ ก่อนนะคะ เอาล่ะที่นี้เราจะมาคุยกันต่อเรื่องว่า ทำอย่างไรเราถึงจะนำเสนอรูปแบบข้อมูลให้อยู่ในรูปที่สามารถนำไปทำ reasoning ได้ ซึ่งก็มีทฤษฎี 2 อย่างที่เราจะพูดถึงคือ Propositional logic และ First-Order logic ซึ่งมีความแตกต่างกันอยู่

เพื่อให้เข้าใจได้ง่ายและกระชับ เราจะไม่อธิบายนิยามแต่ละอันไปทีละนิดนะคะ แต่จะชี้ให้เห็นลอจิกทั้งสองรูปแบบ และตอนต่อไปจึงจะเน้นอธิบาย First-Order logic เลยทีเดียว

ก่อนอื่นเรามารู้จักกับคำว่า Formal language กันก่อน ซึ่งก็คือ ภาษาที่ถูกออกแบบมาเพื่อใช้นำเสนอข้อเท็จจริงต่างๆ(arguments) ซึ่งการออกแบบ formal language นี้จำเป็นต้องประกอบไปด้วย 3 ส่วน คือ
1. Lexicon คือ กลุ่มคำศัพท์ที่ใช้ในภาษา
2. Syntax คือ ไวยากรณ์ หรือจะเรียกว่า grammar นั่นเอง
3. Semantic คือการเชื่อมโยงกันระหว่างคำศัพท์กับความหมาย

ดังนั้น ภาษาลอจิก ทั้ง Propositional logic และ First-Order logic ก็จำเป็นที่จะต้องมีทั้งสามส่วนนี้

สมมติว่า เรามีประโยค P= นกแก้วเป็นนก  Q=นกทุกตัวสามารถบินได้
ด้วย Propositional logic เราสามารถนำเสนอประโยค P ได้ แต่ไม่สามารถนำเสนอประโยคQ
ในขณะที่ First-Order logic สามารถที่จะนำเสนอได้ทั้ง P และQ
ดังนั้นจะเห็นว่า ปัญหาคือ propositional logic ไม่มีโครงสร้างที่ใช้บ่งบอกปริมาณของนามในประโยค

เรามาพิจารณาโครงสร้างของลอจิกทั้งสองแบบในแต่องค์ประกอบของการออกแบบกันเลยนะคะ
1. Lexicon ไม่มีอะไรแตกต่างกัน ทั้ง Propositional และ First-order จะสนใจแค่ กลุ่มของ symbols ที่ถูกใช้เป็นสัญลักษณ์ในการนำเสนอ statements เท่านั้น
2. Syntax มีความแตกต่าง โดยเฉพาะ First-Order logic มีนิยามขององค์ประกอบมากกว่า ดังสรุปในแผนภาพ

Atom คือ statement (ข้อมูลหรือข้อเท็จจริง)
Formula (Well-formed formula) สามารถที่จะสร้างขึ้นมาได้จากเงื่อนไข 4 ข้อต่อไปนี้
- Atom อันนึงก็ถือเป็น formula
- ถ้าเรามี formula G ใดๆ แล้ว (~G) ก็เป็น formula เหมือนกัน
- ถ้าเรามี formula สองอันใดๆ แล้ว การนำ formula 2 อันนั้นมาเชื่อมกันด้วย logical connectives (and , or , if, iff ) ก็ถือเป็น formula เช่นกัน
-  เราจะสร้าง formula ทั้งหมดได้จากการใช้กฎทั้ง 3 ข้างต้นเท่านั้น

จะเห็นว่า สิ่งที่เพิ่มขึ้นมาคือ Quantifier ซึ่งจะมีได้สองแบบ คือ for all กับ for some ใช้นำหน้าตัวแปรใดๆ
และ Atom เอง ก็ไม่ใช่แค่ statement เฉยๆ แต่ว่ามีโครงสร้างที่ซับซ้อนขึ้นเมื่อ
Atom ต้องเป็น Predicate ซึ่ง Predicate นั้นเป็นสัญลักษณ์ที่รับค่า n จำนวนใดๆ และ Predicate เองก็จะทำการ map ค่าไปเป็นคำตอบแค่ จริงหรือเท็จเท่านั้น

ค่าที่จะใส่ลงไปใน Predicate เราเรียกว่า Term ซึ่ง term นั้นสามารถเป็น ค่าคงที่ หรือ ตัวแปร หรือฟังก์ชัน ก็ได้

3. Semantic ในลอจิกส่วนนี้ก็คือ Interpretation นั่นเอง ซึ่งมีความแตกต่างระหว่างลอจิกทั้งสองแบบ เนื่องจากว่าโครงสร้างไวยากรณ์ก็ไม่เหมือนกัน

Propositional Logic มี formula ที่ถูกสร้างมาจาก Atom ซึ่งเป็นแค่ statement เพราะฉะนั้น เราก็เพียงแค่ใส่ค่า ความจริงให้กับแต่ละ atom ว่า Atom/ Statement นั้นเป็นจริงหรือเท็จ แล้วก็ทำการประมวลผลตามหลักตรรกศาสตร์ธรรมดา
ตัวอย่างเช่น
เรากำหนดให้ มี Atom คือ P , Q โดยที่ P และ Q แทนค่า statement ดังนี้
P= นกแก้วเป็นนก   ( A parrot is a bird)
Q=นกบินได้ (A bird can fly)
กำหนดให้ formula G = P ∧ P->Q
และตารางกำหนดค่าความจริงของ Propositional Interpretation คือ

ดังนั้น Interpretation ของ G เมื่อเราให้ค่า P,Q = {T,T} จะได้ผลลัพธ์เป็น T ก็แสดงว่า formula G นี้เป็นจริงสำหรับ interpretation นี้ แต่ถ้าเราให้ค่า P,Q ={F,T} ก็จะได้ว่า G เป็นเท็จ สำหรับ interpretation นี้ (คือให้ว่า นกแก้วไม่เป็นนก , นกบินได้)

First-Order Logic นั้น formula ถูกสร้างมาจาก Atom ที่ซับซ้อน ดังนั้นการทำ interpretation ต้องมีการกำหนดค่า Domain ให้กับตัวแปร(variable) , ค่าคงที่ (constant), ผลลัพธ์ของ function และค่าความจริงของ predicate ร่วมด้วย
จากตัวอย่างข้างต้น
เรากำหนดให้  formula G = (∀x) (P(x) -> Q(x))
ให้ predicate P(x) =  x เป็นนก (x is a bird)  และให้ Q(x) = x บินได้  (x can fly)
ถ้าเรามี domain D = {นกแก้ว (parrot) , เพนกวิน (penguin)}
และมีตารางค่าความจริงของ predicate ของ First-Order Interpretation คือ

ดังนั้น Interpretation ของ G เมื่อเราให้ค่า x เป็น parrot ผลลัพธ์คือ T->T = T ถ้า x เป็น penguin ผลลัพธ์คือ T-> F = F  จะเห็นว่า มีตัวแปร x ตัวนึงใน domain D ให้ผลลัพธ์ interpretation เป็น   F ดังนั้นเราจะถือว่า formula  G เป็นเท็จสำหรับ interpretation

ทีนี้ก็พอจะเห็นความเหมือนและความแตกต่างของลอจิกทั้งสองแบบอย่างคร่าวๆแล้วนะคะ แนะนำว่าให้อ่านเพิ่มเติมอย่างละเอียดจะดีกว่า หนังสือแนะนำ ที่นี่ นะคะ

มาเรียน Logic for Computer Science (3 -- Natural Deduction ภาคสรุป)

ตอนนี้เราก็รู้จัก Natural Deduction ทั้ง 10 ข้อแล้วนะคะ สำหรับใครที่เพิ่งเข้ามาหน้านี้ แนะนำว่าให้อ่าน ที่นี่ ก่อนจะเข้าใจได้มากกว่าค่ะ
เราจะมาดูกันว่า วิธีการให้เหตุผลแบบนิรนัยนั้นจะสามารถนำมาใช้ได้อย่างไร

ตัวอย่างเช่น เราต้องการที่จะพิสูจน์ให้เห็นว่า A->B , B->C แล้ว  A->C
เราจะสมมติว่า A = ท้องฟ้ามีเมฆครึ้มและฟ้าร้อง, B = ฝนตก, C = พื้นถนนเปียก
ดังนั้น เรากำลังจะพิสูจน์ โดยมีข้อเท็จจริงที่ว่า
1. ถ้าท้องฟ้ามีเมฆครึ้มและฟ้าร้อง แล้วฝนตก  
2. ถ้าฝนตก แล้วพื้นถนนเปียก
ดังนั้น ถ้าท้องฟ้ามีเมฆครึ้มและฟ้าร้องแล้วพื้นถนนเปียก
 สามารถเขียน derivation ได้แบบนี้ค่ะ
     ท้องฟ้ามีเมฆครึ้มและฟ้าร้อง       (ท้องฟ้ามีเมฆครึ้มและฟ้าร้อง->ฝนตก)
         _________________________________________________(-> E)

                                          ฝนตก                                              (ฝนตก->พื้นถนนเปียก)

                                           _____________________________________________(-> E)

    พื้นถนนเปียก

 ____________________________________________(->I)

(ท้องฟ้ามีเมฆครึ้มและฟ้าร้อง -> พื้นถนนเปียก )

จะเห็นว่า เริ่มต้นพิสูจน์โดยการที่เราให้ discharged statement= ท้องฟ้ามีเมฆครึ้มและฟ้าร้อง (มีไฮไลท์สีเหลือง)  และใช้ implication elimination rule สองครั้ง และสุดท้ายจึงใช้ implication introduction rule (ซึ่งทำให้ต้อง discharge statement)

จากตัวอย่างนี้ คงจะทำให้พอมองออกแล้วนะคะว่า จริงๆแล้วมนุษย์เรามีการสรุปหาเหตุผลจากข้อเท็จจริงที่มีอยู่กันอย่างไร (ซึ่งได้อธิบายไปแล้วด้วย natural deduction 10 ข้อ)
ทีนี้ปัญหาต่อไปคือ ถ้าเราต้องการให้คอมพิวเตอร์ สามารถที่จะคิดหาเหตุผลแบบมนุษย์บ้างล่ะ  เราจะกำหนดรูปแบบต่างๆเหล่านี้ให้คอมพิวเตอร์ประมวลผลได้อย่างไร

สรุปโดยคร่าวๆเท่าที่เราพอเข้าใจนะคะ คือว่าจะเห็นว่า มนุษย์เราพิสูจน์หาว่า อะไรที่เป็นผลลัพธ์ที่มาจากข้อมูลที่มีอยู่บ้าง ซึ่งตรงนี้ถ้าจะให้คอมพิวเตอร์ประมวลผลได้ ก็ต้องทำการเก็บรูปแบบวิธีการคิดแบบนี้เข้าไปในคอมพิวเตอร์ให้คิดให้เรา ซึ่งทฤษฎีลอจิกที่คุ้นเคยกันดี ก็มี Propositional logic และ First-Order logic ซึ่ง ความแตกต่างของสองอันนี้อยู่ตรงที่
Propositional logic ใช้นำเสนอข้อมูล statement ธรรมดาที่ไม่ได้คำนึงถึงคำบอกปริมาณ ดังนั้นทำให้มันไม่สามารถที่จะนำเสนอข้อมูลตามความเป็นจริงได
First-Order logic จึงถูกสร้างขึ้นมาทดแทนข้อเสียตรงนั้น

เมื่อเราเก็บรูปแบบข้อมูลด้วย First-Order logic ได้แล้ว ต่อไปก็จะพูดถึงทฤษฎีที่ทำการพิสูจน์หาผลลัพธ์ของข้อมูลที่เรามีอยู่ เรียกว่า Logical consequence

จุดนี้ก็จะเห็นว่า ในทางทฤษฎี เรามีครบละ มีส่วนที่นำเสนอรูปแบบข้อมูล กับส่วนที่ทำการ deduce แต่ว่าเวลาจะนำไปใช้จริงล่ะ ก็มีทฤษฎีที่ชื่อว่า Herbrand's Theorem ที่แนะนำวิธีการนำไป implement ในคอมพิวเตอร์ให้ แต่!!!! ปัญหาคือมันเป็นไปได้ยากมากที่จะประสิทธิภาพของคอมพิวเตอร์จะรองรับไหว ต่อมาจึงมีทฤษฎี Resolution ที่นำ Herbrand's Theorem มาปรับใช้ได้จริง

สุดท้ายภาษาสำหรับเขียนโปรแกรมที่ถูก implement มาจากแนวคิด logic programming นี้ก็คือ ภาษา Prolog นั่นเองค่ะ แต่ว่าใน Prolog เองก็ยังมีเทคนิคอื่นๆเพิ่มเติมไปอีกนิดหน่อยนะคะ

เราคิดว่าเราคงจะไม่อธิบายทฤษฎีทั้งหมดนี้อย่างละเอียด เพราะมันมีแต่นิยามทฤษฎีเต็มไปหมด เราคงจะพูดถึงแค่แนวคิดกับการนำไปใช้อย่างง่ายๆ เพื่อเป็นแนวทางให้คนที่สนใจสามารถไปศึกษาต่อเพิ่มเติมได้ต่อไปค่ะ (เอาจริงๆมันอธิบายยากมากเลยล่ะ ไม่รู้จะอธิบายยังไงให้เข้าใจง่าย ฮ่าๆๆ)

เหมือนเดิม เราขอออกตัวก่อนเลยนะคะว่าไม่ใช่ผู้เชี่ยวชาญด้านนี้ เป็นแค่นักศึกษาอาจจะมีผิดถูกบ้าง สามารถแนะนำและพูดคุยกันได้นะคะ ;)

มาเรียน Logic for Computer Science (2 -- Natural Deduction ภาคต่อ)

วันนี้เราจะมาต่อจากเมื่อวานนะคะ จาก Natural Deduction ทั้ง 10 ข้อ เราก็ได้รู้จักไปแล้ว 3 กฎ สำหรับใครที่เพิ่งเข้ามาหน้านี้ แนะนำว่าให้อ่าน ที่นี่ ก่อนจะเข้าใจได้มากกว่าค่ะ
4. Implication Introduction Rule อันนี้เป็นกฎที่เรากำลังจะสร้างเงื่อนไข ถ้า...แล้ว.... ดังนั้น ถ้าเรามี statement (ข้อสันนิษฐาน)นึง และก็มีข้อพิสูจน์อันนึงว่าเกิดอะไรขึ้น เราก็จะสามารถสร้างข้อสรุปได้ว่า ถ้า statement นั้นแล้ว...

ตัวอย่างเช่น

statement = ฝนตก
derivation =                      ท้องฟ้าวันนี้มีเมฆครึ้มและพื้นถนนเปียก

_____________________________________(and E)

    พื้นถนนเปียก

เราก็จะพิสูจน์ข้อสรุปได้คือ conclusion = ถ้า ฝนตก แล้ว พื้นถนนเปียก
ซึ่ง statement = ฝนตก จะเรียกว่า discharged assumption คือมันไม่จำเป็นต้องใช้อีกแล้วสำหรับข้อสรุปบทพิสูจน์ เนื่องจากว่าถ้าดู ข้อสรุปหรือ conclusion ดีๆ จะเห็นว่า statement มันถูกรวมไปใน if ของ conclusion เรียบร้อยแล้ว
สามารถเขียน derivation ได้แบบนี้ค่ะ
                                                             ฝนตก
                                              __________________________

      ท้องฟ้าวันนี้มีเมฆครึ้มและพื้นถนนเปียก

_____________________________________(and E)

    พื้นถนนเปียก

                                      _________________________________(If I)
                                                  (ฝนตก -> พื้นถนนเปียก)

5. Implication Elimination Rule กฎ ข้อนี้บอกว่า ถ้าเรามีข้อพิสูจน์ (derivation) อันแรกที่อยู่ในรูปแบบของถ้าแล้ว(implication) และเรามีข้อพิสูจน์อีกอันที่ตรงกับ statement ใน implication เราก็สามารถที่จะสรุปบทพิสูจน์ออกมาเป็น ข้อสรุปของ implication ได้
พูดง่ายๆก็คือ ถ้าเรามีข้อมูลตรง if ว่าจริง ข้อมูลหลัง then ก็จะเป็นข้อสรุป

ตัวอย่างเช่น
derivation 1 =      ฝนตก
                        ________
                          ฝนตก
derivation 2=                                  ฝนตก -> พื้นถนนเปียก

_____________________________________

     ฝนตก -> พื้นถนนเปียก

เราก็จะพิสูจน์ข้อสรุปได้คือ conclusion =  พื้นถนนเปียก

สามารถเขียน derivation ได้แบบนี้ค่ะ
                                                 ฝนตก         (ฝนตก -> พื้นถนนเปียก)
                                      _______________________________________(If E)
                                                   พื้นถนนเปียก

6. Negation Elimination Rule  เป็นกฎที่บอกเราว่า ถ้ามีข้อพิสูจน์สองข้อใดๆที่มันขัดแย้งกันเอง ข้อสรุปก็คือ contradiction ซึ่งใช้สัญลักษณ์ เหมือนตัว T กลับด้านนะคะ

ตัวอย่างเช่น

derivation 1 =      ฝนตก
                        ________
                          ฝนตก
derivation 2=                                        ฝนไม่ตก

_______________________

  ฝนไม่ตก

เราก็จะพิสูจน์ข้อสรุปได้คือ conclusion =  contradiction เพราะมันขัดแย้งกัน

สามารถเขียน derivation ได้แบบนี้ค่ะ
                                                     ฝนตก            ฝนไม่ตก
                                      _______________________________________(~ E)
                                                                 contradiction

7. Negation Introduction Rule กฎ ข้อนี้บอกว่า ถ้าเรามี statement(ข้อสันนิษฐาน) นึง แล้วพิสูจน์ (derivation) ที่ได้ผลลัพธ์ว่า contradiction ดังนั้นเราจะสรุปข้อพิสูจน์เราได้เป็น ตรงกันข้ามกับ statement (ข้อสันนิษฐาน) ที่คิดไว้

ตัวอย่างเช่น
statement =      ฝนตก
derivation 1 =  พื้นถนนไม่เปียก

derivation 2 =                   ฝนตก               ฝนตก -> พื้นถนนเปียก

_____________________________________

   พื้นถนนเปียก

เราก็จะพิสูจน์ข้อสรุปได้คือ conclusion =  ฝนไม่ตก

สามารถเขียน derivation ได้แบบนี้ค่ะ
                                                 ฝนตก         (ฝนตก -> พื้นถนนเปียก)
                                         _______________________________________(If E)
             พื้นถนนไม่เปียก                             พื้นถนนเปียก
______________________________________________(~ E)
                                contradiction
___________________________________________(~ I)
                              ฝนไม่ตก

ซึ่ง statement = ฝนตก จะเรียกว่า discharged assumption คือมันไม่จำเป็นต้องใช้อีกแล้วสำหรับข้อสรุปบทพิสูจน์ เนื่องจากว่าถ้าดู ข้อสรุปมันตรงกันข้ามกับข้อสันนิษฐานที่เราคิดไว้

8. Reduction Ad Absurdum Rule กฎข้อนี้ตรงกันข้ามกับ ~I เพราะถ้าเรามี negation of statement(ข้อสันนิษฐาน) นึง แล้วพิสูจน์ (derivation) ที่ได้ผลลัพธ์ว่า contradiction ดังนั้นเราจะสรุปข้อพิสูจน์เราได้เป็น ตรงกันข้าม คือได้ statement (ข้อสันนิษฐาน)

ตัวอย่างเช่น
statement =      ฝนไม่ตก
derivation 1 =  พื้นถนนไม่เปียก

derivation 2 =                   ฝนไม่ตก               ฝนไม่ตก -> พื้นถนนไม่เปียก

_____________________________________

   พื้นถนนไม่เปียก

เราก็จะพิสูจน์ข้อสรุปได้คือ conclusion =  ฝนตก

สามารถเขียน derivation ได้แบบนี้ค่ะ
                                                 ฝนไม่ตก         (ฝนไม่ตก -> พื้นถนนไม่เปียก)
                                         _______________________________________(If E)
             พื้นถนนเปียก                             พื้นถนนไม่เปียก
______________________________________________(~ E)
                                contradiction
___________________________________________(RAA)
                              ฝนตก

 ซึ่ง statement = ฝนไม่ตก จะเรียกว่า discharged assumption คือมันไม่จำเป็นต้องใช้อีกแล้วสำหรับข้อสรุปบทพิสูจน์ เนื่องจากว่าถ้าดู ข้อสรุปมันตรงกันข้ามกับข้อสันนิษฐานที่เราคิดไว้

9. Disjunction Introduction Rule กฎ ข้อนี้บอกว่า ถ้าเรามีข้อพิสูจน์ได้ข้อสรุปอันนึง เราก็สามารถที่จะบอกได้ว่ามันเป็นข้อสรุปนั้นหรือข้อสรุปอื่นก็ได้ เพราะการใช้ "หรือ" จะเป็นจริงเมื่ออย่างใดอย่างหนึ่งเป็นจริง

ตัวอย่างเช่น

derivation 1 =  ท้องฟ้าวันนี้มีเมฆครึ้ม (ใช้ axiom rule ดังนั้นขอละไว้ในฐานที่เข้าใจนะคะ)
เราก็จะพิสูจน์ข้อสรุปได้คือ conclusion =  ท้องฟ้าวันนี้มีเมฆครึ้ม หรือ ฝนตก

สามารถเขียน derivation ได้แบบนี้ค่ะ
                                                
                                ท้องฟ้าวันนี้มีเมฆครึ้ม
___________________________________________(or I)
                     ท้องฟ้าวันนี้มีเมฆครึ้ม หรือ ฝนตก
 
10. Disjunction Elimination Rule กฎข้อนี้บอกว่า ถ้าเรามีข้อพิสูจน์ได้ข้อสรุปที่สามารถเป็นอย่างใดอย่างหนึ่ง  เราก็ตั้งข้อสันนิษฐาน(statement) ขึ้นมา แล้วถ้าข้อสันนิษฐานทั้งสองอันนั้นสามารถพิสูจน์ได้ข้อสรุปตรงกัน เราก็สามารถพิสูจน์ได้ข้อสรุปนั้นเช่นกัน

ตัวอย่างเช่น
derivation 1 =  ฝนตก หรือ สปริงเกอร์ถูกเปิดอยู่
derivation 2 =               ฝนตก      (ฝนตก -> พื้นถนนเปียก)
                    ___________________________________________(if E)
                                     พื้นถนนเปียก
derivation 3 =     สปริงเกอร์ถูกเปิดอยู่     (สปริงเกอร์ถูกเปิดอยู่  -> พื้นถนนเปียก)
                    __________________________________________________(if E)
                                                   พื้นถนนเปียก

เราก็จะพิสูจน์ข้อสรุปได้คือ conclusion =  พื้นถนนเปียก

สามารถเขียน derivation ได้แบบนี้ค่ะ

 ซึ่ง statement = it's raining กับ statement = the sprinkler is on จะเรียกว่า discharged assumption คือมันไม่จำเป็นต้องใช้อีกแล้วสำหรับข้อสรุปบทพิสูจน์

 เราพยายามพิมพ์ใหม่ให้เป็นภาษาไทยแล้วแต่มันยาวมากล้นหน้า ทำให้ดูแล้วงง ก็เลยขอตัดแปะเวอร์ชันภาษาอังกฤษจากเอกสารมาแทนแล้วกันนะคะ

ตอนนี้ก็รู้จัก Natural Deduction ทั้ง 10 แบบครบแล้วนะคะ ก็จะเห็นว่าจริงๆมันคือวิธีการคิดหาเหตุผลที่มนุษย์เราใช้กันอยู่แล้ว คราวหน้าจะนำวิธีกฎทั้ง 10 แบบนี้มาเขียนเป็นบทพิสูจน์ที่ยาวๆและตรงกับสถานการณ์จริงดู เพื่อที่ว่าจะได้เข้าใจมากขึ้นว่าถูกเอาไปใช้อย่างไรนะคะ