Chứng minh và bảng ngữ nghĩa

1. Chứng minh là gì

Một lập luận là khẳng định rằng một kết luận nào đó suy ra từ một số tiền đề. Chứng minh là thứ phân định khẳng định ấy: một đối tượng hữu hạn, kiểm tra được, mà bất kỳ ai cũng có thể đọc từng dòng và đồng ý, không phải tin lời bạn. Giá trị của một chứng minh không nằm ở chỗ nó thuyết phục - một bài diễn thuyết hay cũng làm được - mà ở chỗ từng bước trong đó không thể khác đi.

Đó là đòi hỏi khắt khe hơn ta tưởng. «Trời mưa, nên mặt đất ướt» là điều hợp lý để nói, nhưng nó dựa vào những gì bạn biết về mưa và đất. Logic hình thức gạt điều đó sang bên và đặt một câu hỏi hẹp hơn: chỉ dựa vào hình thức của các câu, liệu có cách nào để các tiền đề đúng còn kết luận sai hay không? Nếu không có cách nào, lập luận là hợp lệ, và chứng minh chính là bản ghi vì sao không có.

Hướng dẫn này nói về một cách tạo ra bản ghi đó - phương pháp bảng ngữ nghĩa, còn gọi là cây chân trị. Đây là phương pháp trang này dùng mỗi khi bạn gõ một lập luận vào máy tính, và một khi đã theo nó một lần, bạn có thể kiểm tra một lập luận trên giấy chỉ với một cây bút.

2. Hợp lệ, và làm sao biết được

Viết một lập luận với dấu kéo theo: tiền đề bên trái, kết luận bên phải. Khẳng định p → q, ¬q ⊨ ¬p nói rằng từ một mệnh đề kéo theo và phủ định hậu từ của nó, suy ra phủ định tiền từ của nó. Dấu kéo theo không phải là thêm một liên từ. Nó là một khẳng định về các công thức ở hai bên, và khẳng định ấy hoặc đúng hoặc sai.

Định nghĩa của tính hợp lệ chỉ thẳng tới một cách kiểm tra: duyệt mọi phép gán đúng và sai cho các biến, xem có phép gán nào làm mọi tiền đề đúng và kết luận sai không. Đó chính là việc của bảng chân trị, và với hai hay ba biến thì hoàn toàn ổn. Rắc rối là bảng lớn lên theo 2ⁿ. Mười biến cần một nghìn dòng, hai mươi biến cần một triệu, và bảng chẳng nói gì về việc dòng nào mới quan trọng.

Bảng ngữ nghĩa tiếp cận cùng câu hỏi ấy từ đầu kia. Thay vì liệt kê mọi khả năng rồi tìm một khả năng xấu, nó giả định có một khả năng xấu và cố dựng nó lên. Nếu nỗ lực ấy sụp đổ trong mâu thuẫn trên mọi lối nó có thể đi, thì không tồn tại phép gán như vậy và lập luận là hợp lệ. Nếu nỗ lực thành công, thứ nó dựng được chính là một phản ví dụ bạn đọc ra trực tiếp.

3. Phương pháp bảng ngữ nghĩa

Một bảng ngữ nghĩa là một cây gồm các công thức có dấu. Mỗi dòng là một công thức với chữ T hoặc F đứng trước, và dấu ấy nói nhánh đang giả định gì về công thức đó - không phải giá trị chân lý của nó, mà giá trị cần có để lập luận sụp đổ. Toàn bộ phương pháp gồm bốn bước:

1. Viết mỗi tiền đề với chữ T. Bạn đang giả định mọi tiền đề của lập luận đều đúng.
2. Viết kết luận với chữ F. Bạn đang giả định nó vẫn sai - đây là giả định bạn muốn bác bỏ.
3. Lấy bất kỳ dòng nào chưa phải nguyên tử và áp dụng quy tắc cho liên từ chính cùng dấu của nó, thêm những gì quy tắc sinh ra vào cuối mọi nhánh đi qua dòng ấy.
4. Đóng một nhánh ngay khi nó mang cả T A lẫn F A cho cùng một công thức A. Dừng lại khi mọi nhánh đã đóng, hoặc không còn dòng nào để phân rã.

Không có gì trong vòng lặp ấy đòi hỏi mưu mẹo hay một lựa chọn chiến lược. Mỗi dòng có đúng một quy tắc, và áp dụng chúng theo thứ tự nào cũng cho cùng một phán quyết - vì thế máy làm được, và vì thế bạn có thể tin kết quả khi máy làm.

