Is there a non-trivial consistency preserving transformation?

In ‎set ‎theory ‎"equiconsistency" (and not "consistency") ‎of ‎the ‎theories ‎is the‎ ‎main ‎part ‎of ‎researches. ‎So ‎we ‎usually ‎try ‎to ‎construct a‎ ‎new model ‎using a‎ ‎given ‎one. ‎In ‎the ‎other ‎words ‎we ‎"transform" a ‎‎‎given ‎model ‎to ‎anothe‎r one by some kind of "operations". Even it seems that we can do this transformation in the realm of syntax instead of semantics. For example if ‎$‎‎T$ ‎be a‎ ‎theory ‎which ‎is ‎produced ‎from ‎‎$‎ZFC‎$ ‎by ‎replacing ‎any ‎phrase ‎‎$‎‎x\in y$ with ‎‎$‎‎\neg (x \in y)$ ‎then ‎‎$‎T‎$‎ ‎is ‎equi‎consistent ‎with ‎‎$‎ZFC‎$ ‎because ‎for ‎all ‎set ‎(or proper class) ‎‎$‎M‎$ ‎and ‎for ‎all ‎binary ‎relation ‎‎$‎E‎$ ‎on ‎it ‎we ‎have:‎

$‎‎\langle M,E ‎\rangle ‎\models ZFC ‎\Longleftrightarrow‎ ‎‎\langle M,M\times M\setminus E ‎\rangle ‎\models T‎$ ‎

Now define: ‎‎‎

Definition (1): ‎Let ‎‎$‎‎‎\mathcal{L}‎$ ‎be a‎ ‎first ‎order ‎language‎. A function ‎$‎‎f:‎\mathcal{L}-Form‎\longrightarrow ‎‎\mathcal{L}-Form‎$‎ ‎called a ‎"‎‎syntactical transformation" ‎if ‎it ‎preserves ‎logical ‎operators, ‎i.e.‎ ‎‎

(1)‎‎‎$‎\forall ‎n\in ‎\omega~~~‎\forall ‎\varphi ‎(x_{1},...,x_{n})\in ‎‎\mathcal{L}-Form~~~~~‎$‎‎ ‎

The number of free variables of the formula $f(‎\varphi ‎(x_{1},...,x_{n})‎‎)$ is equal to

the number of free variables of the formula $\varphi ‎(x_{1},...,x_{n})‎$

(2) ‎‎$‎\forall ‎n\in ‎\omega~~~‎\forall ‎\varphi ‎(x_{1},...,x_{n})\in ‎‎\mathcal{L}-Form$

$f(\neg ‎\varphi ‎(x_{1},...,x_{n})‎‎)=\neg f(‎\varphi ‎(x_{1},...,x_{n}))‎$‎‎‎ ‎

(3)‎ ‎‎$‎\forall m,‎n\in ‎\omega~~~‎\forall ‎\varphi ‎(x_{1},...,x_{m}),‎\psi ‎(y_{1},...,y_{n})\in ‎‎\mathcal{L}-Form‎$‎‎‎ ‎

$‎f(‎\varphi ‎(x_{1},...,x_{m})\wedge ‎\psi ‎(y_{1},...,y_{n})‎‎)=$

$f(‎\varphi ‎(x_{1},...,x_{m}))\wedge f(‎\psi ‎(y_{1},...,y_{n}))‎$ ‎

(4)‎‎ ‎‎$‎\forall ‎n\in ‎\omega~~~‎\forall ‎\varphi ‎(x, y_{1},...,y_{n})\in ‎‎\mathcal{L}-Form$

$f(\exists x~‎\varphi ‎(x,y_{1},...,y_{n})‎‎)=\exists x~f(‎\varphi ‎(x, y_{1},...,y_{n}))‎$ ‎‎ ‎

Remark (1): ‎‎In ‎some ‎sense a syntactical transformation ‎is a‎ ‎"homomorphism" ‎from ‎‎$‎‎‎\mathcal{L}-Form‎$ ‎to ‎itself ‎when ‎we ‎look ‎at ‎the ‎set ‎‎$‎‎‎\mathcal{L}-Form‎$ ‎as ‎a ‎structure ‎e‎ndowed with unary and binary logical operators ‎$‎‎\neg~,~‎\exists~,~‎\wedge‎‎$‎. ‎

Remark (2): ‎If ‎‎$f‎$‎ ‎be a‎ ‎syntactical ‎transformation ‎in ‎the ‎first ‎order ‎language ‎‎$‎‎‎\mathcal{L}‎$, ‎then ‎the ‎values ‎of ‎‎$‎f‎$ ‎on $‎‎‎\mathcal{L}-Form‎$ are ‎determined by ‎the ‎values ‎of ‎‎$‎‎f$ ‎on ‎the ‎‎atomic ‎‎$‎‎‎\mathcal{L}‎$-formulas.‎ ‎

