非构造性证明是“表述存在性的命题或定理”的一种证明方式:证明的过程中,不举例而只证明语句是否正确。非构造性证明很多时候依赖于排中律。数学结构主义数学不允许非构造性证明。
非构造性证明是“表述存在性的命题或定理”的一种证明方式:证明的过程中,不举例而只证明语句是否正确。非构造性证明很多时候依赖于排中律。数学结构主义数学不允许非构造性证明。
佩尔·埃里克·罗格·马丁-洛夫,瑞典逻辑学家、统计学家和哲学家。他以其在概率论基础方面的工作而闻名。自20世纪70年代以后,他的工作主要集中在逻辑学方面。在哲学逻辑方面,他的研究专注于蕴涵及判断学说,并在一定程度上受到了弗朗兹·布伦塔诺、弗雷格和胡塞尔先前工作的影响;在数理逻辑方面,他致力于创设直觉类型论作为数学的数学结构主义数学基础。马丁-洛夫在类型论方面的工作深深地影响了计算机科学、尤其是后世编程语言理论的发展。