4. Các quy tắc

Có một quy tắc cho mỗi liên từ dưới mỗi dấu - mười quy tắc cả thảy. Chúng chia làm hai loại, và khác biệt giữa hai loại chính là toàn bộ lý do khiến bảng ngữ nghĩa là một cây chứ không phải một danh sách. Quy tắc α nói rằng nhiều điều phải cùng đúng, nên nó xếp chồng kết quả xuống dọc nhánh. Quy tắc β nói rằng một trong hai điều phải đúng, nên nó tách nhánh làm đôi và để mỗi trường hợp đi đường riêng.

Mỗi quy tắc chẳng qua là điều kiện chân lý của liên từ ấy, đọc ngược lại. Một phép hội chỉ đúng khi cả hai vế đều đúng, nên T (A ∧ B) xếp chồng T A và T B. Một phép hội sai khi ít nhất một vế sai, nhưng công thức không nói vế nào, nên F (A ∧ B) buộc phải thử cả hai: nó tách nhánh. Cùng sự bất đối xứng ấy chạy theo chiều ngược lại với phép tuyển, và một mệnh đề kéo theo sai nghĩa là tiền từ đúng còn hậu từ sai - trường hợp duy nhất một phép kéo theo đổ vỡ.

Hãy để ý điều các quy tắc không bao giờ làm: chúng không bao giờ bịa ra công thức. Mọi thứ một quy tắc sinh ra đều là một mảnh của dòng nó xuất phát. Tính chất ấy - tính chất công thức con - là điều làm cho phương pháp là hữu hạn, và chúng ta sẽ trở lại với nó bên dưới.

5. Đóng một nhánh

Một nhánh là một mạch lập luận duy nhất: đọc từ gốc xuống một lá và bạn có một tập giả định trọn vẹn. Một nhánh đóng lại khi các giả định ấy mâu thuẫn thẳng thừng với nhau, tức là khi nó mang cả T A lẫn F A cho cùng một công thức. Không quan trọng A phức tạp đến đâu hay hai dòng cách nhau bao xa - nếu một nhánh đòi một công thức vừa đúng vừa sai, chẳng có gì thỏa mãn được nó.

Đánh dấu nhánh đã đóng bằng ×, ghi rõ hai dòng đã đóng nó, rồi thôi không làm việc với nhánh ấy nữa. Không còn gì để học từ một giả định vốn đã bất khả.

Khi mọi nhánh đều đóng, bảng đã đóng, và đó chính là chứng minh. Nó cho thấy giả định bạn khởi đầu - mọi tiền đề đúng, kết luận sai - dẫn tới mâu thuẫn trên mọi lối nó có thể đi. Vì không còn lối nào, không tồn tại phép gán như vậy, và lập luận là hợp lệ. Đây là chứng minh phản chứng, bày ra sao cho không bỏ sót trường hợp nào.

6. Một chứng minh, từng dòng một

Lấy modus tollens: p → q, ¬q ⊨ ¬p. Dòng 1 và 2 là các tiền đề, giả định đúng. Dòng 3 là kết luận, giả định sai - và vì kết luận là ¬p, giả định nó sai chính là giả định p đúng, điều mà dòng 5 ghi lại. Dòng 4 đến từ quy tắc phủ định áp dụng cho dòng 2: nếu ¬q đúng thì q sai. Mệnh đề kéo theo ở dòng 1 là dòng duy nhất còn liên từ, và đó là quy tắc β, nên cây tách đôi:

Nhánh trái giả định mệnh đề kéo theo đúng vì tiền từ của nó sai - nhưng dòng 5 đã có p đúng, nên nhánh tự mâu thuẫn và đóng lại. Nhánh phải giả định nó đúng vì hậu từ của nó đúng - nhưng dòng 4 đã có q sai, nên nhánh này cũng đóng.

Cả hai nhánh đều đóng, vậy không có cách nào để p → q và ¬q cùng đúng trong khi ¬p sai. Lập luận là hợp lệ, và cái cây chính là lý do. Hãy để ý rằng chứng minh không hề nhắc tới mưa, tới đất, hay tới việc p và q đại diện cho điều gì. Nó không cần.

7. Khi một nhánh vẫn mở

