On the extended completeness theorem of intuitionistic predicate logic

• Main Authors: Tzu-yu Wu, 吳子瑜
• Other Authors: Jui-lin Lee
• Format: Others
• Language: en_US
• Published: 2008
• Online Access: http://ndltd.ncl.edu.tw/handle/56170722328195681147

碩士 === 國立中正大學 === 哲學所 === 96 === Given a first order language L without equality symbol, we formally define the notion of intuitionistic Kripke semantics using a method similar to that in classical semantics. We introduce a partial order set and for each element of this set there is a corresponding diagram structure for the language L. Then we define the validity in intuitionistic Kripke semantics. For convenience we name all the elements of the domain of each diagram classical structure relative to an element of the partial order set and then we have an equivalent way to describe an intuitionistic Kripke structure. We have an intuitionistic proof system Hi which is an axiomatic proof system. We prove that Hi over a language without equality symbol is complete with respect to corresponding Kripke semantics. We also consider the case of a language with equality symbol. We define the Kripke model for a language with equality symbol and prove that Hi over this language has the extended completeness property.