Regras de tradução lógica

Na lógica matemática, as regras de tradução ditam como os quantificadores se distribuem através dos conectivos lógicos básicos da lógica de primeira ordem. As regras de tradução determinam como qualquer fórmula da lógica de primeira ordem podem ser transformadas na forma normal prenex, e vice-versa.

Tais regras tem origem de escritos do francês Jacques Herbrand.

As regras

Suponha que $Q$ e $Q^{\prime }$ denotem ∀ e ∃, ou vice-versa. Suponha também que β é uma fórmula fechada na qual $x$ não faz parte.
Então, são verdadeiras as seguintes traduções, bicondicionais:

• $Qx[\mathrm{\neg }\alpha (x)]\leftrightarrow \mathrm{\neg }{Q}^{\prime }x[\alpha (x)].$
• $Qx[\beta \vee \alpha (x)]\leftrightarrow (\beta \vee Qx\alpha (x)).$
• $\mathrm{\exists }x[\alpha (x)\vee \gamma (x)]\leftrightarrow (\mathrm{\exists }x\alpha (x)\vee \mathrm{\exists }x\gamma (x)).$
• $Qx[\beta \wedge \alpha (x)]\leftrightarrow (\beta \wedge Qx\alpha (x)).$
• $\mathrm{\forall }x[\alpha (x)\wedge \gamma (x)]\leftrightarrow (\mathrm{\forall }x\alpha (x)\wedge \mathrm{\forall }x\gamma (x)).$

Além das traduções anteriores, temos as seguintes condicionais:

• $\mathrm{\exists }x[\alpha (x)\wedge \gamma (x)]\to (\mathrm{\exists }x\alpha (x)\wedge \mathrm{\exists }x\gamma (x)).$
• $(\mathrm{\forall }x\alpha (x)\vee \mathrm{\forall }x\gamma (x))\to \mathrm{\forall }x[\alpha (x)\vee \gamma (x)].$
• $(\mathrm{\exists }x\alpha (x)\wedge \mathrm{\forall }x\gamma (x))\to \mathrm{\exists }x[\alpha (x)\wedge \gamma (x)].$

Referências

• Willard Quine, 1982. Methods of Logic, 4th ed. Harvard Univ. Press.
• Jean Van Heijenoort, 1967. From Frege to Gödel: A Source Book on Mathematical Logic. Harvard Univ. Press.