A minimalistic many-valued theory of types
Libor Běhounek · Journal of Logic and Computation · 2016
A parsimonious Church-style theory of types TT0 is introduced that admits Henkin-style models over algebras of truth values for a broad class of non-classical logics. The only logical symbols of TT0 are the constants for (many-valued) equality on each type, governed by the derivation rules of substitution, intersubstitutivity of equals, λ-abstraction and extensionality. The strong soundness and completeness of TT0 w.r.t. the Henkin-style semantics is proved. A broad range of non-classical Henkin-style higher-order logics can be cast as extensions of TT0 and their Henkin completeness be obtained by minor addenda to the proof for TT0. Three sample extensions of TT0 are introduced and their Henkin completeness proved.