Int. J. of Computers, Communications & Control, ISSN 1841-9836, E-ISSN 1841-9844
Vol. V (2010), No. 5, pp. 642-653

Tense θ-valued Moisil propositional logic

C. Chiriţă

Carmen Chiriţă
University of Bucharest
Faculty of Mathematics and Computer Science
Romania, 010014 Bucharest, 4 Academiei
E-mail: stama@funinf.cs.unibuc.ro

Abstract: In this paper we study the tense θ-valued Moisil propositional
calculus, a logical system obtained from the θ-valued Moisil propositional logic
by adding two tense operators. The main result is a completeness theorem for
tense θ-valued Moisil propositional logic. The proof of this theorem is based
on the representation theorem of tense θ-valued Łukasiewicz-Moisil algebras,
developed in a previous paper.
Keywords: Łukasiewicz-Moisil algebras, tense Moisil logic.

1 Introduction

The first contribution to the algebraic logic of finite-valued Łukasiewicz propositional calculus
is Moisil’s paper [18], where n-valued Łukasiewicz algebras (named today Łukasiewicz-Moisil
algebras) were introduced. According to an example given by A. Rose (1957), for n ≥ 5 the
Łukasiewicz implication cannot be defined in an n-valued Łukasiewicz-Moisil algebra. Hence,
Moisil discovered a new many-valued logical system (named today Moisil logic), whose algebraic
models are n-valued Łukasiewicz-Moisil algebras.

In 1969, Moisil defined the θ-valued Łukasiewicz algebras, where θ is the order type of a
bounded chain. These structures extend a part of the definition of n-valued Łukasiewicz algebras,
but they differ from these by accepting many negation operations ( [3], [10], [16], [23]). The logic
corresponding to the θ-valued Łukasiewicz-Moisil algebras was developed by Boicescu [1] and
Filipoiu [10] (see also [2]). This logical system is called the θ-valued Moisil propositional logic.
The chrysippian endomorphisms of θ-valued Łukasiewicz-Moisil algebras are reflected in the
syntax of the θ-valued Moisil propositional logic by chrysippian operations.

This paper is devoted to the tense θ-valued Moisil propositional calculus, a logical system
obtained from the θ-valued Moisil propositional calculus by adding the tense operators G and
H. The algebraic basis of this logic consists of tense θ-valued Łukasiewicz-Moisil algebras (tense
LMθ-algebras), algebraic structures studied in our paper [7]. We extend some of the results of [8],
where a tense n-valued propositional logic was studied. The tense θ-valued Moisil propositional
calculus unifies two logical systems: the classical tense logic and the θ-valued Moisil logic. The
connection between these logics is realized by axioms that express the behaviour of the tense
operators with respect to the chrysippian operations.

The paper is organized as follows.
In Section 2 we recall some definitions and basic facts on θ-valued Łukasiewicz-Moisil algebras

and θ-valued Moisil logic, with emphasis on the connectives →k and ↔k and their algebraic coun-
terparts. Section 3 deals with tense θ-valued Łukasiewicz-Moisil algebras (tense LMθ-algebras),
algebraic structures obtained from θ-valued Łukasiewicz-Moisil algebras by adding the two tense
operators G and H. Section 4 contains the syntactical construction of the tense θ-valued Moisil
propositional calculus. We establish some properties regarding the inferential structure of this
logical system.

Copyright c⃝ 2006-2010 by CCC Publications



Tense θ-valued Moisil propositional logic 643

The Lindenbaum-Tarski algebra associated with the tense θ-valued Moisil propositional cal-
culus is studied in Section 5. We obtain the structure of tense LMθ-algebra. The syntactical
properties of the tense θ-valued Moisil logic are reflected in this tense LMθ-algebra, thus we use
the algebraic framework in order to obtain results for the logical system.

In section 6 we define the interpretations of tense θ-valued Moisil propositional calculus and
the k-tautologies of this logic. Our main result is the completeness theorem proved in this section
(Theorem 26). Its proof uses the representation theorem of tense LMθ-algebras applied to the
Lindenbaum-Tarski algebra constructed in the previous section.

2 θ-valued Moisil logic and θ-valued Łukasiewicz-Moisil algebras

Let (I, ≤) be a totally ordered set, with first and last element, denoted by 0 and 1 respectively,
and of order type θ, through this paper.

We fix an element k ∈ I, through this paper.
In this section, we recall the θ-valued Moisil logic Mθ described in [2]. The axiomatiza-

tion of θ-valued Moisil propositional calculus uses the system of axioms of θ-valued calcu-
lus introduced by Boicescu [4] and Filipoiu [10]. The basic results are taken from Filipoiu
[10](see also [2]). The alphabet of Mθ has the following primitive symbols: an infinite set
V of propositional variables; the logical connectives ∨, ∧, φi, φi for all i ∈ I and the paran-
theses (,). The set Prop(V) of propositions of Mθ is defined by canonical induction. For
each i ∈ I, we shall use the following abbreviations: p →i q = φip ∨ φiq and p ↔i q =
= (p →i q) ∧ (q →i p). The θ-valued propositional calculus has the following k-axioms:
(2.1) p →k (q →k p),
(2.2) (p →k (q →k r)) →k ((p →k q) →k (p →k r)),
(2.3) p ∧ q →k p,
(2.4) p ∧ q →k q,
(2.5) (p →k q) →k ((p →k r) →k (p →k q ∧ r)),
(2.6) p →k p ∨ q,
(2.7) q →k p ∨ q,
(2.8) (p →k q) →k ((r →k q) →k (p ∨ r →k q)),
(2.9) φi(p ∧ q) ↔k φip ∧ φiq, for every i ∈ I,
(2.10) φi(p ∨ q) ↔k φip ∧ φiq, for every i ∈ I,
(2.11) φjp ↔k φiφjp, for every i, j ∈ I,
(2.12) φjp ↔k φiφjp, for every i, j ∈ I,
(2.13) φjp ↔k φiφjp, for every i, j ∈ I,
(2.14) φjp ↔k φiφjp, for every i, j ∈ I,
(2.15) φip →k φjp, for every i, j ∈ I, i ≤ j.



