  Type-free systems of logic are designed to consistently handle significant
instances of self-reference. Some consistent type-free systems also have the
feature of allowing the sort of general abstraction or comprehension principle
that infamously leads to paradox in naive set theory. Because type-free systems
possess these features, and avoid the hierarchy of types that is felt to be
unnatural in some contexts, they have the potential to play an important role
in the foundations of mathematics, the theory of classes (producing a richer
notion of class than that currently used in set theory and category theory),
property theory, natural language semantics, the theory of truth, and
theoretical computer science. Clearly, type-free systems must depart from
classical logic in some way, but there is little agreement on what kind of
type-free system to use, and which departures from classical logic should be
allowed.
  Our approach to type-free logic is to study a naturally occurring type-free
system that we believe is in some sense prototypical of systems that will
ultimately prove useful. The logic studied in this paper, called algorithmic
logic, concerns certain basic statements involving algorithms and the
algorithmic rules of inference between such statements. This paper studies the
propositional properties of algorithmic logic. A future paper will show that
algorithmic logic possesses a general abstraction principle.
