[FOM] Formalization Thesis

[Vaughan Pratt]

Timothy Y. Chow wrote:
> Catarina Dutilh wrote:
>> So, unless one can make sense of the idea of 'expressing faithfully' in a 
>> precise way, the Formalization Thesis thus stated does not seem to be 
>> sufficiently precise.
> 
> Well, can you tweak it to *make* it "sufficiently precise"?

With what is currently known about foundations, I doubt it.  Foundations 
today seems to be where quantum mechanics was in the 1910's---vague 
shapes are coming into focus, but there is still no precisely stated 
uncertainty principle permitting a continuous allocation of uncertainty 
to conjugate pairs, which in the case of foundations I would take to be 
theories and classes.

The 1920's saw the formulation of Heisenberg's uncertainty principle, 
that the product of the uncertainties, suitably measured, in such 
conjugate pairs as position and momentum, time and energy, or any two 
orthogonal angular momenta, was bounded below by a universal constant.

Is there any equally symmetric uncertainty principle for theories and 
classes?  Certainly there is a large and growing body of theorems 
indicative of some kind of interference between the two.  But without a 
unifying central theorem from which this body can be seen as simply a 
sampling of its consequences, foundations cannot be said to have as firm 
a handle on the interference of theories and classes as physics does for 
its various conjugate pairs of variables.

For me, Catarina's question is not just a good question, it is *the* 
question the Formalization Thesis needs to answer.

Tim's three examples (CH, 2nd incompleteness, formalizations of 
intuition encountered in specific machine-checkable proofs) purporting 
to illustrate "faithful expression" seemed only to focus Catarina's 
question on particular cases, without however answering it at all.

> Does this clarify what I intend by "expressing faithfully"? 

No, but an assessment of the degree of faithfulness of each example 
might help, especially if the examples covered a representative range of 
degrees of faithfulness.

Vaughan Pratt