COMP-2310 Formula Cheatsheet

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$