644 C. Chiriţă

The notion of formal proof in Mθ is defined in terms of the above k-axioms and the
k-modus ponens inference rule:

p, p →k q
q

.

For briefness, we will say "modus ponens" (m.p) instead of "k-modus ponens" from now on.
We shall denote by ⊢k p that p is a k-theorem.
We remind some k-theorems of Mθ, which will be used in our proofs.

Proposition 1. ( [2], p. 491, Example 3.12) The following propositions are k-theorems of Mθ:

(2.16) ⊢k p →k p,
(2.17) ⊢k p ↔k φkp,
(2.18) ⊢k (φip ∨ φip), for every i ∈ I, j ∈ I,

(2.19) ⊢k (φj(p ∨ q) ↔k φjp ∨ φjq), j ∈ I,
(2.20) ⊢k (φj(p ∧ q) ↔k φjp ∨ φjq), j ∈ I,
(2.21) ⊢k ((p →k q) →k (φkq →k φkp)),
(2.22)

p

φjp
, j ≥ k,

(2.23)
φkp →k φkq

p →k q .
Proposition 2. The following propositions are k-theorems of Mθ:

(2.24) ⊢k p →k (q →k (p ∧ q)),
(2.25) ⊢k (p ∧ q →k r) →k (p →k (q →k r)),
(2.26) ⊢k (p →k (q →k r)) →k ((p ∧ q) →k r),
(2.27) ⊢k (p →k q) →k ((q →k r) →k (p →k r)),
(2.28) ⊢k (p →k q) → ((r →k t) →k (p ∧ r →k q ∧ t)).
Proof: We shall establish only the k-theorems (2.24), (2.25) and (2.28).

(2.24) We shall use (2.5), (2.16), (2.1), modus ponens and the Deduction Theorem (see [2],
p. 495, Proposition 3.17).

{p, q} ⊢k (p →k p) →k ((p →k q) →k (p →k p ∧ q)) (2.5)
{p, q} ⊢k p →k p (2.16)
{p, q} ⊢k (p →k q) →k (p →k p ∧ q)) (m.p)
{p, q} ⊢k q →k (p →k q) (2.1)
{p, q} ⊢k q
{p, q} ⊢k p →k q (m.p)
{p, q} ⊢k p →k (p ∧ q) (m.p)
{p, q} ⊢k p
{p, q} ⊢k p ∧ q (m.p)
{p} ⊢k q →k (p ∧ q) (Deduction Theorem)
⊢k p →k (q →k (p ∧ q)) (Deduction Theorem)



Tense θ-valued Moisil propositional logic 645

(2.25) We shall apply (2.24), modus ponens and the Deduction Theorem.

{p ∧ q →k r, p, q} ⊢k p →k (q →k (p ∧ q)) (2.24)
{p ∧ q →k r, p, q} ⊢k p
{p ∧ q →k r, p, q} ⊢k q →k (p ∧ q) (m.p)
{p ∧ q →k r, p, q} ⊢k q
{p ∧ q →k r, p, q} ⊢k p ∧ q (m.p)
{p ∧ q →k r, p, q} ⊢k p ∧ q →k r
{p ∧ q →k r, p, q} ⊢k r (m.p)
{p ∧ q →k r, p} ⊢k q →k r (Deduction Theorem)
{p ∧ q →k r} ⊢k p →k (q →k r) (Deduction Theorem)
⊢k (p ∧ q →k r) →k (p →k (q →k r)) (Deduction Theorem)

(2.28) We shall use k-axioms (2.3), (2.4), modus ponens, k-theorem (2.24) and the Deduction
Theorem.

{p →k q, r →k t, p ∧ r} ⊢k p ∧ r
{p →k q, r →k t, p ∧ r} ⊢k p ∧ r →k p (2.3)
{p →k q, r →k t, p ∧ r} ⊢k p (m.p)
{p →k q, r →k t, p ∧ r} ⊢k p →k q
{p →k q, r →k t, p ∧ r} ⊢k q (m.p)
{p →k q, r →k t, p ∧ r} ⊢k p ∧ r →k r (2.4)
{p →k q, r →k t, p ∧ r} ⊢k r (m.p)
{p →k q, r →k t, p ∧ r} ⊢k r →k t
{p →k q, r →k t, p ∧ r} ⊢k t (m.p)
{p →k q, r →k t, p ∧ r} ⊢k q →k (t →k (q ∧ t)) (2.24)
{p →k q, r →k t, p ∧ r} ⊢k t →k (q ∧ t) (m.p)
{p →k q, r →k t, p ∧ r} ⊢k q ∧ t (m.p)
Applying the Deduction Theorem three times we obtain that
⊢k (p →k q) → ((r →k t) →k (p ∧ r →k q ∧ t)).

The rest of the proof is straightforward. 2

The θ-valued Łukasiewicz-Moisil algebras constitute the algebraic counterpart of the θ-valued
Moisil logic. The Lindenbaum-Tarski algebra of the θ-valued Moisil propositional calculus is an
θ-valued Łukasiewicz-Moisil algebra (see [2], p. 500, Theorem 3.30).

