Source: Wikipedia, the free encyclopedia.
From
- Note: I'm going to skip rules of identity
- Note: Even if this is a potentional copyright violation, does anyone doubt I can get permission?
- Tautology:
- If
(
is a tautology), then ![{\displaystyle P_{1},P_{2},\cdots ,P_{n}\vdash Q}](https://wikimedia.org/api/rest_v1/media/math/render/svg/d0c08998184171425ae5e0542baa8c77078eeb4e)
- (note that n may equal 0.)
- Tautologically Equivalent Formulas
- If
and
is obtained from
by substituing some occurences of
by
, then ![{\displaystyle \vDash \varphi _{1}\leftrightarrow \varphi _{2}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/64e46cf8cd1f4bc99c20c3b753c4ba9ce2868c86)
- (Implict rule of proof)
- If
,
,
- .
- .
- .
,
, then
![{\displaystyle \Gamma _{1}\cup \Gamma _{2}\cup \cdots \cup \Gamma _{n}\vdash Q}](https://wikimedia.org/api/rest_v1/media/math/render/svg/60eb741145a1229a7da7f3c66cc92c9ff7d21e0c)
Specific tautologies:
Rule of Detachment, Modus Ponens
(Modus Tollendo Tollens)
(Modus Tollendo Ponens)
(Rule of Simplification)
(Rule of Addition)
- Rule of Adjunction
![{\displaystyle P\rightarrow (Q\rightarrow P\land Q)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/1bdf9dbc756bcdd6d44b56d7da841dd906f0df24)
![{\displaystyle (P\rightarrow Q)\land (P\rightarrow R)\rightarrow (P\rightarrow Q\land R)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/717144cdd38f46ccf6f1c1552464b27acf2b288e)
(Rule of Hypothetical Syllogism)
- Rules of Alternative Proof
![{\displaystyle (P\rightarrow Q)\land (\neg P\rightarrow Q)\rightarrow Q}](https://wikimedia.org/api/rest_v1/media/math/render/svg/fcecde991299fbfe3dfb464df9380f369237bf4b)
![{\displaystyle (P\lor Q\rightarrow R)\leftrightarrow (P\rightarrow R)\land (Q\rightarrow R)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/4426573656bad97841f8696ec3aa92220a19fbce)
- Rule of Absurdity
![{\displaystyle (P\rightarrow Q\land \neg Q)\rightarrow \neg P}](https://wikimedia.org/api/rest_v1/media/math/render/svg/eb02db41f1db4b0a63b96679f6d48656943468f9)
![{\displaystyle P\land \neg P\rightarrow Q}](https://wikimedia.org/api/rest_v1/media/math/render/svg/1bf497d1cc92b1d2fb6d760b53bbe515bbf7dcb9)
(Rule of the Excluded Middle)
(Rule of Contradiction)
- Communtative Rules
![{\displaystyle P\lor Q\leftrightarrow Q\lor P}](https://wikimedia.org/api/rest_v1/media/math/render/svg/50af04e973a495c2e2ab8785010aa4feee1679a3)
![{\displaystyle P\land Q\leftrightarrow Q\land P}](https://wikimedia.org/api/rest_v1/media/math/render/svg/542ef0011bd5af6a2a58ed1ddb01187a4915cb1c)
- Associative Rules
![{\displaystyle P\lor (Q\lor R)\leftrightarrow (P\lor Q)\lor R}](https://wikimedia.org/api/rest_v1/media/math/render/svg/ae444f6f57165c05d517a78fb3535af731187f40)
![{\displaystyle P\land (Q\land R)\leftrightarrow (P\land Q)\land R}](https://wikimedia.org/api/rest_v1/media/math/render/svg/46693d913892e5dd34c4fddac3bbf82e9bf0f518)
- Distributive Rules
![{\displaystyle P\lor (Q\land R)\leftrightarrow (P\lor Q)\land (P\lor R)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/67f3170bb7df0ff481b2069eb66bf9715fcd218f)
![{\displaystyle P\land (Q\lor R)\leftrightarrow (P\land Q)\lor (P\land R)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/5e5b5cc01e2378665b56340d12a333b47c0d5567)
- De Morgan's Rules
![{\displaystyle \neg (P\lor Q)\leftrightarrow \neg P\land \neg Q}](https://wikimedia.org/api/rest_v1/media/math/render/svg/fd8887b4a97b961022e037eed56a2a0a908166c1)
![{\displaystyle \neg (P\land Q)\leftrightarrow \neg P\lor \neg Q}](https://wikimedia.org/api/rest_v1/media/math/render/svg/4ed798d61bca84996f4cd974fc313140806b4fe8)
(Rule of Double Negation)
- Rules for the Conditional
![{\displaystyle (P\rightarrow Q)\leftrightarrow \neg P\lor Q}](https://wikimedia.org/api/rest_v1/media/math/render/svg/3f2e2acd845b00d34b225cefca4d3d3e9ddec6ea)
![{\displaystyle \neg (P\rightarrow Q)\leftrightarrow P\land \neg Q}](https://wikimedia.org/api/rest_v1/media/math/render/svg/635872c6cd54ecba59a222afa659110a0290c398)
- Rules for the Biconditional
![{\displaystyle (P\leftrightarrow Q)\leftrightarrow (P\rightarrow Q)\land (Q\rightarrow P)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/b4bc3c9615111cfcf01315ff6e05630575eb2ddb)
![{\displaystyle (P\leftrightarrow Q)\leftrightarrow (P\land Q)\lor (\neg P\land \neg Q)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/b695a8a7cd954049db40fd87cc56bc54544879af)
![{\displaystyle (P\leftrightarrow Q)\leftrightarrow (\neg P\lor Q)\land (P\land \neg Q)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/4a1c9e5b7f15917127b6429ab92d6a69bc4bb31d)
- Idempotency Rules
![{\displaystyle P\lor P\leftrightarrow P}](https://wikimedia.org/api/rest_v1/media/math/render/svg/67051d84a1f31be1e4308f3929d022f9beb2814d)
![{\displaystyle P\land P\leftrightarrow P}](https://wikimedia.org/api/rest_v1/media/math/render/svg/0a1a81f1bc52b5c6689fcd0e05f972ac681a42ca)
- Rules of Contraposition
![{\displaystyle (P\rightarrow Q)\leftrightarrow (\neg Q\rightarrow \neg P)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/41cfef3811e9701ee120a56e35134e7ae5673286)
![{\displaystyle (P\rightarrow \neg Q)\leftrightarrow (Q\rightarrow \neg P)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/950afc4cb7e6bec92f47e643a989ef0f181fefce)
![{\displaystyle (\neg P\rightarrow Q)\leftrightarrow (\neg Q\rightarrow P)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/08baa32437be98be9cc3637cdd317830976990d3)
(Rule of Exportation-Importation)
- Rules of Absorption
![{\displaystyle P\lor (P\land Q)\leftrightarrow P}](https://wikimedia.org/api/rest_v1/media/math/render/svg/02539aa3d529d449e20a7b2549804ef6ec73c486)
![{\displaystyle P\land (P\lor Q)\leftrightarrow P}](https://wikimedia.org/api/rest_v1/media/math/render/svg/41dc728e18b1ac1fc7c3d5e9c77fe0248821e64a)
(non-tautological rules)
- Conditional Proof
- If
then ![{\displaystyle \Gamma \vdash P\rightarrow Q}](https://wikimedia.org/api/rest_v1/media/math/render/svg/11d02190e94bf03a172ecc68bcd2b5803b63ba0c)
- Indirect proof
- If
, then ![{\displaystyle \Gamma \vdash P}](https://wikimedia.org/api/rest_v1/media/math/render/svg/9df165f6098a08849309a503060e2b902b1858f9)
(non-tautological rules of the predicate calculus)
- Existential generalization
if the substitution of t for v in ![{\displaystyle \varphi }](https://wikimedia.org/api/rest_v1/media/math/render/svg/33ee699558d09cf9d653f6351f9fda0b2f4aaa3e)
- Existential Proof
- If
, then
, provided that
- The substitution of v for u in
is valid
- v is not free in
![{\displaystyle \varphi }](https://wikimedia.org/api/rest_v1/media/math/render/svg/33ee699558d09cf9d653f6351f9fda0b2f4aaa3e)
- v is not free in
![{\displaystyle \Gamma }](https://wikimedia.org/api/rest_v1/media/math/render/svg/4cfde86a3f7ec967af9955d0988592f0693d2b19)
- Universal Generalization
- If
, then
,
- if v is not free in
.
- Universal Specification
,
- if the substitution of t for v is valid.