The Coq mailing list

[Marco Servetto <marco.servetto AT gmail.com>]

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