FORMALIZING THE META -THEORY OF FIRST-ORDER PREDICATE LOGIC
- 주제(키워드) formal proofs , first-order predicate logic , Kripke semantics , soundness , completeness
- 관리정보기술 faculty
- 등재 SCIE, SCOPUS, KCI등재
- 발행기관 KOREAN MATHEMATICAL SOC
- 발행년도 2017
- URI http://www.dcollection.net/handler/ewha/000000147280
- 본문언어 영어
- Published As http://dx.doi.org/10.4134/JKMS.j160546
초록/요약
This paper introduces a representation style of variable binding using dependent types when formalizing meta-theoretic properties. The style we present is a variation of the Coquand-McKinna-Pollack's locally-named representation. The main characteristic is the use of dependent families in defining expressions such as terms and formulas. In this manner, we can handle many syntactic elements, among which wellformedness, provability, soundness, and completeness are critical, in a compact manner. Another point of our paper is to investigate the roles of free variables and constants. Our idea is that fresh constants can entirely play the role of free variables in formalizing meta-theories of first-order predicate logic. In order to show the feasibility of our idea, we formalized the soundness and completeness of LIT with respect to Kripke semantics using the proof assistant Coq, where LJT is the intuitionistic first-order predicate calculus. The proof assistant Coq supports all the functionalities we need: intentional type theory, dependent types, inductive families, and simultaneous substitution.
more