Hệ thống Hình thức như một Đồ thị Có hướng
Một hệ thống tiên đề hình thức định nghĩa một đồ thị có hướng:
- Đỉnh: tất cả các công thức hợp lệ có thể xây dựng từ các ký hiệu của hệ thống
- Cạnh: các bước suy luận — một công thức tuân theo các công thức khác theo quy tắc suy luận
- Tiên đề: các đỉnh nguồn được phân biệt không có cạnh vào
- Định lý: tất cả các đỉnh có thể tiếp cận từ tập tiên đề
Một chứng minh của định lý T: một đường đi có hướng từ tập tiên đề đến T. Chứng minh là một dãy các đỉnh A₁, A₂, ..., Aₙ = T trong đó mỗi bước tuân theo quy tắc suy luận.
Hai tính chất cơ bản của một hệ thống hình thức, được biểu thị hình học:
Tính nhất quán: không có công thức F nào và phủ định ¬F của nó đều có thể tiếp cận từ các tiên đề. Hình học: đỉnh định lý F và đỉnh định lý ¬F không cùng có thể tiếp cận. Không tồn tại đường dẫn 'bùng nổ'.
Tính đầy đủ: mọi công thức F hoặc ¬F đều là một định lý (có thể tiếp cận). Hình học: đồ thị được kết nối mạnh theo nghĩa rằng đối với mỗi đỉnh F, ít nhất một trong F hoặc ¬F có một đường đi từ các tiên đề.
Tính Không đầy đủ Gödel như một Tính chất Hình học
Kurt Gödel đã chứng minh vào năm 1931 rằng bất kỳ hệ thống hình thức nhất quán nào đủ mạnh để biểu thị số học cơ bản là không đầy đủ: tồn tại các công thức G sao cho không có G hay ¬G nào có thể chứng minh được.
Hình học: trong bất kỳ hệ thống hình thức nhất quán đủ phong phú nào, có những đỉnh trong đồ thị công thức không thể tiếp cận từ các tiên đề — cả đỉnh G lẫn đỉnh ¬G đều không có đường dẫn từ tập tiên đề.
Xây dựng của Gödel: ông đã mã hóa một công thức G nói rằng, thực tế là, 'Tôi không thể chứng minh được.' Nếu G có thể chứng minh được, hệ thống sẽ không nhất quán (một tuyên bố đúng nói rằng nó không thể chứng minh được). Nếu ¬G có thể chứng minh được, hệ thống sẽ không nhất quán (G sẽ sai nhưng hệ thống chứng minh nó). Vì vậy, cả G lẫn ¬G đều không thể chứng minh được — G là một đỉnh không thể tiếp cận trong một hệ thống nhất quán.
Tính không đầy đủ không phải là một khiếm khuyết của các tiên đề đã chọn: Gödel đã chỉ ra rằng đó là một tính chất cấu trúc của bất kỳ hệ thống nhất quán nào đủ biểu đạt để xử lý số học. Các đỉnh không thể tiếp cận không thể được loại bỏ bằng cách thêm nhiều tiên đề mà không tạo ra những đỉnh mới.
Các Đối tượng Toán học là các Điểm trong một Không gian
Quan điểm Platonic về toán học có thể được chính thức hóa hình học: các đối tượng toán học cư trú trong một không gian trừu tượng có các điểm là các đối tượng chính nó và cấu trúc của nó được cho bởi các mối quan hệ giữa chúng.
Xem xét các số tự nhiên ℕ = {0, 1, 2, 3, ...}. Mối quan hệ chia hết định nghĩa một bộ thứ tự riêng phần: m chia hết n nếu m | n. Bộ thứ tự riêng phần này định nghĩa một hình học — sơ đồ Hasse của mạng chia hết.
Mọi số nguyên tố ngồi ở một vị trí tối thiểu phía trên 1. Mọi số hợp ngồi phía trên các thừa số nguyên tố của nó. Cấu trúc của không gian này mã hóa toàn bộ lý thuyết số.
Cái làm cho nó Platonic: cấu trúc tồn tại cho dù có hay không bất kỳ tâm trí nào nghiên cứu nó. Thực tế là 7 là số nguyên tố — mà 7 không có ước số nào giữa 1 và 7 — là một thực tế về vị trí của 7 trong mạng chia hết, độc lập với ký hiệu, văn hóa, hoặc nền văn minh.
Bất kỳ nền văn minh nào điều tra phép đếm và tính chia hết sẽ khám phá cấu trúc tương tự. Hình học của hệ thống số là phổ quát.
Điều hướng Mạng Chia hết
Trong mạng chia hết, bội số chung nhỏ nhất (lcm) của hai số tương ứng với nối (cận trên thấp nhất) của chúng và ước số chung lớn nhất (gcd) tương ứng với gặp (cận dưới lớn nhất) của chúng.
Gcd có thể được tính toán thông qua thuật toán Euclidean: gcd(a, b) = gcd(b, a mod b), kết thúc khi b = 0.
Trừu tượng hóa Bỏ đi Điều gì
Trừu tượng hóa hình học: chiếu một đối tượng nhiều chiều lên một không gian con có chiều thấp hơn. Phép chiếu làm mất thông tin (các tọa độ không trong không gian con) nhưng giữ nguyên cấu trúc không gian con một cách hoàn hảo.
Trừu tượng hóa toán học hoạt động theo cách tương tự. Một nhóm là một tập hợp với một phép toán nhị phân thỏa mãn bốn tiên đề. Trừu tượng hóa thành cấu trúc nhóm bỏ đi: các phần tử cụ thể, quy tắc tính toán của phép toán cụ thể, bất kỳ cấu trúc bổ sung nào (thứ tự, số liệu, tô pô). Cái còn lại: bộ khung tiên đề bốn.
Phần thưởng: mọi định lý về nhóm áp dụng cho TẤT CẢ các nhóm — số nguyên dưới phép cộng, các phép quay dưới phép hợp, các hoán vị dưới phép hợp, các đối xứng của một phân tử, các nhóm Galois của phương trình đa thức — đồng thời. Định lý trừu tượng có thể chứng minh được một lần; các thể hiện của nó là miễn phí.
Đây là lý do tại sao các nhà toán học thuần túy chống lại việc thêm các giả định dành riêng cho miền: mỗi giả định được thêm vào làm hạn chế tính khả năng áp dụng của định lý. Một định lý về trường (thêm nghịch đảo nhân) áp dụng cho ít cấu trúc hơn một định lý cụ thể về vành (không có nghịch đảo nhân bắt buộc).
Sự Đánh đổi giữa Độ chính xác & Tính chung chung
Có một sự đánh đổi: các định lý trừu tượng hơn áp dụng rộng hơn nhưng nói ít hơn về các thể hiện cụ thể. Một định lý về không gian vector nói ít hơn về ℝ^n so với một định lý cụ thể về ℝ^n (trong đó khoảng cách và góc được định nghĩa).
Quy tắc ngụ ý của Hamming: trừu tượng hóa càng xa càng tốt trong khi vẫn giữ lại các tính chất bạn cần. Trừu tượng hóa quá xa và các định lý của bạn trở nên tầm thường chung (ít nhất một tập hợp có bất kỳ phép toán nào thỏa mãn...). Trừu tượng hóa quá ít và các định lý của bạn không chuyển sang các ứng dụng mới.