Le 04-août-05, à 18:38, Hal Finney a écrit :

Brent Meeker writes:
I'm uncertain whether "instantiated by abstract mathematical patterns" means that the patterns are being physically realized by a process in time (as in the sci-fi above) or by the physical existence of the patterns in some static form (e.g. written pieces of paper) or just by the Platonic "existence" of the
patterns within some mathematic/logic system.

I'd be curious to know whether you think that Platonic existence could
include a notion of time.  Can you imagine a process, something that
involves the flow of time, existing Platonically? Or would you restrict Platonic existence to things like integers and triangles, which seemingly
don't involve anything like time?

How about the case of mathematical proofs?  Could an entire proof
exist Platonically?  A proof has a sort of time-like flow to it, causal
dependency of later steps on earlier ones. It seems to be an interesting
intermediate case.

My tentative opinion is that it does make sense to ascribe Platonic
existence to such things but I am interested to hear other people's

My feeling is that your tentative opinion is sound. First the whole subject of metamathematics (Post, Kleene, Church, Turing, Godel, Lob, Solovay, ...) is based on the fact that "formal proofs" can be coded unambiguously by numbers or by other mathematical objects (for exemples arrows in some categories). Informal proofs can also be considered as existing in Platonia, but then you need some strong assumption (like comp, but I think it could work with less strong assumptions).

Your intuition that a proof has a sort of time-like flow is quite accurate, and is actually the base of many many works in todays theoretical sciences. The idea is that axioms corresponds to "initial conditions", and the inference rules corresponds to the dynamics.
I will illustrate this with the combinators soon or late.

In some logic, that "analogy" can be made even more precise. In linear logic the principle that axiom = initial conditions, and rules = dynamical law, is "so true" that Girard has succeeded in building semantics in term of Hilbert space and operator algebra quite akin to "quantum mechanics". The fact is that linear logic handle a notion of resource (for example from the assumption A you cannot derive A & A (like from 1 dollar you cannot derive 2 dollars!).

Now an important fact is the following: computations themselves can be seen as proofs. But with Church thesis, the notion of computation is absolute: it does not depend on the formal system chosen (java = C = turing = quantum computer = ...). But provability is a relative notion (like the notion of *total* (everywhere defined) computable functions. To say "A is proved" has no meaning, you should always say: A is proved in this or that theory (or by this or that machine). Of course provability can obey universal principles: for example the notion of classical checkable proof in sufficiently rich system is completely captured by the modal logics G and G*.



Reply via email to