How is Post's tautology theorem used in this proof?

Question

Could someone please explain to me how does the proof of I.4.3 reference I.4.1?

In I.4.3, you are given hypotheses about A and B being theorems. However, I.4.1 talks about tautologies (as inputs) not theorems.

How can someone use $\Gamma \vdash A$ + something about tautologies to yield $\Gamma \vdash B \implies A$?

See :Tourlakis (2003), Lectures in logic and set theory.

Answer 1

We have to use I.3.7 Definition (Tautologically Implies), page 31 :

Let $\mathcal A$ and $\Gamma$ be respectively any formula and any set of formulas. The symbol $\Gamma \vDash_{\text{Taut}} \mathcal A$, pronounced “$\Gamma$ tautologically implies $\mathcal A$”, means that every truth assignment $v$ that satisfies $\Gamma$ also satisfies $\mathcal A$.

We have $\mathcal A \vDash_{\text{Taut}} \mathcal B \to \mathcal A$ as well as $\mathcal B \vDash_{\text{Taut}} \mathcal A \to \mathcal B$.

We have to use them in the proof of :

I.4.3 Metatheorem. Any two theorems $\mathcal A$ and $\mathcal B$ are provably equivalent (page 42).

Assume $\Gamma \vdash \mathcal A$.

Using I.4.1 Metatheorem (Post’s “Extended” Tautology Theorem), we have $\mathcal A \vdash \mathcal B \to \mathcal A$.

Thus, by properties of $\vdash$, we get : $\Gamma \vdash \mathcal B \to \mathcal A$.

In the same way, from $\Gamma \vdash \mathcal B$ we have : $\Gamma \vdash \mathcal A \to \mathcal B$.

Finally, using : $\mathcal A \to \mathcal B, \mathcal B \to \mathcal A \vDash_{\text{Taut}} \mathcal A \leftrightarrow \mathcal B$, we conclude with :

$\Gamma \vdash \mathcal A \leftrightarrow \mathcal B$.

Answer 2

In Hilbert style proof systems, it is usually an axiom that the schema $\phi\to(\psi\to \phi)$ is tautological.   Additionally, Modus Ponens is a fundamental rule of inference (typically the only fundamental rule).

So since $A\to(B\to A)$ is a tautology, and using Modus Ponens, therefore if can you derive $A$, then you may infer that $B\to A$ is derivable in the same context.$$\begin{split}\Gamma &\vdash A&&\textsf{derived somehow}\\&\vdash A\to(B\to A)&\qquad&\textsf{via axiom P2}\\\hline\Gamma &\vdash B\to A&&\textsf{via modus ponens} \end{split}$$