Equivalence of Definitions of Consistent Set of Formulas

From ProofWiki
Jump to navigation Jump to search

Theorem

The following definitions of the concept of Consistent Proof System for Propositional Logic are equivalent:


Let $\mathcal L_0$ be the language of propositional logic.

Let $\mathscr P$ be a proof system for $\mathcal L_0$.

Let $\mathcal F$ be a collection of logical formulas.

Definition 1

Then $\mathcal F$ is consistent for $\mathscr P$ if and only if:

There exists a logical formula $\phi$ such that $\mathcal F \not \vdash_{\mathscr P} \phi$

That is, some logical formula $\phi$ is not a $\mathscr P$-provable consequence of $\mathcal F$.

Definition 2

Suppose that in $\mathscr P$, the Rule of Explosion (Variant 3) holds.


Then $\mathcal F$ is consistent for $\mathscr P$ if and only if:

For every logical formula $\phi$, not both of $\phi$ and $\neg \phi$ are $\mathscr P$-provable consequences of $\mathcal F$


Proof