[FOM] Proof "from the book"

[Aatu Koskensilta]

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