User peter smith - MathOverflow

Answer by Peter Smith for Basic results with three or more hypotheses

2013-05-15T14:19:43Z

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)?

Rosserized proof-predicates and the derivability conditions.

2013-04-07T17:57:25Z

[Improved version!!]

Suppose $\mathsf{Prov}_R$ is a Rosserized proof predicate for PA (or some other suitable theory). To fix ideas, suppose

$$\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}))}$$

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$.

Then, as is familiar,

PA $\vdash \neg\mathsf{Prov}_R(\overline{\ulcorner\bot\urcorner})$

So the HBL derivability conditions can't all hold for $\mathsf{Prov}_R$.

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.

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.]

So we know the third condition fails. But -- and here at last is the questions:

Is there a simple counterexample to PA $\vdash \psi \to \mathsf{Prov}_R(\overline{\ulcorner\psi\urcorner})$ for $\Sigma_1$ $\psi$,

and if that counterexample doesn't already involve $\mathsf{Prov}_R$,

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})$

either for the given Rosserized predicate, or some cousin?

Mendelson's Mathematical Logic and the missing Appendix on the consistency of PA

2013-02-12T16:42:27Z

A very soft question, but I hope not out of order here.

In the first edition of Elliott Mendelson's classic Introduction to Mathematical Logic (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

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!

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.

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 http://www.logicmatters.net/students/tyl/

Answer by Peter Smith for Mendelson's Mathematical Logic and the missing Appendix on the consistency of PA

2013-02-15T18:40:58Z

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:

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.

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.

[Prof. Mendelson has kindly allowed me to quote him.]

Answer by Peter Smith for How do quantifiers limit scope?

2012-10-14T17:59:10Z

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.

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!

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 Logic Primer very helpful: see the first four chapters of Part 2 at http://tellerprimer.ucdavis.edu/pdf/

When are provability predicates provably equivalent?

2012-07-08T13:19:32Z

Fix notation

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.

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$.

Questions

A) Is it known what are the (most general?) conditions on the relation between coding schemes 1 and 2 for which we have

$T \vdash \Box_1\varphi \leftrightarrow \Box_2\varphi$, for any sentence $\varphi$?

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?

Answer by Peter Smith for Who introduced the concept of Primitive recursive functions?

2012-07-05T13:02:05Z

I believe the explicit use of definitions by primitive recursion goes back to Grassman, 1861.

Dedekind in 1888 not only highlighted such definitions but had a proof that they work as intended, i.e. define unique functions.

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).

Are there any natural recursively but not primitive-recursively axiomatized theories?

2012-06-29T14:09:40Z

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?

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 T which when presented in a natural way requires open-ended searches to check whether a purported T-proof is indeed a proof according to that specification.

[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!]

Comment by Peter Smith

2013-04-10T14:01:36Z

Thanks for the correction, yep should have been $\leq$. But the wff you display is $\neg\mathsf{Prov}_R(\ulcorner\bot\urcorner)$.

Comment by Peter Smith

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)$.

Comment by Peter Smith

2013-04-08T20:49:23Z

Yes, as I said, the second condition can fail. As for Jereslow's trick see e.g. my Gödel book, §33.5 in the second edition, based on Jeroslow, R. G., 1973, Redundancies in the Hilbert-Bernays derivability conditions for Gödel’s second incompleteness theorem. Journal of Symbolic Logic, 38: 359–367.

Comment by Peter Smith

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!)

Comment by Peter Smith

2013-02-12T19:02:42Z

@AliEnayat Good thought!

Comment by Peter Smith

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.

Comment by Peter Smith

2012-09-16T13:17:47Z

I really 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).

Comment by Peter Smith

2012-07-11T06:33:44Z

Thanks for the extra details!

Comment by Peter Smith

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 ...!

Comment by Peter Smith

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?

Comment by Peter Smith

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 ....!

Comment by Peter Smith

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?

Comment by Peter Smith

2012-07-03T18:25:57Z

[Sorry for the seemingly unappreciative terseness, due to the constraints of the comment box!]

Comment by Peter Smith

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?

User peter smith - MathOverflow

Answer by Peter Smith for Basic results with three or more hypotheses

Rosserized proof-predicates and the derivability conditions.

Mendelson's *Mathematical Logic* and the missing Appendix on the consistency of PA

Answer by Peter Smith for Mendelson's *Mathematical Logic* and the missing Appendix on the consistency of PA

Answer by Peter Smith for How do quantifiers limit scope?

When are provability predicates provably equivalent?

Answer by Peter Smith for Who introduced the concept of Primitive recursive functions?

Are there any natural recursively but not primitive-recursively axiomatized theories?

Comment by Peter Smith

Comment by Peter Smith

Comment by Peter Smith

Comment by Peter Smith

Comment by Peter Smith

Comment by Peter Smith

Comment by Peter Smith

Comment by Peter Smith

Comment by Peter Smith

Comment by Peter Smith

Comment by Peter Smith

Comment by Peter Smith

Comment by Peter Smith

Comment by Peter Smith

Mendelson's Mathematical Logic and the missing Appendix on the consistency of PA

Answer by Peter Smith for Mendelson's Mathematical Logic and the missing Appendix on the consistency of PA