Số học bị chặn (Bounded Arithmetic) là một lĩnh vực nghiên cứu thú vị trong lý thuyết số học, tập trung vào các hệ thống con yếu hơn của số học Peano. Bài viết này sẽ cung cấp một cái nhìn tổng quan về số học bị chặn, khám phá các lý thuyết chính, ứng dụng của chúng trong việc đặc trưng hóa các lớp độ phức tạp tính toán, và mối liên hệ với các hệ thống chứng minh mệnh đề. Nếu bạn quan tâm đến sự giao thoa giữa logic toán học và khoa học máy tính, bài viết này sẽ là một nguồn tài liệu hữu ích.
Số học bị chặn là một họ các lý thuyết con yếu hơn của số học Peano. Các lý thuyết này thường được xây dựng bằng cách giới hạn các lượng tử trong tiên đề quy nạp hoặc các tiên đề tương đương. Một lượng tử bị chặn có dạng ∀x ≤ t hoặc ∃x ≤ t, trong đó t là một biểu thức không chứa x. Mục đích chính của việc nghiên cứu số học bị chặn là để đặc trưng hóa các lớp độ phức tạp tính toán khác nhau. Cụ thể, một hàm là toàn phần chứng minh được nếu và chỉ khi nó thuộc về một lớp độ phức tạp đã cho.
Ngoài ra, các lý thuyết về số học bị chặn còn cung cấp các đối tác đồng nhất cho các hệ thống chứng minh mệnh đề tiêu chuẩn, chẳng hạn như hệ thống Frege. Điều này đặc biệt hữu ích trong việc xây dựng các chứng minh kích thước đa thức trong các hệ thống này. Việc đặc trưng hóa các lớp độ phức tạp tiêu chuẩn và sự tương ứng với các hệ thống chứng minh mệnh đề cho phép chúng ta diễn giải các lý thuyết về số học bị chặn như các hệ thống hình thức nắm bắt các mức độ khác nhau của suy luận khả thi.
Stephen Cook giới thiệu lý thuyết phương trình PV (viết tắt của Polynomially Verifiable - Có thể kiểm chứng trong thời gian đa thức), hình thức hóa các chứng minh mang tính xây dựng khả thi (hay suy luận trong thời gian đa thức). Ngôn ngữ của PV bao gồm các ký hiệu hàm cho tất cả các thuật toán thời gian đa thức, được giới thiệu một cách quy nạp bằng cách sử dụng đặc tính của Cobham về các hàm thời gian đa thức. Các tiên đề và suy diễn của lý thuyết được giới thiệu đồng thời với các ký hiệu từ ngôn ngữ. Lý thuyết này là phương trình, nghĩa là các mệnh đề của nó chỉ khẳng định rằng hai biểu thức bằng nhau.
Một mở rộng phổ biến của PV là lý thuyết PV1, một lý thuyết bậc nhất thông thường. Các tiên đề của PV1 là các câu phổ quát và chứa tất cả các phương trình có thể chứng minh được trong PV. Ngoài ra, PV1 chứa các tiên đề thay thế các tiên đề quy nạp cho các công thức mở.
Samuel Buss giới thiệu các lý thuyết bậc nhất về số học bị chặn S2i. S2i là các lý thuyết bậc nhất với đẳng thức trong ngôn ngữ L = {0, S, +, ⋅, #, |x|, ⌊x/2⌋}, trong đó hàm |x| dùng để chỉ ⌈log(x+1)⌉ (số chữ số trong biểu diễn nhị phân của x) và x#y là 2|x|⋅|y|. Lưu ý rằng |x#x| ∼ |x|2, nghĩa là # cho phép biểu diễn các giới hạn đa thức theo độ dài bit của đầu vào.
Các lượng tử bị chặn là các biểu thức có dạng ∃x ≤ t ... := ∃x(x ≤ t ∧ …) và ∀x ≤ t ... := ∀x(x ≤ t → …), trong đó t là một biểu thức không có sự xuất hiện của x. Một lượng tử bị chặn hẹp nếu t có dạng |s| cho một biểu thức s. Một công thức ϕ bị chặn hẹp nếu tất cả các lượng tử trong công thức là bị chặn hẹp. Hệ thống phân cấp các công thức Σib và Πib được định nghĩa một cách quy nạp:
Các công thức bị chặn nắm bắt hệ thống phân cấp thời gian đa thức: với bất kỳ i ≥ 1, lớp ΣiP trùng với tập hợp các số tự nhiên có thể định nghĩa được bằng Σib trong ℕ (mô hình số học tiêu chuẩn) và tương tự Πib = ΠiP(ℕ). Đặc biệt, NP = Σ1b(ℕ).
Lý thuyết S2i bao gồm một danh sách hữu hạn các tiên đề mở được ký hiệu là BASIC và lược đồ quy nạp đa thức ϕ(0) ∧ ∀x ≤ a (ϕ(⌊x/2⌋) → ϕ(x)) → ϕ(a) trong đó ϕ ∈ Σib.
Buss (1986) chứng minh rằng các định lý Σ1b của S21 được chứng kiến bởi các hàm thời gian đa thức.
Định lý (Buss 1986): Giả sử S21 ⊢ ∀x∃yϕ(x, y), với ϕ ∈ Σ1b. Khi đó, tồn tại một ký hiệu hàm PV sao cho PV ⊢ ∀xϕ(x, f(x)). Hơn nữa, S21 có thể Σ1b-định nghĩa tất cả các hàm thời gian đa thức. Nghĩa là, các hàm Σ1b-có thể định nghĩa trong S21 chính xác là các hàm có thể tính toán được trong thời gian đa thức. Đặc tính này có thể được tổng quát hóa cho các cấp độ cao hơn của hệ thống phân cấp đa thức.
Các lý thuyết về số học bị chặn thường được nghiên cứu liên quan đến các hệ thống chứng minh mệnh đề. Tương tự như cách máy Turing là các đối tượng đồng nhất của các mô hình tính toán không đồng nhất như mạch Boolean, các lý thuyết về số học bị chặn có thể được coi là các đối tượng đồng nhất của các hệ thống chứng minh mệnh đề. Mối liên hệ này đặc biệt hữu ích cho việc xây dựng các chứng minh mệnh đề ngắn. Thông thường, việc chứng minh một định lý trong một lý thuyết về số học bị chặn và dịch chứng minh bậc nhất thành một chuỗi các chứng minh ngắn trong một hệ thống chứng minh mệnh đề dễ dàng hơn là thiết kế các chứng minh mệnh đề ngắn trực tiếp trong hệ thống chứng minh mệnh đề.
Sự tương ứng này được giới thiệu bởi S. Cook. Về mặt không chính thức, một mệnh đề Π1b ∀xΦ(x) có thể được biểu diễn tương đương như một chuỗi các công thức Φn(x) := ∀x(|x|=n → Φ(x)). Vì Φn(x) là một vị từ coNP, mỗi Φn(x) có thể được diễn đạt như một tautology mệnh đề ||ϕ||n (có thể chứa các biến mới cần thiết để mã hóa tính toán của vị từ Φn).
Định lý (Cook 1975): Giả sử S21 ⊢ ∀xΦ(x), trong đó Φ ∈ Π1b. Khi đó, các tautology ||ϕ||n có các chứng minh kích thước đa thức Extended Frege. Hơn nữa, các chứng minh này có thể xây dựng được bằng một hàm thời gian đa thức và PV chứng minh được sự thật này.
Hơn nữa, S21 chứng minh cái gọi là nguyên tắc phản xạ cho hệ thống Extended Frege, điều này ngụ ý rằng hệ thống Extended Frege là hệ thống chứng minh yếu nhất với thuộc tính từ định lý trên: mỗi hệ thống chứng minh thỏa mãn phép kéo theo mô phỏng Extended Frege.
Một bản dịch thay thế giữa các mệnh đề bậc hai và các công thức mệnh đề do Jeff Paris và Alex Wilkie (1985) đưa ra đã thiết thực hơn cho việc nắm bắt các hệ thống con của Extended Frege như Frege hoặc Frege độ sâu không đổi.
Bài viết liên quan