1. On the phrases ``weak logic'' and ``strong logic''. There are
several, sometimes contradictory, senses of these words. First,
there is the ``expressive power'' of the logic. A logic may be
strong in that it can express certain concepts that another logic
cannot. For example, second-order logic has predicate variables
and first-order logic does not. Second, there is ``proof-theoretic
strength''. In this sense, theory (or logic) T is stronger than theory
(or logic) S if
there is a translation from S to T that preserves arithmetic
theorems (theorems about natural numbers expressed using +, *, propositional
logic, and quantifiers over natural numbers). For example, just adding
second-order variables to first-order logic does not make a
strictly stronger logic; one has to also add axioms about the
existence of predicates defined by quantified formulas.
The reason for reviewing these definitions is to point out that
some theories are proof-theoretically weak, but are still very
expressive (some versions of Feferman's theories, for example).
On the other hand, some theories are proof-theoretically strong but
not very expressive (for example, pure ZF without a facility for
defined expressions).
2. First-order logic versus other kinds (type theory, for example).
Take your favorite elaboration L of first-order logic L1; if you haven't
a favorite, take T to be second-order logic L2. You may feel that
T is a much better logic than L; it may be both more expressive and
proof-theoretically stronger. But first-order logic is very general;
by enlarging the language we can encompass your logic T. This is
called ``reifying'' T. For example, let us reify second-order logic:
We need two unary predicate symbols Object and Predicate, distinct
from all the symbols of L1. Expanding L1 by these two symbols, we
can translate each formula A of L1 into a first-order formula A*.
The first-order quantifiers of A become (in A*) quantifiers relativized
to the predicate Object, and the second-order quantifiers become
(in A*), quantifiers relativized to Predicate.
( all x. A) * is (all x.(Object(x) -> A*))
( all X. A) * is (all X.(Predicate(X) -> A*))
Second order logic has the primitive formula member(z,X) (often written
Xz); we add the axiom
Str: (member(a,b)->Object(a) & Predicate(b)).
The second-order comprehension axiom schema CA translates to
a first-order schema CA*. The translation is sound in the sense that
L2 proves A implies CA* + Str proves A*. (Indeed this particular
translation is faithful too: if CA* + Str proves A* then L2 proves A.)
A "more powerful logic" has been reduced to a "weak logic" by
reification. The power of the logic has been packed into first-order
axioms. This can be done with EVERY logic. Essentially, Feferman's
theories are to various typed logics as L2 is to CA* + Str in the above
example. John McCarthy argued for many years that first-order logic
is sufficient for AI, because whatever improvements you want to make
can be reified. This was the basic idea behind his development of
the (first-order) ``situation calculus', which reified notions of
time, agent, and action.
3. By reification, we can reduce logics to first-order theories.
In the next paragraphs the word ``theory'', meaning a finite list of axioms
and axiom schemata in first-order logic, can in principle apply to
all the different logics used in theorem-provers today.
A theory T forms a metatheory for theory S if the syntax of S,
including provability, can be defined in T. The metatheory T can be
weaker (in either sense) than the object theory S. Theorems of
S do not necessarily become theorems of T, but T can prove that
the theorems of S are indeed theorems of S:
T proves S-Proof( Num(p), Num(A)) (1)
whenever p is a proof of a formula A in S; here Num(p) and Num(A) are
the numbers (or character strings, or whatever) that represent the
proof p and formula A in T. If the object theory S is stronger
than the metatheory T, then
exists x.(S-proof(x,Num(A)) -> A
will not be provable for some formula A. (This schema, as A varies,
is called the ``reflection principle'' for S.)
Consider, for concreteness, the case of S = ZF. Of course PRA doesn't
prove the reflection principle for ZF. But each fixed theorem A of ZF
is derivable from a finite list of axioms; let Q be their conjunction;
then Q->A is provable in PRA, indeed in unadorned first-order logic.
If the metatheory T can prove the (formalized) deduction theorem about S,
then it will follow from (1) that for each theorem A of S, T proves
Q->A for some axioms Q of S.
4. Checking proofs produced by theorem-proving programs.
The QED manifesto calls for a proof-theoretically weak, but expressive,
metatheory; let us call it Meta. To spell out one of the points made in
the Manifesto: Suppose theorem-proving program P finds proofs in
logic L. Suppose L is reified to the first-order theory S. Suppose
P finds proof q of theorem A in L. Then there is a proof of A*
from a conjunction Q of axioms of S in first-order logic alone.
This proof can be, in principle, extracted from the output or trace of
P and verified independently of the workings of the complicated program P.
This verification should be much simpler than finding the proof
in the first place, since no search will be involved. It would therefore
provide an independent check on the correctness of the result.
5. In practice this means that each non-first-order logic used in
a theorem-prover must be (once and forever) reified. These sets of
first-order axioms can be kept in a fixed file, for example HOL.ax,
Martin-Lof.ax, COQ.ax, etc. I will refer to these files as
``reification files''.
6. The necessary meta-theory of each of these logics should be
developed in Meta (formally, and machine checked), up through the
deduction theorem for the reification of the logic as expressed in
the reification files.
7. Suppose theorem-prover P finds a proof q of a theorem A in
a logic (or theory) S. The implementors of P (or somebody)
will provide a translation program which translates the output
or trace of P into a first-order proof trans(q) of a theorem of the form
Q->A* as described above. In practice Q will have two parts:
(i) a fixed part contained in the axiom file described in 5.
(ii) some axioms (instances of axioms schemata, e.g. induction,
or other axioms special to the problem)
In the case of theorem-provers like Otter that work directly with
first-order logic, the reification step will not be necessary.
8. The output of the translator in step 7 is a proof in
pure first-order predicate calculus. It can therefore be checked
by an extremely simple program. The project of verifying such a
program is not impossible.
9. As a footnote: Since we need some induction to prove
meta-theorems, when translating theorems that need induction
into Meta, we don't need to list as hypotheses any instances
of induction included in Meta; similarly any other axioms of Meta that
may occur in the reification files can be omitted.
The above, I believe, spells out what the Manifesto says.
I think it makes sense to discuss further whether this is a practicable
or useful thing to do. But first let us see if there is agreement
that this is indeed what the Manifesto does say.