Intensions, Church's Thesis, and the formalization of mathematics (Q1109758)

The main argument of this essay is that the constructive or algorithmic aspect of mathematics cannot be formalized without intensional notions in such an extensional language as ZFC, which is a paradigm case of the sort of theory Quine approves of, for the point of discussing a particular algorithm is usually that it solves some problems that interest us and a problem cannot be formulated in purely extensional terms because it only exists as a problem in a certain epistemic situation. The author discusses in detail on the characteristics of set-theoretical reductionism in mathematics and on the essential gap between informal talk of mathematical algorithm and more formal talk about machine program. It then is remarked that Church's Thesis is not a reductionistic thesis such as grounding the replacement of the informal mathematical notion of algorithm with the formal set-theoretic notion of Turing machine program. The author concludes in such a sense that not all known mathematics can be formulated in ZFC.