A constructive investigation of satisfiability

DOI10.1016/J.APAL.2011.06.019MaRDI QIDQ651313zbMATH OpenOpenAlexFDO

Authors Francesco Ciraulo

Publication date 12 December 2011

Published in Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.apal.2011.06.019

zbMATH Keywords

constructivityintuitionistic logicsatisfiabilitytopological semantics

Mathematics Subject Classification ID

Subsystems of classical logic (including intuitionistic logic) (03B20) Proof theory in general (including proof-theoretic semantics) (03F03) Other constructive mathematics (03F65)

Review text

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.

Recommendations

• A constructive semantics for non‐deducibility
• Satisfiability is false intuitionistically: a question from Dana Scott
• scientific article; zbMATH DE number 517080
• scientific article; zbMATH DE number 4004179
• Satisfiability calculus: the semantic counterpart of a proof calculus in general logics

Cites work

• A constructive semantics for non‐deducibility
• An application of constructive completeness
• Finiteness in a Minimalist Foundation
• Formal topologies on the set of first-order formulae
• Formal Zariski topology: Positivity and points
• scientific article; zbMATH DE number 3853067 (Why is no real title available?)
• scientific article; zbMATH DE number 4152376 (Why is no real title available?)
• scientific article; zbMATH DE number 2247253 (Why is no real title available?)
• Pretopologies and completeness proofs
• Proof theory

Cited in

(17)

• On the satisfiability of circumscription
• Satisfiability is false intuitionistically: a question from Dana Scott
• Satisfiability on mixed instances
• An experiment with satisfiability modulo SAT
• A minimalist foundation at work
• Satisfiability Judgement under Incomplete Information
• scientific article; zbMATH DE number 4160680 (Why is no real title available?)
• scientific article; zbMATH DE number 5287580 (Why is no real title available?)
• scientific article; zbMATH DE number 517080 (Why is no real title available?)
• Testing satisfiability
• scientific article; zbMATH DE number 2084702 (Why is no real title available?)
• Formal topologies on the set of first-order formulae
• Satisfiability: where Theory meets Practice (Invited Talk).
• scientific article; zbMATH DE number 956862 (Why is no real title available?)
• scientific article; zbMATH DE number 2213633 (Why is no real title available?)
• Constructive decision via redundancy-free proof-search
• The overlap algebra of regular opens

This page was built for publication: A constructive investigation of satisfiability

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q651313)