Remark (3): By the condition (1) in the definition (1) it is easy to see that for any ‎syntactical ‎transformation ‎$‎f‎$‎ ‎in ‎a ‎first ‎order ‎language ‎‎$‎‎‎\mathcal{L}‎$ and for any ‎$‎‎‎\mathcal{L}‎$ ‎-sentence ‎$‎‎\sigma$, ‎$‎‎f(\sigma)$ is a sentence too‎. ‎‎So ‎for ‎any ‎‎$‎‎‎\mathcal{L}‎$-theory ‎‎$‎T‎$ ‎the ‎image ‎of ‎‎$‎T‎$ under the function ‎$‎f‎$‎ ‎(‎$‎‎f[T]=\lbrace f(\sigma‎)~|~\sigma \in T‎\rbrace‎$‎) ‎is a‎n ‎$‎‎‎\mathcal{L}‎$‎-‎theory too.‎ ‎

Definition (2): A‎ ‎syntactical ‎transformation ‎‎$‎‎f$ in the language ‎$‎‎\mathcal{L}‎$‎ ‎‎called ‎‎‎‎"consistency preserving" ‎if:‎ ‎

$‎‎‎\forall ‎T\in ‎\mathcal{L}-Theory~~~Con(T)‎\Longrightarrow ‎Con(f[T])‎‎‎$ ‎‎ ‎‎

Remark (4): The identity map is a trivial consistency preserving syntactical transformation in any first order language. ‎

Question (1): ‎Is ‎there a‎ ‎non-trivial consistency ‎preserving ‎‎syntactical ‎transformation ‎in ‎any ‎first ‎order ‎language? ‎Is ‎there ‎such ‎function ‎for ‎the ‎language ‎of ‎set ‎theory ‎‎$‎‎‎\mathcal{L}=\lbrace \in \rbrace‎$‎? ‎ ‎

Definition (3): Assume that ‎‎$‎T‎$ is a theory ‎in the first order language ‎$‎‎\mathcal{L}‎$. Now define the set $Trans(T)$ to be as follows:‎ ‎

$‎‎\lbrace ‎‎f~|‎‎~f‎‎~\text{is a syntactical transformation and}~f[T]~\text{is a consistent theory} \rbrace‎‎$‎ ‎‎

Remark (5): ‎For ‎example ‎in the language of set theory the ‎map‎ping ‎which is given by $‎‎x=y‎\mapsto ‎x=y‎$ ‎and ‎‎$x\in y ‎\mapsto ‎\neg (x\in y)‎$‎ ‎is ‎in ‎‎$‎Trans(ZFC)‎$. ‎But ‎the ‎map ‎‎which is given by $‎‎x=y‎\mapsto \neg (‎x=y)‎$ ‎and ‎‎$x\in y ‎\mapsto ‎x= y‎$‎ ‎is not ‎in ‎‎$‎Trans(ZFC)‎$ ‎because ‎it ‎transforms ‎the Axiom ‎of ‎Extensionality ‎into ‎a ‎non-satisfiable ‎sentence ‎as ‎follows:‎ ‎

$‎‎[‎\forall ‎x~‎\forall ‎y~(x=y‎\leftrightarrow ‎‎\forall ‎z~(z\in x‎\leftrightarrow ‎z\in y‎)‎‎)‎‎]‎\mapsto ‎[‎\forall ‎x~‎\forall ‎y~(\neg (x=y)‎\leftrightarrow ‎‎\forall ‎z~(z=x\leftrightarrow ‎z=y‎)‎‎)]‎$‎

So ‎there ‎is a‎ ‎natural ‎question ‎here:‎ ‎

Question (2): ‎What are ‎‎the members of $‎‎Trans(ZFC)$? ‎

In ‎the ‎other ‎words ‎how ‎free ‎can ‎be ‎the ‎choice ‎of two ‎formulas ‎‎$‎‎\varphi (x,y)$ ‎and ‎‎$‎‎\psi (x,y)$ ‎such ‎that for ‎the ‎syntactical ‎transformation ‎$‎f‎$‎ ‎which ‎is ‎defined ‎by ‎‎$‎‎x=y‎\mapsto‎ ‎‎\varphi (x,y)$ ‎and‎ ‎‎$‎‎x\in y‎\mapsto‎ ‎‎\psi (x,y)$ we have ‎$‎‎Con(ZFC)‎\Longrightarrow ‎Con(f[ZFC])‎$‎‎?

-
Your picture is not accurate. Even when only working on independence results, we are interested in much more than equiconsistency, which is a first order property. We are describing procedures that allow us to obtain models of $T$ starting from models of $T'$ and vice versa, in a way that we in fact obtain mutual interpretability. (And even saying that this is (all) forcing and inner model theory are after is far from the truth.) – Andrés E. Caicedo Oct 6 '13 at 14:28
@Andres: Dear Andres. You are right. the realm of set theory is more complicated than what I described in the first paragraph. It is just a brief and inexact introduction and is not necessary to understand the subject of the question. – user36136 Oct 6 '13 at 14:44
If you weaken your requirement of preserving all logical constructors, then the syntactic presentation of forcing gives a transformation much like what you describe. (But of course it doesn’t preserve $\exists$ and $\lor$.) – Peter LeFanu Lumsdaine Oct 6 '13 at 14:57
@Peter: Dear Peter. Your answer is interesting. Can you explain more? – user36136 Oct 6 '13 at 15:03
If you additionally allow that the transformation may change the language of the formulas to which it is applied, then the transformations become what some people may call "interpretations". The study and application of such mappings is sometimes headed with the term "interpretability". – user42061 Oct 31 '13 at 18:28