A basic question about $\Rightarrow$

Question

I am a beginner in mathematical logic. Sometimes I find expressions like the following

$$\textrm{PA}\vdash A\implies \textrm{PA}\vdash B\tag{$\star$}$$

For example, in Hilbert-Bernays-Lob derivability conditions, I find: $$\textrm{PA}\vdash A\implies \textrm{PA}\vdash\Box A$$

I wonder what the difference is between $(\star)$ and $(\star\star)$?

$$\textrm{PA}\vdash A\to B\tag{$\star\star$}$$

Thanks in advance!

Answer 1

Lets do an example with something other than $\textrm{PA}$.

Say $\textrm{GT}$ is group theory. Say $A$ is "$\forall x, x^2 = e$", that is, every element has order $1$ or $2$. Say $B$ is "$\forall x, x^3 = e$", that is, every element has order $1$ or $3$.

Now $\textrm{GT} \vdash A$ and $\textrm{GT} \vdash B$ are both false. (Group $\mathbb Z/5$ fails both properties, so of course $\textrm{GT}$ cannot prove either one.) Thus

$$ \textrm{GT}\vdash A\;\Longrightarrow\; \textrm{GT}\vdash B\quad\quad(*) $$ is true. On the other hand, GT cannot prove $A \rightarrow B$. (Group $\mathbb Z/2$ satisfies $A$ but not $B$). Thus $$ \textrm{GT}\vdash A\rightarrow B\quad\quad(**) $$ is false.

---

Advice: Don't try to understand logic applied to arithmetic, until you already understand logic applied to more mundane topics (like group theory).

Answer 2

While $(ii)\rightarrow (i)$ is easy to establish per the comments, the other direction breaks down in general - because our metatheory might be too strong for its results to "reflect" down to $\mathsf{PA}$.

(That said, if we're careful about our metatheory we may indeed salvage $(i)\rightarrow (ii)$. But usually we work in a metatheory much stronger than $\mathsf{PA}$ unless explicitly stated otherwise.)

---

An expression like $$\mathsf{PA}\vdash A\quad\implies \mathsf{PA}\vdash B$$ is proved in the metatheory, and that metatheory may be much stronger than $\mathsf{PA}$. For example, what if we accept in the metatheory that $\mathsf{PA}$ is sound? Then our metatheory vacuously accepts $$\mathsf{PA}\vdash\neg Con(\mathsf{PA})\quad\implies\mathsf{PA}\vdash \perp$$ (because it rejects the antecedent), but on the other hand it also knows $$\mathsf{PA}\not\vdash (\neg Con(\mathsf{PA}))\rightarrow \perp.$$ This is because "$\neg Con(\mathsf{PA})\rightarrow \perp$" is $\mathsf{PA}$-provably (indeed, purely logically) equivalent to $Con(\mathsf{PA})$, and our metatheory knows via Godel that $\mathsf{PA}\not\vdash Con(\mathsf{PA})$.

So actually this is a very strong failure of $(i)\rightarrow (ii)$ in general:

If our metatheory is strong enough, it establishes an explicit instance of $(i)$ holding and $(ii)$ failing.