Discharging an assumption for a theorem

103 Views Asked by At

So it's my understanding that theorems do not rely on an assumption set. However, this theorem that I have come across seems like I will have to make at least one undischarged assumption.

$$├ (P \rightarrow Q) \lor (Q \lor R)$$

My initial approach was to use arrow introduction, so assume P then eventually discharge it once I had gotten Q. But I just don't see how I can get Q.

The rest of the theorem I can get using wedge introduction once I have one of the sides, I just don't see a way to get them.

1

There are 1 best solutions below

0
On

As noted above, this "theorem" is false: making $P$ true and $Q$ and $R$ false results in $(P\rightarrow Q)\vee (Q\vee R)$ being false.


Separately, it's also worth noting that a theorem with hypotheses can be turned into a theorem without hypotheses:

  • If $\varphi_1,...,\varphi_n\vdash\psi$, then $\vdash (\varphi_1\wedge ...\wedge\varphi_n)\rightarrow\psi$; this is the deduction theorem.

  • What about if we have $\Gamma\vdash \psi$ where $\Gamma$ is infinite (so we can't take the conjunction of everything in $\Gamma$)? Well, proofs can only involve finitely many propositions, so there is some finite $\{\varphi_1,...,\varphi_n\}\subseteq\Gamma$ such that $\varphi_1,...,\varphi_n\vdash\psi$; and now we're in the situation above.

In a previous edit I mentioned the compactness theorem in the context of the second bulletpoint above. This was a slip-up on my part: the compactness theorem is about $\models$, not $\vdash$. Of course they're actually equivalent, but this question is about $\vdash$ instead of $\models$ and $\vdash$ is "finitary" by definition; so compactness isn't relevant here.