Study On Lattice-valued Logic Based On Lattice Implication Algebra And Its Model Theory

At present, logic is applied widely in computer science, such as the design of logic circuits, analysis of programming, validation of security protocol, artificial intelligence. Various kinds of logic systems not only provide language tools for knowledge representation, but also afford mechanized algorithms for knowledge inference. The research results on this lay a theoretical foundation for realizing the automatization of calculation and inference. On the other hand, the rapid development of computer science, especially artificial intelligence, provides the vast background and real requirements for theroetical research and actual applications of logic. Lattice-valued logic is a kind of very important non-classical logics, it not only describes totally ordered information, but also non-totally ordered (incomparable) uncertain information. Based on the outcome on lattice implication algebra and lattice-valued logic, the following aspects are investigated deeply in this paper: Part One. The study of lattice implication algebra1. The notion of locally finite lattice implication algebra is introduced and its basic properties are discussed. It is proved that every locally finite lattice implication algebra is a chain and equivalent to a simple lattice implication algebra;2. Some properties of prime dual ideals of lattice implication algebra are discussed;3. Priestley duality of lattice implication algebra is obtained from that of distributive lattice and MV-algebra;4. The uniqueness of LIA-implication (namely, the implication operation satisfying the definition of lattice implication algebra ) on Kleene algebra is discussed and a method for constructing new lattice implication algebras on Kleene algebra is given;5. At least countable lattice implication algebras different from Lukasiewicz implication algebra on [0,1] are given, furthermore, it is denoted that they are locally finite.Part Two. The study of lattice-valued logic systemsInternal truth values are incorporated in the language of lattice-valued propositional logic system LP(X) and its corresponding first-order logic system LF{X), which enhances their abilities of knowledge representation. However, these two logic systems are based on more complicated axiom systems, and some important tautologies are difficult or cannot be inferred from the axioms of LP(X) and LF{X). So in this paper, LP{X) and LF{X) are simplified and improved, lattice-valued propositional logic system p and its corresponding first-orderlogic system p based on lattice implication algebra are constructed. This part consists of the following points:1. Basic structures of the system p, namely, its language, semantics and syntax are given and some theorems are proved;2. Some important properties of the system pLF based on locally finite lattice implication algebra are discussed, and soundness theorem, deduction theorem, completeness theorem and consistency theorem are obtained;3. Basic structures and some theorems of the system F are given;4. In the system FLF based on locally finite lattice implication algebra, soundness theorem, deduction theorem, completeness theorem, consistency theorem, upward and downward L-S-T theorem are proved.Part Three . The study of model theory of lattice-valued first-order logic FIn virtue of the idea and methods of classical model theory, model theory of lattice-valued first-order logic F based on lattice implication algebra are investigated elementarily. This part comprises the following points:1. The concepts of homomorphism, isomorphism, expansion, reduct, submodel and extension and so forth in classical model theory are generalized to lattice-valued ones and their related properties are discussed;2. The similarity measurement between lattice-valued models are defined based on fuzzy equalities;3. Elementary chain theorem of lattice-valued models is proved;4. The ultraproduct basic theorem based on finite lattice implication algebra is obtained and its two applications are given.In this paper, on the one hand, lattice implication algebra, lattice-valu...