Lý thuyết chứng minh

Lý thuyết chứng minh là một nhánh chính ^[1] trong logic toán mà tại đó ta biểu diễn các chứng minh toán học như các đối tượng toán học chính thức, giúp tạo điều kiện thuận lợi cho việc phân tích các chứng minh bằng các phương pháp toán học. Chứng minh thường được trình bày dưới dạng cấu trúc dữ liệu như danh sách thuần túy, danh sách đóng hộp hoặc cây, được xây dựng theo các tiên đề và quy tắc suy luận của hệ thống logic. Do đó, lý thuyết chứng minh có bản chất cú pháp, trái ngược với lý thuyết mô hình có bản chất ngữ nghĩa.

Tham khảo

^ According to Wang (1981), pp. 3–4, proof theory is one of four domains mathematical logic, together with model theory, axiomatic set theory, and recursion theory. Barwise (1978) consists of four corresponding parts, with part D being about "Proof Theory and Constructive Mathematics".

Bài viết liên quan đến toán học này vẫn còn sơ khai. Bạn có thể giúp Wikipedia mở rộng nội dung để bài được hoàn chỉnh hơn.

x t s Logic toán
Chung	Ngôn ngữ hình thức Formation rule Hệ hình thức Hệ suy luận Chứng minh hình thức Ngữ nghĩa hình thức (logic) Well-formed formula Tập hợp Phần tử (toán học) Lớp (lý thuyết tập hợp) Classical logic Tiên đề Natural deduction Rule of inference Quan hệ (toán học) Định lý toán học Logical consequence Hệ tiên đề Lý thuyết hình thái Symbol (formal) Syntax (logic) Lý thuyết (logic toán)
Thuật ngữ logic	Mệnh đề toán học Suy luận Luận cứ logic Validity Cogency Tam đoạn luận Square of opposition Sơ đồ Venn
Propositional calculus Đại số Boole	Boolean functions Phép tính mệnh đề Công thức mệnh đề Logical connectives Truth tables
Logic vị từ	Logic bậc nhất Lượng từ (logic) Predicate (mathematical logic) Logic bậc hai Monadic predicate calculus
Naive set theory	Tập hợp Tập hợp rỗng Enumeration Extensionality Tập hợp hữu hạn Tập hợp vô hạn Tập hợp con Tập lũy thừa Tập hợp đếm được Tập hợp không đếm được Recursive set Tập xác định Range (mathematics) Ánh xạ Song ánh Đơn ánh Toàn ánh Hàm số Phép toán hai ngôi Cặp được sắp
Lý thuyết tập hợp	Nền tảng toán học Lý thuyết tập hợp Zermelo–Fraenkel Tiên đề chọn General set theory Lý thuyết tập hợp Kripke–Platek Lý thuyết tập hợp Von Neumann–Bernays–Gödel Lý thuyết tập hợp Morse–Kelley Lý thuyết tập hợp Tarski–Grothendieck Phép đẳng cấu
Lý thuyết mô hình	Cấu trúc (logic toán) Interpretation (logic) Non-standard model Lý thuyết mô hình hữu hạn Giá trị chân lý Validity
Lý thuyết chứng minh	Formal proof Deductive system Hệ hình thức Định lý toán học Hệ quả logic Rule of inference Syntax (logic)
Lý thuyết tính toán	Đệ quy Tập đệ quy Tập tuần tự đệ quy Bài toán quyết định Church–Turing thesis Hàm tính được Primitive recursive function