Skip to main content
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