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/
