---
# System prepended metadata

title: 'Lab: Propositional Proofs'

---

# Lab: Propositional Proofs

## Problem: 1

Claim 1

$\cdot $

proof:
* x:A-->B, $\vdash$ A-->B [assumption x]
* by assumption x A-->B is equivalent to (A --> B) and can be substituted

* A implies (A-->B) which implies (B-->C) which implies C. Therefore A-->C

Claim 2:
proof:
* $h:A\vdash(A \rightarrow B)\rightarrow (B\rightarrow C)\rightarrow C$
* $[intro \rightarrow ]$
* $h:A, x:(A \rightarrow  B)$\vdash$(B\rightarrow  C) \rightarrow C$
* $[intro \rightarrow ]$
* $h:A, x:(A \rightarrow B), y:(B\rightarrow C)\vdash C $

    + $h:A, x:(A\rightarrow  B), y:(B\rightarrow C)\vdash A$
    + [Assumption h]
    + $h:A, x:(A\rightarrow  B), y:(B\rightarrow C), z:B\vdash A$
* $h:A, x:(A\rightarrow  B), y:(B\rightarrow C), z:B\vdash C$
    * $h:A, x:(A\rightarrow  B), y:(B\rightarrow C), z:B\vdash B$
    * [Assumption z]
* $h:A, x:(A\rightarrow  B), y:(B\rightarrow C), z:B\vdash B$
* $[elim \rightarrow ]$
* $h:A, x:(A\rightarrow  B), y:C, z:B\vdash C$
* [Assumption y]


Problem 2: Logical Equivalences
* $\vdash p \wedge p ≡ p$
* $[elim-\wedge -left]$
* $x:p\vdash  p ≡ p$
* [Assumption x]
According to $elim-\wedge -left$ proof rule p is equivalent to p and this is confirmed by logical equivalence which can rewrite p ≡ p as $ p\rightarrow p$.

Claim 2:
* $\vdash p \vee ( p\wedge q) ≡ p
* $[intro \vee left]$
    * $\vdash p ≡ p$
According to $intro \vee left$ proof rule p is equivalent to p and this is confirmed by logical equivalence which can rewrite p ≡ p as $p\rightarrow p$.