Contained here are the main equivalences and inference rules for the COMP-2310 class at UWindsor.
Equivalences
E1. \( \alpha \land \sim \alpha \equiv false \)
E2. \( \alpha \lor \sim \alpha \equiv true \)
E3. \( \alpha \land \alpha \equiv \alpha \)
E4. \( \alpha \lor \alpha \equiv \alpha \)
E5. \( \alpha \land true \equiv \alpha \)
E6. \( \alpha \lor false \equiv \alpha \)
E7. \( \alpha \land false \equiv false \)
E8. \( \alpha \lor true \equiv true \)
E9. \( \alpha \land \beta \equiv \beta \land \alpha \)
E10. \( \alpha \lor \beta \equiv \beta \lor \alpha \)
E11. \( (\alpha \land \beta) \land \gamma \equiv \alpha \land (\beta \land \gamma) \)
E12. \( (\alpha \lor \beta) \lor \gamma \equiv \alpha \lor (\beta \lor \gamma) \)
E13. \( \alpha \land (\beta \lor \gamma) \equiv (\alpha \land \beta) \lor (\alpha \land \gamma) \)
E14. \( \alpha \lor (\beta \land \gamma) \equiv (\alpha \lor \beta) \land (\alpha \lor \gamma) \)
E15. \( \sim \sim \alpha \equiv \alpha \)
E16. \( \sim (\alpha \land \beta) \equiv (\sim \alpha \lor \sim \beta) \)
E17. \( \sim (\alpha \lor \beta) \equiv (\sim \alpha \land \sim \beta) \)
E18. \( \alpha \implies \beta \equiv \sim \alpha \lor \beta \)
E19. \( \alpha \implies \beta \equiv \sim \beta \implies \sim \alpha \)
E20. \( (\alpha \implies \beta) \land (\beta \implies \alpha) \equiv \alpha \iff \beta \)
Inference Rules
I1. \( \frac{p}{p \lor q} \)
I2. \( \frac{p \land q}{p} \)
I3. \( \frac{p, p \implies q}{q} \)
I4. \( \frac{\sim q, p \implies q}{\sim p} \)
I5. \( \frac{p \implies q, q \implies r}{p \implies r} \)
I6. \( \frac{p, q}{p \land q} \)
First-Order Logic Equivalences
FE1. \( (\forall x)\alpha(x) \equiv (\forall y)\alpha(y) \quad (\alpha(x) \text{ does not contain } y) \)
FE2. \( (\exists x)\alpha(x) \equiv (\exists y)\alpha(y) \quad (\alpha(x) \text{ does not contain } y) \)
FE3. \( (\forall x)\alpha(x) \lor \beta \equiv (\forall x)(\alpha(x) \lor \beta) \quad (\beta \text{ contains no free occurrence of } x) \)
FE4. \( (\exists x)\alpha(x) \lor \beta \equiv (\exists x)(\alpha(x) \lor \beta) \quad (\beta \text{ contains no free occurrence of } x) \)
FE5. \( (\forall x)\alpha(x) \land \beta \equiv (\forall x)(\alpha(x) \land \beta) \quad (\beta \text{ contains no free occurrence of } x) \)
FE6. \( (\exists x)\alpha(x) \land \beta \equiv (\exists x)(\alpha(x) \land \beta) \quad (\beta \text{ contains no free occurrence of } x) \)
FE7. \( \sim (\forall x)\alpha(x) \equiv (\exists x)\sim \alpha(x) \)
FE8. \( \sim (\exists x)\alpha(x) \equiv (\forall x)\sim \alpha(x) \)
FE9. \( (\forall x)\alpha(x) \land (\forall x)\beta(x) \equiv (\forall x)(\alpha(x) \land \beta(x)) \)
FE10. \( (\exists x)\alpha(x) \lor (\exists x)\beta(x) \equiv (\exists x)(\alpha(x) \lor \beta(x)) \)
First-Order Logic Inference Rules
Gen: Generalization
\( \frac{\alpha(x)}{(\forall x)\alpha(x)} \)
\( x \text{ is a variable} \)
UI: Universal Instantiation
\( \frac{(\forall x)\alpha(x)}{\alpha(t)} \)
\( \alpha(x) \text{ is free for } t \text{ (} t \text{ is a variable or constant)} \)
\( \text {where }\alpha(t) \text{ results from } \alpha(x) \text{ after all free occurrences of x in } \alpha(x) \text{ are replaced by } t \)
EQ: Existential Quantification
\( \frac{\alpha(t)}{(\exists x)\alpha(x)} \)
\( \alpha(x) \text{ is free for } t \text{ (} t \text{ is a variable or constant)} \)
\( \text {where }\alpha(x) \text{ results from } \alpha(t) \text{ after some (may be all) free occurences of t in } \alpha(t) \text{ are replaced by } x \)