Ref : Peter Andrews, An Introduction to Mathematical Logic and Type Theory To Truth Through Proof (1986).

Exercise X1210 :

Does $\mathscr{P}$ have any theorems in which there are no occurrences of disjunction?


No such theorems exist.


I think I should prove this by assuming that such a theorem exists and then look for a contradiction. However, I am unsure how to proceed. Can someone give me some pointers? I am studying mathematical logic on my own and occasionally have problems with the exercises. I will be grateful for any help.


Let $\mathscr{P}$ be the following ligistic system:

The set of wffs of $\mathscr{P}$ is the intersection of all sets $\mathscr{S}$ of formulas such that:

(i) $\mathbf{p} \in \mathscr{S}$ for each propositional variable $\mathbf{p}$.

(ii) For each formula $\mathbf{A}$ if $\mathbf{A} \in \mathscr{S}$, then $\mathord{\sim} \mathbf{A} \in \mathscr{S}$.

(iii) For all formulas $\mathbf{A}$ and $\mathscr{B}$, if $\mathbf{A} \in \mathscr{S}$ and $\mathbf{B} \in \mathscr{S}$, then $\left[\mathbf{A} \lor \mathbf{B} \right] \in \mathscr{S}$.

The Axioms of $\mathscr{P}$ are

(1) $\mathord{\sim} \left[ \mathbf{A} \vee \mathbf{A} \right] \vee \mathbf{A}$

(2) $\mathord{\sim} \mathbf{A} \vee {}_\blacksquare \mathbf{B} \vee \mathbf{A}$

(3) $\mathord{\sim} \left[ \mathord{\sim} \mathbf{A} \vee \mathbf{B} \right] \vee {}_\blacksquare \mathord{\sim} \left[ \mathbf{C} \vee \mathbf{A} \right] \vee {}_\blacksquare \mathbf{B} \vee \mathbf{C}$

$\mathscr{P}$ has one rule of inference:

Modus Ponens (MP). From $\mathbf{A}$ and $\mathord{\sim} \mathbf{A} \vee \mathbf{B}$ to infer $\mathbf{B}$.

A theorem of $\mathscr{p}$ is defined as follows:

Def1. A proof of a wff $\mathbf{B}$ from the set $\mathscr{H}$ of hypotheses is a finite sequence $\mathbf{B}_1,\ldots,\mathbf{B}_m$ of wffs such that $\mathbf{B}_m$ is $\mathbf{B}$ and for each $j$ ($1 \leq j \leq m$) at least one of the following conditions is satisfied:

(1) $\mathbf{B}_j$ is an axiom.

(2) $\mathbf{B}_j$ is an member of $\mathscr{H}$.

(3) $\mathbf{B}_j$ is inferred by modus ponents from wffs $\mathbf{B}_i$ and $\mathbf{B}_k$, where $i < j$ and $k < j$.

Def2. A proof of a wff $\mathbf{B}$ is a proof of $\mathbf{B}$ from the emtpy set of hypotheses.

Def3. A theorem is a wff which has a proof.

  • $\begingroup$ Hint: There are very few formulas that are disjunction-free. $\endgroup$ – André Nicolas Nov 26 '13 at 2:36
  • $\begingroup$ @AndréNicolas The wffs which are disjunction-free consist of the propositional variables and formulas of the form $\mathord{\sim} \mathbf{A}$ where $\mathbf{A}$ is also disjunction-free. So I guess I need to prove that neither of these is a theorem. $\endgroup$ – Code-Guru Nov 26 '13 at 2:38
  • $\begingroup$ That's right, they are all a finite string of $\sim$ followed by a propositional variable. The easiest approach is semantic, if a formula is a theorem then it has truth value T under all truth assignments to its propositional variables. $\endgroup$ – André Nicolas Nov 26 '13 at 2:47
  • $\begingroup$ @AndréNicolas So I'm probably just making this harder than it is. Such formulas cannot have a value of truth under all assignments. Since there is only one propositional variable, there are only two assignments. One of these will result in a value of truth and one will result in a value of falsehood. $\endgroup$ – Code-Guru Nov 26 '13 at 2:51
  • $\begingroup$ That's under the assumption that the result "if a formula is a theorem $\dots$" that I mentioned earlier has already been proved. If it hasn't, one has to prove it, a fairly straightforward induction on the length of a proof. But that's a much bigger and more important thing than this exercise. $\endgroup$ – André Nicolas Nov 26 '13 at 2:55

Your Answer

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

Browse other questions tagged or ask your own question.