We shall recall the definition of θ-valued Łukasiewicz-Moisil algebras.

Definition 3. A θ-valued Łukasiewicz-Moisil algebra (LMθ-algebra) is an algebra
L = (L, ∧, ∨, {φi}i∈I, {φi}i∈I, 0L, 1L) of type (2, 2, {1}i∈I, {1}i∈I, 0, 0) such that for all x, y ∈ L,

(2.29) (L, ∧, ∨, 0L, 1L) is a bounded distributive lattice,

(2.30) φi is a bounded distributive lattice endomorphism for all i ∈ I,

(2.31) φix ∧ φix = 0L; φix ∨ φix = 1L for all i ∈ I,

(2.32) φi ◦ φj = φj for all i, j ∈ I,

(2.33) If i ≤ j then φi ≤ φj for all i, j ∈ I,

(2.34) If φix = φiy for all i ∈ I, then x = y (this is known as Moisil’s determination principle).



646 C. Chiriţă

Let L = (L, ∧, ∨, {φi}i∈I, {φi}i∈I, 0L, 1L) be an LMθ-algebra.
We say that L is complete if the lattice (L, ∧, ∨, 0L, 1L) is complete. L is completely chrysippian if
for every {xk}k∈K (xk ∈ L for all k ∈ K) such that

∧
k∈K

xk and
∨
k∈K

xk exist, the following properties

hold: φi(
∧
k∈K

xk) =
∧
k∈K

φixk, φi(
∨
k∈K

xk) =
∨
k∈K

φixk (∀i ∈ I).

Example 4. Let B = (B, ∧, ∨,− , 0B, 1B) be a Boolean algebra.
The set D(B) = B[I] = {f|f : I → B, i ≤ j ⇒ f(i) ≤ f(j)} of all increasing functions from I
to B can be made into a LMθ-algebra D(B) = (D(B), ∧, ∨, {φi}i∈I, {φi}i∈I, 0D(B), 1D(B)) where
0D(B), 1D(B) : I → B are defined by 0D(B)(i) = 0B and 1D(B)(i) = 1B for every i ∈ I, the ope-
rations of the lattice (D(B), ∧, ∨, 0D(B), 1D(B)) are defined pointwise (cf. [2], p.6, Example 1.10)
and (φif)(j) = f(i), (φif)(j) = (f(i))− (∀j ∈ I) (∀i ∈ I).

Let L = (L, ∧, ∨, {φi}i∈I, {φi}i∈I, 0L, 1L) be an LMθ-algebra. For each j ∈ I we consider the
binary operation →j on L defined by (2.35) a →j b = φ̄ja∨φjb = (φja∧φ̄jb)− for all a, b ∈ L.
This implication is associated to ∧ (like for Boolean algebras), but like for Boolean algebras also,
there exists the following implication: a ;j b = φ̄ja ∧ φjb, associated to ∨.
The notion of morphism of LMθ-algebras is defined as usual ( [2]). Of course, a morphism of
LMθ-algebras preserves the operation →j.
3 Tense θ-valued Łukasiewicz-Moisil algebras

In this section we shall recall some definitions and basic results on tense θ-valued Łukasiewicz-
Moisil algebras from [7].

Definition 5. A tense LMθ-algebra is a triple At = (A, G, H), where A = (A, ∧, ∨, {φi}i∈I, {φi}i∈I,
0A, 1A) is an LMθ-algebra and G, H : A → A are two unary operations on A such that for all
x, y ∈ A,

(3.1) G(1A) = 1A, H(1A) = 1A,

(3.2) G(x ∧ y) = G(x) ∧ G(y), H(x ∧ y) = H(x) ∧ H(y),

(3.3) G ◦ φi = φi ◦ G, H ◦ φi = φi ◦ H, for any i ∈ I,

(3.4) G(x) ∨ y = 1A iff x ∨ H(y) = 1A.

Definition 6. Let (A, G, H) be a tense LMθ-algebra. For any i ∈ I, let us consider the unary
operations Pi, Fi defined by Pix = φiHφix and Fix = φiGφix, for any x ∈ A.

Proposition 7. Let A = (A, ∧, ∨, {φi}i∈I, {φi}i∈I, 0A, 1A) be an LMθ-algebra and G, H be two
unary operations on A that satisfy conditions (3.1), (3.2) and (3.3). Then, the condition (3.4) is
equivalent with (3.4′) φi ≤ G ◦ Pi and φi ≤ H ◦ Fi for all i ∈ I.

Thus, if we replace in Definition 5 the axiom (3.4) with the condition (3.4′), we obtain an
equivalent definition of tense LMθ-algebra.

Proposition 8. Let A = (A, ∧, ∨, {φi}i∈I, {φi}i∈I, 0A, 1A) be an LMθ-algebra and G, H be two
unary operations on A that satisfy conditions (3.1) and (3.3). Then, the condition (3.2) is
equivalent to (3.2′) G(a →k b) ≤ G(a) →k G(b); H(a →k b) ≤ H(a) →k H(b) for all k ∈ I where→k is defined by (2.35).



Tense θ-valued Moisil propositional logic 647

Thus, if in Definition 5 we replace the axiom (3.2) by (3.2’), we obtain an equivalent definition
for tense LMθ-algebra.

Definition 9. A frame is a pair (X, R), where X is a nonempty set and R is a binary relation on
X.

