Kripke Completeness of First-Order Constructive Logics with Strong Negation

Autor:	Ryo Kashima, Ichiro Hasuo
Rok vydání:	2003
Předmět:	Predicate logic Discrete mathematics Logic Classical logic Modal logic Kripke semantics Intuitionistic logic Intermediate logic Negation as failure Axiom Mathematics
Zdroj:	Logic Journal of IGPL. 11:615-646
ISSN:	1368-9894 1367-0751
DOI:	10.1093/jigpal/11.6.615
Popis:	This paper considers Kripke completeness of Nelson’s constructive predicate logic N3 and its several variants. N3 is an extension of intuitionistic predicate logic Int by an contructive negation operator ∼ called strong negation. The variants of N3 in consideration are by omitting the axiom A → (∼A → B), by adding the axiom of constant domain ∀x(A(x) ∨ B) → ∀xA(x) ∨ B, by adding (A → B) ∨ (B → A), and by adding ¬¬(A ∨ ∼A); the last one we would like to call the axiom of potential omniscience and can be interpreted that we can eventually verify or falsify a statement, with proper additional information. The proofs of completeness are by the widely-applicable treesequent method; however, for those logics with the axiom of potential omniscience we can hardly go through with a simple application of it. For them we present two different proofs: one is by an embedding of classical logic, and the other by the TSg method, which is an extension of the tree-sequent method.
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=doi_dedup___::073db3baa79cfc712ab5b9adab251f9a https://doi.org/10.1093/jigpal/11.6.615 Zobrazit plný text záznamu Plný text ve formátu PDF