More precisely, we consider formulas of the form A=B, where A and B are GLP formulas in the language with propositional variables and the following connectives: T (truth), &, and <n>, for all n. = means logical equivalence. The problem asks to axiomatize all GLP-provable equations of the above form.

An example of a valid principle is (<n>A & <m>B)= <n>(A & <m>B), if n>m.

We conjecture that this is essentially the only needed principle.

This problem is motivated by the fact that the ordinal notation system used for the analysis of PA is built by variable-free formulas in the language above. So, instead of working in the full GPA we could have worked in the presumably simpler (less expressive) structure.

This observation may become more essential for the further development of
GPAs, where there is a need to interpret variables as * theories *,
not just sentences. For theories the operation of negation does not make
sense, however the operations <n> and & do. <n> is just the
usual n-consistency, and & is union of theories. (Obviously, we could also
interpret disjuction as the intersection of the two theories.)

For example, one could then naturally enrich the language of GPA by a new modality <omega>. The meaning of <omega>A could be {<n>A: n<omega}, that is, the full reflection principle.

So, we have the second related general question: Develop an arithmetical interpretation of the above language, where the variables are interpreted as (possibly infinitely axiomatized) arithmetical theories.