Abstract:
There is significant interest in type-free systems that allow flexible
self-application. Such systems are of interest in property theory,
natural
language semantics, the theory of truth, theoretical computer science,
the theory of classes, and category theory. While there are a variety
of proposed type-free systems, there is a particularly natural
type-free system that we believe is prototypical: the logic of
recursive algorithms. Algorithmic logic is the study of basic
statements concerning algorithms and the algorithmic rules of inference
between such statements. The threat of paradoxes, especially the Curry
paradox, requires care in implementing rules of inference in this
context. As in any type-free logic, some traditional rules will fail.
Our work has led to the creation of rich library of inference rules
that are unproblematic in algorithmic logic and have a property we call
stability. We have also identified a number of traditional rules of
logic that are problematic in algorithmic logic, and so should be
viewed with suspicion in type-free logic. We conjecture that by freely
using stable libraries, limiting the scope of the problematic rules,
and using multiple libraries, we can create a type-free logic that is
viable for a wide range of applications.