Logic คืออะไร?

Basic Framework of Logic

โดยทั่วไป Logic framework ใดๆจะประกอบด้วย 3 ส่วนหลักๆคือ

1. Syntax ใช้สำหรับระบุว่า สัญลักษณ์อะไรบ้างที่กำหนดให้ใช้ได้ในระบบที่เราสนใจ
2. Semantics ซึ่งอธิบายเกี่ยวกับ Validity ของประโยคที่สร้างมาจากสัญลักษณ์ที่อนุญาตให้ใช้
3. Proof Theory ใช้อธิบายว่า “อะไรคือประโยคที่สามารถสร้างขึ้นได้ใน syntax ที่ถูกกำหนด”

Proof Theory ถือเป็นส่วนประกอบที่สำคัญในการหา Logical Consequence ซึ่งจะกล่าวในลำดับต่อไป

Logical Consequence

หากพิจารณาความหมายของ Proof Theory ในภาษาบ้านๆ เราอาจจะตีความได้ว่า มันคือกระบวนการที่ช่วยค้นพบประโยคที่เป็นจริงที่ถูกซ่อนอยู่ เช่น สมมุติระบบของ Propositional Logic เราอาจกำหนดให้ propostion p แทนประโยค “ฝนตก”, q แทนประโยค “รถติด”, และประโยค p -> q แทน “ถ้าฝนตก แล้วรถติด” เป็นจริง เราอาจสรุปได้ว่า ประโยค q ก็เป็นจริงเหมือนกัน ถึงแม้ว่าประโยคนั้นอาจไม่ได้ถูกกำหนดให้เป็นจริงในตอนเริ่มต้น

กระบวนการหา Logical Consequence ทำได้หลายวิธี เช่น Resolution-based Calculus, Sequent-based Calculus, Natural Deduction เป็นต้น แต่ละเทคนิคมีข้อดีและข้อเสียที่แตกต่างกัน ซึ่งผู้เขียนขออนุญาตไม่อธิบายในโพสต์นี้

การจัดการกับ Contradiction ในระบบ

ในความเป็นจริง การหา logical consequnce อาจไม่สามารถหลีกเลี่ยงกับการเจอ Contradiction ได้ ขอโน๊ตไว้ว่า contradiction หมายถึง สิ่งที่แสดงถึงความขัดแย้ง

Contradiction ถือว่าเป็นอันตรายใน Classical Logic เพราะการมี contradiction ในระบบทำให้ระบบสามารถสร้างประโยคอะไรก็ได้แล้วเป็นจริงตลอด (ผู้ที่สนใจสามารถอ่านเพิ่มเติมเกี่ยวกับ Reductio ad absurdum). ประเด็นนี้นำไปสู่การพัฒนาของระบบที่ฉลาดขึ้นเรียกว่า Non-monotonic Reasoning. ปัญหานี้ถือเป็นปัญหาที่สำคัญปัญหาหนึ่งในวงการ Theoritical Artificial Intelligence และมีงานวิจัยที่พัฒนาเรื่อยมาต่อเนื่อง เช่น Defeasible Logic, Answer Set Programming, และ Argumentation Framework เป็นต้น

Herbrand’s Theorem

การคิดค้น Proof Theory เพื่อที่จะตอบคำถาม ประโยคอะไรถูกต้อง (หรือ เป็นจริง) ได้บ้าง มีการศึกษามายาวนาน อาจจะกล่าวพอสังเขปได้ว่า Leibniz (1646 – 1716) คือผู้บุกเบิกที่สำคัญในปัญหานี้

อย่างไรก็ตาม Gödel ค้นพบว่า มีประโยคในระบบจำนวนที่ไม่สามารถพิสูจน์ว่าเป็นจริงได้ด้วยกระบวนการใดๆ (algorithm) ถึงแม้ว่าจะเป็นจริงก็ตาม  (อ่าน Gödel’s incompleteness theorems) Church และ Turing ได้ขยายความข้อสรุปของ Gödel (ทั้งคู่ไม่ได้ทำงานร่วมกัน) ต่อว่า มันไม่มีกระบวนการที่จะพิสูจน์ว่าเป็นจริงสำหรับประโยคใดๆที่สร้างในระบบ First-order Logic (ประเด็นนี้เกี่ยวกับ Semantics Completeness ซึ่งผู้เขียนจะขอเล่าในคราวต่อไป) แต่การค้นพบที่สำคัญของช่วงการศึกษาสมัยนั้นคือ ถ้าเรารู้ว่าประโยคใดๆเป็นจริง เราสามารถแสดงได้ว่าประโยคนั้นเป็นจริง (ความสัมพันธ์นี้เรียกอีกอย่างได้ว่า Soundness ซึ่งจะขอเก็บไว้เล่าภายหลังเช่นกัน)

ทฤษฎีที่เข้ามาช่วยเติมเต็มการพัฒนา Automatic Theorem Provers คือการค้นพบของ Herbrand ในปี 1930. ใจความสำคัญของทฤษฏี Herbrand คือ เราสามารถที่จะหา Universe เพื่อแสดงว่าประโยคใดๆนั้นไม่เป็นจริงได้ การค้นพบนี้คือจุดสำคัญ และเป็นพื้นฐานต่อมาในการสร้าง Automatic Theorem Provers เพราะหากประโยคใดๆนั้นเป็นจริงทุกประการ เราจะไม่สามารถหา Universe นั้นได้ และกระบวนการ Proof จะยุติ (terminate) ในเวลาจำกัด

หมายเหตุ

เนื่องจากโพสต์นี้เป็นโพสต์แรก ผู้เขียนขอละไม่ใช้ศัพท์ทางเทคนิค แต่จะพยายามอธิบายในภาษาที่น่าจะเข้าใจได้ง่ายและกระชับ

First blog post

This is your very first post. Click the Edit link to modify or delete it, or start a new post. If you like, use this post to tell readers why you started this blog.