The Coq mailing list

[Valentin Blot <coq-club AT valentinblot.org>]

Dear Marco,

What you suggest is perfectly valid and it is a fragment of what is
usually called first-order arithmetic at finite types. The idea is that
you can translate a second-order syntax into a first-order (multi-
sorted) one. However, this system is conservative over first-order
arithmetic, and therefore much weaker that second-order.

The real difference between first-order and second-order arithmetic
lies in the second-order elimination rule that says that from forall X
A you can deduce A[B/X] for an arbitrary formula B. This is valid in
second-order logic, but fails in first-order logic.

At first-order, since your variable X ranges over lambda-terms of type
T_1->...->T_n->bool, you can only instantiate it with computable
predicates (in your case, computable in simply-typed lambda-calculus)
and therefore you only have very restricted instances of second-order
elimination. For example if you take:
B(x)="Turing machine x terminates"
you will of course not be able to compute it with a lambda term so B
falls outside the domain of X. You can't deduce A[B/X] for this B from
forall X A.

One way to obtain the full second-order elimination rule (and therefore
full second-order arithmetic) in a first-order setting is by adding to
your system the comprehension axiom scheme: exists X (A(t_1,...t_n) <-> 
X(t_1,...t_n)) for all formulas A. With this scheme you can derive the
second-order elimination rule and you have the full power of second-
order arithmetic. But of course this scheme is not valid if you
interpret predicates as lambda-terms: every instance where
A(t_1,...t_n) is not computable is invalid in this setting.

I hope this answers (at least partially) your question.

Valentin

On mer., 2017-11-08 at 06:10 +1300, Marco Servetto wrote:
> Difference between first and second order logic
> (when predicates are lambda terms)
> 
> Assume a simply typed lambda calculus, where the
> conventional church encoding for True and False are typed in "Bool".
> A predicate is a well typed lambda abstraction typed  T1->..->Tn-
> >Bool
> All elements in all domains are well typed lambda abstraction (for
> some type)
> 
> Considering Execute[T0..Tn]
> =lambda xo:T0,..,xn:Tn . x0..xn
> and a second order logic on those predicates and elements,
> Of course I can translate every
> logic term of form "forall P P(x1..xn)"
> into "forall P Execute[_](P,x1..xn)"
> So, it seams like there is no real difference between first and
> second
> order logic.
> 
> -Does this makes sense? I would expect this to be a well known
> result.
> 
> -Is this valid for COQ too? COQ is based on
> calculus of inductive constructions, that is a variation of lambda
> calculus.. but I would expect that there is a point where this
> breaks...
> 
> 
> Marco