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$

  • 1
    $\begingroup$ Okay. What kind of thing is $L$? I'm not sure what "propositional calculus system" means. Could you perhaps clarify by showing an example of a particular $L$ that is (or is not) not consistent? $\endgroup$ – Henning Makholm Jun 24 at 12:52
  • $\begingroup$ @HenningMakholm Thank you for thinking about my question. To make sure, I wrote some definitions. $\endgroup$ – amoogae Jun 24 at 13:14
  • 1
    $\begingroup$ Can you give an example of what an inconsistent system according to that definition could look like? $\endgroup$ – Henning Makholm Jun 24 at 13:19
  • $\begingroup$ @HenningMakholm I think I can't do that. Because the propositional calculus system is consistent. However, my question is to show that "For every proposition symbol $p$ in $L$, $\not \vdash p$" is equivalence condition for consistency. $\endgroup$ – amoogae Jun 24 at 13:27
  • $\begingroup$ So you want to produce an equivalence between two claims of which one is known to be true for every $L$? Then proving that the other one is also true for every $L$ will formally show they're equivalent, but it's a somewhat degenerate kind of equivalence ... $\endgroup$ – Henning Makholm Jun 24 at 14:40

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.

  • $\begingroup$ First-order logic does not have any propositional variables at all, so the right-hand side is pretty trivial in that case... $\endgroup$ – Henning Makholm Jun 24 at 14:41
  • $\begingroup$ For FOL you could replace "propositional variable" with "atomic formula" to make things more meaningful $\endgroup$ – Vsotvep Jun 24 at 14:49

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.

  • $\begingroup$ For the first direction, the real question is how you prove $\vdash q$ and $\vdash \lnot q$ from $\vdash p$. It's not at all trivial. The second direction does not prove anything relevant, it just shows that if the propositional calculus is inconsistent and sound, then it has no models. The assumption that $\not\vdash p$ is irrelevant in this. $\endgroup$ – Vsotvep Jun 25 at 0:46
  • $\begingroup$ @Vsotvep The propositional calculus has a rule of inference called uniform substitution. It states that given a theorem, you can uniformly substitute each instance of a variable within that well-formed formula by any well-formed formula. Thus, given $\vdash$p, $\vdash$q and $\vdash$ $\lnot$q follow by uniform substitution. No, the second direction does not work as you think. First you assume inconsistency Then a contradiction gets derived. So, we can remove the negation the assumption of inconsistency giving consistency (check the propositional calculus... CCNpqCCNpNqp is a tautology). $\endgroup$ – Doug Spoonwood Jun 25 at 18:26

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.