raph: A few points about your translation:

• You don't need to encode first-order terms as singleton second-order variables when moving from quantification over functions to quantification over predicates. Instead you can replace each quantification over functions by two (or more) quantifiers, one over predicates that occurs in the same place as the original (together with an implication to effectively retrict the quantifier to total functions), and a transformation of each equation into a derived proposition with only first-order quantifiers.
• Secondly, I am not sure, but the way you word your diary entry suggests you may not be respecting the distinction between the set of total functions and the set of functions that SOA can prove total.
• Finally, you need to check your translation actually captures the properties you are after. I think the most natural way to do this is to have translations going in each direction (say phi, psi), with the property that for each proposition P of Z_2^{fun} P<=>psi(phi(P)) and for each proposition P of Z_2^{pred} P<=>phi(psi(P)). I'd also add an informal requirement: each of phi and psi can reasonably be considered `meaning conserving', ie. they establish the same proposition in a different form.

The point I made in my last diary entry about saying the two formulations of Z_2 were `trivially' the same was not to say the translations don't have tricky details, but rather to say there is no real conceptual distance between the two formulations: we can give translation functions that have only linear growth in the size of propositions, and satisfies the above criteria, and has exactly the same consequence relation on first-order terms. Such translations cannot be found between Z_2 and systems based on the polymorphic lambda-calculus, even though some of the latter class of systems have the same provability strength as the former. In other words, you have to choose between Z_2-like consequence relations and Coq-like consequence relations right at the start. I think that Z_2 is the right choice if you care about mathematics more than metamathematics and proving existing programs correct rather than automatic program extraction.

Given that you want a Z_2-like consequence relation, I don't think either formulation is `the right thing' as a proof exchange format: the theories should have a rich set of datatypes and quantifiers, split into first order data-types of countable cardinality (finite enumeration sets, finite lists and tuples of countables, integers, rationals, polynomials, algebraic numbers, finite binary trees, etc.), and second-order data-types of uncountable cardinality (eg. infinite streams of bits, infinite streams of integers, infinite binary trees, n-ary relations over finite datatypes, n-ary functions upon finite datatypes, etc.). The point is that one can find good translations from such richer theories into the simpler axiomatisations of Z_2 that metamathematicians use.

Bram: Quite so, I'm afraid I am guilty of being careless about the terminology complexity theorists use: I come from graph rewriting where I call this the graph matching problem. Sorry for wasting your time.

graydon: Sorry for the long time in responding to your last response to me. I keep meaning to reply, but each time I start composing a diary entry, I spend far too long thinking about raph's ideas about proofs and run out of time. Just briefly, I want to explain what the serious problems are with Hehner's article, and give a reasonable definition of syntactic metaprogramming. At least I can deal with one of your points about LISP macros: a macro system by definition gives a static code transformation. It is just that it makes sense for most LISP macro systems to carry out this transformation at run-time, as happens when there is no compile time (eg. interpreters), in the context of (eval ...) statements, and when you want staged computation (eg. in dynamic compilation). Insisting on pre-processing as your source transformation system causes all kinds of tiresome difficulties when you move away from the C batch-processing paradigm.