Miscellaneous Notes

Encoding and Correspondence

2026 oct 29

Consider two systems F and G and suppose that F can be modelled in G — that for each object f in F (a well-formed term, operator, predicate, expression, or whatnot) there is an object 𝔠 ( f ) in G. The encoding 𝔠 is not necessarily an injection but should not discard so many distinctions between objects in F as to be uninteresting; all we really require is that 𝔠 preserves the truth values of statements, e.g. φ(a) ∧ ψ(b) ⟺ 𝔠φ(𝔠a) ∧ 𝔠ψ(𝔠b) . (And possibly G can be modelled in F — for each object g in G there is an object 𝔡( g ) in F, though 𝔡 may not be the left inverse of 𝔠 or vice versa.)

Then I’ve often seen people go about using G to do work on F (or objects in F), and then they begin to use F and G interchangeably in discussion. This latter practice bothers me for two reasons.

First, it is incorrect, or at least imprecise; F should not be identified with G, but with the image 𝔠 ( F ), and it can be confusing to neglect this.

Second, there are often different intuitive structures or semantic interpretations for F and G, so although the encoding may be useful mechanically or the correspondence a curiosity, using F and G interchangeably can be less than enlightening,* or may even be limiting (if extensions to F are not readily representable or not possible in G). . . . requiring constant mental translation — a translation which may not even be easy, if 𝔠 is difficult to invert or if meaning­fulness is not faith­fully preserved in one direction or the other.

Using F and G interchangeably can be less than enlightening [ . . . ] if meaning­fulness is not faith­fully preserved. As a weak example, consider how all functions over the integers are proofs of “Integer → Integer” under the Curry–Howard correspondence. A programmer cares a great deal about which specific functions she uses (adding 1 to an index is very different than multiplying it by 2), whereas the fact “Integer → Integer” is inane and the choice of proof irrelevant. I would contend that, here, significance in the computational language does not correlate with significance in the corresponding logic. (For other endeavours, using type theories as proof systems is, of course, an extremely good idea.)