### Abstract

This formalization verifies a decision procedure due to Cantone and Zarba for a quantifier-free fragment of set theory. The fragment is called multi-level syllogistic with singleton, or MLSS for short. Its syntax syntax includes the usual set operations union, intersection, difference, membership, equality as well as the construction of a set containing a single element. We specify the semantics of MLSS in terms of hereditarily finite sets and provide a sound and complete tableau calculus for it. We also provide an executable specification of a decision procedure that applies the rules of the calculus exhaustively and prove its termination. Furthermore, we extend the calculus with a light-weight type system that paves the way for an integration of the procedure into Isabelle/HOL.

### License

BSD License

### Topics

- Logic/General logic/Classical propositional logic
- Logic/Set theory
- Logic/General logic/Decidability of theories

### Related publications

- Stevens, L. (2022). Towards a Verified Tableau Prover for a Quantifier-Free Fragment of Set Theory (Version 2). arXiv. https://doi.org/10.48550/ARXIV.2209.14133

### Session MLSS_Decision_Proc

- MLSS_Logic
- MLSS_HF_Extras
- MLSS_Realisation
- MLSS_Semantics
- MLSS_Typing_Defs
- MLSS_Calculus
- MLSS_Typing
- MLSS_Proc
- MLSS_Suc_Theory
- MLSS_Typing_Urelems
- MLSS_Proc_Code
- MLSS_Proc_All

### Depends on

- Fresh identifiers
- Graph Theory
- The Hereditarily Finite Sets
- List Index

### Auto-related entries

- First-Order Theory of Rewriting
- Soundness of the Q0 proof system for higher-order logic
- Category Theory for ZFC in HOL II: Elementary Theory of 1-Categories
- Recursion Theorem in ZF
- Category Theory with Adjunctions and Limits

## Cite

×

MLSS_Decision_Proc-AFP

    @article{MLSS_Decision_Proc-AFP,
      author  = {Lukas Stevens},
      title   = {MLSS Decision Procedure},
      journal = {Archive of Formal Proofs},
      month   = {May},
      year    = {2023},
      note    = {\url{https://isa-afp.org/entries/MLSS_Decision_Proc.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- May 18, 2023 : Isabelle2022