Suy diễn tự nhiên và Giải tích tuần tự

Suy diễn tự nhiên và giải tích tuần tự là hai hệ thống hình thức kiểu Gentzen đại diện cho các chứng minh thông qua các quy tắc giới thiệu và loại bỏ cho các phép nối logic, tạo thành bộ máy cơ bản của lý thuyết chứng minh cấu trúc.

Definition

Suy diễn tự nhiên suy ra các công thức từ các giả định bằng cách sử dụng các quy tắc giới thiệu và loại bỏ phản ánh lý luận không chính thức, trong khi giải tích tuần tự thao tác các tuần tự, các khẳng định rằng một danh sách các công thức kéo theo một công thức khác, thông qua các quy tắc tác động lên bên trái và bên phải của một phép kéo theo.

Scope

Chủ đề này bao gồm các quy tắc của suy diễn tự nhiên với các cặp giới thiệu và loại bỏ của chúng, cấu trúc của giải tích tuần tự với các quy tắc trái và phải cùng các quy tắc cấu trúc, chuẩn hóa cho suy diễn tự nhiên, mối quan hệ giữa hai hệ thống, và các biến thể trực giác và cổ điển của chúng.

Core questions

• Các quy tắc giới thiệu và loại bỏ mang lại ý nghĩa cho các phép nối logic như thế nào?
• Tuần tự là gì và các quy tắc của nó khác với các quy tắc của suy diễn tự nhiên như thế nào?
• Chuẩn hóa đơn giản hóa các chứng minh suy diễn tự nhiên như thế nào?
• Các phiên bản cổ điển và trực giác của các phép tính này có liên quan với nhau như thế nào?

Key theories

Các quy tắc giới thiệu và loại bỏ

Mỗi phép nối được điều chỉnh bởi các quy tắc giới thiệu nó và các quy tắc khai thác nó, và sự hài hòa của chúng, rằng việc loại bỏ phục hồi chính xác những gì giới thiệu đưa vào, thể hiện ý nghĩa của phép nối.

Định lý chuẩn hóa

Prawitz đã chỉ ra rằng các chứng minh suy diễn tự nhiên có thể được rút gọn về một dạng chuẩn không có đường vòng, nơi một phép giới thiệu ngay lập tức bị hủy bỏ bởi một phép loại bỏ, tương tự như loại bỏ cắt trong suy diễn tự nhiên.

Sự tương ứng của hai phép tính

Suy diễn tự nhiên và giải tích tuần tự chứng minh cùng một định lý và có thể được dịch sang nhau, với các quy tắc trái của tuần tự tương ứng với các quy tắc loại bỏ của suy diễn tự nhiên.

Clinical relevance

Các phép tính này là các định dạng tiêu chuẩn để nghiên cứu các chứng minh một cách cấu trúc: suy diễn tự nhiên làm nền tảng cho lý thuyết kiểu và các trợ lý chứng minh thông qua sự tương ứng chứng minh-như-chương trình, trong khi giải tích tuần tự, với tính chất công thức con của nó sau khi loại bỏ cắt, là cơ sở của tìm kiếm chứng minh tự động và bảng phân tích.

History

Gentzen đã giới thiệu cả suy diễn tự nhiên và giải tích tuần tự vào năm 1934 và 1935, phát triển giải tích tuần tự để đạt được định lý loại bỏ cắt của mình sau khi nhận thấy suy diễn tự nhiên khó phân tích hơn. Prawitz đã khôi phục suy diễn tự nhiên vào năm 1965 với một nghiên cứu chuẩn hóa kỹ lưỡng, và các hệ thống này trở thành trung tâm cho các phát triển chứng minh-như-chương trình sau này.

Key figures

• Gerhard Gentzen
• Dag Prawitz
• Stanislaw Jaskowski
• Jan von Plato

Seminal works

• troelstra2000
• prawitz1965
• negri2001

Frequently asked questions

Sự khác biệt giữa suy diễn tự nhiên và giải tích tuần tự là gì?

Suy diễn tự nhiên hoạt động với các công thức trong một ngữ cảnh giả định và sử dụng các quy tắc loại bỏ, gần giống với chứng minh không chính thức. Giải tích tuần tự hoạt động với các phép kéo theo rõ ràng và thay thế các quy tắc loại bỏ bằng các quy tắc giới thiệu trái, một định dạng làm cho việc loại bỏ cắt và tính chất công thức con trở nên minh bạch.

Tại sao chuẩn hóa lại quan trọng?

Một chứng minh chuẩn không chứa đường vòng và có tính chất công thức con, do đó mọi công thức trong đó đều là một công thức con của kết luận hoặc tiền đề. Điều này hạn chế hình dạng của các chứng minh, mang lại kết quả nhất quán, và, thông qua sự tương ứng chứng minh-như-chương trình, tương ứng với việc đánh giá một chương trình thành một giá trị.