×

zbMATH — the first resource for mathematics

Many-valued modal propositional calculi. (English) Zbl 0661.03011
This paper discusses three modal many-valued propositional calculi, viz. \({}_ nT\), \({}_ nS4\) and \({}_ nS5\) (n\(\in {\mathbb{N}})\). Semantical and syntactical characterizations of these logics are given.
An n-valued Kripke model is a triple \(<W,R,val>\), where W is a nonempty set, the elements of which are called possible worlds, R is a binary relation on W, called the accessibility relation, and val assigns to any world w and to any propositional variable p an element of \(\{0,1/(n- 1),...,k/(n-1),...,1\}.\) The value val(w,f) of a formula f in a world w of a given n-valued Kripke model is defined recursively as follows: \(val(w,\sim f)=1-val(w,f),\) \(val(w,f\to g)=\min \{1,1- val(w,f)+val(w,g)\},\) \(val(w,\square f)=\min \{val(w',f)| \quad wRw'\}.\)
A formula is valid in \({}_ nT\) if its value is 1 in any world of any n- valued Kripke model with R reflexive. \({}_ nT\) is syntactically characterized by
AO: the axioms and rules of classical propositional calculus
A1: \(\square (p\to q)\to (\square p\to \square q)\)
A2: \((\square p+\square q)\to \square (p+q)\), where \(p+q:=\sim p\to q\)
A3: \(\square (p+p)\to (\square p+\square p)\)
A4: \((\diamond p+\diamond p)\to \diamond (p+p)\)
A5: \(\square p\to p\)
and the inference rule of necessitation: if f is formally provable (in \({}_ nT)\), then so is \(\square f.\)
The completeness of \({}_ nT\) with respect to n-valued Kripke semantics is proved in a constructive way. First a decision procedure for \({}_ nT\) is described. Then the following two theorems are shown: 1. If f is a valid formula, then the procedure applied to f succeeds (the proof is by contraposition). 2. If the procedure applied to a formula f succeeds, then f is a theorem.
The definitions and results obtained for \({}_ nT\) can easily be extended to systems like \({}_ nS4\), \({}_ nS5\), \({}_ nQ\), \({}_ nB\), and so on.
Reviewer: H.C.M.de Swart

MSC:
03B45 Modal logic (including the logic of norms)
03B50 Many-valued logic
PDF BibTeX XML Cite
Full Text: DOI