0
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ Gödel's incompleteness theorems are in some sense impossibility theorems. But you apparently don't mean those. What do you mean? $\endgroup$ – Mees de Vries May 2 '18 at 13:26
  • $\begingroup$ Gödel states that there are propositions that cannot be proved. But can you prove that a specific proposition can not be proved? $\endgroup$ – Francesco Bertolaccini May 2 '18 at 13:27
  • $\begingroup$ 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})$. $\endgroup$ – Mees de Vries May 2 '18 at 13:30
  • $\begingroup$ 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'$. $\endgroup$ – Mauro ALLEGRANZA May 2 '18 at 13:32
  • 1
    $\begingroup$ This might help math.stackexchange.com/q/2027182/471959 $\endgroup$ – ℋolo May 2 '18 at 13:35
0
$\begingroup$

Gödel showed how to construct a statement in any sufficiently powerful formal system that states its own unprovability within the language of the formal system itself (he did this by showing that propositions in the language of the formal system can be translated into numbers and that "provability" can be translated into artithmetical properties of those numbers). But his construction method creates a specific proposition - it cannot be used to determine the provability of a general proposition.

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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