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 $\LL_0$ be the language of propositional logic.

Let $\mathscr P$ be a proof system for $\LL_0$.

Let $\FF$ be a collection of logical formulas.

Definition 1

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

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

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

Definition 2

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


Then $\FF$ 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 $\FF$


Proof