Re: Turing machines and tape length

HP: I still have a problem with the implication that formal proofs necessarily carry a priori knowledge about the real world.

TG: You've got the whole Rosen argument in Life Itself flipped exactly upside-down. Formal proofs (in this case, Turing-computability proofs) do not carry a priori knowledge about the real world, in the sense of knowledge of limitations of the natural world. One of the major themes in Life Itself is to hypothesize - for the sake of argument - what it would be like if the world were mechanistic, if Church's Thesis were elevated to a Law of Nature, and then, to characterize that world. Clearly, if Church's Thesis were true, then the inferential equivalent would be a formal world characterized by the Church-Turing Thesis and all the models of the world would be simulable (i.e., Turing-computable). Thus the corresponding definitions of mechanism and machine that Rosen gives are not arbitrary definitions, but rather follow directly from the above hypothesis. This is an entirely artefactually limited natural world, and correspondingly limited formal world of models.

Rosen's whole thrust is that such artefactual restrictions do not represent a priori restrictions on the limits of the natural world. However, the point of his making the lengthy characterization of a mechanistic, Church's Thesis world is to clearly delineate what such a world must entail (e.g., reductionism, context-independence, etc.) and also what it must not allow (e.g., causal loops, context-dependence, etc.).

You can call his hypothetical mechanistic world a straw man, if you like, but that misses the point entirely. This artefactual world merely serves to clarify that if physics and biology do indeed affirm that the natural world does not abide by Church's Thesis, and so it is not mechanistic, then what follows from that affirmation is Rosennean complexity, and the implications that ensue thereof, including the validity of noncomputable (e.g. relational) models, context-dependence, impredicativities, etc., on an equal epistemological footing with predicative, quantitative models.

TG: As to your "approximation" arguments, since at least FM (and probably long before), Rosen has identified measurements (encodings) and predictions (decodings) in modelling relations as being formally characterized by equivalence relations on some underlying set, usually the real numbers. Nowhere does he assert that we must (or can) utilize infinite precision reals in order for a modelling relation to commute. By changing those equivalence relations as we deem fit, we change the "granularity" or approximateness of our measurements and predictions. Within limits, these changes in granularity do not affect a models basic characteristics or entailment structures. They are simply part and parcel of the encoding/decoding in any modelling relation, whether it is a formal mathematical equation on paper, or a simulable formal model running on a desktop computer.

By contrast, an N-body computer simulation is not an "approximation" in the same sense: it is different than a change of precision or granularity. In the N-body simulation, the impredicative entailment structure of simultaneously interacting bodies is replaced with a predicative sequence of entailments (because that is all the entailment that the computer hardware is capable of). Such programs suffice very well for the sake of emulating the behavior of an N-body system, but because the entailment structure is now entirely different from the entailment structure of the natural system, it is a simulation rather than a model, in the Rosennean sense of those terms.

Tim,

I understand how "indefinitely extensible" can substitute for "infinite" in Turing computation and many other constructivist proofs. I still have a problem with the implication that formal proofs necessarily carry a priori knowledge about the real world. It is not clear to me why an entirely syntactic formal limitation like the Halting Problem (i.e., derived from an errorless rewriting of unencoded symbol strings) is a priori a limitation on any empirically testable encoded model that is necessarily verifiable only by approximate measurements. Einstein said it clearly: "In so far as the propositions of mathematics are certain they do not apply to reality; and in so far as they apply to reality they are not certain." I don't see why any formal proof can be assumed to be relevant for models of nature.

A classic example is Euclidean geometry that was once assumed to apply to nature but which turned out to be just a useful approximation for local models. All proofs have this approximation problem. There is the formal proof that you can't trisect an idealized angle with straightedge and compass, but the constructive limits are categorically different from the formal limits. Formal proofs cannot be approximate or have errors. By contrast, measurements are always approximate and always have error limits. Consequently, if you can measure angles with a certain accuracy, then you can always trisect an angle with that accuracy, so the formal proof limitation is actually no limitation at all for trisecting material angles.

Another example is the three-body problem that has clear, provable limits on a formal solution. However, in practice no astronomer considers this formal limit as relevant for his models of orbits or his actual calculations. These examples are typical and could be multiplied indefinitely.

Rosen uses the fact that formally the rationals are rare compared to the reals as an analogy to his belief that physical models are rare compared to biological models. But again, this is only true as a formal condition. Constructive, empirically verifiable models have much more severe limits than formal proofs. Specifically, when modeling with real computers we can represent only a very limited number of the rationals. Real numbers are only formally definable. We don't even know whether the continuum of real numbers conforms to any empirical reality, so such formal facts about real numbers do not in practice limit our models or affect their empirical verification. In other words, while the proof that enumeration of real numbers is impossible (and this is certainly a logical limitation) this formal limitation is not a significant limit on our practical empirical models.

Turing equivalency is also a formal concept. All the proofs about the limits of computation are obviously formal, and assuming the Church-Turing thesis none of the alternative disparate formalisms can escape these limitations on what number theoretic functions can be effectively computed. But like all formal statements, no approximations or errors are tolerated in such proofs.

By contrast, encoded empirically testable models are never exact, and none of these formal proofs say anything about calculating approximations of functions. Consequently, as in the examples above, I see no reason why any formal limits of computation, while they are certain and always hold, should of necessity be relevant in an empirically encoded model or simulation that must be tested only by approximate measurements. I am not claiming that formal limits are never relevant. I am only pointing out that a formal limitation is often irrelevant for models of nature in the absence of an empirical test to the contrary.

Howard