Triết học toán học
Trường phái tư tưởng đương đại > Chủ nghĩa hình thức

Chủ nghĩa hình thức cho rằng các phát biểu toán học có thể được coi là tuyên bố về hậu quả của các quy tắc thao tác chuỗi nhất định. Ví dụ, trong "trò chơi" hình học Euclide (được xem là bao gồm một số chuỗi gọi là "tiên đề" và một số "quy tắc suy luận" để tạo ra các chuỗi mới từ các chuỗi đã cho), người ta có thể chứng minh rằng định lý Pythagore giữ (nghĩa là, người ta có thể tạo ra chuỗi tương ứng với định lý Pythagore). Theo chủ nghĩa hình thức, các sự thật toán học không phải là về các con số và tập hợp và hình tam giác và giống như trên thực tế, chúng không "nói về" bất cứ điều gì cả.
Một phiên bản khác của chủ nghĩa hình thức thường được gọi là chủ nghĩa khấu trừ. Trong suy luận, định lý Pythagore không phải là một sự thật tuyệt đối, mà là một quan hệ tương đối: nếu người ta gán nghĩa cho các chuỗi theo cách các quy tắc của trò chơi trở thành đúng (nghĩa là các phát biểu đúng được gán cho các tiên đề và quy tắc suy luận là bảo tồn sự thật), sau đó người ta phải chấp nhận định lý, hay nói đúng hơn, cách giải thích người ta đã đưa ra nó phải là một tuyên bố đúng. Điều tương tự cũng được tổ chức là đúng với tất cả các báo cáo toán học khác. Do đó, chủ nghĩa hình thức không có nghĩa là toán học không là gì ngoài một trò chơi tượng trưng vô nghĩa. Người ta thường hy vọng rằng có tồn tại một số giải thích trong đó các quy tắc của trò chơi giữ. (So sánh vị trí này với chủ nghĩa cấu trúc.) Nhưng nó cho phép nhà toán học làm việc tiếp tục công việc của mình và để lại những vấn đề như vậy cho nhà triết học hoặc nhà khoa học. Nhiều nhà chính thức sẽ nói rằng trong thực tế, các hệ tiên đề được nghiên cứu sẽ được đề xuất bởi các yêu cầu của khoa học hoặc các lĩnh vực khác của toán học.
Một người đề xướng sớm của chủ nghĩa hình thức là David Hilbert, người có chương trình dự định là một tiên đề hoàn chỉnh và nhất quán của tất cả các toán học. Hilbert nhằm mục đích cho thấy tính nhất quán của các hệ thống toán học từ giả định rằng "số học tài chính" (một hệ thống con của số học thông thường của các số nguyên dương, được chọn là không gây tranh cãi về mặt triết học) là nhất quán. Các mục tiêu của Hilbert trong việc tạo ra một hệ thống toán học vừa hoàn chỉnh vừa nhất quán đã bị làm suy yếu nghiêm trọng bởi các định lý bất toàn thứ hai của Gôdel, trong đó tuyên bố rằng các hệ tiên đề nhất quán có thể biểu hiện đủ không bao giờ có thể chứng minh tính nhất quán của chúng. Vì bất kỳ hệ tiên đề nào như vậy sẽ chứa số học chính xác như là một hệ thống con, nên định lý của Gôdel ngụ ý rằng không thể chứng minh tính nhất quán của hệ thống với điều đó (vì khi đó nó sẽ chứng minh tính nhất quán của chính nó, điều mà Gôdel đã thể hiện là không thể). Do đó, để chứng minh rằng bất kỳ hệ thống tiên đề nào của toán học trên thực tế là nhất quán, trước tiên người ta cần phải thừa nhận tính nhất quán của một hệ thống toán học theo nghĩa mạnh hơn hệ thống được chứng minh là nhất quán.
Hilbert ban đầu là một người khấu trừ, nhưng, có thể rõ ràng từ trên, ông đã xem xét các phương pháp siêu hình nhất định để mang lại kết quả có ý nghĩa nội tại và là một người thực tế đối với số học tài chính. Sau đó, ông giữ quan điểm rằng không có toán học có ý nghĩa nào khác, bất kể giải thích.
Các nhà chính thức khác, như Rudolf Carnap, Alfred Tarski và Haskell Curry, coi toán học là cuộc kiểm tra các hệ tiên đề chính thức. Các nhà logic toán học nghiên cứu các hệ thống chính thức nhưng thường là những người theo chủ nghĩa hiện thực vì họ là những người theo chủ nghĩa hình thức.
Người theo chủ nghĩa hình thức tương đối khoan dung và mời gọi các phương pháp tiếp cận logic, hệ thống số không chuẩn, lý thuyết tập hợp mới, v.v. Chúng ta càng học nhiều trò chơi thì càng tốt. Tuy nhiên, trong cả ba ví dụ này, động lực được rút ra từ các mối quan tâm toán học hoặc triết học hiện có. Các "trò chơi" thường không tùy ý.
Phê bình chính của chủ nghĩa hình thức là các ý tưởng toán học thực tế chiếm lĩnh các nhà toán học đã bị loại bỏ khỏi các trò chơi thao tác chuỗi được đề cập ở trên. Do đó, chủ nghĩa hình thức im lặng trước câu hỏi hệ thống tiên đề nào nên được nghiên cứu, vì không có ý nghĩa nào hơn hệ thống khác theo quan điểm chính thức.
Gần đây, một số nhà toán học chính thống đã đề xuất rằng tất cả các kiến thức toán học chính thức của chúng ta nên được mã hóa một cách có hệ thống các định dạng có thể đọc được trên máy tính, để tạo điều kiện kiểm tra bằng chứng tự động các bằng chứng toán học và sử dụng định lý tương tác chứng minh sự phát triển của lý thuyết toán học và phần mềm máy tính. Do mối liên hệ chặt chẽ với khoa học máy tính, ý tưởng này cũng được các nhà trực giác toán học và các nhà xây dựng ủng hộ trong truyền thống "tính toán", xem dự án QED để biết tổng quan.