Normal Form Theorems for Deductions and Normalization Processes in
Some Higher Order Systems
Grigori Mints and Sergei Tupailo
Preface
This report contains four papers on cut-elimination-type results in second
order logic and type theory. Joint paper of the authors establishes
termination of a higher order extension of the epsilon substitution
method. Next two papers by G. Mints provide cut-elimination theorems
for simple type theory with extensionality and epsilon-symbol, and for
the second order linear logic. The last paper contains a new proof of
completeness of certain strategy for the first order logic which
finitistically implies omega-consistency of arithmetic.
This research was supported in part by the Center for the Study of
Language and Information, Stanford University, and by the NSF grant
DMS-9206976.
Home Page
CSLI Home Page
Stanford Home Page
pubs@roslin.stanford.edu
Date last updated: January 30, 1996