Metaproving Question.

Question

Prove that $ \vdash ((A \rightarrow B) \rightarrow A) \rightarrow A $

I want to make sure my answer is right as the textbook has no solutions.

I am using Equational Proof. The textbook is "Mathematical Logic" For Tourlakis.

My answer :

$$ ((A \rightarrow B) \rightarrow A) \rightarrow A $$ $$ \Rightarrow \ <axiom + leib; c-part:(p\rightarrow A)\rightarrow A; p \ fresh>$$ $$ ((A \lor B \equiv B)\rightarrow A)\rightarrow A$$ $$\Rightarrow <axiom + leib; c-part: p \rightarrow A; p\ fresh>$$ $$(A \lor B \equiv B \lor A \equiv A) \rightarrow A$$ $$\Rightarrow <axiom + leib: c-part : A \lor B \equiv B \lor p\ ; p\ fresh>$$ $$(A \lor B \equiv B \lor T) \rightarrow A$$ $$\Rightarrow <axiom + leib: c-part : A \lor p \lor T:\ p\ fresh>$$ $$(A \lor T \lor T)\rightarrow A$$ $$\Rightarrow <axiom + leib ; c-part: (A \lor p) \rightarrow A; p\ fresh>$$ $$(A \lor T) \rightarrow A$$ $$\Rightarrow<axiom>$$ $$A \lor T \lor A \equiv A$$ $$\Rightarrow <axiom + leib; c-part: p \lor T \equiv A ; p\ fresh>$$ $$A \lor T \equiv A$$ $$\Rightarrow <axiom>$$ $$A \lor A \equiv T$$ $$\Rightarrow <axiom>$$ $$A \equiv T$$ $$\Rightarrow<axiom>$$ $$A$$

Axioms and theorems :

Answer 1

Prove that

$ \vdash ((A \rightarrow B) \rightarrow A) \rightarrow A $

in Equational Logic [all references to the textbook of George Tourlakis, Mathematical Logic (2008)].

I think that we must use 2.6.1 Metatheorem. (Deduction Theorem) :

If $\Gamma \cup \{ C \} \vdash D$, then also $\Gamma \vdash C \rightarrow D$.

This theorem allows us to "reduce the complexity" of the formula to be proved, starting from the "assumption" $C$ and deriving $D$.

In our case :

$\Gamma = \emptyset $ , $\quad C$ will be $(A \rightarrow B) \rightarrow A \quad $ and $\quad D$ will be $A$.

I will use the Equational Proof Layout [page 65], as done by the OP, i.e. a chain of equivalences with annotations : $A_1 \Leftrightarrow$ (annotation) ... $\Leftrightarrow$ (annotation) $A_n$

Having said that, we will start with :

$$ (A \rightarrow B) \rightarrow A $$ $$ \Leftrightarrow \ < \text{axiom + Leib; "C-part" is} \ p \rightarrow A \ >$$

Note. We have used axiom (11) : Implication [page 43] : $A \rightarrow B \equiv A \lor B \equiv B$, and we have used Equanimity and Leibniz merged, that is the "derived rule" [see Tourlakis, page 57, 2.1.16 Theorem (Eqn + Leib Merged)] : $C[p := A], A \equiv B \vdash C[p := B]$; we will call it "Leib".

$$ (A \lor B \equiv B)\rightarrow A$$ $$\Leftrightarrow \ < \text{axiom + Leib; "C-part" is} \ (A \lor B) \equiv B \equiv p \ >$$

Note. We have used as axiom : Th.2.4.11 [page 70] : $\vdash C \rightarrow A \equiv \lnot C \lor A$. $$\lnot [(A \lor B) \equiv B ]\lor A$$ $$\Leftrightarrow \ < \text{axiom + Leib; "C-part" is} \ p \lor A \ >$$

Note. We have used axiom (4) : Introduction of $\lnot$ : $\lnot A \equiv A \equiv \bot$. $$((A \lor B )\equiv B) \equiv \bot) \lor A$$ $$\Leftrightarrow \ < \text{axiom + Leib, with axiom (8) : Distributivity of} \lor \text{over} \equiv \ >$$ $$[(A \lor B) \equiv B] \lor A \equiv A \lor \bot$$ $$\Leftrightarrow \ < \text{axiom + Leib, where axiom is Th.2.4.10} \vdash A \lor \bot \equiv A \ >$$ $$[(A \lor B) \equiv B] \lor A \equiv A $$ $$\Leftrightarrow \ < \text{axiom + Leib, with axiom (8) : Distributivity of} \lor \text{over} \equiv \ >$$ $$(A \lor B) \lor A \equiv (A \lor B) \equiv A$$ $$\Leftrightarrow \ < \text{by axioms (5) and (6) : Associativity and Symmetry of} \lor \ >$$ $$(A \lor A) \lor B \equiv A \lor B \equiv A$$ $$\Leftrightarrow \ < \text{by axiom (7) : Idempotency of} \lor \ >$$ $$A \lor B \equiv A \lor B \equiv A$$ $$\Leftrightarrow \ < \text{axiom + Equanimity, where axiom is Th.2.1.12} \vdash A \equiv A \ >$$ $$A$$

Finally having derived $A$ from the "assumption" $(A \rightarrow B) \rightarrow A$, i.e.

$(A \rightarrow B) \rightarrow A \vdash A$

we may invoke the Deduction Theorem [2.6.1 Metatheorem] and conclude :

$\vdash ((A \rightarrow B) \rightarrow A) \rightarrow A$.

Please, check !