Timeline for Is true arithmetic + $\lnot Con (TA)$ consistent?
Current License: CC BY-SA 3.0
9 events
when toggle format | what | by | license | comment | |
---|---|---|---|---|---|
Jun 1, 2018 at 17:38 | comment | added | Noah Schweber | @PyRulez This is super late, but I just noticed a serious typo in my commet above: it should read: $${}{}$$" . . . There's no reason to believe $P(\ulcorner p\urcorner)\wedge P(\ulcorner p\implies q\urcorner)\implies P(\ulcorner q\urcorner)$. . . ." $${}{}$$ Omitting the "$\ulcorner$$\cdot$$\urcorner$s" isn't too bad, since they're clear from context, but the last "$P$" is quite important. | |
Apr 7, 2018 at 19:17 | history | edited | Noah Schweber | CC BY-SA 3.0 |
added 1097 characters in body
|
Apr 7, 2018 at 18:12 | comment | added | Wojowu | Alternative "fix" is to not only add $P(n)$ for codes of true sentences, but also $\neg P(n)$ for codes of false sentences. But then adding $P(\ulcorner 0=1\urcorner)$ leads to contradiction immediately. | |
Apr 7, 2018 at 18:01 | comment | added | Noah Schweber | I think it will be helpful to you to drop the symbol "$TA\vdash$" from your language, and write it in terms of a new, arbitrary unary predicate symbol "$P$" - this will prevent conflation of internal and external reasoning. | |
Apr 7, 2018 at 18:00 | comment | added | Noah Schweber | @PyRulez The fact that TA satisfies modus ponens has nothing to do with it. Remember that we're working with an abstract unary predicate symbol here, and there's no reason to believe $P(p)\wedge P(p\implies q)\implies q$. You can see this directly by noting that the structure of standard arithmetic augmented by interpreting $P$ as the set of Godel numbers of sentences in TA or of $0=1$ satisfies your theory. That is, you need to add something to your theory to make it satisfy the intuitive principles you want it to. | |
Apr 7, 2018 at 17:58 | history | edited | Noah Schweber | CC BY-SA 3.0 |
added 540 characters in body
|
Apr 7, 2018 at 17:58 | comment | added | Christopher King | Basically, $TA + \lnot Con (TA)$ sees a theory, and sees that it is first order arithmetic, and that implies certain statements. It does not know that it is "true". | |
Apr 7, 2018 at 17:57 | comment | added | Christopher King | "The theory can only see what TA implies, and that TA is a theory of first order arithmetic." That implies that TA satisfies modus ponens. | |
Apr 7, 2018 at 17:55 | history | answered | Noah Schweber | CC BY-SA 3.0 |