FOM: Heyting's logic

[Harvey Friedman]

This is a first followup of my posting 6:37PM 9/9/98.

I want to give a somewhat simplified version of a completeness theorem for
Heyting's propositional calculus (HPC) that I published in

Some Applications of Kleene's methods for intuitionsitic systems, the
Proceedings of the Cambridge Summer School in Mathematical Logic, held in
August 1 - 21, 1971, ed. A.R.D. Mathias, Lecture Notes in Mathematics, 337,
Theorem 1.3, page 120.

(This gives some idea how ancient Friedman and Mathias are).

The results in this posting are straightforwardly obtained from that work.

Let X be a subset of the standard propositional connectives
&,v,implies,not,iff,t,f. Then L(X) is the set of finitary formulas
generated by the propositional letters p1,p2,..., and the connectives in X.

We use HPC(&,v,implies,not,iff,t,f) for the least set of formulas in
L(&,v,implies,not,iff,t,f) that contain the usual axiom schemes for HPC and
are closed under modus ponens. We use HPC(X) for the elements of
HPC(&,v,implies,not,iff,t,f) that lie in L(X).

We write A1 implies A2 implies ... implies An, n >= 1, to indicate iterated
implication associated to the right. Thus, e.g., A implies B implies C is A
implies (B implies C). In the presence of conjunction, this is equivalent
over HPC to (A1 & ... & An-1) implies An. Of course, if n = 1 then this is
just A1.

We say that a finite sequence K of formulas is *distinguished* if and only
if it obeys the following conditions:

a) every term in K is either a propositional letter or an implication;
b) no propositional letter in K is the antecedent of a term in K.

For any finite sequence K = K1,...,Kn of formulas and any formula A, we
write (K implies A) for K1 implies K2 implies K3 ... implies A, associated
to the right; if n = 0 then this is just A.

Let T be any set of formulas in L(X), where X includes implies. Consider
the following conditions on T:

1. T is closed under modus ponens.
2. HPC(&,v,implies,not,iff,t,f) is contained in T.
3. Let K be a distinguished finite set of formulas in
L(&,v,implies,not,iff,t,f). Suppose (K implies R) is in T, where R is a
letter. Then R is a term of K, or some term in K has an antecedent A which
is not a propositional letter and for which (K implies A) is in T.
4. Let K be a distinguished finite set of formulas in
L(&,v,implies,not,iff,t,f). Suppose (K implies (D v E)) is in T. Then (K
implies D) is in T, or (K implies E) is in T, or some term in K has an
antecedent A which is not a propositional letter and for which (K implies
A) is in T.

THEOREM 1. T obeys 1-4 if and only if T = HPC(X). If X does not include v,
then clause 4 can be removed.

Question to the FOM. Had some form of this result of mine from 1971 made
its way into the literature? And has it been extended to the predicate
calculus?