Re: Name the thesis: "Formal sentences capture informal ones"

From: Mitch Harris (harrisq_at_tcs.inf.tu-dresden.de)
Date: 01/31/05 

Date: Mon, 31 Jan 2005 11:02:07 +0100

tchow@lsa.umich.edu wrote:
> The Church-Turing thesis is familiar to many people, largely because it
> has been widely discussed both in textbooks and in popular science writing.
> Having a name helps, too.
>
> There is an analogous thesis that is relevant to logic and the foundations
> of mathematics:
>
> (*) Formal sentences (in PA or ZFC for example) adequately express
> their informal counterparts.
>
> Years of discussion, on USENET and elsewhere, has convinced me that the
> average level of understanding of foundational issues would be enormously
> improved if (*) were, like the Church-Turing thesis, given a name and
> widely discussed.
>
> As matters stand today, a lot of people don't seem to even acknowledge the
> existence of informal mathematical discourse, despite the fact that all but
> a tiny fraction of mathematical discourse they've ever seen is informal (in
> the sense of (*)).

(given that "people" really refers to mathematicians) I'd expect that
most would not be terribly put out if confronted with the distinction
(i.e. that the work they do is not formal).

> Any candidates for a catchy name for (*)?

Whether the concept is well-defined or not, we can still give the
thing we want to talk about a name.

"Hilbert's thesis" seems to have been taken by a related but much more
specific concept

   "the informal concept of proof is adequately modeled by the
    first-order model of proof"

   http://www.cs.nyu.edu/pipermail/fom/1997-October/000127.html

how about the "formalization thesis/principle/program"? 

-- 
Mitch Harris
(remove q to reply)