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

## Advertising

Brent Meeker writes:I'm uncertain whether "instantiated by abstract mathematicalpatterns" meansthat the patterns are being physically realized by a process in time(as in thesci-fi above) or by the physical existence of the patterns in somestatic form(e.g. written pieces of paper) or just by the Platonic "existence" ofthepatterns 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 thatinvolves the flow of time, existing Platonically? Or would yourestrictPlatonic existence to things like integers and triangles, whichseeminglydon'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, causaldependency of later steps on earlier ones. It seems to be aninterestingintermediate 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 thoughts.

`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*.`

Bruno http://iridia.ulb.ac.be/~marchal/