Hình thức luận, trực giác luận, Platon luận

Định lý này là minh họa sắc bén nhất trong lớp học cho chia rẽ Hình thức/Platon luận với Trực giác luận: chứng minh cổ điển (phi cấu trúc) thiết lập tồn tại bằng chia trường hợp trên một mệnh đề chưa quyết định, không bao giờ cho biết trường hợp nào là thật, còn chứng minh cấu trúc đưa ra giá trị tường minh.

Chứng minh cổ điển (phi cấu trúc). Xét $\sqrt{2}^{\sqrt{2}}$. Theo luật bài trung, hoặc $\sqrt{2}^{\sqrt{2}} \in \mathbb{Q}$ hoặc $\sqrt{2}^{\sqrt{2}} \notin \mathbb{Q}$ — ta không cần biết cái nào đúng.

Trường hợp 1: nếu $\sqrt{2}^{\sqrt{2}} \in \mathbb{Q}$, lấy $a = \sqrt{2}^{\sqrt{2}}, b = \sqrt{2}$: cả hai đều vô tỉ ($\sqrt{2}$ vô tỉ theo chứng minh phản chứng cổ điển về tính chẵn lẻ của $p,q$ trong $p/q=\sqrt 2$), và $a^b = \sqrt{2}^{\sqrt{2}}$ hữu tỉ theo giả thiết trường hợp này. Xong.

Trường hợp 2: nếu $\sqrt{2}^{\sqrt{2}} \notin \mathbb{Q}$, lấy $a = \sqrt{2}^{\sqrt{2}}$ (vô tỉ theo giả thiết trường hợp này) và $b = \sqrt{2}$ (vô tỉ). Khi đó $a^b = 2$: $a^b = (\sqrt{2}^{\sqrt{2}})^{\sqrt{2}} = \sqrt{2}^{2} = 2$. Vì $2 \in \mathbb{Q}$, xong.

Dù trường hợp nào ta cũng đã chỉ ra $a,b$ vô tỉ với $a^b \in \mathbb{Q}$ — nhưng chứng minh không bao giờ cho biết trường hợp nào đúng, tức $\sqrt{2}^{\sqrt 2}$ hữu tỉ hay vô tỉ. Người Hình thức luận chấp nhận ngay (đây là dẫn xuất hợp lệ trong logic cổ điển bậc nhất); người Trực giác luận bác bỏ đây là chứng minh tồn tại thực sự vì nó không tạo ra một cặp $(a,b)$ tường minh duy nhất kèm chứng minh rằng chính cặp đó hoạt động.

Chứng minh cấu trúc (loại bỏ chia trường hợp). Lấy $a = \sqrt{2}$ và $b = \log_2 9$. Cả hai đều vô tỉ: $\sqrt 2$ vô tỉ như trên; $\log_2 9$ vô tỉ vì nếu $\log_2 9 = p/q$ tối giản với $q>0$ thì $2^{p/q}=9$, nên $2^p = 9^q$, nhưng vế trái là lũy thừa của $2$ còn vế phải là lũy thừa của $3$ (với $q \ge 1$, $9^q$ chỉ có ước nguyên tố $3$), buộc $p=q=0$, mâu thuẫn với $9^q=2^p>1$.

Bây giờ tính tường minh: $a^b = \sqrt{2}^{\log_2 9} = 2^{\frac{1}{2}\log_2 9} = 2^{\log_2 3} = 3$, dùng $\sqrt{2} = 2^{1/2}$, nên $a = \sqrt{2}, b = \log_2 9$ cho $a^b = (2^{1/2})^{\log_2 9} = 2^{\frac{1}{2}\log_2 9} = 2^{\log_2 3} = 3 \in \mathbb{Q}$.

Lần này không chia trường hợp, không có tuyển chưa giải quyết — câu hỏi mở ban đầu của Chứng minh 1 (là $\sqrt2^{\sqrt2}$ hữu tỉ hay không?) hoàn toàn bị bỏ qua, và người Trực giác luận chấp nhận cặp $(\sqrt{2}, \log_2 9)$ là chứng cứ thực sự. (Chú thích lịch sử: Gelfond–Schneider (1934) sau đó chứng minh $\sqrt{2}^{\sqrt 2}$ thực ra vô tỉ — thậm chí siêu việt — giải quyết Trường hợp 2 là "đúng", nhưng chứng minh cổ điển ở trên không cần định lý sâu sắc đó.)

