Equivalence condition of consistency of the system

Question

I read the following statement in my modal logic book.

Propositional calculus system $L$ is consistent if and only if for every proposition symbol $p$ in $L$, $\not\vdash p$

I wonder how to prove this statement. And is this also true in FOL?

---

To make sure, I write some definitions here.

The propositional calculus system $ L $ is a formal system $(A,C)$ where:

a) The set $A$ is a countably infinite set of proposition symbols.

b) The set $C$ is a set of logical connectives, that is $\{\neg, \vee, \wedge, \to \}$.

And we use natural deduction as a proof system. And by definition, system $L$ with the proof system is consistent if and only if there is no WFF $\alpha$ such that $\vdash \alpha$ and $\vdash \neg \alpha$

Answer 1

I don't know what kind of natural deduction system you use, so the details might look different, but the process should be the same for any natural deduction system.

For one direction, assume $L$ is inconsistent, so there is a WFF $\alpha$ such that $\vdash\alpha$ and $\vdash\lnot\alpha$. Then:

1. Prove that $\vdash \alpha\land\lnot\alpha$
2. Prove that $\vdash(\alpha\land\lnot\alpha)\to p\quad\quad$ (probably using an axiom called "tertium non datur" / "principle of excluded middle" or a rule called the "ex falsum quodlibet" / "principle of explosion")
3. Prove that $\vdash p$

For the other direction, assume that $L$ in consistent. Check that $\vdash p$ is not an instance of an axiom (scheme), and show that $\vdash p$ cannot be the conclusion of any of the derivation rules, except if we had proved $\vdash\alpha\land\lnot\alpha$ in an earlier step (it might be your system uses $\bot=\alpha\land\lnot\alpha$ instead, as the symbol for contradiction). Then use that if $\vdash\alpha\land\lnot\alpha$ was proved earlier, we could reshape that proof to prove $\vdash\alpha$ and $\vdash\lnot\alpha$.

---

All of the steps in this are valid rules in (classical) propositional logic, and all rules of propositional logic are valid in FOL, so yes, this does also work in FOL. Furthermore, you mention that this is a book about modal logic, and all propositional logic is also valid in ML, so this works in ML as well.

Answer 2

The following should work for any propositional calculus where the axioms are tautologies and the rules of inference are valid.

Suppose that L is consistent. Then there is no formula q such that $\vdash$ q and $\vdash$ $\lnot$q. Suppose that there existed some propositional symbol p such that $\vdash$ p. But then, $\vdash$ q as well as $\vdash$ $\lnot$q. Consequently, it follows that ⊬ p for an arbitrary propositional symbol. Thus, for every propositional symbol ⊬ p.

Suppose that for every propositional symbol p, ⊬ p. Suppose that propositional calculus is inconsistent. Then, by definition, there exists some formula q such that $\vdash$ q and $\vdash$ $\lnot$q. Propositional calculus is sound, so it would follow that |= q and |= $\lnot$q. But, then propositional calculus would entail both a true and a false statement, since either q or $\lnot$ q is true and the other is false. But, then propositional calculus would be unsound. Thus, the soundness theorem would lead to a contradiction of itself. But, the soundness theorem holds by assumption. So, propositional calculus is consistent.