Lambda the Ultimate

A theorem might establish an important property about a proposed formalism. The formalism might not be taken up "as is" in future work, due to various shortcomings, but the idea of such a formalism having such a property could still become influential on future work.

In general, a theorem and its proof might be influential without being used in a deductive sense in later work.

yet

which program invariants established by your typechecker don't really contribute to the correctness of the program. You could ask, but the answer might change.

(It's also a lot like the annoying "unreachable code" warnings that some compilers are want to emit when the optimizer discovers dead code in the program text. It may be an indication of a problem, or it may be simply an indication that the compiler is doing its job; programmers and especially metaprogrammers frequently have very good reasons to insert unreachable code into program source).

I'm not sure I'd agree that establishing a type system as sound is a dead-end theorem. It establishes that the upper bound on the usefulness of the system is sufficiently high that further work is of interest--there is little practical use of unsound type systems, after all.

Charles & Scott are of course correct that being dead-end does not mean the theorem is useless or unimportant. This is why I did not say it does, and asked about a more well-defined property (i.e., being "dead-end" as define above).

Burton, you may be right. I should have made my definition more exact: "that is not currently used in the proofs of other results". Anyway, in many routine cases it is easy to tell that chances re the theorem as is is going to be of little use in future proofs (it may be used once or twice, of course...)

Suppose I prove Theorem A. Then I prove, independent of my first proof, Theorem B.

Then I write a second proof of A, depending on B; and likewise use A to prove B.

A and B are nowhere else cited.

Are they dead? (Are we using tracing or ref-counting to evaluate the liveness of the theorem?)

:)

Maybe the "publication" metaphor helps us here. An object which is created on the heap, but whose sole reference is immediately discarded, is of course semantic garbage. An object which is created somewhere and then "published" in a directory of some sort, such that other clients who have a reference to the containing repository and who can (re)generate the key necessary to reach the object, is certainly not garbage. Even if nobody else bothers to access it; the fact that it is published means it probably should be left alone. (One could subsequently decide to withdraw it--removing it from the repository--at which point it might then become garbage, assuming no other references).

Likewise, a theorem jotted down on an envelope and then crumpled up and thrown into the trash, is (literally, in this case), garbage. A theorem which finds its way onto the pages of Communications of the ACM has been (literally again) published, and by that act of publication, is live. Even if nobody ever uses it in their research. (What happens if CACM subsequently withdraws the paper is left as an exercise to the reader).

Theorems are, of course,immutable creatures, so copies are as good as aliases--meaning that withdrawing one from the totality of man's knowledge is nigh near impossible, once the horse has left the barn.

But still... the liveness of an object is really only an interesting property when the size of the set of objects is bounded, and one needs to find objects to cull. While it's often good sport to complain about "junk research" (and tenure committees and others may have good reason to identify producers of excessive trivial research prior to granting tenure), the global information capacity of academia is not so constrained. Unused thorems simply get ignored, after all.

Switching gears away from garbage collection metaphors, perhaps relevance logic has some relevance...