Research Area: Foundations of Mathematics
Mathematics is built on a formal system, including logic and the axioms of set theory. The study of the foundations of mathematics focuses on this formal system and possible alternative.
Algebraic logic offers algebraic descriptions of models appropriate for the study of various logics. The classical example is the equivalence of propositional calculus and Boolean algebras.
We are interested in residuated lattices (which include Boolean algebras, Heyting algebras and MV-algebras, for instance) and the corresponding logics. We also study decidability and the properties of proofs in substructural logics, i.e., logics that lack one of the usual structural rules.
Set theory constitutes a foundation for all of mathematics. In its inception, set theory dealt with axiomatics, clarifying and studying the axioms on which mathematics is based, and discovering their consequences as well as their limitations. Modern set theory continues this line of investigation as well as others, in particular, giving precise methods for studying real analysis, measure theory, and topology. The main tools of modern set theory are cardinal invariants, combinatorics, forcing, forcing axioms, inner models, and large cardinal axioms.
At DU, we work on set theory involving all of the above. Of particular interest are ultrafilters and their applications in logic, set theory and topology, including the Stone–Čech compactification of the natural numbers. The classification of ultrafilters up to Tukey (cofinal) type is one current focus of research. This study is connecting Ramsey theory to ultrafilters in an interesting manner.
Automated deduction is a field of artificial intelligence focused on rigorous, computer assisted proofs of mathematical theorems. Automated deduction can provide early insights into increasingly more technical areas of mathematics and also establish original, state-of-the-art theorems. While some human guidance is usually necessary to obtain complicated proofs by "automated" deduction, the proofs can then be routinely checked for correctness.
We are mostly using automated deduction in the area of nonassociative mathematics. Many proofs we obtained were humanized for publication in standard mathematical research journals. Other proofs are too long (tens of thousands of steps) but they nevertheless impact the field. Furthermore, feedback from working mathematicians helps researchers in automated deduction and leads to software improvements.