Intensions, Church's Thesis, and the formalization of mathematics
type: Item
instance of: scholarly article
title: Intensions, Church's Thesis, and the formalization of mathematics
zbMATH Open document ID: 0656.03004
author: Nicolas D. Goodman
published in: Notre Dame Journal of Formal Logic
publication date: 1987-01-01T00:00:00Z
review text: 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.
Mathematics Subject Classification ID: 03A05
Mathematics Subject Classification ID: 00A30
zbMATH DE Number: 4070856
zbMATH Keywords: intensionality
zbMATH Keywords: formalization
zbMATH Keywords: constructivity
zbMATH Keywords: Quine's doctrine
zbMATH Keywords: algorithm
zbMATH Keywords: set-theoretical reductionism in mathematics
zbMATH Keywords: Church's Thesis
zbMATH Keywords: Turing machine program
reviewed by: Osamu Sonobe
MaRDI profile type: Publication
full work available at URL: https://doi.org/10.1305/ndjfl/1093637644
OpenAlex ID: W1964525083
DOI: 10.1305/NDJFL/1093637644
description: scientific article; zbMATH DE number 4070856