On Mon, Jan 07, 2008 at 01:37:46AM -0600, Duncan Patton a Campbell wrote: > On Sun, 6 Jan 2008 22:21:14 -0500 > "Eliah Kagan" <[EMAIL PROTECTED]> wrote: > > > (There are also multiple useful, > > mutually-inconsistent formal systems in both fields.) > > Provably so?
Yes. For example, in intuitionistic analysis every real-valued function of a real-valued variable is continuous, whereas classically most of them (e.g., in the sense of cardinality) are not. (To anticipate (the substance of) a remark: Yes, e.g., there is no Heaviside function in intuitionistic analysis and no, that does not prevent intuitionistic analysis from being able to do the work in applications that the Heaviside function does for classical analysis (just somewhat differently).) The full picture is more complicated, however. There are translations between the formal systems (or perhaps of one into an expansion by imaginaries, higher types and/or modal operators of (possibly a reduct of) the other). Semantically, this often corresponds to a construction in one formal system of a structure that faithfully (perhaps only relative to certain formulae) models the other formal system. Examples: classically one can verify the foregoing result of intuitionistic analysis, e.g., by interpreting it in a gros topos of subcanonical sheaves on a category of spaces (an extension[1] of Cohen's method of forcing for constructing models of set theory); Klein's model of the hyperbolic plane and the (essentially) Grassmann construction of projective space, each of which is a construction on (part of) an euclidean space. Observe that this does not contradict Matthew's original remark; if anything, it reveals some of the depth of that remark. Matthew knows what he is talking about. [1] This word conceals a lengthy description of an involved relationship; I am sure that some would dispute its aptness.
