New SAT result for a fragment of set theory

Stream: maths

[Lars Ericson]

This is a new paper by an old friend. It is of potential interest maybe somewhere in the realm of Lean tactic implementation: Decidability of the satisfiability problem for Boolean set theory with the unordered Cartesian product operator.

In general this family of results on decidable sublanguages of set theory depends on algorithms with iterated exponential time complexity, so really only feasible on a conventional computer for a small number of variables. If there were a quantum computer Lean you might be able to get a few more variables out of these, though saying how much more is pretty technical and may be disappointing, for example see Quantum 3-SAT is QMA1-complete.

[Notification Bot]

This topic was moved here from #announce > New SAT result for a fragment of set theory by Scott Morrison.