[FOM] Proof "from the book"

[Jeffrey Ketland]

Aatu Koskensilta:

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

I define "substantial theory of truth" to mean, roughly, "non-conservative".
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.

>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.
In a very deep sense, the epistemological description of a language (i.e.,
the semantical truth theory) lies outside the original language. The truth
axioms of Tr(S) are not implicit anywhere in S. Rather, the arithmetic
conseqences of Tr(S) are implicit in S.
We can call the hierarchy you mention the Kripke-Tarski hierarchy: we pass
from a base model M to the partial structure (M, S1, S2), where (S1, S2) is,
say, the least Kripke fixed-point over M. We next treat this structure as a
classical structure M* ("closing-off"), and iterate. Kripke himself hinted
at such an idea in his 1975 paper, where he commented that "the ghost of the
Tarski hierarchy is still with us".

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

Agreed. I don't worry about totalizing the partial truth and falsity
predicates after they've done their work in implementing Kripke's notion of
groundedness. If a sentence is not groundedly true and not groundedly false,
then this is a definite state of affairs. Interpreted over the classical
structure, the strenghtened liar statement comes out true (but ungrounded).
Indeed, KF proves this sentence, since KF proves the scheme T("A")->A. There
is a subtle change of meaning in passing from (M, S1, S2) interpreted with
3-valued semantics, and reinterpreted as a classical structure with bivalent
semantics.
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.

--- Jeff
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Jeffrey Ketland
School of Philosophy, Psychology and Language Sciences
University of Edinburgh, David Hume Tower
George Square, Edinburgh  EH8 9JX, United Kingdom
jeffrey.ketland at ed.ac.uk
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~