Let $A$ be a set of propositional symbols, $\alpha$ ba a WFF on $A$ and $M$ be a subset of $A$. And let $M^+: = M \cup \{(\neg a): a\in (A-M)\}$. Then, only one of $M^+ \vdash \alpha$ or $M^+ \vdash \neg \alpha$ be true.

I think this proposition is true. Because the propositional logic system is complet. But can we prove this proposition only in syntactic ways without thinking semantics? And please let me know if this proposition has a name.

  • $\begingroup$ If I have correctly understood your question, the result in your post is a rather direct consequence of the Soundness and Completeness of the Propositional Calculus. $\endgroup$ – Ramiro Apr 18 at 11:37
  • $\begingroup$ See Kalmar's proof of completeness. You can find it also in Mendelson's textbook. $\endgroup$ – Mauro ALLEGRANZA Apr 18 at 11:50
  • $\begingroup$ @Ramiro I think so too. I just wonder if we can prove this without thinking of semantics. $\endgroup$ – amoogae Apr 18 at 11:51

Sure, this can be proven purely syntactically. It's probably easiest just to do a straight induction on formulas. To minimize the amount of work, assume $\neg$ and $\land$ are the only connectives (all others being defined in terms of these).

The base case is a proposition variable $p\in A$. By definition of $M^{+}$, either $p\in M^{+}$ or $\neg p\in M^{+}$ so we can prove $M^{+}\vdash p$ or $M^{+}\vdash\neg p$ immediately by assumption.

For the $\land$ case, we have two cases: either $M^{+}\vdash\alpha_i$ for $i\in\{1,2\}$ in which case we can immediately prove $M^{+}\vdash\alpha_1\land\alpha_2$, or $M^{+}\vdash\neg\alpha_i$ for some $i\in\{1,2\}$ from which it is easy to prove $M^{+}\vdash\neg(\alpha_1\land\alpha_2)$.

Finally, for the $\neg$ case, we have either $M^{+}\vdash\alpha$ or $M^{+}\vdash\neg\alpha$ by induction hypothesis, and we want to show $M^{+}\vdash\neg\alpha$ or $M^{+}\vdash\neg\neg\alpha$. Clearly, if we have $M^{+}\vdash\neg\alpha$, we are done immediately. Otherwise, we have $M^{+}\vdash\alpha$ from which we can prove $M^{+}\vdash\neg\neg\alpha$ with a standard proof.

Normally the problem is the base case. We usually can't say anything one way or the other about proposition variables.

Now, to be precise, this doesn't quite prove the claim. This only proves that $M^{+}\vdash\alpha$ or $M^{+}\vdash\neg\alpha$. It doesn't show that only one of these is true. If you can show $M^{+}\nvdash\bot$, that would establish it though. Alternatively, you could modify the above proof fairly easily to cover the exact claim given an assumption (or proof) of consistency, i.e. $\nvdash\bot$.

  • $\begingroup$ Thank you very much. But I have one more question, is it possible to prove "only one" part syntactically? I think this is impossible because syntax tells us that "some WFF is provable," but it does not tell us that "some WFF is not provable." If I misunderstand something, please let me know. $\endgroup$ – amoogae Apr 19 at 13:04
  • 1
    $\begingroup$ @amoogae You can definitely prove consistency syntactically given a proof system. This is what Gentzen did for classical first-order logic using the sequent calculus. Proving consistency by showing soundness is usually much less technical. Propositional logic is much simpler, though. The approach would be induction on derivations in your proof system to show that no (closed) derivation ends in $\bot$. $\endgroup$ – Derek Elkins Apr 19 at 20:12

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.