Email Gateway (Apr 09 2026 at 09:56): Email Gateway (Apr 09 2026 at 09:56):From: Tobias Nipkow <nipkow@in.tum.de>
Abstract Consistency Properties
Asta Halkjær From :e-mail: and Anders Schlichtkrull
Smullyan used abstract consistency properties to great effect in unifying meta
theoretical results in first-order logic. By abstractly specifying when a set of
formulas is consistent, he proved a single model existence result for all sets
that met the specification, reusing this result in proving completeness,
compactness, etc. Fitting later defined abstract consistency properties for a
range of other logics. In this work we use locales to mechanize abstract
consistency properties without fixing a particular logic or syntax, generalizing
the work of Smullyan and Fitting. We use Fitting's technique for closing a
consistency property under limits to guarantee the existence of a maximal
element. This yields a maximal consistent set for any notion of consistency
expressible in the framework. The usual conjunctive, disjunctive, universal and
existential conditions of abstract consistency properties ---based on Smullyan's
uniform notation--- arise as special cases of our abstract development. Users of
the framework can define an abstract consistency property for their own syntax
and logic, prove that it is well behaved, and receive a corresponding maximal
consistent set from which to prove model existence. We provide three example
instantiations. First, compactness and completeness for a first-order logic
where we only instantiate universal quantifiers with already occurring terms.
Second, completeness over general models for a second-order logic. Third,
completeness of our own natural deduction system for Prior's Ideal Language, a
recently developed hybrid logic with propositional quantification.
https://www.isa-afp.org/entries/Abstract_Consistency_Property.html
Enjoy!
Last updated: Apr 12 2026 at 02:50 UTC