Rule of Conjunction/Sequent Form/Formulation 2

From ProofWiki
Jump to navigation Jump to search

Theorem

The Rule of Conjunction can be symbolised by the sequent:

$\vdash p \implies \paren{ q \implies \paren{ p \land q } }$


Proof

This proof is derived in the context of the following proof system: Instance 2 of the Hilbert-style systems.

By the tableau method:

$\vdash p \implies \paren{ q \implies \paren{ p \land q } }$
Line Pool Formula Rule Depends upon Notes
1 $\neg p \lor p$ Law of Excluded Middle
2 $\paren{ \neg p \lor p } \implies \paren{ p \lor \neg p }$ Axiom $A3$ $\neg p \,/\, p, p \,/\, q$
3 $p \lor \neg p$ Rule $RST \, 3$ 1,2
4 $\paren{ \neg p \lor \neg q } \lor \neg \paren{ \neg p \lor \neg q }$ Rule $RST \, 1$ 3 $\paren{ \neg p \lor \neg q } \,/\, p$
5 $\paren{ \neg p \lor \neg q } \lor \paren{ p \land q }$ Rule $RST \, 2 (1)$
6 $\paren{ \paren{ \neg p \lor \neg q } \lor \paren{ p \land q } } \implies \paren{ \neg p \lor \paren{ \neg q \lor \paren{ p \land q } } }$ Rule of Association $\neg p \,/\, p, \neg q \,/\, q, \paren{ p \land q } \,/\, r$
7 $\neg p \lor \paren{ \neg q \lor \paren{ p \land q } }$ Rule $RST \, 3$ 5,6
8 $p \implies \paren{ q \implies \paren{ p \land q } }$ Rule $RST \, 2 (2)$ 7

$\blacksquare$


Sources