This is a response to Richard's remark on the previous post:
Well, yeah, I didn't say it's the most useful or intuitive one. I just said it's simple. The main question is whether the formula strongly represents in T the consistency of T, no?
So if you check out Mostowski's "Thirty years of Foundational Studes" his way of defining this is this. He first assumes that T is consistent (and extends PRA). Then he says:
A slightly different approach is not to assume the consistency of T, and to say that Pr' captures (in T) provability (in T) iff both:
(also, correct me if I'm wrong, but if T is PA, then Con'(PA) captures PA's consistency, and there's nothing wrong about PA proving Con'(PA) if PA is inconsistent.)
Now, if you call a consistency claim of T any formula that in T strongly represents T's consistency, Mostowski's formula is a consistency claim.
This all only shows that strong representation requirement isn't as hard to satisfy as one might initially think. And of course, there are other requirements you might put on formulas to count as "real" consistency claims.
This has an unfortunate property that RCon doesn't have. If T is inconsistent, then, PA |- Con'(T). So this doesn't really have much claim to being called a consistency statement, does it?Since it was too long to post in one piece in the comments, here it is.
Well, yeah, I didn't say it's the most useful or intuitive one. I just said it's simple. The main question is whether the formula strongly represents in T the consistency of T, no?
So if you check out Mostowski's "Thirty years of Foundational Studes" his way of defining this is this. He first assumes that T is consistent (and extends PRA). Then he says:
"We shall say that a formula F with one free variable is a weak description of a set X of integers if for any integer n the formula F(\bar n) is provable in T just in case n is an element of X. If F is a weak description of X and ~F is a weak description of the complement of X, then we call F a strong description of X in T."Right, so what we care about in this setting is whether Pr' strongly represents in T provability in T. And indeed, it does.
A slightly different approach is not to assume the consistency of T, and to say that Pr' captures (in T) provability (in T) iff both:
If [n]If T is consistent, then everything works out just fine for Pr', and if T is inconsistent, then vacuously also both conditions are satisfied, right?(the object whose godel number is n) is a proof of [m], then T proves Pr'(n,m), and
if [n]is not a proof of [m], then T proves ~Pr'(n,m).
(also, correct me if I'm wrong, but if T is PA, then Con'(PA) captures PA's consistency, and there's nothing wrong about PA proving Con'(PA) if PA is inconsistent.)
Now, if you call a consistency claim of T any formula that in T strongly represents T's consistency, Mostowski's formula is a consistency claim.
This all only shows that strong representation requirement isn't as hard to satisfy as one might initially think. And of course, there are other requirements you might put on formulas to count as "real" consistency claims.
Comments