This is the most tentative section of the present article. At present we have two approaches to writing Elephant programs as sentences of logic. The first approach is analogous to Algol 50. It is based on updating a state of the program and a state of the world. Of course, the functions updating the state of the world will be only partially known. Therefore, unknown functions will occur, and the knowledge we have about the world will be expressed by subjecting these functions to axioms. The second approach expresses the program and tentatively what we know about the world in terms of events. The events occur at times determined by axioms. We describe the events that we assert to occur and rely on circumscription to limit the set of occurrences to those that follow from the axioms given. We begin with the Algol 50 approach.
As with Algol 50, in our first approach we use a state
vector 
for the state of the program during operation.
The program is expressed by a formula for 
. Since the
program interacts with the world, we also have a state vector
world(t) of the world external to the computer. Because we
can't have complete knowledge of the world, we can't expect to
express world(t+1) by a single formula, but proving
accomplishment specifications will involve assumptions about the
functions that determine how world(t) changes.
We have
and
Notice that we have written 
and world on the right sides
of the two equations rather than and world(t), which
might have been expected. This allows us to let and
world(t+1) depend on the whole past rather than just the present.
(It would also allow equations expressing dependence on the future,
although such equations would be consistent only when subjected
to rather strong conditions.)
We have written part of the reservation program in this form, but it isn't yet clear enough to include in the paper.
The second approach uses separate functions and predicates with time as an argument. In this respect it resembles Algol 48.
Note the use of admit with a variable ?seat.
We may suppose that admit actually has a large set of arguments with
default values. When an 
expression is encountered,
it is made obvious which arguments are being given values by the
expression and which get default values. The signals for this are
the name of the variable or an actual named argment as in Common
Lisp. In the present case, the compiler will have to come up with a
way of assigning a seat from those available.
Asserting that certain outputs occur and that certain propositions
hold doesn't establish that others don't occur. Therefore, the program
as given is to be supplemented by circumscribing certain predicates,
namely 
, 
and 
.