Implement Rules of Inference

[ed963]

• Definition 2.4.5. If $\Gamma$ is a finite set of $\cal L$-formulas, $\phi$ is an $\cal L$-formula, and $\phi$ is a propositional consequence of $\Gamma$, then $(\Gamma, \phi)$ is a rule of inference of type (PC).
• Definition 2.4.6. Suppose that the variable $x$ is not free in the formula $\psi$. Then both of the following are rules of inference of type (QR):
  • $({\psi\rightarrow\phi}, \psi\rightarrow(\forall x\phi))$
  • $({\phi\rightarrow\psi}, (\exists x\phi)\rightarrow\psi)$

[ed963]

5581d0531f6e48fd12b63fd22276f3f460ceb24a