FOM: Intuitionism (Tait)

[Vladimir N.Krupski]

> >> Since (Proposition 3.23, p. 131, Elliott Mendelson, 1964, Introduction to
> Mathematical Logic, Van Nostrand, New York),  then I would expect as much.
> >> Charlie Volkstorf
>
> > Thank you.  Now I see that the corresponding proof predicate can be
> constructed via Fixed Point Theorem but I don't see any direct ("suitable for
> programming") construction of a decidable (\Delta_{1}-formula) proof
> predicate with the property Prf(n,F)->Prf(n,Prf(n,F)).
> > Vladimir N. Krupski
>
> Must the proof of P be the same as the proof that this proof proves P?  As a
> proof proves only one sentence (if we defined it to include corollaries, then
> Prf would no longer be recursive, but only recursively enumerable), then F
> would have to coincide with Prf(n,F).
No, it is a wrong argument. Recusive multy-valued proof predicates
are studied intensively in Artemov's logic LP (Logic of Proofs)
[see S.Artemov, Explicid provability and constructive semantics,
Bull. Symbolic Logic 7 (2001) 1-36]. He considered the
finitely-valued proof predicates there -- a proof proves a finite set
of sentences. The Tait's proof predicate is infinitely-valued.

I made the same mistake firts (while answering
the initial question about Tait's statement). Your previous posting
moved me to construct an arithmetical \Delta_{1}-formula Prf(x,y)
(the corresponding predicate is recursive) which really represents a proof
predicate  (i.e. (PA proves F) <-> (PA proves Prf(n,F) for some n) ) and
for which
        Prf(n,F) -> Prf(n,Prf(n,F))
holds (and is PA-provable too).
Roughly speaking it is possible to define
by a Fixed Point equation a multy-valued proof predicate

Prf(n,F) <->
"n is a Godel number of a (standard) proof of some
formula G and G is the shortest formula for which
F = Prf(...,Prf(..., ... Prf(...,G)...))".

All the quantifiers inside it are bound, so it gives a recursive relation.
The statemetns F and Prf(n,F) in this case remain different but have
the same "reflected proofs" (proofs in the sense of Prf )
provided Prf(n,F) is valid.

The problem come when I try to link this Prf with some external representation
of PA (or HA, or HA+... ) as a calculus and to use n s.t. Prf(n,F) as
a code of external derivation of F. What kind of calculus should it be ?
Another related problem is the implementation of this Prf as a proof
checking program. We may simply rewrite its definition in ML or we may
first solve the fixed poin equation "by hands" and than program the
solution. What is the difference? Which is better ?  Is it pracically
possible to solve the equations "by hands"? Any other methods
(in particular those which involve the external proofs)?

> Would a recursive f such that Prf(n,F)->Prf(f(n),Prf(n,F)) be helpful?
> (Shall we make the implication two-way?)  Or perhaps combine them into
> Prf(n,F^Prf(n,F))?
>
> Charlie Volkstorf

There is a relation but it is in some sense a "backward relation" for me.
My interest to Tait's proof predicate comes from  Artemov's propositional
proof logic LP.  LP already contains the unary operation "!" denoting this f .
In LP there are two sorts of objects -- proof terms (or proof polynomials)
and formulas. When t is a proof term and F is a formula then (t:F) is
a formula "t proves F". Proof terms are build from atomic proofs  using
the operations:
* (modus ponens),
+ (union of proofs)
! (proof checker -- for which    t:F->!t:(t:F)   holds).
In LP all proof terms are finite and denote particular PA-proofs.
I am thinking about the semantics for infinite series of proof terms
t0+t1+...
The Tait's notion of proof gives a good example -- it is a series
x+!x+!!x+...

Vladimir N. Krupski
Associate Professor
Department of Mathematical Logic and Theory of Algorithms
Moscow State University, Russia.

homepage: http://lpcs.math.msu.ru/~krupski/
e-mail: krupski at lpcs.math.msu.ru  (office)
        kru at voll.math.msu.su      (home)