July 9, 1980 — Arend Hayting: Mathematics that rejects “if it’s not false, it must be true.”
Today in the history of mathematics. | อาเรนด์ เฮย์ทิง ถึงแก่กรรม 9 กรกฎาคม ค.ศ. 1980
บทนำ: บทพิสูจน์ที่ไม่บอกอะไรเลย
โจทย์: จงแสดงว่ามีจำนวนอตรรกยะ $a, b$ ซึ่ง $a^b$ เป็นจำนวนตรรกยะ
บทพิสูจน์: พิจารณา $\sqrt{2}^{\sqrt{2}}$
- กรณี 1: ถ้ามันเป็นตรรกยะ ก็เลือก $a = b = \sqrt{2}$ เสร็จ
- กรณี 2: ถ้ามันเป็นอตรรกยะ ก็เลือก $a = \sqrt{2}^{\sqrt{2}}$ และ $b = \sqrt{2}$ จะได้
$$ a^b = \left(\sqrt{2}^{\sqrt{2}}\right)^{\sqrt{2}} = \sqrt{2}^{,2} = 2 $$
ซึ่งเป็นตรรกยะ เสร็จ $\blacksquare$
คำถามที่ควรทำให้คุณอึดอัด: แล้ว $a$ กับ $b$ ที่ว่านั้นคือตัวไหนกันแน่?
บทพิสูจน์บอกว่า “มีอยู่” แต่ไม่บอกว่า “คืออะไร” มันอาศัยกฎที่เรียกว่า กฎการมีค่าความจริงกลางแบบไม่รวม (Law of the Excluded Middle)
$$ P \lor \neg P $$
และนี่คือกฎที่นักคณิตศาสตร์กลุ่มหนึ่ง — นักอินทูอิชันนิสต์ (intuitionists) — ปฏิเสธ
ผู้ที่ทำให้ปรัชญานี้กลายเป็นระบบตรรกศาสตร์ที่ใช้งานได้จริง คือ อาเรนด์ เฮย์ทิง (Arend Heyting, 1898–1980) ผู้จากไปในวันนี้
1. ปรัชญาของ Brouwer และปัญหาของมัน
L. E. J. Brouwer เสนอว่า คณิตศาสตร์คือ กิจกรรมทางความคิดของมนุษย์ สิ่งที่ “มีอยู่” หมายถึงสิ่งที่ สร้างขึ้นมาได้จริง
ในโลกทัศน์นี้:
- การพิสูจน์ $\exists x, P(x)$ ต้อง แสดง $x$ ที่ชัดเจนออกมา (หรือวิธีสร้างมัน)
- การพิสูจน์ $P \lor Q$ ต้อง ระบุได้ว่าข้อไหนจริง
- $\neg\neg P \Rightarrow P$ ไม่จริงเสมอไป — การที่ “การสมมติว่าไม่ $P$ นำไปสู่ความขัดแย้ง” ไม่ได้แปลว่าเราสร้าง $P$ ขึ้นมาได้
แต่ปัญหาคือ Brouwer เขียนอธิบายแนวคิดของตนอย่างจงใจ ไม่เป็นรูปนัย ในสไตล์ส่วนตัวมาก จนแทบไม่มีใครนอกวงเข้าใจ
2. เฮย์ทิงเข้ามาแปลภาษา
เฮย์ทิงเกิดที่อัมสเตอร์ดัม 9 พฤษภาคม 1898 เป็นลูกศิษย์ของ Brouwer และเป็นผู้ที่ทุ่มเทให้อินทูอิชันนิสม์มากที่สุด
- 1925 — วิทยานิพนธ์ปริญญาเอก Intuitionistische axiomatiek der projectieve meetkunde (สัจพจน์เชิงอินทูอิชันของเรขาคณิตเชิงภาพฉาย) ซึ่งเป็น การศึกษาการวางสัจพจน์ในคณิตศาสตร์เชิงสร้างครั้งแรกของโลก ในช่วงนั้นเขาเป็นเพียงครูมัธยมในเมือง Enschede เมืองอุตสาหกรรมสิ่งทอที่ห่างไกลจากวงวิชาการ เขาทำวิจัยในเวลาว่างทั้งหมด
- 1927–1928 — สมาคมคณิตศาสตร์เนเธอร์แลนด์ตั้งคำถามชิงรางวัล: ขอให้ทำ formalisation ของทฤษฎีอินทูอิชันนิสม์ของ Brouwer เรียงความของเฮย์ทิงชนะรางวัล
- 1930 — ตีพิมพ์ฉบับขยาย ซึ่งกลายเป็น ระบบตรรกศาสตร์อินทูอิชันนิสม์อย่างเป็นรูปนัยระบบแรก
ความย้อนแย้งที่งดงาม: Brouwer เองต่อต้านการทำ formalisation ในเชิงหลักการ และเคยพูดถึงงานของลูกศิษย์ตนอย่างไม่ปลื้ม (มีบันทึกว่าเขาเรียกมันว่าเป็นการฝึกที่ไร้ผล) การใส่ชื่อ Brouwer ไว้ใน “การตีความ Brouwer–Heyting–Kolmogorov” จึงเป็นเรื่องของการให้เกียรติเป็นหลัก
3. ตรรกศาสตร์อินทูอิชันนิสม์ต่างจากตรรกศาสตร์คลาสสิกอย่างไร
สิ่งที่ยังใช้ได้:
$$ P \Rightarrow \neg\neg P, \qquad \neg\neg\neg P \Leftrightarrow \neg P, \qquad \text{modus ponens} $$
สิ่งที่ใช้ไม่ได้:
| สูตร | ชื่อ | สถานะ |
|---|---|---|
| $P \lor \neg P$ | Excluded Middle | ✗ |
| $\neg\neg P \Rightarrow P$ | Double Negation Elimination | ✗ |
| $(\neg Q \Rightarrow \neg P) \Rightarrow (P \Rightarrow Q)$ | Contraposition (ทิศนี้) | ✗ |
| $\neg\forall x, P(x) \Rightarrow \exists x, \neg P(x)$ | — | ✗ |
| $\neg(P \land Q) \Rightarrow (\neg P \lor \neg Q)$ | De Morgan (ข้อนี้) | ✗ |
หมายเหตุที่สำคัญมาก: การที่ $P \lor \neg P$ พิสูจน์ไม่ได้ ไม่ได้แปลว่า มันเป็นเท็จ ที่จริง $\neg\neg(P \lor \neg P)$ พิสูจน์ได้ ในตรรกศาสตร์อินทูอิชันนิสม์ กล่าวคือ เราปฏิเสธมันไม่ได้เช่นกัน — เราแค่ยืนยันมันไม่ได้
4. การตีความ BHK: ความหมายของ “การพิสูจน์”
หัวใจของระบบนี้คือการนิยาม ความหมายของตัวเชื่อม ผ่าน สิ่งที่นับเป็นบทพิสูจน์
การตีความ Brouwer–Heyting–Kolmogorov (BHK)
- บทพิสูจน์ของ $P \land Q$ คือ คู่ ของบทพิสูจน์ $P$ และบทพิสูจน์ $Q$
- บทพิสูจน์ของ $P \lor Q$ คือ ป้ายกำกับ ว่าเลือกข้างไหน + บทพิสูจน์ของข้างนั้น
- บทพิสูจน์ของ $P \Rightarrow Q$ คือ ฟังก์ชัน ที่แปลงบทพิสูจน์ของ $P$ เป็นบทพิสูจน์ของ $Q$
- บทพิสูจน์ของ $\exists x, P(x)$ คือ คู่ $(a,; \text{บทพิสูจน์ของ } P(a))$
- บทพิสูจน์ของ $\forall x, P(x)$ คือ ฟังก์ชัน ที่รับ $a$ ใด ๆ แล้วคืนบทพิสูจน์ของ $P(a)$
- $\neg P$ นิยามเป็น $P \Rightarrow \bot$ (บทพิสูจน์ของ $P$ นำไปสู่ความขัดแย้ง)
อ่านตารางนี้อีกครั้งช้า ๆ แล้วเปลี่ยนคำว่า “บทพิสูจน์” เป็น “โปรแกรม” และ “ประพจน์” เป็น “ชนิดข้อมูล (type)”
| ตรรกศาสตร์ | การเขียนโปรแกรม |
|---|---|
| $P \land Q$ | tuple / struct |
| $P \lor Q$ | tagged union / Either |
| $P \Rightarrow Q$ | ฟังก์ชัน P -> Q |
| $\forall x., P(x)$ | dependent function |
| $\exists x., P(x)$ | dependent pair |
นี่คือ Curry–Howard correspondence: บทพิสูจน์คือโปรแกรม ประพจน์คือชนิดข้อมูล
ตรรกศาสตร์อินทูอิชันนิสม์ของเฮย์ทิงจึงกลายเป็นรากฐานของระบบพิสูจน์ Coq, Agda, Lean, Idris และของ ภาษาโปรแกรมเชิงฟังก์ชัน ทั้งมวล
ความคิดเชิงปรัชญาจากทศวรรษ 1920 กลายเป็นเทคโนโลยีในทศวรรษ 2020
5. พีชคณิตเฮย์ทิง (Heyting Algebra)
ในทางพีชคณิต ตรรกศาสตร์คลาสสิกสอดคล้องกับ พีชคณิตบูล (Boolean algebra) ส่วนตรรกศาสตร์อินทูอิชันนิสม์สอดคล้องกับ พีชคณิตเฮย์ทิง
นิยาม พีชคณิตเฮย์ทิงคือแลตทิซมีขอบเขต $(H, \land, \lor, 0, 1)$ ที่สำหรับทุก $a, b \in H$ มีสมาชิก $a \to b$ ซึ่ง $$ c \le (a \to b) \quad\Longleftrightarrow\quad (c \land a) \le b $$
นิยาม $\neg a := (a \to 0)$ จะพบว่า $a \lor \neg a = 1$ ไม่จำเป็นต้องเป็นจริง
ตัวอย่างที่งดงามที่สุด: เซตของ เซตเปิด ทั้งหมดของปริภูมิทอพอโลยีใด ๆ เป็นพีชคณิตเฮย์ทิง โดย
$$ \neg U = \operatorname{int}(X \setminus U) $$
ลองให้ $X = \mathbb{R}$ และ $U = (-\infty, 0)$ จะได้ $\neg U = (0, \infty)$ ดังนั้น
$$ U \lor \neg U = (-\infty,0) \cup (0,\infty) \neq \mathbb{R} $$
จุด $0$ หายไป — นั่นคือ excluded middle ล้มเหลว และเรามองเห็นมันได้ด้วยตาเปล่า
6. ชีวิตในบั้นปลาย
- 1936 — Privatdozent ที่ University of Amsterdam
- 1948 — ศาสตราจารย์ที่อัมสเตอร์ดัม (ภายหลังสืบทอดเก้าอี้ของ Brouwer)
- 1956 — ตำรา Intuitionism: An Introduction ซึ่งยังเป็นหนังสือแนะนำมาตรฐานจนถึงวันนี้
- 1968 — เกษียณ
- 9 กรกฎาคม 1980 — ถึงแก่กรรมที่เมือง Lugano ประเทศสวิตเซอร์แลนด์ อายุ 82 ปี
เพื่อนร่วมงานจดจำเขาในฐานะผู้ปกป้องอุดมคติทางปรัชญาของตนอย่างมั่นคง ควบคู่กับความเมตตากรุณาที่ไม่มีวันหมด
Thought-provoking activities
- หาบทพิสูจน์ เชิงสร้าง ของโจทย์ในบทนำ (คำใบ้: ใช้ $a = \sqrt{2}$ และ $b = 2\log_2 3$ แล้วแสดงว่า $b$ เป็นอตรรกยะ ส่วน $a^b = 3$)
- พิสูจน์ในตรรกศาสตร์อินทูอิชันนิสม์ว่า $\neg\neg(P \lor \neg P)$ เป็นทฤษฎีบท (ใช้การตีความ BHK)
- เขียนฟังก์ชันที่มี type signature ตรงกับ $P \Rightarrow \neg\neg P$ นั่นคือ
p -> ((p -> Void) -> Void)แล้วอธิบายว่าเหตุใดจึงเขียน((p -> Void) -> Void) -> pไม่ได้ - บนปริภูมิ $X = \mathbb{R}^2$ ให้ $U$ เป็นดิสก์เปิดหนึ่งหน่วยที่ เอาจุดศูนย์กลางออก จงหา $\neg U$ และ $\neg\neg U$ แล้วตรวจสอบว่า $\neg\neg U = U$ หรือไม่
- อภิปราย: บทพิสูจน์โดยข้อขัดแย้งที่นักศึกษาเรียนในวิชาคณิตศาสตร์ดิสครีต — ข้อไหนใช้ได้ในตรรกศาสตร์อินทูอิชันนิสม์ ข้อไหนใช้ไม่ได้? (เช่น การพิสูจน์ว่า $\sqrt{2}$ เป็นอตรรกยะ ใช้ได้หรือไม่?)
References
- Heyting, A. (1930). Die formalen Regeln der intuitionistischen Logik. Sitzungsberichte der Preussischen Akademie der Wissenschaften.
- Heyting, A. (1956). Intuitionism: An Introduction. North-Holland.
- Troelstra, A. S., & van Dalen, D. (1988). Constructivism in Mathematics: An Introduction. North-Holland.
- Moschovakis, J. R. (2007). The Logic of Brouwer and Heyting. In Handbook of the History of Logic.
- Sørensen, M. H., & Urzyczyn, P. (2006). Lectures on the Curry–Howard Isomorphism. Elsevier.
- O’Connor, J. J., & Robertson, E. F. Arend Heyting. MacTutor History of Mathematics Archive.
ชุดบทความ “วันนี้ในประวัติศาสตร์คณิตศาสตร์” — เผยแพร่ 9 กรกฎาคม 2569
