Timeline for Can FPA really prove its consistency?
Current License: CC BY-SA 4.0
20 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jun 25, 2021 at 1:15 | comment | added | David Roberts♦ | @abo thanks for that! | |
| Jun 24, 2021 at 20:26 | comment | added | abo | @DavidRoberts. I found a corrected version and put it here. researchgate.net/publication/… | |
| Apr 28, 2020 at 15:43 | comment | added | abo | @Dave Roberts. No problem. There's an old (unauthorized!) copy here: citeseerx.ist.psu.edu/viewdoc/… This older version makes the incorrect assertion that the system can really prove its consistency at the very end; pages 117 and 118 are to be disregarded. | |
| Apr 27, 2020 at 14:38 | comment | added | David Roberts♦ | @abo sorry to ping you, but I was trying to track down your documents on arithmetic without total successor that got up to, I believe, quadratic reciprocity? Are they available anywhere? | |
| Feb 2, 2019 at 19:23 | comment | added | abo | Thank you Emil. I agree with what you have written and that $A_n$ is a counterexample. I am not at home and do not have my notes with me, so will not be able to write more at this time. Thank you for taking the time to vet the proof. | |
| Feb 2, 2019 at 19:03 | comment | added | abo | I will leave the proof up for now, but if there is a strong preference, I can delete. | |
| Feb 2, 2019 at 18:58 | comment | added | abo | Because of the 30000 character limit in the post, I must restrict my full reply to Emil to comments. | |
| Feb 2, 2019 at 18:56 | history | edited | abo | CC BY-SA 4.0 |
added 34 characters in body
|
| Feb 1, 2019 at 17:48 | comment | added | Emil Jeřábek | ... for every sequence $(c_1,\dots,c_n)\in\{\bot,\top\}^n$, there is a leaf $u$ of $T'$ such that $c_i=c_i^u$ for all $i=1,\dots,n$. (This implies that $T'$ has $\ge2^n$ leaves, hence in particular, $|T|\ge2^n$.) If this were not the case, let $\sigma$ be the variable assignment such that $\sigma(p_i^u)=c_i$ for each $i$ and each $u$. The discussion above ensures that this definition is consistent, as each variable corresponds to at most one $x_i$. Then $v_\sigma^u=0$ for all $u$, a contradiction. | |
| Feb 1, 2019 at 17:44 | comment | added | Emil Jeřábek | ... going through the node, but in each of these branches, $p$ is assigned to the same quantifier $\forall x_i$. Now, let $\sigma$ be an assignment to all the variables. It is easy to see from the definition that quantifier-free formulas in $T$ are evaluated in the usual fashion, hence a leaf $u$ of $T'$ gets the value $v_\sigma^u:=\bigwedge_i(\sigma(p_i^u)\leftrightarrow c_i^u)$. Then the value assigned to the top is the disjunction of $v_\sigma^u$ over all $u$. Thus, for every assignment $\sigma$, there exists a leaf $u$ of $T'$ such that $v_\sigma^u=1$. I claim that this implies that ... | |
| Feb 1, 2019 at 17:38 | comment | added | Emil Jeřábek | ... Let $T'$ denote the top part of $T$ consisting of split, $\forall$, and $\exists$ branches. For each leaf $u$ of $T'$, the branch of $T'$ ending with $u$ introduces variables $p_1^u,\dots,p_n^u$ for the $\forall x_1\dots\forall x_n$ quantifiers, and assigns constants $c_1^u,\dots,c_n^u\in\{0,1\}$ to the $\exists y_1\dots\exists y_n$ quantifiers. The leaf $u$ is then labelled with the quantifier-free formula $\bigwedge_{i=1}^n(p_i^u\leftrightarrow c_i^u)$. The definition requires that any variable $p$ is introduced only in one node of the tree; this may be shared by multiple branches ... | |
| Feb 1, 2019 at 17:31 | comment | added | Emil Jeřábek | In fact, it is easy to show that your Theorem 22 is false for the actual G system, thus either G has exponential speed-up over your proof system, or there is an error in your proof. To see this, take the formulas $A_n=\forall x_1\dots\forall x_n\exists y_1\dots\exists y_n\,\bigwedge_{i=1}^n(x_i\leftrightarrow y_i)$. These formulas have simple G proofs with $O(n)$ steps and total size $O(n^2)$. However, I claim that every semtree $T$ labelled with $A_n$ such that $\mathrm{val}_\sigma(T)=1$ for every variable assignment $\sigma$ has to have size at least $2^n$. ... | |
| Feb 1, 2019 at 17:22 | comment | added | Emil Jeřábek | The proof system you are using, with target formulas restricted to $\top$ and $\bot$, is not polynomially equivalent to G, but much weaker. I am aware that the systems are claimed to be equivalent on p. 176 of the Cook&Nguyen book, but this appears to be an error. They give no proof, relegating the claim to Exercise VII.3.7, but the proof they hint at, using Exercise VII.3.6, does not work, because VII.3.6 needs variables to be used as target formulas. They give a reference to the PhD thesis of Morioka, but the proof system in his Thm. 5.11 allows variables and constants as target formulas. | |
| Jan 23, 2019 at 21:30 | comment | added | Andrej Bauer | Well then, poke a whole or endorse :-) | |
| Jan 23, 2019 at 21:08 | comment | added | David Roberts♦ | @AndrejBauer I think abo would need an endorser for the arXiv | |
| Jan 23, 2019 at 20:29 | comment | added | Andrej Bauer | Wouldn't it be more prudent to write up the proof and put it on arXiv? | |
| Jan 23, 2019 at 14:00 | comment | added | Asaf Karagila♦ | Interesting this just got mentioned a few times yesterday at the arctic set theory conference... | |
| Jan 23, 2019 at 9:41 | comment | added | David Roberts♦ | Can't edit this in, as it goes over the character limit: Logical Foundations of Proof Complexity by Stephen Cook and Phuong Nguyen (draft version, errata) | |
| Jan 23, 2019 at 9:28 | comment | added | David Roberts♦ | Good to see you back :-) | |
| Jan 23, 2019 at 9:21 | history | answered | abo | CC BY-SA 4.0 |