Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

$\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.

share|cite|improve this question
What logical system are you working in? – Zhen Lin Jan 16 '12 at 18:28
up vote 4 down vote accepted

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.

share|cite|improve this answer

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.

share|cite|improve this answer

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

A beautiful theorem of Martin Löb (see 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$.

share|cite|improve this answer

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.