A subsystem of Kripke-Platek set theory proof-theoretically equivalent to primitive recursive arithmetic is isolated; Aczel's (relative) consistency argument for the Anti-Foundation Axiom is adapted to a (related) weak setting; and the logical complexity of the largest bisimulation is investigated.
The author is gratefully indebted to Prof. S. Feferman for supervision, to CWI for refuge, and to the Netherlands Organization for the Advancement of Research (project NF 102/62-356, 
Structural and Semantic Parallels in Natural Languages and Programming Languages
) for funding.