hide
Free keywords:
-
Abstract:
We define a weak second--order extension of first--order logic.
We prove a second--order cut elimination theorem for this logic
and use this to prove a conservativity and a realisability
result. We give applications to formal program development and
theorem proving, in particular, in modeling techniques
in formal metatheory.