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

1. 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".