FOM: FoundationalCompleteness

[Vaughan R. Pratt]

>I find it curious that quantum mechanics is being held up as a paradigm for
>what might be hoped for in FOM.
>Paraphrasing Feynman: "If you think you understand quantum mechanics, you're
>mistaken."

That's a bit out of context.  Quantum mechanics is *implicated* in many
controversial aspects of physics: the interplay of measurement and
wavefunction collapse/path integrals/what have you, the bizarrely ad
hoc renormalizations of QED, the mismatch of QM with relativity, the
nature of quantum gravity, the possibility of quantum computation,
etc. etc., all of which are not well understood today.

What is perfectly well understood however is Heisenberg's and
Schroedinger's original theories, their complete duality as proved by
Schroedinger, and their common embedding by von Neumann into the
framework of separable Hilbert space.  This is the domain in which one
solves Schroedinger's equation, and physics students today routinely
study and grasp this model.

A more reasonable objection might be that too few logicians understand
even this much of QM for it to serve as a convincing role model.

Ok, so this would be a fair objection.  Fortunately one doesn't even
need Hilbert space for my analogy.  At the core of QM's dualism is the
Fourier transform, as used in more down-to-earth subjects as signal
processing and image processing.  Treating signal or image space as a
suitably dimensioned vector space (as many dimensions as there are
sample points in the signal), the Fourier transform realizes a change
of basis between temporal coordinates (spatial in the image case) and
frequency coordinates.

There is no information gained or lost by this change, just a
perceptual shift with algorithmic consequences.  For example
convolution, which looks like a quadratic time process, is transformed
to pointwise multiplication, a linear time process.

The parallel I'm drawing here is between propositions as points in time
or space and proofs as points in the frequency domain.  The idea is that
you have the same information in either case, but reorganized to suit
the occasion.

I would claim that linear logic is, in the loose sense of this analogy,
the "Fourier transform" of first order logic, preserving its content
while reorganizing its structure to give the dual perspective.  I have
no idea whether this can be made literally true (*that* would nice), as
it stands it's mainly just a metaphor.  What it does do is convey the
message that the dual point of view is not being proposed to replace
the status quo but quite literally to complement it.

Vaughan