Không phải lập luận nào cũng hợp lệ, và đây là chỗ phương pháp chứng tỏ giá trị. Nếu bạn xử lý một nhánh cho tới khi không còn gì trên đó phân rã được nữa - chỉ còn các nguyên tử và nguyên tử bị phủ định - mà nó vẫn chưa đóng, thì nhánh ấy đã bão hòa và đang mở. Nó không đóng, và không phải vì bạn dừng quá sớm: đơn giản là chẳng còn gì để thử.

Một nhánh mở còn hơn cả phán quyết «không hợp lệ». Đọc dấu trên các nguyên tử của nó và bạn có một phép gán: mọi nguyên tử mang T là đúng, mọi nguyên tử mang F là sai. Phép gán ấy làm mọi tiền đề đúng và kết luận sai, tức đúng là một phản ví dụ. Các nhà logic gọi nó là phản mô hình, và đó là câu trả lời cụ thể cho câu hỏi «vì sao không?» chứ không phải một lời từ chối.

Khẳng định hậu từ, p → q, q ⊨ p, là trường hợp kinh điển. Bảng của nó để lại một nhánh mở với p sai và q đúng - tình huống mà mệnh đề kéo theo vẫn đúng, hậu từ vẫn đúng, thế mà tiền từ thì không. Chỉ một phép gán ấy đã đủ bác bỏ lập luận.

8. Vì sao nó luôn kết thúc

Mỗi quy tắc thay một công thức bằng chính các công thức con của nó, và mọi công thức con đều ngắn hơn hẳn công thức sinh ra nó. Vậy nên không nhánh nào có thể lớn lên mãi: mỗi bước đi xuống một cái thang hữu hạn gồm các mảnh của lập luận ban đầu, và cái thang ấy có đáy. Sớm muộn gì mọi dòng trên một nhánh cũng là một nguyên tử hoặc phủ định của một nguyên tử, và không còn gì để làm.

Đó là một bảo đảm thực sự, không phải một hy vọng. Nó có nghĩa phương pháp này là một thủ tục quyết định cho logic mệnh đề: chạy nó trên bất kỳ lập luận nào, nó sẽ dừng, với một cây đã đóng hoặc một nhánh còn mở, và không bao giờ nhún vai. Bộ chứng minh của trang này còn áp thêm một hạn mức số nút, nhưng chỉ để đề phòng một công thức bệnh lý làm kiệt một thẻ trình duyệt - bản thân toán học không cần giới hạn nào như vậy.

9. Những hệ chứng minh khác

Bảng ngữ nghĩa là một trong nhiều hệ chứng minh, và là hệ mang hình thức bác bỏ: nó làm việc bằng cách loại trừ khả năng thất bại. Suy diễn tự nhiên đi theo chiều ngược lại, dựng kết luận tiến về phía trước từ các tiền đề, với những quy tắc như modus ponens và chứng minh có điều kiện, và đọc lên giống cách một nhà toán học lập luận bằng văn xuôi hơn nhiều. Một chứng minh theo suy diễn tự nhiên thường ngắn hơn; tìm ra nó thường đòi hỏi nhiều sáng tạo hơn.

Phép tính tuần tự hình thức hóa chính dấu kéo theo và xử lý các khẳng định kéo theo như những đối tượng, khiến nó thành công cụ ưu tiên khi cần chứng minh điều gì đó về các chứng minh. Phép phân giải quy mọi thứ về các mệnh đề tuyển và một quy tắc duy nhất, đọc lên thì khô khan mà chạy thì cực nhanh - phần lớn các bộ chứng minh tự động và bộ giải SAT đều dựng trên nền ấy.

Tất cả đều nhất trí về việc lập luận mệnh đề nào là hợp lệ; chúng khác nhau ở dáng vẻ của một chứng minh và ở chỗ cái gì dễ tìm. Bảng ngữ nghĩa thân thiện nhất với người học, vì một chứng minh thất bại ở đây không phải ngõ cụt - nó trao cho bạn phản ví dụ.

10. Luyện tập

Cách nhanh nhất để học phương pháp là chạy nó. Gõ một lập luận vào máy tính với ⊨, ⊢ hoặc |= và bảng sẽ được vẽ bên cạnh bảng chân trị, để bạn đối chiếu cây với các dòng. Sau đó hãy làm vài chứng minh trên giấy trước khi xem đáp án.