A Proof-Theoretical Study on Logics with Constructible Falsity
Ichiro Hasuo, Ryo Kashima · 2003
Constructible falsity A, also called strong negation, is an alternative to Heyting's negation :A ($ (A ! ?)) in intuitionistic logics. In this paper we give the proofs for Kripke completeness of the basic logic N: and its five variations. Among them the most novel results are about the logics with what we call omniscience axiom, ::(AA). We present two different proofs based on tree-sequents: one is by an embedding of classical logic, and the other is by an extended version of tree-sequent.