Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

• Forgot your password?
• Apply for membership

1. • CommentRowNumber1.
   • CommentAuthorDavidRoberts
   • CommentTimeSep 22nd 2011
   • (edited Sep 22nd 2011)
   • PermaLink
   Author: DavidRoberts
   Format: MarkdownItexAt [this old blog post](http://xorshammer.com/2008/08/18/hardest-logic-puzzle-ever/), I found the following statement: >This sentence is false and it has a well-defined truth-value. In the comments, we find this statement >$\neg\square P \wedge (\square P \vee \square\neg P).$ where $\square P$ is '$P$ is provable in PA' (insert other system here if desired). Clearly the first version is not the same as the second, constructively (aside from other issues like translating 'has a well-defined truth value). The author (Michael O’Connor) goes on to say: >It occurred to me that the fact that $\neg\square P \wedge (\square P \vee \square\neg P)$ is a sentence whose decidability is undecidable in PA is actually not at all remarkable: every sentence which is undecidable in PA is such that its decidability is undecidable in PA, since for PA to prove a sentence is undecidable in PA, it would have to prove that it can’t prove something, which is equivalent to it proving its consistency. So I will have to work a little harder to find a provability model of this. However, what can we say if we drop LEM?

   At this old blog post, I found the following statement:

   This sentence is false and it has a well-defined truth-value.

   In the comments, we find this statement

   $\neg\square P \wedge (\square P \vee \square\neg P).$

   where $\square P$ is ’$P$ is provable in PA’ (insert other system here if desired).

   Clearly the first version is not the same as the second, constructively (aside from other issues like translating ’has a well-defined truth value). The author (Michael O’Connor) goes on to say:

   It occurred to me that the fact that $\neg\square P \wedge (\square P \vee \square\neg P)$ is a sentence whose decidability is undecidable in PA is actually not at all remarkable: every sentence which is undecidable in PA is such that its decidability is undecidable in PA, since for PA to prove a sentence is undecidable in PA, it would have to prove that it can’t prove something, which is equivalent to it proving its consistency. So I will have to work a little harder to find a provability model of this.

   However, what can we say if we drop LEM?

2. • CommentRowNumber2.
   • CommentAuthorTobyBartels
   • CommentTimeSep 23rd 2011
   • PermaLink
   Author: TobyBartels
   Format: MarkdownItexI wrote an email to Jim Dolan once about a related issue. While Gödel's Incompleteness Theorem is very important, even in constructive mathematics, the allegedly *shocking* thing about it (that some statements are neither provable nor refutable) couldn't possibly be shocking to a constructivist. To a philosophical intuitionist like Brouwer, in fact, this is a truism: as long as unsolved problems remain in arithmetic (or whatever is relevant), then some things have been neither proved nor refuted, and this is the same thing as being provable or refutable so far, so what would you expect? However, there is a closely related property that a formal system for arithmetic might have, which Gödel's Incompleteness Theorem proves that PA (or any consistent system for arithmetic in classical logic) lacks but which Heyting Arithmetic (HA) *does* have: the disjunction property $$ \square (P \vee Q) \iff (\square P \vee \square Q) $$ (one direction of which is trivial). If the system in question uses classical logic, then the left-hand side holds when $Q \coloneqq \neg P$, so the disjunction property implies that every statement is provable or refutable. But for a system using constructive logic, it proves no such thing. From this perspective, we see that syntactic completeness (provability or refutability of every formula) is a red herring, the disjunction property is what really matters, and constructive mathematics is better than classical mathematics because the DP is actually attainable. However, if you really want to deal with syntactic completeness as such, then consider $$ \neg\square P \iff \square\neg P $$ (one direction of which is completeness and the other is consistency), which is obvious analogue of the disjunction property (and the trivial conjunction property). This makes no real difference, however, since the formula in the comments simplifies to $$ \neg\square P \wedge \square\neg P $$ whether the classical or constructive version of completeness is used.

   I wrote an email to Jim Dolan once about a related issue. While Gödel’s Incompleteness Theorem is very important, even in constructive mathematics, the allegedly shocking thing about it (that some statements are neither provable nor refutable) couldn’t possibly be shocking to a constructivist. To a philosophical intuitionist like Brouwer, in fact, this is a truism: as long as unsolved problems remain in arithmetic (or whatever is relevant), then some things have been neither proved nor refuted, and this is the same thing as being provable or refutable so far, so what would you expect?

   However, there is a closely related property that a formal system for arithmetic might have, which Gödel’s Incompleteness Theorem proves that PA (or any consistent system for arithmetic in classical logic) lacks but which Heyting Arithmetic (HA) does have: the disjunction property

   $$\square (P \vee Q) \iff (\square P \vee \square Q)$$

   (one direction of which is trivial). If the system in question uses classical logic, then the left-hand side holds when $Q \coloneqq \neg P$, so the disjunction property implies that every statement is provable or refutable. But for a system using constructive logic, it proves no such thing. From this perspective, we see that syntactic completeness (provability or refutability of every formula) is a red herring, the disjunction property is what really matters, and constructive mathematics is better than classical mathematics because the DP is actually attainable.

   However, if you really want to deal with syntactic completeness as such, then consider

   $$\neg\square P \iff \square\neg P$$

   (one direction of which is completeness and the other is consistency), which is obvious analogue of the disjunction property (and the trivial conjunction property). This makes no real difference, however, since the formula in the comments simplifies to

   $$\neg\square P \wedge \square\neg P$$

   whether the classical or constructive version of completeness is used.

3. • CommentRowNumber3.
   • CommentAuthorTodd_Trimble
   • CommentTimeSep 23rd 2011
   • (edited Sep 23rd 2011)
   • PermaLink
   Author: Todd_Trimble
   Format: MarkdownItexActually, I was confused by what Michael O'Connor wrote. Shouldn't it be $\neg \Box P \vee (\Box P \wedge \Box \neg P)$? In other words, we can't prove $P$, unless we can prove both $P$ and $\neg P$ (i.e., unless the system is inconsistent).

   Actually, I was confused by what Michael O’Connor wrote. Shouldn’t it be $\neg \Box P \vee (\Box P \wedge \Box \neg P)$? In other words, we can’t prove $P$, unless we can prove both $P$ and $\neg P$ (i.e., unless the system is inconsistent).