Toán học kiến thiết

Trong triết học toán học, toán học kiến thiết hay chủ nghĩa kiến thiết là tư tưởng cho rằng cần thiết phải tìm ra (hoặc xây dựng) một vật thể toán học để khẳng định là nó tồn tại. Trong toán học cổ điển, ta có thể chứng minh sự tồn tại của một vật thể toán học bằng phép phản chứng. Chứng mình bằng phản chứng không có tính kiến thiết.

Toán học kiến thiết có nhiều trường phái.^[1] Ta có thể kể tên trường phái trực giác (intuitionism) sáng lập bởi Luitzen Egbertus Jan Brouwer, trường phái hữu hạn (finitism) sáng lập bởi David Hilbert và Paul Bernays, toán học đệ quy kiến thiết sáng lập bởi Nikolai Aleksandrovich Shanin và Andrei Markov, giải tích kiến thiết bởi Errett Bishop. Toán học kiến thiết cũng bao gồm cả lý thuyết tập hợp kiến thiết (như là CZF) và lý thuyết topos.

Nhiều hệ thống toán học kiến thiến sử dụng logic trực giác, tức là logic cổ điển bỏ đi luật loại trừ trung gian (phát biểu rằng một khẳng định hoặc là đúng hoặc là sai - bỏ theo nghĩa người ta không sử dụng nó như là một tiên đề; trong nhiều trường hợp, nó vẫn được nghiệm đúng). Luật phi mâu thuẫn (phát biểu rằng một khẳng định không thể vừa đúng vừa sai) vẫn được giữ.

Ví dụ, trong số học Heyting, ta có thể chứng minh rằng với mọi mệnh đề p không chứa lượng từ logic, ${\displaystyle \forall x,y,z,\ldots \in \mathbb {N} :p\vee \neg p}$ là một khẳng định đúng (với x, y, z... là các biến tự do của mệnh đề p).

Brouwer cho rằng luật loại trừ trung gian là một sự trừu tượng hóa từ các kinh nghiệm hữu hạn, và được áp dụng cho trường hợp vô hạn mà không có căn cứ. Ví dụ, giả thuyết Goldbach phát biểu rằng mọi số chẵn lớn hơn hai là tổng của hai số nguyên tố. Hiện nay vẫn chưa có lời giải nào cho giả thuyết Goldbach. Theo Brouwer, ta không có căn cứ để khẳng định rằng "hoặc là giả thuyết Goldbach sai, hoặc là nó đúng", dù rằng có thể một ngày nào đó người ta sẽ giải được giả thuyết này. Brouwer nghĩ rằng luật loại trừ trung gian tương đương với việc cho rằng bài toán nào cũng có lời giải.

• Leopold Kronecker (chủ nghĩa kiến thiết cũ, nửa trực giác)
• L. E. J. Brouwer (sáng lập trường phái trực giác)
• A. A. Markov (cây đại thụ của toán học kiến thiết Nga)
• Arend Heyting (hình thức hóa logic trực giác và lý thuyết trực giác)
• Per Martin-Löf (sáng lập lý thuyết hình thái kiến thiết)
• Errett Bishop (đưa ra một phiên bản toán học kiến thiết nhất quán với toán học cổ điển)
• Paul Lorenzen (phát triển giải tích kiến thiết)
• Phan Đình Diệu (nghiên cứu giải tích hàm kiến thiết)

• Logic kiến thiết
• Lý thuyết hình thái kiến thiết
• Giải tích kiến thiết
• Giải tích không chuẩn mực kiến thiết

• Anne Sjerp Troelstra, Dirk van Dalen, "Constructivism in Mathematics: An Introduction, Volume 1", 1988
• Anne Sjerp Troelstra, Dirk van Dalen, "Constructivism in Mathematics: An Introduction, Volume 2", 1988
• A. S. Troelstra (1977a), "Aspects of constructive mathematics", Handbook of Mathematical Logic, pp. 973–1052.
• A. S. Troelstra (1977b), Choice sequences, Oxford Logic Guides. ISBN 0-19-853163-X
• A. S. Troelstra (1991), "A History of Constructivism in the 20th Century", University of Amsterdam, ITLI Prepublication Series ML-91-05, https://web.archive.org/web/20060209210015/http://staff.science.uva.nl/~anne/hhhist.pdf,
• Douglas Bridges, Fred Richman, "Varieties of Constructive Mathematics", 1987.
• H. M. Edwards (2005), Essays in Constructive Mathematics, Springer-Verlag, 2005, ISBN 0-387-21978-1
• Michael J. Beeson, "Foundations of constructive mathematics: metamathematical studies", 1985.
• Phan Đình Diệu. Some questions in constructive functional analysis. Proceedings of the Steklov Institute of Mathematics, No. 114 (1970). Translated from the Russian by J. M. Danskin. American Mathematical Society, Providence, R.I., 1974. iv+228 pp.
• Solomon Feferman (1997), Relationships between Constructive, Predicative and Classical Systems of Analysis, http://math.stanford.edu/~feferman/papers/relationships.pdf.

• Constructive mathematics tại Bách khoa toàn thư Stanford về Triết học