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. |
|
---|
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 | |
---|
| - 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 | |
---|
Lý thuyết tập hợp | |
---|
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
|
---|