FOM: Intuitionism (Tait)

[charles silver]

    It's interesting that a thread once referring to Tait turned into
something completely different, and now seems to loop back to Tait again.
What I have in mind is to ask some questions about reflection principles
that I know are confused.   Please bear with me; I would appreciate any
helpful responses from those who are knowledgeable about such matters (Tait,
for example):

    Let some property of numbers or sets be labeled P.  In some formal
system (could be PA, could be ZFC,...?), I'd like to distinguish the
following:
                                        For P |- P  vs. |-P

I realize right away that the above isn't quite correct, P could be any
property at all, and the question I'm asking seems to pertain more directly
to finite sets of some sort, where 'finite' appears on the left but not on
the right of the 'For P|-P' version.   Where P normally
--as far as I know--turns up is when P is shorthand for things like
"for any finite set X1, X2,...,Xn have P"    Hence, filling in P
appropriately would make the left version:

For any finite set X1, X2,...,Xn that have P,  |-X1,X2,...,Xn have P

    Whereas, making the same substitution on the right version gives:
                         |- For any finite set X1, X2,...,Xn have P

    So, clearly the left side of the earlier characterization should
have looked more like "For P|-P' ", where P' in the case spelled out
eliminated the "For any finite set".

    I am at any rate interested in varieties of reflection principles and
thus did not wish to single out any particular version, but ask
about the class of them in general. First, why is the move
across the '|-' called a "reflection principle"?   Who first called it that?
Is it simply called reflection because the thing on the left is (sort-of)
pushed to the right--or "reflected," so to speak?  Second, when
exactly does reflection seem to hold and why?  (This second
question relates to the earlier, mistaken, but more general
contrast between 'For P |- P' and just ' |-P'.  I'd like to
know what P *has* to be--on the left, even though
only some truncated part of it would appear on the right.)

    I probably am very mixed up about this, because, though looked at
in one way reflection seems harmless, in another way it seems altogether
unjustified. Incidentally, the occasion for this question is Neil's response
below where Neil refers to an interesting paper of his that uses a
reflection principle to prove the truth of Godel's G ("I am not provable")
in an extension S* of S, where S* employs reflection.   (It is also a
concern of Neil's to argue in favor of a deflationary view of truth.)
Oh, a third thing I'm wondering about is whether there are instances
of reflection principles that clearly seem *not* to be justified
(that is, the push across the '|-' seems *wrong*).   If it's true that
some seem okay (well-motivated, intuitive, natural, etc.) and some
seem not at all okay, why the difference?

    Having written the above, I realize that it's all but incomprehensible.
I'm sure that before the week's over, I won't be able to fathom what I was
talking about myself.   So, apologies in advance for all the confusion and
also thanks in advance for any clarification.

Charlie Silver


 Neil Tennant said earlier:
> The proof that the Godel-sentence G for a formal system S is true (or: the
> proof of the Godel-sentence G for a formal system S) is of course
> formalizable in a suitable (proper) extension (call it S*) of S. It is an
> interesting question what principles not in S are to be added so as to
> obtain S*, with an eye to proving, in S*, a formal proof recognizably
> preserving the structure of the informal proof of G as given in the
> so-called "semantical argument" for the truth of G. In the following paper
> I make the case that the best new principle to adopt is the uniform
> reflection principle for S for primitive recursive sentences, and show
> that the resulting S*-proof of G makes no use of a truth-predicate, and
> hence is acceptable to the deflationist.
>
> 'Deflationism and the Godel-Phenomena', Mind Vol. 111, 443, July 2002,
> pp. 551-582.
>
> Neil Tennant
>