[FOM] Proof "from the book"

[Aatu Koskensilta]

Jeffrey Ketland wrote:

>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".
>
Ok, but that's not quite what I meant. I consider iterating the Kripkean 
construction of
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 
convince ourselves
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. 
autonomous progressions
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 
Gödelian reasons
- 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 
consistent, which
contradicts Gödel's 2nd incompleteness theorem - and because I can't see 
how we
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 
predicatively recognizable
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 
means of
iterated reflection, can't be predicatively recognized as a correct 
procedure. So iterating
this procedure can not tell us anything epistemologically interesting 
about predicitivism.
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 
the acceptance
of S.

>The truth
>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 
notation for
an ordinal.

-- 
Aatu Koskensilta (aatu.koskensilta at xortec.fi)

"Wovon man nicht sprechen kann, daruber muss man schweigen"
 - Ludwig Wittgenstein, Tractatus Logico-PHilosophicus