[FOM] Proof "from the book"
Aatu Koskensilta
aatu.koskensilta at xortec.fi
Wed Sep 1 05:49:23 EDT 2004
Jeffrey Ketland wrote:
>The notion of "reflective consequence" has been analysed by Feferman. Using
>the Kripke-Feferman truth axioms, Feferman defines a theory Ref(S) which he
>calls the "reflective closure" of S. This is meant to contain the sentences
>one "ought to accept", when one initially accepts a mathematical theory S.
>In a sense, Ref(S) is the result of iterating the construction from S to
>Tr(S). Feferman doesn't advocate iterating Ref(S), but I do not see why.
>
The problem here seems to be that if you advocate iterating Ref(S),
you're committing
yourself to theories of truth which are substantial and might not follow
from what one
is implicitly committing oneself when accepting S. This might be
illustrated by the fact
that Ref(Ref(S)) will in general be stronger than what you get by
autonomously iterating
reflection, so accepting iterating S |-> Ref(S) leads you beyond the
constructive well
orderings which are recognizable as such by principles implicit in the
acceptance of S.
Of course, if one accepts Feferman's analysis, then for any theory S
which is acceptable,
Ref(S) will also be acceptable, and so will be Ref(Ref(S)) and so forth,
for any constructive
well ordering which is or becomes recognizable as such. But it seems
that the acceptability
of such a process depends on commitments about the nature of truth.
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.
That said, I don't think there's any reason not to iterate S |-> Ref(S),
unless one worries, as does
Feferman, that there's something inherently fishy about totalizing the
partial predicates. But this
just means that given a theory T accepted as correct and any means R of
generating theories form
theories which is recognized as correctness-preserving, T|->R(T) can be
iterated along any well-ordering
recognized as such. There is no guarantee that the result of such
iteration is epistemologically
interesting, however. For example, one could start from a theory T and
iterate some sort of a reflection principle
along the well-orderings which are autonomous for some theory stronger
than T, and if we accept this stronger
theory, also come up with a theory containing theorems recognizable as
correct. But it's not at all obvious
what this resulting theory has to do with T.
--
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
mailing list