An Omnidirectional Extension Of The First-order Logic:Syntax And Semantics

The most discussed, classical and famous logic in modern logic is the first-order predicate logic. However, first-order logics have limited expressive power to express meanings such as "here exist infinite many". Hence we need to enhance it in many ways in order to make it more powerful. Higher order logics are to extend on the "height", admit predicate variables and their quantization; infinitary logics are to extend on the "length", allow us to conjunct infinite number of formulae as well as to quantify infinite number of variables (precisely a set of infinite many formulae and a set of infinite many variables); first-order logics with generalized quantifiers, which can be said extensions on the "mood", contain quantifiers other than universal and existential quantifiers. Hence a question naturally arise:what can we get if we extend a first-order logic in many ways isochronically? The purpose of this paper is to answer this question. In chapter2, we designed a new type theory, which can talk about the type of function variable symbols, connective symbols, quantifier symbols. At the first, we defined domain types, i.e. a kind of type for higher-order domains. Then defined symbol types for both non-logical and logical symbols (except auxiliary symbols such as parentheses).In chapter3we constructed a kind of language which integrated higher-order languages, classical infinitary languages and languages with some generalized quantifiers:unified language. Firstly we introduced some conversion functions used in the construction of languages; then defined semantic types such as similar type, signature, logic type; at the last, we found a kind of generative grammar for unified languages.On the basis of the work in previous chapters, in chapter4we constructed unified logics, which are generalization of higher-order logics, classical infinitary logics and logics with some generalized quantifiers. Firstly we defined structures and models; subsequently defined part the semantics; finally defined some semantic attributes such as consistency and completeness. In the fifth chapter we discussed some properties of unified logics. We cited some relevant conclusions in order theory, proved that the theory operator on extension class (w.r.t (?)) and the model class operator on intension class (w.r.t (?)) of unified logic constitute a pair of Galois connection. Furthermore, we also proved that on a unified logic, its logic lattice, extension lattice, intension lattice, extension Lindenbaum-Taski structure and intension the Lindenbaum-Taski structure are isomorphic to each other.