Let (X, R) be a frame and L = (L, ∧, ∨, {φi}i∈I, {φ̄i}i∈I, 0L, 1L) be a complete and completely
chrysippian LMθ-algebra. LX has a canonical structure of LMθ-algebra. Let’s us define for all
p ∈ LX and x ∈ X: G∗(p)(x) =

∧
{p(y)|y ∈ X, xRy}, H∗(p)(x) =

∧
{p(y)|y ∈ X, yRx}.

Proposition 10. For any frame (X, R), (LX, G∗, H∗) is a tense LMθ-algebra.

Let (B, G, H) be a tense Boolean algebra. We define on D(B) the unary operations D(G)
and D(H) by: D(G)(f) = G ◦ f, D(H)(f) = H ◦ f for all f ∈ D(B).

Lemma 11. If (B, G, H) is a tense Boolean algebra then (D(B), D(G), D(H)) is a tense LMθ-
algebra.

Theorem 12. (The representation theorem for tense LMθ-algebras) For every tense
LMθ-algebra (A, G, H) there exist a frame (X, R) and an injective morphism of tense LMθ-algebras
α : A → (D(L2))X, where L2 = {0, 1}, the standard Boolean algebra.
4 Tense θ-valued Moisil logic (the syntax)

In this section we introduce the tense θ-valued Moisil propositional calculus TMθ, a logical
system obtained from the θ-valued propositional calculus (see [2]) by adding the two tense
operators G and H. We define the notion of k-theorem and k-deduction then we establish some
syntactical properties of TMθ.
The alphabet of TMθ has the following primitive symbols: an infinite set V of propositional
variables; the logical connectives ∨, ∧, φi, φi for all i ∈ I; the tense operators G and H and
parantheses (, ). The set E of propositions of TMθ is defined by canonical induction.

Definition 13. We shall use the following abbreviations: for all α, β ∈ E and i ∈ I, we define
α →i β = φiα ∨ φiβ; α ↔i β = (α →i β) ∧ (β →i α); Fiα = φiGφiα; Piα = φiHφiα.
Definition 14. We call a k-axiom of tense θ-valued Moisil propositional calculus a proposition
of one of the following forms:

(4.1) The k-axioms of θ-valued Moisil propositional calculus ((2.1)-(2.15) in Section 2);

(4.2) G(α →k β) →k (Gα →k Gβ); H(α →k β) →k (Hα →k Hβ);
(4.3) Gφiα ↔k φiGα; Hφiα ↔k φiHα, for all i ∈ I;
(4.4) φiα →k GPiα; φiα →k HFiα, for all i ∈ I.

The notion of formal k-proof in TMθ is defined in terms of the above axioms and the following

inference rules:
α, α →k β

β
(modus ponens);

α

Gα

α

Hα
(Temporal Generalizations)

Definition 15. We say that a proposition α is a k-theorem of TMθ if there exists a k-proof of
it. We will denote by ⊢k α the fact that α is a k-theorem of TMθ.

Definition 16. Let Γ ⊆ E and α ∈ E. We say that α is a k-deduction from Γ and write Γ ⊢k α

if there exist n ∈ N = {0, 1, 2, ...} and α1, ..., αn ∈ Γ such that ⊢k
n∧
i=1

αi →k α.



648 C. Chiriţă

We remark that the logical structure of TMθ (k-theorems and k-deduction) combines the
logical stuctures of two logical systems: the θ-valued Moisil logic and tense classical logic.
Further we shall prove some syntactical properties.

Lemma 17. Let Γ ⊆ E and α ∈ E. Then Γ ⊢k α iff there exist n ∈ N and α1, ..., αn ∈ Γ such
that ⊢k α1 →k (α2 →k ...(αn →k α)...).
Proof: By Definition 16 and k-theorems (2.25) and (2.26). 2

Lemma 18. Let Γ ⊆ E and α ∈ E. Then Γ ⊢k α iff there exists Γ ′ ⊆ Γ, Γ ′ finite, such that
Γ ′ ⊢k α.

Proof: By Definition 16 and Lemma 17. 2

Proposition 19. Let Γ, Σ ⊆ E and α, β ∈ E. The following properties hold:
(i) If ⊢k α then Γ ⊢k α;
(ii) If Γ ⊆ Σ and Γ ⊢k α then Σ ⊢k α;
(iii) If α ∈ Γ then Γ ⊢k α;
(iv) {α} ⊢k β iff ⊢k α →k β;
(v) If Γ ⊢k α and {α} ⊢k β then Γ ⊢k β;
(vi) If Γ ⊢k α and Γ ⊢k α →k β then Γ ⊢k β;
(vii) Γ ⊢k α ∧ β iff Γ ⊢k α and Γ ⊢k β.

Proof: (i) Using Definition 16 for n = 0. (ii) By applying Definition 16.
(iii) Using k-theorem (2.16) and Definition 16.
(iv) We assume that ⊢k α →k β. Then, by Definition 16, we obtain that {α} ⊢k β. Conversely, if
{α} ⊢k β then there exists n ∈ N such that ⊢k (α ∧ ... ∧ α︸ ︷︷ ︸

n

) →k β. By using k-axioms (2.4) and
(2.5), we get that ⊢k (α ∧ ... ∧ α︸ ︷︷ ︸

n

) ↔k α, so ⊢k α →k β.
(v) We suppose that Γ ⊢k α and {α} ⊢k β. Then there exist n ∈ N and α1, .., αn ∈ Γ such that

⊢k
n∧
i=1

αi →k α. Using (iv), it follows that ⊢k α →k β and by applying k-theorem (2.27) and
modus ponens, we obtain that ⊢k

