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.