島根大学総合理工学研究科

ISSN:1342-7121

number of downloads : ?

Use this link to cite this item : https://ir.lib.shimane-u.ac.jp/3363

Memoirs of the Graduate School of Science and Engineering, Shimane University. Series B, Mathematics 33

2000-03 発行

Kondo, Michiro

File

Description

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.

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.

About This Article

Other Article

PP. 31 - 46