Mathematical Sciences: Applied Mathematical Logic

点击翻译按钮获取中文摘要

In automated deduction, the project involves the computer verification of proofs of mathematical theorems. It addresses the problem of automatically generating proofs of individual lemmas, and also sets forth a general framework for verifying large fragments of mathematics through a development of axiomatic set theory. In logic programming, the project considers Prolog-style languages. These derive from logic, but there are serious questions about their semantics, and there are several divergent points of view on what a logic program "should" mean. The goal is to clean up the semantics, while still maintaining Prolog's efficiency as a programming language. In set theory and topology, three topics of research are planned. (1) Homogeneity properties of compact spaces. (2) Real-valued measurable cardinals; recent advances by Gitik and Shelah make it reasonable to reconsider some old questions in this area. (3) Martin's Axiom (MA) and uncountable cardinals below the continuum. Specifically, the investigator would like to find models where MA first fails at a singular cardinal of cofinality greater than omega-one and would like to discover consistent PFA-style axioms which allow the continuum to be greater than omega-two. This project thus involves several apparently unrelated areas, logic programming and proof verification on the one hand and set theoretic topology on the other hand. The former has a more obvious relation to practical problems of computer science, but the underlying connection is through the habits of mind cultivated by long study of mathematical logic.