Timeline for How does one prove the consistency of $\mathrm{PA}$ in $\mathrm{Z_2}$?
Current License: CC BY-SA 4.0
6 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Sep 22, 2022 at 16:10 | vote | accept | cody | ||
| Sep 20, 2022 at 2:44 | comment | added | Noah Schweber | E.g. four of the rules for a witnessing subtree are: it must contain the root, all leaves it contains must be true (note that this only uses $\models$ restricted to atomic-or-negated-atomic sentences with parameters!), if a $\forall$-node is in the subtree then so are all of its children, and if an $\exists$-node is in the subtree then so is $\ge$ one of its children. Note that only quantifiers correspond to infinitely-branching nodes, and their infinite-branching-ness is entirely predictable (one branch per natural number) - and for simplicity we may assume that all negations are "pushed in." | |
| Sep 20, 2022 at 2:43 | comment | added | Noah Schweber | @cody $T_\varphi$ is an infinite, but very computable, object. For example, if $\varphi$ is the sentence "$\forall x\exists y(x<y)$," then $T_\varphi$ consists of: a root labelled "$\forall x$" which branches $\omega$-many times, then each of its children are labelled "$\exists y$" and branch another $\omega$-many times, then each leaf is labelled with the corresponding atomic sentence. The truth of $\varphi$ is witnessed, for example, by the subtree $S$ consisting of the root, every child of the root, and every child-of-a-child whose $y$-label is $17$ + their parents $x$-label. | |
| Sep 20, 2022 at 2:04 | comment | added | cody | Hmm, I'm actually still a little stumped: is $T_\varphi$ coded by an infinite sequence? | |
| Sep 19, 2022 at 18:47 | comment | added | cody | Full disclosure; I'm trying to prove normalization of system T in $HA_2$, but I asked the question above because I think it's of broader interest, and presents the same difficulties. | |
| Sep 19, 2022 at 16:40 | history | answered | Noah Schweber | CC BY-SA 4.0 |