In mathematical logic, the rules of passage govern how quantifiers distribute over the basic logical connectives of first-order logic. The rules of passage govern the "passage" (translation) from any formula of first-order logic to the equivalent formula in prenex normal form, and vice versa.
The rules
See Quine (1982: 119, chpt. 23). Let Q and Q' denote ∀ and ∃ or vice versa. β denotes a closed formula in which x does not appear. The rules of passage then include the following sentences, whose main connective is the biconditional:
![{\displaystyle Qx[\lnot \alpha (x)]\leftrightarrow \lnot Q'x[\alpha (x)].}](https://wikimedia.org/api/rest_v1/media/math/render/svg/b961999c3968f88576f63d40c72b70e62e173674)
The following conditional sentences can also be taken as rules of passage:
![{\displaystyle \exists x[\alpha (x)\land \gamma (x)]\rightarrow (\exists x\alpha (x)\land \exists x\gamma (x)).}](https://wikimedia.org/api/rest_v1/media/math/render/svg/52c0f8feae0cbe98c9d578df99cbb16635bbbff6)
![{\displaystyle (\forall x\,\alpha (x)\lor \forall x\,\gamma (x))\rightarrow \forall x\,[\alpha (x)\lor \gamma (x)].}](https://wikimedia.org/api/rest_v1/media/math/render/svg/edf3154c7ac26391c17d9c5e3daa1441fe4a37be)
![{\displaystyle (\exists x\,\alpha (x)\land \forall x\,\gamma (x))\rightarrow \exists x\,[\alpha (x)\land \gamma (x)].}](https://wikimedia.org/api/rest_v1/media/math/render/svg/130c2724d84bd81615ea1f2775c97572e965253e)
"Rules of passage" first appeared in French, in the writings of Jacques Herbrand. Quine employed the English translation of the phrase in each edition of his Methods of Logic, starting in 1950.
See also
References
- 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.
External links
![{\displaystyle \ Qx[\beta \lor \alpha (x)]\leftrightarrow (\beta \lor Qx\alpha (x)).}](https://wikimedia.org/api/rest_v1/media/math/render/svg/d65c2767d0661c2096f9155b96cc49342b1ca398)
![{\displaystyle \exists x[\alpha (x)\lor \gamma (x)]\leftrightarrow (\exists x\alpha (x)\lor \exists x\gamma (x)).}](https://wikimedia.org/api/rest_v1/media/math/render/svg/8f675624fa68829b757547e555842d8d5a09f899)
![{\displaystyle \ Qx[\beta \land \alpha (x)]\leftrightarrow (\beta \land Qx\alpha (x)).}](https://wikimedia.org/api/rest_v1/media/math/render/svg/c521f5a8a1674c6fa22d3ed82e878ca8e0719236)
![{\displaystyle \forall x\,[\alpha (x)\land \gamma (x)]\leftrightarrow (\forall x\,\alpha (x)\land \forall x\,\gamma (x)).}](https://wikimedia.org/api/rest_v1/media/math/render/svg/14022047c6c7f720dcf0fe10a7025da873826f99)
