Timeline for The disjunction property in Peano Arithmetic?
Current License: CC BY-SA 3.0
20 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Apr 28, 2011 at 6:13 | vote | accept | Alex Gavrilov | ||
| Apr 28, 2011 at 3:50 | comment | added | Joel David Hamkins | Yes, please check it! I think your point was subtle and important, but it seems to be resolved by making the sentences syntactically different. | |
| Apr 28, 2011 at 3:43 | comment | added | Alex Gavrilov | I think you are right. I was a bit dumb. I am going to check this all. | |
| Apr 28, 2011 at 3:15 | comment | added | Joel David Hamkins | It's easy to see that they needn't be syntactically the same, by making $\theta_1(x,y)$ a conjunction of a formula with itself, but make $\theta_2(x,y)$ not have that form. | |
| Apr 28, 2011 at 3:12 | comment | added | Joel David Hamkins | Let $k$ be the number that $M$ thinks is the smallest code of a proof of one of them, which exists by PA. Thus, because the sentences are not the same, it is not a code of a proof of the other. If $M$ thinks that $k$ is a code of a proof of $\phi$, then $\psi$ is true in $M$, and if $M$ thinks $k$ is a code of a proof of $\psi$, then $\phi$ will be true in $M$, contrary to assumption. | |
| Apr 28, 2011 at 3:12 | comment | added | Joel David Hamkins | Alex, your issue is addressed by observing that $\phi$ and $\psi$ are syntactically distinct sentences, since $\phi$ is $\theta_1(n,m)$ and $\psi$ is $\theta_2(n,m)$, and these assertions are different if you trace it through (or one can easily make them have different lengths, by changing $\theta_1$ to its conjunction with itself). Once you know that they are syntactically different, then $\phi\vee\psi$ is provable in PA, since in any model of PA, if both are false, then because of what they say, both are thought to be provable in that model, possibly with nonstandard proofs. (continued) | |
| Apr 28, 2011 at 3:11 | history | edited | Joel David Hamkins | CC BY-SA 3.0 |
Explain about making them distinct
|
| Apr 28, 2011 at 3:05 | comment | added | Alex Gavrilov | Well, I think it would be reasonable to write down $A$ and $B$ explicitely to clear the mess. | |
| Apr 28, 2011 at 2:03 | comment | added | Alex Gavrilov | Joel, there is a gap. Applying the lemma, we may get $\phi$ provably equivalent to $\psi$. In this case $\phi\vee\psi$ is equivalent to $Con(PA)$. Then, the lenghts of nonstandard proofs are nonstandard numbers, which may be incompatible. So, we need another argument to show that $\phi\vee\psi$ can be proved. | |
| Apr 27, 2011 at 19:05 | comment | added | Joel David Hamkins | And by the way, David, let me add that I am very impressed by your comments on this thread! | |
| Apr 27, 2011 at 18:33 | history | edited | Joel David Hamkins | CC BY-SA 3.0 |
edited body; added 6 characters in body
|
| Apr 27, 2011 at 18:31 | comment | added | Joel David Hamkins | Thanks, David. I went ahead and proved the full binary fixed point lemma, which I think is due to Smullyan. The proof, which is fundamentally similar to your suggestion, generalizes the Goedel proof to two statements. | |
| Apr 27, 2011 at 18:27 | history | edited | Joel David Hamkins | CC BY-SA 3.0 |
Added proof of double fixed point lemma
|
| Apr 27, 2011 at 17:07 | comment | added | David E Speyer | $F$ has variables, but $Q_1(F,G)$, which does not, is $\phi$. The analogous way to build the Godel sentence is to let $Q$ be the operator which takes a statement $F$ about a variable $X$ and returns the sentence that $F$ holds when $X$ is replaced by the Godel number of $F$. Then Q("Not Q(X) is provable") is the Godel sentence. Unless I'm doing something dumb... | |
| Apr 27, 2011 at 16:46 | comment | added | Joel David Hamkins | David, I'm not quite clear on your proposal; your $F$ semms to have variables in it, but we need sentences. I believe that one can use those assertions along with the syntactic version of the double recursion theorem to find the desired fixed points, but I would be happier if I could find a clear reference for this. I think Smullyan did things very like this. | |
| Apr 27, 2011 at 16:41 | comment | added | Joel David Hamkins | Eric, if $\phi$ is false in $\mathbb{N}$, then it would be a false but provable statement, which contradicts that PA is true in $\mathbb{N}$. So $\phi$ is true. (I had edited that paragraph to make this clearer, evidently just as you posted your comment.) | |
| Apr 27, 2011 at 16:29 | comment | added | Eric Hall | If $\phi$ is false, then there is a proof of $\phi$ such that every proof of $\psi$ is longer. I don't understand the claim that the assumption that $\phi$ is false leads to the existence of a proof of $\psi$ (in particular a small proof of $\psi$). Am I missing something? | |
| Apr 27, 2011 at 16:26 | comment | added | David E Speyer |
@Joel Can't we directly prove the fixed point statement you want? Let $Q_1$ be the operator which, given two statements F and G with free variables X and Y, returns F with the Godel codes of F and G substituted for X and Y; let $Q_2$ be the similar operator which substitutes into G. Let F be "For every proof of $Q_1(X, Y)$, there is a shorter proof of $Q_2(X, Y)$" and let G be vice versa. Then I think $(Q_1(F,G), Q_2(F,G))$ is your $(\phi, \psi)$. Unless I've done something dumb.
|
|
| Apr 27, 2011 at 16:25 | history | edited | Joel David Hamkins | CC BY-SA 3.0 |
deleted 5 characters in body
|
| Apr 27, 2011 at 15:05 | history | answered | Joel David Hamkins | CC BY-SA 3.0 |