2

I need help about proving the following sequent:

$$ \vdash Q \rightarrow (P \rightarrow Q) $$

I tried to prove it by trying to introduce a conditional proof, but somehow can't get the suppositions correctly in the beginning. I would appreciate some help.

Additionally, here is another similar sequent I've supposedly proved, but not completely sure:

$$ \vdash Q \rightarrow (P \rightarrow P) $$

Stackoverflow doesn't let me insert a picture yet, so this is a link to the proof.

Explanations for the proof:

CP: Conditional Proof Introduction

A: Assumption

Leftmost Column: Score-board for keeping track of suppositions.

I'd appreciate any help and suggestions.

Mauro ALLEGRANZA
  • 94,169
itsafox
  • 21

3 Answers3

2

Try the following:

  1. $Q$ (Assumption)
  2. --- $P$ (Assumption)
  3. --- --- $Q$ (Restating 1)
  4. --- $P \rightarrow Q$ (Conditional proof discharging assumption 2)
  5. $Q \rightarrow (P \rightarrow Q)$ (Conditional proof discharging assumption 1)

The tricky bit here is understanding what role line 3 plays: we need to restate the first assumption to make it the conclusion of the second inner proof which starts by assuming $P$.

Chessanator
  • 5,448
2

The conditional proofs are rather similar. For the second you have.

  • Suppose $Q$. Suppose $P$. Reiterate $P$. Discharge the assumptions.

[Well, the reiteration is redundant, but shows how they are similar.]

$$\def\fitch#1#2{\quad\begin{array}{|l}#1\\\hline#2\end{array}}\begin{array}{l}\begin{array}{l}\text{The above}\\\fitch{}{\fitch{~~1.~Q}{\fitch{~~2.~P}{~~3.~P}\\~~4.~P\to P}\\~~5.~Q\to(P\to P)}\end{array}&&\begin{array}{l}\text{What you had (also valid)}\\\fitch{}{\fitch{~~1.~Q}{\fitch{~~2.~P}{~}\\~~3.~P\to P}\\~~4.~Q\to(P\to P)}\end{array}\end{array}$$

Just do the same for the first proof.

  • Suppose $Q$. Suppose $P$. Reiterate $Q$. Discharge the assumptions.

tl;dr Basically what you need is the rule of reiteration. If something was derivable under a subset of the current assumptions, you may inference it.

In your system, anything derived (or assumed) under assumptions (1) or (2) may be inferenced to hold under (1)(2).

Graham Kemp
  • 129,094
0

Here are both proofs providing results similar to the other answers but in a Fitch-style proof checker:

enter image description here

Line 3 using reiteration (R) repeating line 1.

enter image description here

Note that line 2 is both the antecedent and consequent of the conditional represented as a subproof with only one line 2-2.

Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/

Frank Hubeny
  • 1,527