An [omega]-order predicate logic with types

Abstract

A type is a symbol used to separate objects in the universe into different groups. The objects in traditional predicate logic have no types (or, equivalently, they all have the same type), so in some theories which need at least two classes of object, such as the theory of vector spaces or homomorphisms of two groups, we can not write some theorems using untypes predicate logic. This thesis proposes a predicate logic with types. In it we will formulate syntax, sematics, and formal proofs, and prove some metatheorems, including the soundness theorem. Finally, we will give counterexamples to show that the compactness and completeness theorems fail in this logic.