Quantification Theory with Identity and Functional Constants

Abstract

We wish now to extend our theory to include identity and functions. The system will be an extension of HPC which we will call HPC⁼. The primitive symbols are -, ⊃, ∀, ), (, and =; an infinite list of individual variables x₀, x₁, x₂,..., an infinite list of predicate letters F ⁿ₀ , F ⁿ₁ , F ⁿ₂ ,... for each n > 0, an infinite list of constants, c₀, c₁,... and for each n > 0 an infinite list of function letters f ⁿ₀ , f ⁿ₁ ,...