LISA -- A Modern Proof System

TL;DR

LISA is a modern proof system and assistant designed for schematic first-order logic and set theory, featuring a polynomial-time proof checker, a domain-specific language, and proof tactics, demonstrated through formalizations like Cantor's theorem.

Contribution

The paper introduces LISA, a new proof system with a user-friendly language and tactics, supporting formalization in set theory and efficient proof checking.

Findings

Implemented polynomial-time proof checking.

Developed proof tactics leveraging ortholattice properties.

Formalized Cantor's theorem in LISA.

Abstract

We present LISA, a proof system and proof assistant for constructing proofs in schematic first-order logic and axiomatic set theory. The logical kernel of the system is a proof checker for first-order logic with equality and schematic predicate and function symbols. It implements polynomial-time proof checking and uses the axioms of ortholattices (which implies the irrelevance of the order of conjuncts and disjuncts and additional propositional laws). The kernel supports the notion of theorems (whose proofs are not expanded), as well as definitions of predicate symbols and objects whose unique existence is proven. A domain-specific language enables construction of proofs and development of proof tactics with user-friendly tools and presentation, while remaining within the general-purpose language, Scala. We describe the LISA proof system and illustrate the flavour and the level of abstraction of proofs written in LISA. This includes a proof-generating tactic for propositional tautologies, leveraging the ortholattice properties to reduce the size of proofs. We also present early formalization of set theory in LISA, including Cantor's theorem.