Máy tính Logic

Chứng minh mẫu

Mỗi trang chứng minh một lập luận bằng bảng ngữ nghĩa: giả định các tiền đề đúng và kết luận sai, rồi phân tích cho tới khi mọi nhánh tự mâu thuẫn hoặc còn lại một phép gán. Bảng ngữ nghĩa hoạt động thế nào →

Lập luận hợp lệ

Modus ponensp→q, p ⊨ qNếu p → q đúng và p đúng thì q theo sau. Modus ponens là quy tắc mà hầu hết mọi chứng minh đều dựa vào, và bảng dưới đây đóng mọi nhánh.
Modus tollensp→q, ¬q ⊨ ¬pNếu p → q đúng và q sai thì p cũng phải sai: điều gì làm p đúng thì cũng làm q đúng. Phủ định hệ quả là phủ định tiền đề.
Tam đoạn luận giả địnhp→q, q→r ⊨ p→rHai mệnh đề kéo theo chung một công thức ở giữa sẽ nối lại: từ p → q và q → r ta được p → r. Những bước ngắn dựng nên lập luận dài như thế.
Tam đoạn luận tuyểnp∨q, ¬p ⊨ qMột tuyển cần ít nhất một vế đúng, nên p ∨ q cùng với ¬p để lại q. Loại một vế thì vế kia đứng vững.
Song đề kiến thiếtp∨q, p→r, q→r ⊨ rDù p hay q đúng thì r vẫn theo sau — vậy r theo sau vô điều kiện. Một tuyển cộng với một kéo theo từ mỗi vế cho ra kết luận chung.
Phản đảop→q ⊨ ¬q→¬pp → q và ¬q → ¬p nói cùng một điều: không gì làm tiền đề đúng trong khi hệ quả sai. Một kéo theo tương đương với phản đảo của nó.
Định luật De Morgan¬(p∧q) ⊨ ¬p∨¬q¬(p ∧ q) không nói vế nào sai, chỉ nói cả hai không thể cùng đúng — đó chính là ¬p ∨ ¬q. Phủ định một hội sẽ trải phủ định ra.
Kéo theo vật chấtp→q ⊨ ¬p∨qp → q đúng đúng ở những dòng mà ¬p ∨ q đúng: hoặc tiền đề sai, hoặc hệ quả đúng. Kéo theo là một tuyển trá hình.
Phủ định kép¬¬p ⊨ p¬¬p và p đúng ở cùng những dòng, nên phủ định kép có thể bỏ đi ở bất cứ đâu. Hai phủ định triệt tiêu nhau.
Loại bỏ tương đươngp↔q, p ⊨ qHai vế của p ↔ q luôn mang cùng giá trị chân lý, nên p cho ta q — và q sẽ cho ta p. Tương đương hoạt động theo cả hai chiều.
Luật bài trung⊨ p∨¬pp ∨ ¬p đúng ở mọi dòng và không cần tiền đề nào cả: mọi mệnh đề đều đúng hoặc sai, không có khả năng thứ ba.
Nguyên lý bùng nổp, ¬p ⊨ qTừ p và ¬p suy ra bất cứ điều gì: không phép gán nào làm cả hai tiền đề đúng, nên cũng không phép gán nào làm chúng đúng mà kết luận sai.

Lập luận không hợp lệ