# 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)