# On the statement $Q=A \text{ is provable}$

$\newcommand{\provable}{\text{ is provable}}$ Which of these are correct $A\leftrightarrow (A \provable)$, $A\leftarrow A\provable)$, if the latter, is there an example of such a deduction, i.e. we didn't derive A first, but we derived $Q=(A \provable)$ first?

And if $B$ is any statement, can we always deduce $(B \lor\neg B)$, even if we cant deduce $B$ or $\neg B$?

In ZFC or PA.

-
What logical system are you working in? –  Zhen Lin Jan 16 '12 at 18:28

Levon's answer settles the question whether the claims "$A\rightarrow A$ is provable" and "$A\leftrightarrow A$ is provable" are themselves provable.

Whether they are true (independent of being provable) is a different matter.

Let $M$ bet whatever foundation of mathematics we choose to work with. Gödel's incompleteness theorem tells us that $A\Rightarrow (M\vdash A)$ cannot be not true in general for interesting $M$'s. Thus $(M\vdash A)\Leftrightarrow A$ must be rejected.

On the other hand, we should very much hope that $(M\vdash A) \Rightarrow A$ is a Platonically true statement -- that is, we only want true statements to be provable. If that doesn't hold, then either the logic implicit in the $\vdash$ symbol is flawed, or the axioms of $M$ are not true.

Gödel and Rosser tell us that we cannot establish $(M\vdash A)\Rightarrow A$ this by purely formal means, but most mathematicians manage to somehow convince themselves informally or intuitively. If not, they either become formalists or leave the field.

As for $B\lor \neg B$, this is indeed always a theorem in mainstream mathematical logic, so-called "classical logic".

About a century ago, there was a movement called "the intuitionists" who rejected this and favored a more restricted mode of mathematical reasoning where $B\lor \neg B$ was not always a theorem. There are very few today who seriously think mathematics in general should be so restricted, though it is not uncommon to investigate the restricted intuitionistic logic as an object of study rather than as a foundation of mathematics. Viewed this way it turns out to have some interesting applications in, e.g., computer science.

-

As demonstrated by Gödel, there is an arithmetical statement (and, actually, an infinitude of such statements) that is true if and only if it is not provable. Basically, this statement says "I'm not provable in such-and-such system" using a clever arithmetical encoding of provability and self-reference.

Every statement that can be checked by finite means is provable in $PA$. For example, if a statement $A$ is provable in $PA$ or $ZFC$ (meaning that it has a finite proof that can be formally checked), then it is provable in $PA$ that $A$ is provable. Another example: if the Riemann Hypothesis is false, then its negation is provable in $PA$.

On the other hand, it is possible to construct a consistent (but unsound) logical system $T$ and a statement $S$ such that it is provable in $T$ that $S$ is provable in $T$, but in fact $S$ is not provable in $T$.

Yes, we can always deduce $B \lor \neg B$, this is a tautology in propositional calculus.

-

Let $\Box A$ abbreviate the statement "$A$ is provable''.

A beautiful theorem of Martin Löb (see http://en.wikipedia.org/wiki/L%C3%B6b%27s_theorem) states that if $PA \vdash \Box A \to A$ then $PA \vdash A$. The converse is obvious and so $PA \vdash \Box A \to A$ if and only if $PA \vdash A$.

Similarly, if $PA \vdash \Box A \leftrightarrow A$, then $PA \vdash A$ by Löb's theorem. Conversely if $PA \vdash A$, then $PA \vdash \Box A$ and so $PA \vdash \Box A \leftrightarrow A$. Thus $PA \vdash \Box A \leftrightarrow A$ if and only if $PA \vdash \Box A \to A$ if and only if $PA \vdash A$.

-