n∧
i=1

αi →k β, so Γ ⊢k β.
(vi) Let Γ ⊢k α and Γ ⊢k α →k β. By applying Lemma 18, there exist Γ1, Γ2 ⊆ Γ such that
Γ1 ⊢k α and Γ2 ⊢k α →k β. By (ii), it follows that Γ1 ∪ Γ2 ⊢k α and Γ1 ∪ Γ2 ⊢k α →k β.
If we consider Γ1 ∪ Γ2 = {γ1, ..., γn}, we obtain that ⊢k

n∧
i=1

γi →k α and ⊢k n∧
i=1

γi →k (α →k
→k β). By applying k-axiom (2.2) and modus ponens, we get that ⊢k n∧

i=1

γi →k β, so Γ ⊢k β.
(vii) We assume that Γ ⊢k α ∧ β. By using k-axioms (2.3) and (2.4) and applying (i) and (vi),
we obtain that Γ ⊢k α and Γ ⊢k β. Conversely, we assume that Γ ⊢k α and Γ ⊢k β. By using
k-theorem (2.24) and (i), we obtain that Γ ⊢k α →k (β →k α ∧ β). By applying twice (vi), we
get Γ ⊢k α ∧ β. 2

Theorem 20. (The deduction theorem) Let Γ ⊆ E and α, β ∈ E. Then Γ ∪ {α} ⊢k β iff Γ ⊢k
α →k β.
Proof: We assume that Γ ∪ {α} ⊢k β. Then there exist n ∈ N and α1, ..., αn ∈ Γ such

that ⊢k (
n∧
i=1

αi ∧ α) →k β. By applying k-theorem (2.25) and modus ponens, it follows that



Tense θ-valued Moisil propositional logic 649

⊢k
n∧
i=1

αi →k (α →k β). Using Definition 16, we obtain that Γ ⊢k α →k β. Conversely, we
suppose that Γ ⊢k α →k β. Thus, by Proposition 4.1 (ii), we get Γ ∪ {α} ⊢k α →k β. Also, by
Proposition 4.1 (iii), we have that Γ ∪ {α} ⊢k α, hence by applying Proposition 4.1 (vi), it results
that Γ ∪ {α} ⊢k β. 2

Proposition 21. In TMθ, the following properties hold:

(4.5) If ⊢k α ↔k β, then ⊢k Gα ↔k Gβ,
(4.6) ⊢k G(α ∧ β) ↔k (Gα ∧ Gβ).
Proof: (4.5) By using k-axioms (2.3), (2.4), k-theorem (2.24) and modus ponens, we obtain that:
⊢k α ↔k β iff ⊢k α →k β and ⊢k β →k α. Applying the temporal generalization rule G, we get
that ⊢k G(α →k β) and ⊢k G(β →k α). Then, by k-axiom (4.2) and modus ponens, it follows
that ⊢k Gα →k Gβ and ⊢k Gβ →k Gα, hence ⊢k Gα ↔k Gβ.

(4.6) We shall prove that ⊢k G(α ∧ β) →k (Gα ∧ Gβ) and ⊢k (Gα ∧ Gβ) →k G(α ∧ β). By
applying Proposition 21 (4.5) for k-axioms (2.3), (2.4), we obtain that ⊢k G(α ∧ β) →k Gα and
⊢k G(α ∧ β) →k Gβ. Using k-axiom (2.5) and modus ponens, it results that
⊢k G(α ∧ β) →k (Gα ∧ Gβ). By k-teorem (2.24) and the temporal generalization rule G,
we obtain that ⊢k G(α →k (β →k α∧β)). Applying k-axiom (4.2), modus ponens and k-theorem
(2.27), it follows that ⊢k Gα →k (Gβ →k G(α∧β)). Using k-theorem (2.26) and modus ponens,
we get that ⊢k (Gα ∧ Gβ) →k G(α ∧ β). Thus ⊢k G(α ∧ β) ↔k (Gα ∧ Gβ). 2

We remark that there exists a similar Proposition concerning H.

5 The k-Lindenbaum-Tarski algebra of tense θ-valued Moisil logic

In this section we shall prove that the k-Lindenbaum-Tarski algebra of TMθ is a tense θ-
valued Łukasiewicz-Moisil algebra. Therefore, the tense θ-valued Łukasiewicz-Moisil algebras
constitute the algebraic structures of TMθ and the properties of tense LMθ-algebras reflect the
syntactical properties of TMθ.
We consider the binary relation ∼k on the set of all propositions E, defined by: α ∼k β iff
⊢k φiα ↔k φiβ for all i ∈ I.
Lemma 22. ∼k is an equivalence relation on E.

For any proposition α ∈ E, we denote by [α]k the equivalence class of α. We can define the
following operations on the set E/∼k : [α]k∨[β]k = [α∨β]k; [α]k∧[β]k = [α∧β]k; φi[α]k = [φiα]k;
φi[α]k = [φiα]k for all i ∈ I; G([α]k) = [Gα]k; H([α]k) = [Hα]k; 0k = [φkα]k, 1k = [φkα]k, where
α is a k-theorem of TMθ.

Proposition 23. (E/∼k, ∧, ∨, {φi}i∈I, {φi}i∈I, 0k, 1k, G, H), the k-Lindenbaum-Tarski algebra of
TMθ, is a tense LMθ-algebra.

