A Sound and Complete Proof System for STTwU

William M. Farmer

2004

Abstract

STTwU is a very simple version of simple type theory that admits
undefined terms and statements about definedness.  This paper gives a
Hilbert-style proof system for STTwU and proves that it is sound
and complete for the general model semantics for STTwU.