Metaproving 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 :



 A: 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 !


