Re: [mizar] [gmane.comp.science.types.announce] [Agda] CFP: Dependently Typed Programming (FI Special Issue)

[Robert Boyer <boyer@cs.utexas.edu>]

Hi Andrzej,

So good to hear from you.

> Why you think that first order logic is dubious (PRA
> is a first order theory, isn't it?).

I am not sure whether I think that first order logic is
dubious, and I apologize for apparently making you
think that.  I was merely reflecting on the mental
states of some possible people in some possible
universes.

It is certainly the case that Primitive Recursive
Arithmetic can be cast within first order logic, to
resemble, a first-order theory.

However, PRA can also be cast quite independently in a
considerably weaker logical setting.  I think that
officially, PRA is often viewed as a quantifier free
system of equations, implicitly universally quantified
on the far outside.  Good enough for calculation, and
all other government work :).  The induction principle
is cast as a rule of inference: if you can prove the
base case and the induction step, then you may infer a
new theorem by induction.  The definition principle of
PRA gets one all the primitive recursive functions.
Goodstein's book has a nice development of Skolem's
vision, which I think is not dissimilar to McCarthy's
systems for reasoning about Lisp functions, using
cons/car/cdr instead of 0 and s(x).  In official PRA
you cannot even state, much less prove, that theorem of
first order logic I previoulsy mentioned:

   For some x, P(x) or not P(x).

I think that intuitionists and constructivists tend to
regard Primitive Recursive Arithmetic as 'OK', or even
'trivially OK'.  Thus, while they may generally not
accept

       P or not P

for arbitrary P, they will agree that

       for all nonnegative integers x, 
         fn(x) = 0 or fn(x) /= 0,

where fn is a specific function, say 'factorial' (!),
that we have defined by primitive recursion.

There is no doubt that one can prove the consistency of
first order logic!  But assuming what?  Nihilo ex
nihilo.  I believe that if you look hard, you can
always find some rational, thinking,
mathematician/logician who refuses to assume whatever
it is you wish to assume to prove the consistency of
first order logic.

To prove the consistency of first order logic, you'd
probably want the notion of a model, a set theoretic
structure.  But in what set theory?  You might need
something, gasp, as strong as Koenig's lemma!  And you
might find someone who is uneasy about assuming that.

I think that instead of contemplating logics, which
always feel a tad artificial to me, one can cut to
heart of the matter by look at 'the thing':

   P(N) =  {x : x is a subset of N}

where N is the set of nonnegative integers.  I mean the
'power set' of N.  Some people won't let you get past
your wish to believe that P(N) exists, or can be talked
about, or treated as more than a string of charcters.
de Bruijn likes to say that mathematical objects have
the same reality as the characters in, say, a Sherlock
Holmes story.

I do not happen to agree 100% with any of the
constructivists and the intutionists.  First of all, I
am too slow and dumb even to say I even fully
comprehend any of their positions.  But I do not assert
that any of them are wrong.  There are too many of
them, and they are all smarter than me, as are you!

But I am also not an agnostic anarchist.  I think I am
sure about the associativity of addition on the
nonnegative integers.  At least up to a Gogol, 10^100,
because we have recently checked that result with 'bdd'
technology, a kind of mechanical propositional calculus
reasoning commonly used in hardware verification. :)

Bob