Proof: By ( [2], p.500, Theorem 3.30), we have that (E/∼k, ∧, ∨, {φi}i∈I, {φi}i∈I, 0k, 1k) is an
LMθ-algebra. What is left to prove is that the operations G and H are well defined and the
conditions (3.1)-(3.4) are satisfied. Due to the symmetrical position of G and H we shall only
include the proofs for G. Let α, β ∈ E such that α ∼k β. Thus, ⊢k φiα ↔k φiβ for all i ∈ I.
Applying Proposition 21 (4.5), we obtain that ⊢k Gφiα ↔k Gφiβ for all i ∈ I. Using k-axiom
(4.3), it follows that ⊢k φiGα ↔k φiGβ for all i ∈ I, so Gα ∼k Gβ.



650 C. Chiriţă

(3.1) We have to prove that G([φkα]k) = [φkα]k i.e. by definition of ∼k that ⊢k φiGφkα ↔k
φiφkα for every α such that ⊢k α and for all i ∈ I. Let α ∈ E such that ⊢k α and i ∈ I.
By k-theorem (2.22), we obtain that ⊢k φkα and by applying the temporal generalization
rule G, we obtain that ⊢k Gφkα. Using k-axiom (2.1) and modus ponens, it results that
⊢k φkα →k Gφkα and ⊢k Gφkα →k φkα. Thus, we get that (i) ⊢k φkα ↔k Gφkα. Using
k-axiom (2.11), we have that (ii) ⊢k φiφkα ↔k φkα and by using Proposition 21(4.5), we
obtain that (iii) ⊢k Gφiφkα ↔k Gφkα. Using k-axiom (4.3) and the conditions (i),(ii),
(iii), it results that ⊢k φiGφkα ↔k φiφkα.

(3.2) Let α, β ∈ E. We must prove that G([α]k ∧ [β]k) = G([α]k) ∧ G([β]k) i.e. G(α ∧ β) ∼k
Gα ∧ Gβ which is equivalent with ⊢k φiG(α ∧ β) ↔k φi(Gα ∧ Gβ) for all i ∈ I. Let i ∈ I.
By using Proposition 21(4.6) for α = φiα and β = φiβ, we obtain that (i) ⊢k G(φiα ∧
∧φiβ) ↔k (Gφiα ∧ Gφiβ). By using k-axiom (2.9) and Proposition 21(4.5), we get
that (ii) ⊢k Gφi(α ∧ β) ↔k G(φiα ∧ φiβ). By conditions (i) and (ii), we obtain that
(a) ⊢k Gφi(α∧β) ↔k (Gφiα∧Gφiβ). By k-axiom (4.3), we have: ⊢k Gφiα ↔k φiGα and
⊢k Gφiβ ↔k φiGβ. Applying k-theorem (2.28), it follows that (b) ⊢k (Gφiα ∧ Gφiβ) ↔k↔k (φiGα∧φiGβ). By conditions (a), (b) and k-axiom (4.3), we obtain that ⊢k φiG(α∧
∧β) ↔k φi(Gα ∧ Gβ).

(3.3) We have to prove that ⊢k φjGφiα ↔k φjφiGα for all i, j ∈ I. Let i, j ∈ I. By k-
axiom (2.11), we obtain that (a) ⊢k φjφiGα ↔k φiGα. Using k-axiom (4.3), we have
that (b) ⊢k φjGφiα ↔k Gφjφiα. By k-axioms (2.11) and Proposition 21(4.5), it fol-
lows that (c) ⊢k Gφjφiα ↔k Gφiα. By (a), (b), (c) and k-axiom (4.3), we get that
⊢k φjGφiα ↔k φjφiGα.

(3.4) Since by Proposition 7, the condition (3.4) is equivalent with (3.4’), we shall prove that
[φiα]k ≤ [GPiα]k for all i ∈ I, i.e. ⊢k φjφiα →k φjGPiα for all i, j ∈ I. Let i, j ∈ I. By
k-axiom (2.13), we have that ⊢k Piα ↔k φjPiα. Applying Proposition 21 (4.5), it follows
that ⊢k GPiα ↔k GφjPiα. Using k-axiom (4.3), it results that (1) ⊢k GPiα ↔k φjGPiα.
Also, by k-axiom (2.11), we have that (2) ⊢k φiα ↔k φjφiα. By (1), (2) and k-axiom
(4.4), we get that ⊢k φjφiα →k φjGPiα.

2

6 Semantics and completeness theorem of tense θ-valued Moisil
logic

This section concernes with the semantics of TMθ, which combines the properties of Kripke
semantics for T and the algebraic semantics for Mθ. We establish a completeness theorem for
TMθ by using the representation theorem of tense θ-valued Łukasiewicz-Moisil algebras [7].

Definition 24. Let (X, R) be a frame. A valuation of TMθ is a function v : E × X → L[I]2 such
that for all α, β ∈ E and x ∈ X, the following equalities hold: v(α →k β, x) = v(α, x) →k v(β, x);
v(α ∧ β, x) = v(α, x) ∧ v(β, x); v(α ∨ β, x) = v(α, x) ∨ v(β, x); v(φiα, x) = φiv(α, x) for any
i ∈ I; v(φiα, x) = φiv(α, x) for any i ∈ I; v(Gp, x) =

∧
{v(p, y)|xRy}; v(Hp, x) =

∧
{v(p, y)|yRx}.

The first five conditions of the previous definition reflect "the many-valued past" of TMθ
(see [2], p.487) and the last two conditions correspond to "the tense past" of TMθ (see [5],
p.93).

Definition 25. We say that a proposition α is a k-tautology and we write |=k α if for every
frame (X, R), for any valuation v : E × X → L[I]

2
and for all x ∈ X, we have v(α, x)(k) = 1.



