User peter smith - MathOverflow most recent 30 from http://mathoverflow.net 2013-05-18T17:20:52Z http://mathoverflow.net/feeds/user/14111 http://www.creativecommons.org/licenses/by-nc/2.5/rdf http://mathoverflow.net/questions/43148/basic-results-with-three-or-more-hypotheses/130723#130723 Answer by Peter Smith for Basic results with three or more hypotheses Peter Smith 2013-05-15T14:19:43Z 2013-05-15T14:28:12Z <p>What about the textbook general version of the original Gödel incompleteness theorem: if $T$ is recursively axiomatized, sufficiently strong, and $\omega$-consistent, it is incomplete (where sufficient strength means representing every recursive function)?</p> http://mathoverflow.net/questions/126792/rosserized-proof-predicates-and-the-derivability-conditions Rosserized proof-predicates and the derivability conditions. Peter Smith 2013-04-07T17:57:25Z 2013-04-10T09:01:46Z <p>[Improved version!!]</p> <p>Suppose $\mathsf{Prov}_R$ is a Rosserized proof predicate for PA (or some other suitable theory). To fix ideas, suppose </p> <p>$$\mathsf{Prov}_R(\overline{\ulcorner\varphi\urcorner}) = \mathsf{\exists x(Prf(x, \overline{\ulcorner\varphi\urcorner}) \land (\forall y \leq x)\neg Prf(y, \overline{\ulcorner\bot\urcorner}))}$$</p> <p>where $\mathsf{Prf}$ represents the relation that $m$ has to $n$ when $m$ numbers a proof of the sentence numbered $n$. We can construct a $\Delta_0$ wff $\mathsf{Prf}$, making $\mathsf{Prov}_R$ $\Sigma_1$.</p> <p>Then, as is familiar, </p> <blockquote> <p>PA $\vdash \neg\mathsf{Prov}_R(\overline{\ulcorner\bot\urcorner})$</p> </blockquote> <p>So the HBL derivability conditions can't all hold for $\mathsf{Prov}_R$. </p> <p>The first condition still holds. And it is reasonably easy to see why the second condition might fail (suppose that ordered by Gödel numbers the proof of $A$ and $A \to C$ precede the first proof of $\bot$ which precedes the first proof of $C$). But we also know that using Jereslow's trick we can get a version of the unprovability of consistency without appeal to the second condition, so the third condition should be the crucial failure. </p> <p>Well the usual proof of the third condition runs by showing PA $\vdash \psi \to \mathsf{Prov}(\overline{\ulcorner\psi\urcorner})$ for any $\Sigma_1$ $\psi$, and then remarking that $\mathsf{Prov}(\overline{\ulcorner\varphi\urcorner})$ is itself $\Sigma_1$. But this line of argument is presumably going to be blocked at the first stage when we turn to the Rosserized predicate $\mathsf{Prov}_R$: i.e. we won't have PA $\vdash \psi \to \mathsf{Prov}_R(\overline{\ulcorner\psi\urcorner})$ for every $\Sigma_1$ $\psi$. [And it is plausible this should fail, I guess.]</p> <p>So we know the third condition fails. But -- and here at last is the questions:</p> <blockquote> <p>Is there a simple counterexample to PA $\vdash \psi \to \mathsf{Prov}_R(\overline{\ulcorner\psi\urcorner})$ for $\Sigma_1$ $\psi$, </p> </blockquote> <p>and if that counterexample doesn't already involve $\mathsf{Prov}_R$, </p> <blockquote> <p>Are there known constructions of suitable wffs $\theta$ such that we have a nice illustration of a case where PA $\nvdash \mathsf{Prov}_R(\overline{\ulcorner\theta\urcorner}) \to \mathsf{Prov}_R(\overline{\ulcorner\mathsf{Prov}_R(\overline{\ulcorner\theta\urcorner})\urcorner})$</p> </blockquote> <p>either for the given Rosserized predicate, or some cousin?</p> http://mathoverflow.net/questions/121621/mendelsons-mathematical-logic-and-the-missing-appendix-on-the-consistency-of-p Mendelson's *Mathematical Logic* and the missing Appendix on the consistency of PA Peter Smith 2013-02-12T16:42:27Z 2013-02-15T18:40:58Z <p>A very soft question, but I hope not out of order here.</p> <p>In the first edition of Elliott Mendelson's classic <em>Introduction to Mathematical Logic</em> (1964) there is an appendix, giving a version of Schütte's (1951) variation on Gentzen's proof of the consistency of PA. This is intriguing stuff, crisply and quite accessibly presented. The appendix is, however, suppressed in later editions (in fact, from the second onwards), even though there is plenty of room given to other materials and a new appendix</p> <p>Now, a number of people have said that the appendix is one of the most interesting things about the book. I agree. I too remember being quite excited by it when I first came across it a long time ago!</p> <p>So: has anyone heard a folkloric story about why Mendelson suppressed the appendix? I've never heard it suggested that there is a problem with the consistency proof as given.</p> <p>Context, if you are interested: I asked this a couple of weeks ago on math.SE (without getting an answer) when starting to write up a survey of some of the Big Books on Mathematical Logic that will become part of my Teach-Yourself-Logic Guide (mostly for philosophers, though others might be interested), and I'd got to Mendelson. You can get the current version of the Guide by going to <a href="http://www.logicmatters.net/students/tyl/" rel="nofollow">http://www.logicmatters.net/students/tyl/</a></p> http://mathoverflow.net/questions/121621/mendelsons-mathematical-logic-and-the-missing-appendix-on-the-consistency-of-p/121930#121930 Answer by Peter Smith for Mendelson's *Mathematical Logic* and the missing Appendix on the consistency of PA Peter Smith 2013-02-15T18:40:58Z 2013-02-15T18:40:58Z <p>Before posting this question I did search around a bit (probably inefficiently and certainly quite ineffectively) to see if I could find an email for Elliott Mendelson to ask him directly! But anyway, he picked up my similar query on FOM and very kindly wrote to me:</p> <blockquote> <p>I was intrigued by your comments about the consistency proof of PA that appeared in the First Edition of my logic book. I omitted it in later editions because I felt that the topic needed a much more thorough treatment than what I had given, a treatment that would require more space than would be appropriate in an introduction to mathematical logic. </p> </blockquote> <p>I can understand that. Though I think the pointers he gave in that Appendix did spur on quite a few readers to find out more, so I still think it was a Very Good Thing, and it was perhaps a pity to drop it. </p> <p>[Prof. Mendelson has kindly allowed me to quote him.]</p> http://mathoverflow.net/questions/109625/how-do-quantifiers-limit-scope/109632#109632 Answer by Peter Smith for How do quantifiers limit scope? Peter Smith 2012-10-14T17:59:10Z 2012-10-14T17:59:10Z <p>I'm afraid your suggested answer is wrong. Suppose $a$ is in the domain and a non-triangle. Then $$\forall s(\text{triangle}(a)\wedge\text{square}(s)\rightarrow\text{above}(a, s))$$ is vacuously true as it always has a false antecedent (recall $\land$ binds tighter than $\to$). Hence $$\exists t\forall s(\text{triangle}(t)\wedge\text{square}(s)\rightarrow\text{above}(t, s))$$ is true even if no triangle is above a square. </p> <p>What you need is $$\exists t(\text{triangle}(t)\wedge \forall s(\text{square}(s)\rightarrow\text{above}(t, s)))$$ or equivalently $$\exists t\forall s(\text{triangle}(t)\wedge(\text{square}(s)\rightarrow\text{above}(t, s)))$$ Bracketing matters!</p> <p>As for $$\forall xP(x)(Q(x))\equiv\forall x(P(x)\rightarrow Q(x))$$ what's on the left is horribly ill-formed by normal standards and so is to be deprecated. But the thought that restricted universals are to be rendered using conditionals, and restricted existentials rendered using conjunctions is of course right. Your students might find the (freely available) chapters on transcription in Paul Teller's <em>Logic Primer</em> very helpful: see the first four chapters of Part 2 at <a href="http://tellerprimer.ucdavis.edu/pdf/" rel="nofollow">http://tellerprimer.ucdavis.edu/pdf/</a> </p> http://mathoverflow.net/questions/101660/when-are-provability-predicates-provably-equivalent When are provability predicates provably equivalent? Peter Smith 2012-07-08T13:19:32Z 2012-07-10T11:39:22Z <p><em>Fix notation</em></p> <p>Suppose that $Prf_1(m, n)$ is the numerical relation that holds when $m$ numbers a $T$-proof of the sentence numbered $n$, according to scheme 1 for numbering wffs and sequences of wffs. Likewise $Prf_2(m, n)$ is the relation that holds when $m$ numbers a $T$-proof of the sentence numbered $n$ according to a different numbering scheme 2.</p> <p>Let $\mathsf{Prf_1}$ represent $Prf_1$ in $T$, and put $\Box_1\varphi =_{def}$ $\exists \mathsf{x}\mathsf{Prf_1(x,\overline{\ulcorner\varphi\urcorner})}$, where $\overline{\ulcorner\varphi\urcorner}$ is $T$'s standard numeral for the number for $\varphi$ under scheme 1. Similarly for $\Box_2\varphi$.</p> <p><em>Questions</em></p> <p>A) Is it known what are the (most general?) conditions on the relation between coding schemes 1 and 2 for which we have</p> <p>$T \vdash \Box_1\varphi \leftrightarrow \Box_2\varphi$, for any sentence $\varphi$?</p> <p>B) What are the nicest/weakest(?) "derivability conditions" on a box $\Box$ in $T$, which if satisfied by both $\Box_1$ and $\Box_2$, mean that $T$ can again prove that equivalence?</p> http://mathoverflow.net/questions/101393/who-introduced-the-concept-of-primitive-recursive-functions/101401#101401 Answer by Peter Smith for Who introduced the concept of Primitive recursive functions? Peter Smith 2012-07-05T13:02:05Z 2012-07-05T13:02:05Z <p>I believe the explicit use of definitions by primitive recursion goes back to Grassman, 1861. </p> <p>Dedekind in 1888 not only highlighted such definitions but had a proof that they work as intended, i.e. define unique functions. </p> <p>But it is probably Skolem who first clearly recognised the primitive recursive functions as together forming a class of functions of particular interest. Indeed, his 1923 paper is entitled "The foundations of elementary arithmetic established by means of the recursive mode of thought ...", and, as with Gödel in 1931, by "recursive" Skolem here means "primitive recursive". This paper is usually credited with isolating Primitive Recursive Arithmetic as of particular interest for finitism (and hence for the Hilbert Programme).</p> http://mathoverflow.net/questions/100934/are-there-any-natural-recursively-but-not-primitive-recursively-axiomatized-theor Are there any natural recursively but not primitive-recursively axiomatized theories? Peter Smith 2012-06-29T14:09:40Z 2012-07-04T17:32:23Z <p>In principle, we could have a recursively axiomatized theory for which the property numbers-an-axiom (even relative to some routine Gödel numbering scheme) is recursive but not primitive recursive. But are there any natural examples?</p> <p>Of course, any such theory can be primitive-recursively reaxiomatized using Craig's trick. So we know that there can't be theories which are recursively axiomatizABLE but not primitive-recursively aziomatizABLE. But that's not the issue. The question is whether there is a theory <em>T</em> which <em>when presented in a natural way</em> requires open-ended searches to check whether a purported <em>T</em>-proof is indeed a proof according to that specification. </p> <p>[I couldn't think of one when I wrote the first edition of my Gödel book, and I still can't as I work on the second edition. But maybe I'm just being dim/ignorant!] </p> http://mathoverflow.net/questions/126792/rosserized-proof-predicates-and-the-derivability-conditions/126809#126809 Comment by Peter Smith Peter Smith 2013-04-10T14:01:36Z 2013-04-10T14:01:36Z Thanks for the correction, yep should have been $\leq$. But the wff you display <i>is</i> $\neg\mathsf{Prov}_R(\ulcorner\bot\urcorner)$. http://mathoverflow.net/questions/126792/rosserized-proof-predicates-and-the-derivability-conditions/126809#126809 Comment by Peter Smith Peter Smith 2013-04-09T15:59:15Z 2013-04-09T15:59:15Z Arguing inside PA, logic ensures $\neg(\mathsf{Prf(a, \ulcorner\bot\urcorner)} \land \neg\mathsf{Prf(a, \ulcorner\bot\urcorner))}$. So trivially, we can infer $\neg(\mathsf{Prf(a, \ulcorner\bot\urcorner)} \land \mathsf{(\forall y \leq a)}\neg\mathsf{Prf(y, \ulcorner\bot\urcorner))}$. Apply universal quantifier introduction to conclude $\neg\mathsf{Prov}R(\ulcorner\bot\urcorner)$. http://mathoverflow.net/questions/126792/rosserized-proof-predicates-and-the-derivability-conditions/126809#126809 Comment by Peter Smith Peter Smith 2013-04-08T20:49:23Z 2013-04-08T20:49:23Z Yes, as I said, the second condition can fail. As for Jereslow's trick see e.g. my G&#246;del book, &#167;33.5 in the second edition, based on Jeroslow, R. G., 1973, Redundancies in the Hilbert-Bernays derivability conditions for G&#246;del’s second incompleteness theorem. <i>Journal of Symbolic Logic</i>, 38: 359–367. http://mathoverflow.net/questions/126792/rosserized-proof-predicates-and-the-derivability-conditions/126809#126809 Comment by Peter Smith Peter Smith 2013-04-08T07:26:55Z 2013-04-08T07:26:55Z Oops, no excuses, I was having bad senior moment: yes of course you can, as a best case, construct a suitable $\Sigma_0$ wff for Prf. I've rephrased the question! (Thanks!) http://mathoverflow.net/questions/121621/mendelsons-mathematical-logic-and-the-missing-appendix-on-the-consistency-of-p Comment by Peter Smith Peter Smith 2013-02-12T19:02:42Z 2013-02-12T19:02:42Z @AliEnayat Good thought! http://mathoverflow.net/questions/107760/should-functions-be-assumed-to-behave-like-the-identity-function-when-evaluated-o Comment by Peter Smith Peter Smith 2012-09-21T15:55:06Z 2012-09-21T15:55:06Z I'm with @Andrej Bauer. The Fregean alternative of turning partial functions into total ones by stipulating a default value has, inter alia, the nasty feature of (in general) turning partial computable functions into total non-computable functions. http://mathoverflow.net/questions/44620/undergraduate-logic-textbook/44621#44621 Comment by Peter Smith Peter Smith 2012-09-16T13:17:47Z 2012-09-16T13:17:47Z I <i>really</i> wouldn't recommend Mendelson. Great when it first came out in the sixties, but most students will find it quite unnecessarily hard going (it's logical systems are not nice ones to use, and the book goes for excess rigour at the expense of attractive explanations of why the subject unfolds as it does). http://mathoverflow.net/questions/101660/when-are-provability-predicates-provably-equivalent/101767#101767 Comment by Peter Smith Peter Smith 2012-07-11T06:33:44Z 2012-07-11T06:33:44Z Thanks for the extra details! http://mathoverflow.net/questions/101660/when-are-provability-predicates-provably-equivalent/101767#101767 Comment by Peter Smith Peter Smith 2012-07-09T20:00:36Z 2012-07-09T20:00:36Z Thanks, this looks very promising! But (I'm no doubt being dim here) it would be helpful if you could spell out more of the proof of the final claim ...! http://mathoverflow.net/questions/101660/when-are-provability-predicates-provably-equivalent/101732#101732 Comment by Peter Smith Peter Smith 2012-07-09T06:48:30Z 2012-07-09T06:48:30Z Noah: Thanks for this -- and I suspect that my Qn A misfires (I was wondering about fiddling with coding schemes, forgetting to keep other things constant!). But with your construction, do we get the second half of the defn for representing a relation? If not-$\mathit{Prf}_1(m, n)$ we get $T \vdash \neg\mathsf{Prf_1(m, n)}$. And by your hypothesis, for all $m$ we get $T \vdash \neg\mathsf{Prf_1(m, [\psi])}$. But that won't give us that if not-$\mathit{Prf}_1(m, n)$ then $T \vdash \neg\mathsf{Prf_1(m, n)} \land \neg\mathsf{\exists x Prf_1(x, [\psi])}$ will it? http://mathoverflow.net/questions/100934/are-there-any-natural-recursively-but-not-primitive-recursively-axiomatized-theor/100999#100999 Comment by Peter Smith Peter Smith 2012-07-03T23:14:36Z 2012-07-03T23:14:36Z Yep my hope is that there's little mathematics at stake. But I was a bit worried I was missing something interesting ....! http://mathoverflow.net/questions/100934/are-there-any-natural-recursively-but-not-primitive-recursively-axiomatized-theor/100961#100961 Comment by Peter Smith Peter Smith 2012-07-03T18:31:48Z 2012-07-03T18:31:48Z My comment, on reflection, is the same as for Ali Enayat's lovely case. Here too we have an r.e. set of sentences, but not recursively decidable as presented, so not a recursively axiomatized theory in the (I hope non-deviant) sense I was using. No? http://mathoverflow.net/questions/100934/are-there-any-natural-recursively-but-not-primitive-recursively-axiomatized-theor/100999#100999 Comment by Peter Smith Peter Smith 2012-07-03T18:25:57Z 2012-07-03T18:25:57Z [Sorry for the seemingly unappreciative terseness, due to the constraints of the comment box!] http://mathoverflow.net/questions/100934/are-there-any-natural-recursively-but-not-primitive-recursively-axiomatized-theor/100999#100999 Comment by Peter Smith Peter Smith 2012-07-03T18:24:23Z 2012-07-03T18:24:23Z A lovely example, of course! But what exactly it is an example of? $T_{ZFC}$ is, as you say, a natural r.e. set of sentences of great interest. But it isn't, as presented, a recursively axiomatized theory in the sense in my question -- taking those sentences as the axioms, the property-of-numbering-an-axiom (i.e. of numbering an arithmetical consequence on ZFC) isn't recursive. And the nice reaxiomatizations are primitively recursively axiomatized, no? So the question remains doesn't it? Are there natural cases of decidable axiomatized theories, where the decision requires unbounded search?