The following builds upon ideas presented by Jan Lukasiewicz and A. K. Bierman's Logic a Dialogue [1], scholars who invented reverse Lukasiewicz notation, and work of abstract algebra theorists.

Suppose we have some set G which we call a Group and for all x, y, z, a, b, c belonging to G consider the following axioms for that set:
(1) S is a closed binary operation on G in prefix language. That is, for all x, y there exists at least one element of G a such that Sxy=c. * is a closed binary operation in infix language. That is, there exists at least one element of G such that x*y=c. A is a closed binary operation on G in suffix language. That is, similar to the other parts of this axiom, xyA=c. Explanatory comment: S takes x and then y as its arguments in that order only. * takes x and then y as its arguments in that order only. xyA takes x and then y as its arguments in that order only.

(2) Associativity: For all x, y, z belonging to G, SxSyz=SSxyz, x*(y*z)=(x*y)*z, xyAzA=xyzAA

(3) Complement: For all x there exists an element x' such that there exists another element n, such that Sxx'=Sx'x=n, x*x'=x'*x=n, xx'A=x'xA=n.

(4) Existence of a neutral element: There exists an n belonging to G such that for all x belonging to G, Sxn=Snx=x, x*n=n*x=n, xnA=nxa=n.


(5) Formal Hypothesis introduction: if a=b, then for all x, Sxa=Sxb, x*a=x*b, xaA=xbA.

(6) Variable substitution holds for individual variables as well as pairs of variables within a binary operation.

(7) We can treat = as a closed binary equivalence relation which satisfies the axiom "=xx, x=x, xx= can get replaced with x".

Lemma 1: SxSyz, SSxyz, x*(y*z), (x*y)*z, xyAzA, xyzAA all are closed expressions.

Proof: This follows from the closure of each binary operation. E. G. SxSyz=Sxa by closure and specifically replacing the variable pair xy in (1) from Sxy, with the variable pair yz in Syz by (6), such that SxSxy=SxSyz. Then substituting a for Sxy and for Syz by (6), both sides become Sxa=Sxa. By variable substitution we can substitute xa in Sxa with xy in Sxy from (1). So, Sxa=Sxa becomes Sxy=Sxy. By (1), it then follows that Sxy=Sxy becomes c=c. By (7), we can simply write c. This shows that SxSyz=c in the form specified. With (1), (6), and (7) similar to the above one can prove in detail that SSxyz, x*(y*z), (x*y)*z, xyAzA, xyzAA as closed, such that we obtain the same form of the axiom. All these proofs get left as exercises so this discussion can move on.

Corollary 1: All expressions in this axiom system are closed.

Proof: Since we have (2) as closed, we only need to use variable substitution to prove (3), (4), and (5) as closed expressions in detail using a similar technique to the proof of lemma 1.

Principle of Proof Triplication for Group Theory Proofs: For any proof in prefix, infix, or suffix language we can generate proofs in the other two languages according to the following scheme: Sxy corresponds to x*y which corresponds to xyA, with Sxy, x*y, and xyA all considered as wfe, wffs, or simply logical formulas.

Proof: Since for each proof we have a list of the axioms used in each proof, and since by Corollary 1 all expressions are closed, we can replace each axiom in language A by the corresponding axiom in language B or C which belongs to (2), (3), (4), or (5). Suppose we replace each axiom used in a proof in language A with the axiom in language B such that we generate a proof in language B. Then, since each axiom in language B corresponds to a specific axiom in language C we can then replace each axiom in the proof given in language B by axioms in language C. This generates a proof in language C. Since A, B, and C represent any given of these three languages, this means that from a proof in one language we can generate a proof in any other similar language by replacing the corresponding axioms according to the scheme Sxy corresponds to x*y which corresponds to xyA, such that each of those *particular* expressions can get thought of mapping to both of the other two languages isomorphically since we've considered them as wfes. This does not imply that more complicated expressions before elements which a formula specifically in the infix language represented by X*Y can map isomorphically to the other languages, since ambiguity of order arises in infix language. This only works here since those three expressions only need three symbols to get expressed and closure holds for *all* expressions by Lemma 1.

Corollary: For any abstract algebraic system where closure holds and we can treat all formulas as well-formed logical expressions (wffs, wfes, or simply formulas, as the proof above makes explicit), we can generate three proofs for any given theorem. One of those proofs lays in a prefix language, one in an infix language, and one in a postfix language. Instead of using specific operators as above, one can correspond any given operators X, Y, Z and then instantiates them into a particular form, with the correspondence Xab with aYb to abZ where a and b now represent variables of variables. Since all theorems follow from axioms in any given language, proofs can get converted to the other language step-by-step by the Principle of Proof Triplication. Or if one prefers not to think of each proof as a separate entity of the same theorem, we can express a proof in three different ways, in prefix language, infix language, and suffix language by the Principle of Triplication.

Theorem: For any Group, a cancellation law is valid. That is, if Sxy=Sxz, then y=z. By the correspondence above if x*y=x*z, then y=z. If xyA=xzA, then y=z.

Proof: Left as an exercise. Specifically I suggest proving in detail each if-then assertion above. If you don't know how to or where to begin, look up a proof of the cancellation law for groups. Then rewrite such a proof according to the correspondence scheme above in one of the other languages step-by-step. Then do such for the third language. The author's experience is such that doing this clears up conceptual difficulties as to which axioms get hidden in proofs like say of a cancellation law when usually presented, since no statement of hypothesis introduction as an axiom, and how much one really has to assume to *thoroughly* write a proof.

[1] Logic: A dialogue . 1964, Holden-Day Inc.