Timeline for Is true arithmetic + $\lnot Con (TA)$ consistent?
Current License: CC BY-SA 3.0
39 events
when toggle format | what | by | license | comment | |
---|---|---|---|---|---|
Apr 8, 2018 at 15:36 | comment | added | Noah Schweber | @EmilJeřábek Oh yes quite right. (To the OP, and using obvious abbreviations: suppose we have $P(p)$ and $P(q)$. Well, in TA we have $P(p\implies (q\implies p\wedge q))$. By IMP we get $P(q\implies p\wedge q)$ and then by IMP again we get $P(p\wedge q)$.) | |
Apr 8, 2018 at 7:36 | comment | added | Emil Jeřábek | IAI follows from modus ponens. | |
Apr 8, 2018 at 4:53 | review | Close votes | |||
Apr 16, 2018 at 3:04 | |||||
Apr 8, 2018 at 2:05 | answer | added | none | timeline score: 3 | |
Apr 7, 2018 at 23:33 | comment | added | Christopher King | @მამუკაჯიბლაძე it probably would've been better for math.se. | |
Apr 7, 2018 at 23:32 | comment | added | მამუკა ჯიბლაძე | Since I find the question very interesting I feel obliged to confess that I downvoted it :D | |
Apr 7, 2018 at 23:23 | comment | added | Noah Schweber | @PyRulez Ah, ok. Note that TA is strong enough that we actually only need IMP and "internal and-introduction" IAI (the other rule in my previous comment) to get the desired closure properties, since whenever a finite set of sentences of arithmetic $\Delta$ proves a sentence of arithmetic $\psi$ we have $(\bigwedge\Delta)\implies\psi$ in TA. May I edit my edit to bring IMP and IAI in as axioms of your theory $T_0$? | |
Apr 7, 2018 at 23:20 | comment | added | Christopher King | @NoahSchweber yes | |
Apr 7, 2018 at 23:17 | comment | added | Noah Schweber | @PyRulez What exactly does "$TA$ is a first order arithmetic" mean? I think you mean that you're adding axioms corresponding to the usual logical inference rules (such as IMP, and $(P(m)\wedge P(n))\implies P(and(m, n))$, and so on) - is that correct? | |
Apr 7, 2018 at 23:16 | comment | added | Christopher King | @NoahSchweber sorry, I forgot to specify that "$TA$ is a first order arithmetic" is an axiom (or axiom schema, if needed). | |
Apr 7, 2018 at 23:15 | comment | added | Noah Schweber | Put it another way, suppose I told you I have a set $S$ of sentences containing every sentence of TA and also containing $0=1$. You would need additional information about $S$ to conclude that it contains, say, $1=2$; all you know is that $0=1$ and $(0=1)\implies (1=2)$ are in $S$, but you don't have any "global" facts about $S$ yet. | |
Apr 7, 2018 at 23:14 | comment | added | Noah Schweber | @PyRulez But that needs to be built in via additional axioms governing the behavior of $P$ (this is exactly what IMP is). On the face of it, $P$ just describes some set of natural numbers; saying that $P(n)$ holds whenever $n$ is a Godel number of true arithmetic doesn't give $P$ the modus ponens property. | |
Apr 7, 2018 at 23:13 | comment | added | Christopher King | @NoahSchweber well, the fact that it follows all deduction rules of first order logic. They are added as axioms. | |
Apr 7, 2018 at 23:11 | comment | added | Noah Schweber | @PyRulez "it knows that TA is a first-order theory of arithmetic" What does that mean, exactly? (More to the point, what axioms do you add to $T_0$ to ensure this?) | |
Apr 7, 2018 at 23:05 | history | edited | Martin Sleziak | CC BY-SA 3.0 |
minor typos
|
Apr 7, 2018 at 22:51 | comment | added | Christopher King | @NoahSchweber Oh whoops, misread. One property you forgot to mention is that it knows that $TA$ is a first-order theory of arithmetic (which implies deduction rules (including IMP) hold). It's not a big deal, since the question turned out to be pretty bad anyways, but just thought I'd mention it. | |
Apr 7, 2018 at 22:49 | history | rollback | Christopher King |
Rollback to Revision 5
|
|
Apr 7, 2018 at 22:48 | comment | added | Noah Schweber | @PyRulez I only mentioned reflection as something explicitly not part of the theory (see "meanwhile ...") - I thought it was relevant to mention natural properties the theory didn't have. | |
Apr 7, 2018 at 22:44 | comment | added | Christopher King | @NoahSchweber good except I never intended there to be reflection. I've fixed it. | |
Apr 7, 2018 at 22:43 | history | edited | Christopher King | CC BY-SA 3.0 |
deleted 113 characters in body
|
Apr 7, 2018 at 19:07 | comment | added | Noah Schweber | @PyRulez I've made an edit; please delete it, preserve it, alter it, or tell me to do one of those three as you will. | |
Apr 7, 2018 at 19:05 | history | edited | Noah Schweber | CC BY-SA 3.0 |
added 1511 characters in body
|
Apr 7, 2018 at 18:54 | comment | added | Christopher King | @NoahSchweber sure | |
Apr 7, 2018 at 18:54 | comment | added | Noah Schweber | @PyRulez I think your question does a better job of describing the theory in question, but is still not completely clear; may I add a "below-the-fold" part to give a description of the theory along the lines suggested in my answer? | |
Apr 7, 2018 at 18:45 | answer | added | Joel David Hamkins | timeline score: 8 | |
Apr 7, 2018 at 17:55 | answer | added | Noah Schweber | timeline score: 4 | |
Apr 7, 2018 at 17:51 | history | edited | Christopher King | CC BY-SA 3.0 |
added 38 characters in body
|
Apr 7, 2018 at 17:50 | comment | added | Christopher King | @NoahSchweber Okay, I edited the post to reflect that. | |
Apr 7, 2018 at 17:49 | comment | added | Noah Schweber | As far as I can tell, the symbol for $TA$ is extraneous: you really just want a unary relation symbol $P$ and axioms of the form $P(n)$ whenever $n$ is a Godel number of a sentence of true arithmetic, or the Godel number of "$0=1$." I think it will be easier to precisely define your object of study in this more limited language. Is there any real reason to include a constant symbol (which you'll need to think of as representing some natural number)? | |
Apr 7, 2018 at 17:49 | comment | added | Wojowu | If $TA$ is a constant symbol, then it ought to be interpreted as some natural number. I don't think this is what you intend. | |
Apr 7, 2018 at 17:48 | comment | added | Christopher King | @Wojowu $TA$ is a constant symbol, and $\vdash$ is a binary relation. | |
Apr 7, 2018 at 17:47 | comment | added | Wojowu | What are $TA$ and $\vdash$ in this language? Constants, relations, functions? I can't figure how in either of the cases $TA\vdash 0=1$ is a well-formed formula | |
Apr 7, 2018 at 17:47 | history | edited | Christopher King | CC BY-SA 3.0 |
added 55 characters in body
|
Apr 7, 2018 at 17:45 | comment | added | Christopher King | @Wojowu $TA \vdash 0=1$ (or rather $TA \vdash \text{godel code of }0=1$). | |
Apr 7, 2018 at 17:44 | comment | added | Wojowu | Okay then. How do you express $\neg Con(TA)$ in the language of arithmetic with this adjoined symbol? | |
Apr 7, 2018 at 17:44 | comment | added | Christopher King | @Wojowu Arithmetic+a symbol for $TA$ and $\vdash$. | |
Apr 7, 2018 at 17:44 | history | edited | Christopher King | CC BY-SA 3.0 |
added 95 characters in body
|
Apr 7, 2018 at 17:42 | comment | added | Wojowu | How do you express $\neg Con(TA)$ in the language of arithmetic? Or what language do you express your theory in? | |
Apr 7, 2018 at 17:39 | history | asked | Christopher King | CC BY-SA 3.0 |