Tense θ-valued Moisil propositional logic 651

The following result establishes the equivalence between the k-theorems and the k-tautologies
of TMθ. The proof of the main implication is based on the representation theorem for tense θ-
valued Łukasiewicz-Moisil algebras (Theorem 12).

Theorem 26. (Completeness theorem). For any proposition α of TMθ, we have: ⊢k α iff |=k α.

Proof: (⇒). We shall prove by induction on the definition of ⊢k α that for every frame (X, R)
and for any valuation v : E × X → L[I]

2
, we have v(α, x)(k) = 1, for all x ∈ X.

Let (X, R) be a frame, v : E × X → L[I]
2

be a valuation and x ∈ X.
• We suppose that α is a k-axiom.

(a) Let α be G(p →k q) →k (Gp →k Gq) with p, q ∈ E. It is known that a →k (b →k c) =
= (a ∧ b) →k c ( [7], p.6, Proposition 2.1 (l)). We have: v(α, x)(k) =
= v(G(p →k q) →k (Gp →k Gq), x)(k) = [v(G(p →k q), x) →k (v(Gp, x) →k v(Gq, x))](k) =
= [(v(G(p →k q), x) ∧ v(Gp, x)) →k v(Gq, x)](k) = [∧

xRy

((v(p, y) →k v(q, y)) ∧ v(p, y)) →k
→k ∧

xRy

v(q, y)](k) = [φk
∧
xRy

((v(p, y) →k v(q, y)) ∧ v(p, y)) ∨ φk ∧
xRy

v(q, y)](k) =

= [(
∧
xRy

(v(p, y) →k v(q, y))∧v(p, y))(k)]−∨(∧
xRy

v(q, y))(k) = [
∧
xRy

((v(p, y)(k))−∨v(q, y)(k))∧

∧v(p, y)(k)]− ∨ (
∧
xRy

v(q, y)(k)) = [
∧
xRy

(v(q, y)(k) ∧ v(p, y)(k))]− ∨ (
∧
xRy

v(q, y)(k)).

Since v(q, y)(k), v(p, y)(k) ∈ L2 and v(q, y)(k) ∧ v(p, y)(k) ≤ v(q, y)(k), we obtain that∧
xRy

(v(q, y)(k) ∧ v(p, y)(k)) ≤
∧
xRy

v(q, y)(k). Since in a Boolean algebra we have a ≤ b iff

ā ∨ b = 1, we get that [
∧
xRy

(v(q, y)(k) ∧ v(p, y)(k))]− ∨ (
∧
xRy

v(q, y)(k)) = 1.

(b) Let α be Gφip ↔k φiGp with p ∈ E and i ∈ I. Then v(α, x)(k) =
= v(Gφip ↔k φiGp, x)(k) = v((Gφip →k φiGp) ∧ (φiGp →k Gφip), x)(k) =
= [(v(Gφip, x) →k v(φiGp, x)) ∧ (v(φiGp, x) →k v(Gφip, x))](k). Since L[I]2 is complete
and completely chrysippian, it follows that v(Gφip, x) =

∧
xRy

φiv(p, y) = φi(
∧
xRy

v(p, y)) =

= v(φiGp, x). We know that a →k a = 1 ( [7], p.6, Proposition 2.1 (f)), hence v(α, x)(k) =
1.

(c) Let α be φip →k GPip with i ∈ I. We have: v(α, x)(k) = v(φip →k GPip, x)(k) =
= (v(φip, x) →k v(GPip, x))(k) = (φiv(p, x) →k ∧

xRy

v(Pip, y))(k) =

= (φiv(p, x) →k ∧
xRy

∨
zRy

φiv(p, z))(k) = φk(φiv(p, x))(k) ∨ φk(
∧
xRy

∨
zRy

φiv(p, z))(k) =

= [v(p, x)(i)]− ∨
∧
xRy

∨
zRy

v(p, z)(i). Let y ∈ X such that xRy. Then v(p, x)(i) ≤
∨
zRy

v(p, z)(i),

hence v(p, x)(i) ≤
∧
xRy

∨
zRy

v(p, z)(i). We obtain that [v(p, x)(i)]− ∨
∧
xRy

∨
zRy

v(p, z)(i) = 1.

• We assume that α was obtained by applying the modus ponens rule. We have that
v(β, x)(k) = 1 and v(β →k α, x)(k) = 1. But v(β →k α, x)(k) = (v(β, x) →k v(α, x))(k) =
= (φkv(β, x) ∨ φkv(α, x))(k) = φk(v(β, x))(k) ∨ φk(v(α, x))(k) = [v(β, x)(k)]

− ∨ v(α, x)(k).
We deduce that v(α, x)(k) = 1.



652 C. Chiriţă

• We suppose that α = Gβ such that ⊢k β. We have that v(β, x)(k) = 1, for every x ∈ X. Then
v(Gβ, x)(k) = (

∧
xRy

v(β, y))(k) =
∧
xRy

v(β, y)(k) = 1.

(⇐). We shall prove that if ̸⊢k α then ̸|=k α. Assume that ̸⊢k α, so [α]k ̸= 1k. By u-
sing Proposition 23, we have that the k-Lindenbaum-Tarski algebra (E/∼k, G, H) of TMθ is a
tense LMθ-algebra. Applying the representation theorem for tense LMθ-algebras (Theorem 12),
there exist a frame (X, R) and an injective morphism of tense LMθ-algebras d : (E/∼k, G, H) →→ (D(L2)X, G∗, H∗). Let us consider the function v : E × X → L[I]2 defined by
v(α, x) = d([α]k)(x), for all α ∈ E and x ∈ X. It is straightforward to prove that v is a val-
uation. Since d is injective and [α]k ̸= 1k, we obtain that d([α]k) ̸= 1D(L2)X, hence there exists
a ∈ X such that v(α, a) = d([α]k)(a) ̸= 1D(L2). Thus α is not a k-tautology. 2