Kolmogorov (1925) và Gödel (1933) độc lập chỉ ra logic cổ điển nhúng được vào logic trực giác qua "phép dịch âm" này: ta không bao giờ khôi phục được LEM đầy đủ, nhưng luôn khôi phục được phủ định kép của nó, chính là điều cần thiết để nhúng chứng minh số học cổ điển vào hệ trực giác, một bước then chốt trong các trợ lý chứng minh hình thức hóa sau này.

Bước 1: Cố định các luật trực giác được phép dùng. Logic trực giác giữ modus ponens và luật suy diễn tự nhiên cho $\wedge, \vee, \to$, và định nghĩa $\neg P := (P \to \bot)$ với $\bot$ là phi lý ("từ chứng minh $\bot$ suy ra mọi thứ" — ex falso quodlibet — hợp lệ theo trực giác). Điều không được giả định là $P \vee \neg P$ hay luật khử phủ định kép $\neg\neg P \to P$.

**Bước 2: Chứng minh chiều dễ $P \to \neg\neg P$ theo trực giác.** Giả sử có chứng minh của $P$. Ta cần tạo chứng minh của $\neg\neg P = (( P \to \bot) \to \bot)$, tức giả sử có chứng minh của $(P \to \bot)$ và suy ra $\bot$. Áp dụng hàm giả sử này vào chứng minh $P$ của ta cho ngay chứng minh $\bot$. Vậy $P \to \neg\neg P$ đúng mà không cần chia trường hợp — chiều này không bao giờ cần LEM.

**Bước 3: Xây trực tiếp chứng minh của $\neg\neg(P \vee \neg P)$.** Ta cần chỉ ra $((P \vee \neg P) \to \bot) \to \bot$. Giả sử có chứng minh $h$ của $(P \vee \neg P) \to \bot$ (tức $h$ bác bỏ tuyển); ta cần suy ra $\bot$. Quan sát rằng $h$, giới hạn lên vế phải tuyển, cho hàm nhận mọi chứng minh của $P$ tới chứng minh $\bot$ — đó chính xác là chứng minh của $\neg P$ (áp dụng $h$ sau khi bọc bằng phép nhúng phải $\text{inr}$). Gọi chứng minh suy ra này là $n : \neg P$.

Bước 4: Khép vòng. Bây giờ vì có $n : \neg P$, ta lập được $\text{inr}(n) : P \vee \neg P$ (vế phải của $P \vee \neg P$, khởi tạo với chứng minh $n$). Đưa hạng tử này ngược vào $h$: $h(\text{inr}(n))$ là chứng minh của $\bot$, chính xác là $\bot$ ta cần suy ra ở Bước 3. Điều này khép giả định ở Bước 3, cho chứng minh trực giác đầy đủ của $\neg((P\vee\neg P)\to\bot)$, tức của $\neg\neg(P \vee \neg P)$.

*Bước 5: Vì sao điều này không* trả lại $P \vee \neg P$.** Bước 4 tạo ra $\neg\neg(P \vee \neg P)$, nhưng theo trực giác $\neg\neg Q \to Q$ không suy ra được nói chung (điều đó đòi hỏi chính nguyên lý giống LEM mà ta thiếu). Vậy phép dịch thực sự yếu hơn: nó chỉ ra "luật" của logic cổ điển tồn tại như một khẳng định không thể bác bỏ (phủ định của nó luôn mâu thuẫn) ngay cả khi nó không thể khẳng định trực tiếp — chính khoảng cách này cho phép toán học cấu trúc cùng tồn tại với, và diễn giải, toán học cổ điển qua phép dịch âm Gödel của mọi công thức $\phi \mapsto \phi^N$ (thay mỗi công thức nguyên tố và mỗi liên từ bằng tương ứng phủ định kép trực giác của nó), gửi mọi mệnh đề số học chứng minh được cổ điển thành mệnh đề chứng minh được theo trực giác.