[FOM] Mismatch

[Harvey Friedman]

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