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
> 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/
Received on Fri Aug 05 2005 - 06:47:28 PDT