The Journal of Symbolic Logic

We study logical systems for reasoning about equations involving recursive de#nitions. In particular, we are interested in #propositional# fragments of the functional language of recursion FLR [18, 17], i.e., without the value passing or abstraction allowed in FLR. The #pure,# propositional fragment FLR 0 turns out to coincide with the iteration theories of [1]. Our main focus here concerns the sharp contrast between the simple class of valid identities and the very complexconsequence relation over several natural classes of models