Pseudoconsistent Logic and Tense Logic

その他

In our usual logic, we do not infer arbitrary proposition from a contradictory one. Also in executing programs, there is a state that a proposition A holds in some program and in another there is a state in which A does not hold. To explain these situations, recently, the logic called paraconsistent is proposed and investigated. ([1, 2, 3] etc.) Since the logic has two kinds of negation operators, there are cases such that both A and not A are theorems and hence it is difficult to obtain the concept of truth. To the contrary, De Glas has proposed in [4] a pseudoconsistent logic (PCL) in which AΛ～ A → ⊥ is not a theorem but so ～ (AΛ ～ A) is. He also gave the axiomatization of PCL and proved the completeness theorem by two kinds of models, PC-models and I-models. These models are based on PC-algebras and partially ordered sets, respectively.
But there is an important question which is not referred : Is the logic PCL decidable ?
In the present paper we prove the decidabily of PCL according to the following steps:
1. PCL is characterized by the the class of pre-ordered sets instead of that of
partially ordered sets, that is ├_PCL A ⇔ A : PO-valid;
2. TL is characterized by the class of some kinds of Kripke-type models, that
is, ├_TL A ⇔ A : TL-valid;
3. PCL can be embedded into a certain tense logic (TL), that is, for some
map ε, A : PO-valid ⇔ ε(A) : TL-valid;
4. TL is decidable and hence so PCL is.