A constructive investigation of satisfiability (Q651313)

A constructive analysis of the logical notion of satisfiability for first-order intuitionistic formulae is presented. Satisfiability is considered in the framework of the topological semantics. ``Constructivity'' means that the law of excluded middle, the power-set axiom, and the axiom of choice are not used. The main idea is that the semantical notions are treated strictly in the ``constructive'' formal topology theory. The author's considerations are based on constructive proofs of soundness and completeness for first-order intuitionistic logic proposed by G. Sambin and T. Coquand [\textit{G. Sambin}, ``Pretopologies and completeness proofs'', J. Symb. Log. 60, No. 3, 861--878 (1995; Zbl 0839.03022); \textit{T. Coquand} and \textit{J. Smith}, ``An application of constructive completeness'', Lect. Notes Comput. Sci. 1158, 76--84 (1996; Zbl 0852.00045); \textit{T. Coquand} et al., ``Formal topologies on the set of first-order formulae'', J. Symb. Log. 65, No. 3, 1183--1192 (2000; Zbl 0965.03072)]. Namely, satisfiability of a formula is defined in terms of a canonical topology on the set of all formulas. This notion is characterized also by a syntactic calculus operating with the sequents of the form \(\Gamma\underline{\vee}\Delta\) whose intended meaning is that the conjunction of all the formulas in \(\Gamma\) and \(\Delta\) has a model.