# Proving the impossibility of a proof

Given that according to Gödel's theorems there are propositions in any language equivalent to first order logic that cannot be proven right or wrong, is it possible to prove that some of such propositions are not provable? I am thinking of something like a proof of impossibility applied to propositions.

• Gödel's incompleteness theorems are in some sense impossibility theorems. But you apparently don't mean those. What do you mean? – Mees de Vries May 2 '18 at 13:26
• Gödel states that there are propositions that cannot be proved. But can you prove that a specific proposition can not be proved? – Francesco Bertolaccini May 2 '18 at 13:27
• Yes, that is Gödel's second incompleteness theorem; it states that an (appropriate for for the theorem) theory cannot prove its own consistency. E.g., $\mathsf{PA} \not \vdash \mathrm{Con}(\mathsf{PA})$. – Mees de Vries May 2 '18 at 13:30
• Gödel states that for a specific formal system $F$ there is a proposition $G_F$ (a formula in the language of $F$) that cannot be proved in $F$. $G_F$ is "specific" in the sense that we can "build" it. Of course, it makes little sense to ask about "absolute" impossibility: we can simply add $G_F$ to the system $F$ as axiom to get a new system $F'$ and $G_F$ is provable in $F'$. – Mauro ALLEGRANZA May 2 '18 at 13:32
• This might help math.stackexchange.com/q/2027182/471959 – ℋolo May 2 '18 at 13:35

This is analagous to how Liouville showed that transcendental numbers exist by constructing a family of numbers with properties which allowed him to prove they were not algebraic. It is much more difficult to prove that a particular number such as $e$ or $\pi$ is transcendental.