Immersion operation

In mathematical logic, this is an operation that converts an expression in one logical language into an expression in another while preserving deductive properties. Immersion operations are widely used in establishing relationships between different logical theories or calculi (see Calculus).

For example, if a formula $A$ in formal arithmetic is put into correspondence with a formula $A^*$ in the same language by inserting two negations in front of it and in front of each of its subformulas (for example, $(A\lor B)^*$ is $\neg\neg(\neg\neg A^*\lor\neg\neg B^*)$, while $(\exists xA)^*$ is $\neg\neg\exists x\neg\neg A^*$, etc.), then derivability of $A$ in classical formal arithmetic implies derivability of $A^*$ in intuitionistic formal arithmetic. This means that the consistency of intuitionistic formal arithmetic implies the consistency of classical formal arithmetic. This Gödel negative interpretation thus yields an important relationship between intuitionistic and classical arithmetic.

Another typical example of an immersion operation is the Gödel–Tarski translation, which relates modal and intuitionistic logics. The construction of models in axiomatic set theory can also usually be regarded syntactically as the construction of some immersion operation: an internal model in set theory.

References

[1]	J.R. Shoenfield, "Mathematical logic" , Addison-Wesley (1967)
[2]	R. Feys, "Modal logics" , Gauthier-Villars (1965)
[3]	A.G. Dragalin, "Mathematical intuitionism. Introduction to proof theory" , Amer. Math. Soc. (1988) (Translated from Russian)

Comments

It is more common to call an immersion operation an interpretation or a translation.

An "interpretation" may be thought of as a "homomorphism" from one logical theory to another, a point of view which has been extensively exploited in categorical logic (see [a1]).

References

[a1]	A. Kock, G.E. Reyes, "Doctrines in categorical logic" J. Barwise (ed.) , Handbook of mathematical logic , North-Holland (1987) pp. 283–313
[a2]	K. Gödel, "Zur intuitionistischen Arithmetik und Aussagenkalküls" Ergebn. eines Math. Kolloq. , 4 (1933) pp. 34–38
[a3]	K. Gödel, "Eine Interpretation des intuitionistischen Aussagenkalküls" Ergebn. eines Math. Kolloq. , 4 (1933) pp. 39–40