Axiom Problems (Intro to Computer Logic)

Question

"Show that—or prove that—$ \Gamma \vdash A $" means "write a $ \Gamma $-proof that establishes $ A $". The proof can be Equational or Hilbert-style.

Show that $ A \equiv C \vdash A \rightarrow (B \rightarrow C) $

I am not sure if I did this right..

Proving RHS:

$$ \begin{align} A \rightarrow (B \rightarrow C) &\ \ \langle \mbox{Implication, properties of} \rightarrow \rangle \\ A → (B \lor C) &\ \ \langle \mbox{Implication, properties of} \rightarrow \rangle \\ A → (C) &\ \ \langle \mbox{Implication, properties of} \rightarrow \rangle \\ A \lor C &\ \ \langle \mbox{Golden Rule, Properties of } \ \lor \rangle \\ A \equiv C &, \end{align} $$

Therefore I proved RHS to LHS

List of Axioms

Associativity of $ \equiv $

• $ ((A \equiv B) \equiv C) \equiv (A \equiv (B \equiv C)) $ (1)

Symmetry of $ \equiv $

• $ (A \equiv B) \equiv (B \equiv A) $ (2)

Properties of $ \bot $, $ \top $

• $ \top \equiv \bot \equiv \bot $ (3)

Properties of $ \neg $

• $ \neg A \equiv A \equiv \bot $ (4)

Properties of $ \lor $

• $ (A \lor B) \lor C \equiv A \lor (B \lor C) $ (5)
• $ A \lor B \equiv B \lor A $ (6)
• $ A \lor A \equiv A $ (7)
• $ A \lor (B \equiv C) \equiv A \lor B \equiv A \lor C $ (8)
• $ A \lor \neg A $ (9)

Properties of $ \land $

• Golden Rule: $ A \land B \equiv A \equiv B \equiv A \lor B $ (10)

Properties of $ \rightarrow $

• Implication: $ A \rightarrow B \equiv A \lor B \equiv B $ (11)

Answer 1

We cannot prove it only by "chain-of-equivalences", because the conclusion is implied by the premise but it is not equivalent to it.

Thus we need rules of inference, e.g. Equanimity :

$\dfrac {A, A \equiv C} {C}$

In addition, we can use two meta-theorems :

Hypothesis Strengthening : If $\Gamma \vdash A$ and $\Gamma \subseteq \Delta$, then also $\Delta \vdash A$

and the

Deduction Theorem : If $\Gamma \cup \{ A \} \vdash B$, then also $\Gamma \vdash A \to B$.

---

Proof :

1) $\{ A \equiv C, A \} \vdash C$ --- Equanimity

2) $\{ A \equiv C, A, B \} \vdash C$ --- Hypothesis Strengthening

3) $\{ A \equiv C, A \} \vdash B \to C$ --- Deduction Th

4) $A \equiv C \vdash A \to (B \to C)$ --- Deduction Th.