FOM: Tennant's Principle

[Harvey Friedman]

I wish to thank Tennant 10:15PM 10/19/98 for a vastly improved posting,
which raises some interesting matters which are both conceptually and
formally interesting. Note that his posting does confirm to my surmise in
10:28PM 10/18/98 that

>**Perhaps Tennant thinks that he has the best justification of all for it
>[classical logic], that is superior to other justifications?**

Aside from the philosophical issues raised, which suggest a kind of
"falsifiability justification or interpretation of classical logic," one
can easily distill a principle of intuitionism that can be asserted at
various levels of formality or informality. At the informal level, there is
the following principle, which might be called "Tennant's principle" TP:

TP: every classically true sentence is equivalent over classical predicate
calculus (with equality) to an intuitionistically true sentence with no
universal quantifiers.

One can use conjunction to deal with sets of sentences here. We are
deliberately unspecific about the primitives used for the sentences under
question, a matter that will be taken up below.

Note that TP mixes both classical and intuitionistic truth, which can be
questioned or objected to. So one would like formulations that mention only
intuitionistic truth. To begin with, consider:

*: every sentence whose double negation translation (Godel) is
intuitionistically true is equivalent over classical predicate calculus to
an intuitionistically true sentence with no universal quantifiers.

However, this is clearly correct in light of the following:

LEMMA 1. Let A be a sentence in predicate calculus with equality. Then the
double negation translation of A is equivalent to a sentence involving only
existential quantifiers, negation, disjunction over intuitionistic
predicate calculus with equality. The same is true is we replace
"disjunction" by "conjunction," or by "implication."

Thus TP follows from the following principle:

**: the double negation translation of every classically true sentence is
intuitionistically true.

It is convenient to let CPC(=) be classical predicate calculus with
equality, and IPC(=) be intuitionistic predicate calculus with equality.

On the other hand, suppose that TP holds, and let A be classically true.
Let B be an intuitionistically true sentence with no universal quantifiers,
which is equivalent to A over CPC(=). Then the double negation translation
of (A iff B) is provable in IPC(=). But by the following lemma, the double
negation translation of B follows from B in IPC(=). Therefore the double
negation translation of A is intuitionistically true.

We have therefore shown that TP is equivalent to **!

LEMMA 2. Let A be a sentence in PC(=) with no universal quanitifers. Then A
implies the double negation translation of A in IPC(=).

Now how do we best formalize this argument? For each finite relational type
t, construct a base intuitionsitic system I(t) based on a small amount of
arithmetic and a truth predicate for all formulas in the language over that
finite relational type. Normally this would be done by introducing a new
sort for natural numbers. Since the background logic is intuitionistic, the
truth predicate is viewed as an intuitionistic formulation of
intuitionistic truth. Now add a predicate symbol C(n) for classical truth;
i.e., C(n) intuitively menas that "n" is classically true. Make sure there
is a little bit of induction for the extended language. Then there is no
problem formulating TP and its variants. We of course add some trivial
axioms about C(n).

Then we get the following results:

THEOREM A. Let X be any subset of (therexists,not,and,or,implies} which
contains therexists, not, and at least one of the remaining. Let t be a
finite relational type. The following are all equivalent in the system
I(t).
	1. every classically true sentence is provably eqivalent over
CPC(=) to an intutionistically true sentence without universal quantifiers.
	2. every classically true sentence is provably eqivalent over
CPC(=) to an intutionistically true sentence in X.
	3. the double negation translation of every classically true
sentence is intuitionistically true.

We now formulate TP for particular contexts.

*THE CONTEXT OF FIRST ORDER ARITHMETIC*

Arithmetic TP. Every classically true arithemtic sentence is equivalent
over CPC(=) to an intuitionstically true sentence with no universal
quantifiers.

Arithmetic **: The double negation translation of every classically true
arithemtic sentence is intuitionistically true.

As above, these are demonstrably equivalent. But now, we wish to plug a
specific formal system in for TP:

TP for PA. Every sentence provable in PA is equivalent over CPC(=) to an
intuitionistically true sentence with no universal quantifiers.

** for PA. The double negation translation of every sentence provable in PA
is intuitionistically true.

