[FOM] Mismatch
Harvey Friedman
friedman at math.ohio-state.edu
Sun Jun 15 15:47:15 EDT 2003
Reply to Gugliemi 4:23AM 6/15/03.
There are many subscribers, including me, who are surely very
grateful to see such a substantive posting on a (essentially) new
topic for FOM.
However, many, including me, need some slower background material to
appreciate the issues.
In particular, my knowledge of linear logic is restricted to the following:
1. It is at least originally motivated by trying to model the
tracking of resources, so that having two copies of something is not
the same as having one copy - in accordance with the fact, say, that
having two copies of a gold bar is not the same as having one copy of
that gold bar.
2. Nobody is claiming to have any completeness theorem associated
with 1, that goes to the heart of the purpose of linear logic.
So I, for one, paid no attention to linear logic, assuming that item
2 is the principal open question. I was waiting to see some
particularly coherent and attractive expository or otherwise article
about 1,2 so that I would have a crack at getting to the bottom of
what an appropriate completeness theorem would look like.
I have been seriously involved in completeness proofs of
intuitionistic logic over the years, and for various reaons,
intuitionistic logic has, from many points of view, proved its
permanent value.
The situation with modal logic is much more murky, and certainly
there is a good start at it proving its permanent value, but the case
is nowhere near as clear as it is for intuitionistic logic.
Relevance logic is, as far as I can tell, less clearly of permanent
value than modal logic, but again there are some interesting faint
flashes of light.
The standards for introducing a new logic and having it attain
permanent value are quite high.
In fact, we need a major new thread in FOM called something like "the
essences of nonclassical logics". Here subscribers to FOM could take
the point of view that all nonclassical logics are guilty before they
are proved innocent. The idea being that in each case, one should see
just how clearly one can state the purpose of it, and just how
clearly this leads to a completeness theorem.
I should add that I have no doubt that there are VERY clarifying
results that fall short of a decisive completeness theorem. As an
example, the disjunction and existence properties in intuitionistic
systems, as well as the existence of effective outer Skolem functions
for provable AE... sentences.
Gugliemi is a natural candidate for discussing the case for linear
logic in the most elemental of terms.
Now in order to make this thread on the FOM effective, we need
a. Gugliemi to be prepared to cast matters in the most elemental of terms.
b. Gugliemi to be prepared for the possibility that FOM subscribers
may be unconvinced of the value of linear logic, even to the point of
coming to the conclusion that it is of no value.
c. FOM subscribers who already believe or think they know that linear
logic is of no value, or are highly skeptical of any nonclassical
logic on its face, to be prepared to be convinced that linear logic
is of the greatest possible importance, perhaps so important that
substantial advances in it are much more important than their own
research.
Harvey Friedman
More information about the FOM
mailing list