Phép dịch phủ định kép Gödel–Kolmogorov

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.