As usual, TP for PA is equivalent to ** for PA. But ** for PA is outright
true; in fact (Godel), the double negation translation of every sentence
provable in PA is provable in HA (Heyting arithmetic).

*THE CONTEXT OF SECOND ORDER ARITHMETIC*

Here we have variables over natural numbers, variables over sets of natural
numbers, equality between natural numbers only, +,x,0,S, and epsilon
between terms denoting natural numbers and set variables. We have the usual
axioms for successor, defining equations for +,x, full induction, and full
comprehension. THis system is well studied with both classical and
intuitionistic logic. Let us call this language L2. And the systems Z2 and
IZ2 (classical and intuitionistic).

Of course, we have the informal

TP for L2. Every classically true L2 sentence is equivalent over CPC(=) to
an intuitionstically true sentence with no universal quantifiers.

** for L2. The double negation translation of every classically true L2
sentence is intuitionistically true.

as well as their informal equivalence.

Now consider

TP for Z2. Every sentence provable in Z2 is equivalent over CPC(=) to an
intuitionistically true sentence with no universal quantifiers.

** for Z2. The double negation translation of every sentence provable in Z2
is intuitionistically true.

And again this *can be viewed as* outright true, since the double negation
translation of every sentence provable in Z2 is provable in IZ2. However, I
think that intuitionistists may disagree on the intuitionistic truth of
IZ2.

*THE CONTEXT OF RESTRICTED SET THEORY*

Here we consider set theory as the theory of V(omega + omega), where
Replacement or Collection is not an issue. Let Z be the usual Zermelo set
theory without the axiom of choice.

Of course, we have the informal

TP for V(omega + omega). Every classically true sentence about V(omega +
omega) is equivalent over CPC(=) to an intuitionstically true sentence with
no universal quantifiers.

** for V(omega + omega). The double negation translation of every
classically true sentence about V(omega + omega) is intuitionistically true.

as well as their informal equivalence.

But there is a major headache here. Consider the axiom of extensionality:
if two sets have the same elements then they are equal. Or if we ban
equality entirely, then: if two sets have the same elements then they are
elements of the same sets. The double negation of extensionality is
suspicious intuitionistically. In fact, I suspect that it is downright
incompatible with the intuitionsitc point of view. However, I have not
investigated this metamathemtically, always just assuming that it is bad.
Tennant's ideas prompt me to look further into this.

I do, however, regard extensionality itself - as distinct from its double
negation translation - as fine intuitionistically. I have studied IZ, which
is just Z with intuitionistic logic, and this is a sensible system.

Now there is a kind of nonextensional notion of V(omega + omega) that seems
natural enough. There is no attempt to identify sets with the same
elements. This makes sense both classically and intuitionistically. So we
consider:

TP for nonextensional V(omega + omega).  Every classically true sentence
about nonextensional V(omega + omega) is equivalent over CPC(=) to an
intuitionstically true sentence with no universal quantifiers.

** for nonextensional V(omega + omega). The double negation translation of
every classically true sentence about nonextensional V(omega + omega) is
intuitionistically true.

However, here there is an issue about power set. There is the ordinary
power set axiom, and there is a weaker power set axiom that is important.
This weaker one asserts that every set x has a weak power set y, in the
sense that every subset of x is extensionally equal to some element of y.
Thus if we use Z' for Z with extensionality dropped and power set replaced
by weak power set, then:

TP for Z':  Every sentence provable in Z' is equivalent over CPC(=) to an
intuitionstically true sentence with no universal quantifiers.

** for Z': The double negation translation of every sentence provable in Z'
is intuitionistically true.

are outright true in light of the following. That the double negation
translation of every sentence provable in Z' is provable in intuitionistic
Z'. This argument is valid if one accepts Z' or the larger system Z as
intuitionistically true.

I have not investigated the system Z'' which is obtained from Z by dropping
extensionality and leaving power set unmodified. The problem is that the
double negation translation of unmodified power set apparently is not
provable in intuitionistic Z.

*THE CONTEXT OF FULL SET THEORY*

If Collection is used instead of the more common Replacement, then all of
the issues and difficulties here are already present in the previous
discussion of "the context of restricted set theory." In fact, the issue of
extensionality (not power set) can already be joined in the section "the
context of second order arithmetic" if we allow equality between sets of
natural numbers. I haven't even had time to straighten this out.