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?
Claim:
No such theorems exist.
Discussion:
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.
Definitions:
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.
