[FOM] Proof "from the book"
aatu.koskensilta at xortec.fi
Mon Sep 6 11:41:32 EDT 2004
Jeffrey Ketland wrote:
>>The problem here seems to be that if you advocate iterating Ref(S),
>>yourself to theories of truth which are substantial and might not follow
>>from what one
>>is implicitly committing oneself when accepting S.
>I define "substantial theory of truth" to mean, roughly, "non-conservative".
Ok, but that's not quite what I meant. I consider iterating the Kripkean
partial truth predicate more substantial than what is required in order
to accept autonomously
iterated reflection. We need to know very little about truth in order to
that if we accept a theory T as true, then we should accept reflection
principles for it.
>In a similar sense, second-order arithmetic comprises a substantial theory
>of sets of numbers in that it is non-conservative over PA. Impredicative
>second-order set theory (like MK) is also substantial in this sense. Note
>that already the construction S |-> Tr(S) is substantial in this sense, for
>Tr(S) proves "All theorems of S are true" (modulo a subtlety about extending
>the induction scheme to permit the truth predicate). So, even the Tarskian
>extension is substantial, if you accept the analysis of substantiality to
>mean non-conservation. This is the point of recent articles by Stewart
>Shapiro and myself against deflationism.
I agree with your point. However, I like to think that with e.g.
we are trying to characterise not what is implicit in S, but rather what
is implicit in the
acceptance of S. Obviously some sort of reflection principles for S are
implicit in the
acceptance of S.
What sort of reflection principles should be itereated if we're
interested what's implied by
acceptance of S? Clearly S |--> S+Con(S), S |--> S+Prov_S("A")-->A and
so forth are to
be accepted. But where - and more importantly, how - do we draw the
line? The optimal
solution would be that we accept any reflective procedure which provably
in S carries
acceptable theories to acceptable theories. Alas, this doesn't work for
- otherwise in the theory R(S) we could prove that S is consistent, and
R(S) is a theory
obtained from S by a correct reflection procedure, and hence is
contradicts Gödel's 2nd incompleteness theorem - and because I can't see
could in general define in S what it means for a theory to be correct.
A concrete example is provided by predicativism. It's surely
that adding, say, uniform reflection to a theory accepted as correct
produces a correct
theory, and same goes for iterating this operation. However, the
transition from T
to the theory containing the theorems autonomously provable from T by
iterated reflection, can't be predicatively recognized as a correct
procedure. So iterating
this procedure can not tell us anything epistemologically interesting
Perhaps what sort of reflective procedures should be allowed varies from
case to case...
>>Since Ref(S) is obtained
>>from S by adding to it the Kripke-Feferman axioms (and extending the
>>schemata of S to cover
>>sentences containing the truth predicate) going to Ref(Ref(S)) means
>>something like introducing
>>the first level of a hierarchy of fixed points of the Kripke
>>construction, and iterating this
>>process autonomously will lead to a pseudo-Tarskian hierarchy the length
>>of which is the first
>>constructive well ordering which can't be autonomously recognized as
>>such. I think it's hardly
>>plausible that this sort of hierarchy was implicit in acceptance of S.
>I agree. But the same is true of Tarskian extension Tr(S), for we know by
>Tarski's theorem that the truth theory Tr(S) cannot be interpreted within S.
One could argue that Tr(S), while not interpretable in S, is implicit in
>axioms of Tr(S) are not implicit anywhere in S. Rather, the arithmetic
>conseqences of Tr(S) are implicit in S.
Well, implicit in the acceptance of S, I would say.
>Feferman's idea in defining Ref(S) is to define the reflective consequences
>of S. But if Ref(S) is acceptable, then the reflective consequences of
>Ref(S) itself are also acceptable, despite the fact that they are no longer
>implicit only in S.
Of course. Similarly T_alpha in a reflective progression is acceptable
for any theory
T which is accepted and any notation alpha we somehow recognize as a
Aatu Koskensilta (aatu.koskensilta at xortec.fi)
"Wovon man nicht sprechen kann, daruber muss man schweigen"
- Ludwig Wittgenstein, Tractatus Logico-PHilosophicus
More information about the FOM