ตรรกศาสตร์: รูปแบบปกติประพจน์รวม

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

Propositional Logic กับ Predicate Logic

ก็ ถ้าพูดง่าย ๆ ก็คือ Predicate จะมีตัวแปรด้วย เช่น P(x) หรือ P(x, y) แต่ Proposition จะไม่มีตัวแปร คือเป็น P เฉย ๆ ค่าความจริงก็จะตายตัว ไม่ขึ้นกับตัวแปรใด ๆ

เราจะศึกษาตรรกศาสตร์ของประพจน์ (Proposition) ก่อน แล้วจึงขยายเป็นภาษาอันดับหนึ่ง (คือ มี ∀ กับ ∃ และประพจน์ภาคแสดง) ด้วยหลักการคล้าย ๆ กัน

รูปแบบปกติประพจน์รวม (Conjunctive Normal Form)

ใน Propositional Logic สมมติว่าเรามีประพจน์ ที่ประกอบด้วยตัวเชื่อมต่าง ๆ กัน เราจะสามารถเขียนใหม่ให้มีแต่ตัวเชื่อม ∧ ∨ และ ¬ ได้ เช่น

p → q ≡ ¬p ∨ q
p ↔ q ≡ (¬p ∨ q) ∧ (p ∨ ¬q)

คราวนี้ เราจะจัดรูปให้เป็นรูปแบบปกติประพจน์รวม ได้ โดยเขียนให้เป็น "ผล ∧ ของผล ∨" เช่น

p ∨ (q ∧ (r ∨ s)) ≡ (p ∨ q) ∧ (p ∨ r ∨ s)

เพื่อให้เขียนสะดวก เรามักจะเขียนแยก ๆ กัน เป็น

p ∨ q
p ∨ r ∨ s

ประโยชน์ของประพจน์ในรูปแบบนี้ก็คือ เราสามารถใช้วิธีการรวมของ Robinson (Robinson's Resolution) ได้ ซึ่งหลักการก็คือ

(p ∨ q) ∧ (¬p ∨ r) ≡ (p ∨ q) ∧ (¬p ∨ r) ∧ (q ∨ r)

จะได้พจน์ใหม่เกิดขึ้นจากการรวม p กับ ¬p ในสองพจน์แรก คือ q ∨ r

วิธีพิสูจน์อันนี้ไม่ยากเท่าไหร่ แค่คิดว่า ถ้า p เป็นจริงแล้วเป็นยังไง ถ้า p เป็นเท็จแล้วเป็นยังไง ก็พิสูจน์ได้แล้ว

ตัวอย่างการใช้งาน เช่น สมมติว่าต้องการพิสูจน์ว่า

((p → q) ∧ (q → r)) → (p → r)

บทพิสูจน์โดยใช้ต้นไม้พิสูจน์ มีให้ดูแล้วใน ตรรกศาสตร์: ต้นไม้การพิสูจน์ และต้นไม้ตัวอย่างขัดแย้ง แต่คราวนี้จะแสดงอีกวิธีให้ดู เรียกว่า Resolution-Refutation

เริ่มโดยการใส่นิเสธเข้าไปก่อน

¬[((p → q) ∧ (q → r)) → (p → r)]

เราจะแสดงว่า ประพจน์นี้เป็นเท็จ ... กำจัดเครื่องหมาย "→" ซะก่อน

¬[¬((¬p ∨ q) ∧ (¬q ∨ r)) ∨ (¬p ∨ r)]

แล้วก็กระจายเข้าไป

(¬p ∨ q) ∧ (¬q ∨ r) ∧ p ∧ ¬r

ได้เป็นรูปแบบปกติประพจน์รวมแล้ว ประกอบด้วยวรรค (Clause) สี่วรรค คือ

¬p ∨ q
¬q ∨ r
p
¬r

คราวนี้ก็ใช้ resolution ได้ละ ลองรวม 2 วรรคแรกก่อน ... วรรคใหม่จะไม่มี q

¬p ∨ q
¬q ∨ r
p
¬r
¬p ∨ r

จะเห็นว่า ถ้าเรารวมวรรคใหม่นี้กับ p (วรรคที่ 3) ก็จะเหลือ r ซึ่งพอรวมกับ ¬r (วรรคที่ 4) จะได้วรรคว่าง แสดงว่า ประพจน์ตั้งต้นเป็นสัจพจน์ (นิเสธมันเลยเป็นเท็จ)

¬p ∨ q
¬q ∨ r
p
¬r
¬p ∨ r
r
∅

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

แล้ว ... ภาษาอันดับหนึ่งหละ?

พอจะทำแบบเดียวกันในภาษาอันดับหนึ่ง ปัญหามันก็เกิดหละ ... จริง ๆ เราก็ทำให้อยู่ในรูปแบบปกติประพจน์รวมได้นะ แต่มันมีขั้นตอนเพิ่ม ... ดูตัวอย่างนี้ละกัน

∀x[∀y[P(x, y) → ∃z[Q(x, y, z)]] ↔ R(x)]

เริ่มโดยกำจัดตัวเชื่อม → และ ↔ ออกก่อน แล้วย้ายเครื่องหมาย ¬ เข้าไปในสุด (คือ ติดกับตัวประพจน์)

∀x[∀y[¬P(x, y) ∨ ∃z[Q(x, y, z)]] ↔ R(x)]
≡ ∀x[(¬∀y[¬P(x, y) ∨ ∃z[Q(x, y, z)] ∨ R(x)) ∧
(∀y[¬P(x, y) ∨ ∃z[Q(x, y, z)] ∨ ¬R(x))]
≡ ∀x[(∃y[P(x, y) ∧ ∀z[¬Q(x, y, z)]] ∨ R(x)) ∧
(∀y[¬P(x, y) ∨ ∃z[Q(x, y, z)] ∨ ¬R(x))]

แล้วตอนนี้จะทำไงต่อดีหละ ??? ... ติดตามตอนหน้าละกัน (ตอนหน้าชื่อว่า ตรรกศาสตร์: รูปแบบปกติสโกเล็ม นะ มันเป็นขั้นตอนต่อจากนี้เลยหละ)