7 Concluding Remarks

The tense θ-valued Moisil propositional calculus TMθ can be viewed as a common generali-
zation of the θ-valued Moisil propositional logic Mθ and the classical tense logic T.
TMθ combines the logical structures of these logical systems and its semantic is inspired from
the semantics of T and Mθ. The main result of this paper is a completeness theorem for TMθ.
Its proof is derived from the representation theorem of tense θ-valued Łukasiewicz-Moisil algebras
[7].

An open problem is to obtain a proof of the representation theorem for tense θ-valued
Łukasiewicz-Moisil algebras by using Theorem 26.

The next step in the study of tense aspects of Moisil logic is to define the tense θ-valued pre-
dicate logic (the syntax and the semantic) and the algebras corresponding of this logic (polyadic
tense θ-valued Łukasiewicz-Moisil algebras). We hope to prove a completeness theorem for tense
θ-valued Moisil predicate logic and a representation theorem for the corresponding algebras. The
tense logics corresponding to the LMθ-algebras with negations [16] will be the subject of another
paper.

Bibliography

[1] V. Boicescu, Sur les systèmes déductifs dans la logique θ-valente, Publ. Dép. Math. Lyon, 8,
123-133, 1971.

[2] V. Boicescu, A. Filipoiu, G. Georgescu and S. Rudeanu, Łukasiewicz-Moisil algebras, North-
Holland, 1991.

[3] V. Boicescu, Contributions to the study of Łukasiewicz-Moisil algebras (Romanian), Ph.D.
Thesis, University of Bucharest, 1984.

[4] V. Boicescu, Sur une logique polyvalente, Rev. Roumaine Sci. Soc., sér. Philos. et Logique,
17, 393-405, 1973b.

[5] J. P. Burgess. Basic tense logic. In: Dov Gabbay and F. Guenthner, Eds., Handbook of
philosophical logic, chapter II.2, Reidel, 89-134, 1984.

[6] R. Cignoli, I.M.L. D’Ottaviano and D. Mundici, Algebraic Foundations of Many-valued Rea-
soning, Kluwer, 2000.

[7] C. Chiriţă, Tense θ-valued Łukasiewicz -Moisil algebras, to appear in Journal of Multiple-
Valued Logic and Soft Computing.



Tense θ-valued Moisil propositional logic 653

[8] D. Diaconescu, G. Georgescu, Tense operators on MV-algebras and Łukasiewicz-Moisil alge-
bras, Fundamenta Informaticae XX: 1-30, 2007.

[9] I. Dziţac, L. Andrei, 65 Years from Birth of Prof. Gheorghe S. Nadiu (1941-1998), Interna-
tional Journal of Computers, Communications & Control Vol. I, No. 3, pp. 93-98, 2006.

[10] A. Filipoiu, θ-valued Łukasiewicz-Moisil algebras and logics (Romanian), Ph.D.Thesis, Uni-
versity of Bucharest, 1981.

[11] G. Georgescu, A. Iorgulescu, S. Rudeanu, Grigore C. Moisil (1906-1973) and his School in
Algebraic Logic, Int. Journal of Computers, Communications & Control, Vol. I, No. 1, pp.
81-99, 2006.

[12] G. Georgescu, A. Iorgulescu, S. Rudeanu, Some Romanian researches in algebra of logic, In:
Grigore C.Moisil and his followers, Editura Academiei Romane, 86-120, 2007.

[13] G. Georgescu, A. Iorgulescu, I. Leuştean, Monadic and closure MV-algebras, Multiple-
Valued Logic, 3, 235-257, 1998.

[14] R. Goldblatt, Logics of Time and Computation, CSLI Lecture Notes No. 7, 1992.

[15] P. Hájek, Metamathematics of fuzzy logic, Kluwer Acad.Publ., Dordrecht, 1998

[16] A. Iorgulescu, 1 + θ -valued Łukasiewicz-Moisil algebras with negation (Romanian). Ph.D.
Thesis, University of Bucharest, 1984.

[17] J. Łukasiewicz, On three-valued logic, Ruch Filozoficzny (Polish), 5, 60-171, 1920.

[18] Gr. C. Moisil, Recherches sur les logiques non-chrysippiennes, Ann. Sci. Univ. Jassy, 26,
431-466, 1940.

[19] Gr. C. Moisil, Notes sur les logiques non-chrysippiennes, Ann. Sci. Univ. Jassy, 27, 86-98,
1941.

[20] Gr. C. Moisil, Logique modale, Disquis. Math. Phys, 2, 1942.

[21] Gr. C. Moisil, Łukasiewiczian algebras, Computing Center, University of Bucharest
(preprint), 311-324, 1968.

[22] Gr. C. Moisil, Essais sur les logiques non-chrysippiennes, Ed. Academiei, Bucharest, 1972.

[23] Gh. S. Nadiu, Cercetări asupra logicilor necryssipiene/Research about Necryssipiene Logics,
1972 (PhD Thesis, supervisor Grigore C. Moisil).

[24] H. Rasiowa, An algebraic approach to non-classical logics, North-Holland Publ., Amsterdam,
Polish Scientific Publ., Warszawa, 1974.