STUDIES IN LOGIC, GRAMMAR AND RHETORIC 1 (14)

Dariusz Surowik

SOME REMARKS ABOUT INTUITIONISTIC TENSE LOGIC

Abstract

In this article I would like to consider the system of intuitionistic tense logic. The axioms of the considered system were presented in the article (See [8]) however the semantics of this system was changed. Suggested semantics is simpler and by using it we can better express philosophical ideas described by the considered system. In further part of this article it is shown that if we impose some conditions upon R then we get temporal order with corresponding properties.

Introduction

In this article indeterministic tense logic system is considered. The problem of logical determinism was shown in many scientific papers. Deterministic arguments showed in these papers are following:

Let T (p) means “p is true”, F (p) means “p is false” and N(p) means “p is necessary”. Then if we accept the principle of the causality and the principle of the bivalency we have that:

1) T (p) → N(p) – the principle of the causality

2) F (p) → N(¬p) – the principle of the causality

3) T (p) ∨ F (p) – the principle of bivalency

4) N(p) ∨ N(¬p) by 1,2,3 and \frac{α→γ,β→δ,α∨β}{γ∨δ} Then if we accept the principle of the causality and the law of the

excluded middle we have that:

1) T (p) → N(p) – the principle of the causality

Dariusz Surowik

2) T (¬p) → N(¬p) – the principle of the causality 3) T (p) ∨ T (¬p) – the law of the excluded middle

4) N(p) ∨ N(¬p) by 1,2,3 and \frac{α→γ,β→δ,α∨β}{γ∨δ} The formula N(p)∨N(¬p) expresses determinism. /Lukasiewicz showed

(See [5]) that rejection of causal principle did not exclude determinism. Then if we try to create indeterministic logic system we have to reject the principle of bivalency or the excluded middle law. In purpose of solution the problem of determinism /Lukasiewicz was created tree-valued logic (rejected the principle of bivalency). The meaning of this logic system to solve the problem of the logical determinism is controversial (Kotarbi/nski, [4]). To solve the problem of determinism we have to introduce difference between past and future. Past is determined (if something was, that can not be changed), future is not determined. We have asymmetry of time and if we would like to express this asymmetry using logical utils we must introduce time to logic. However if we accept, that time has a linear structure (this structure is used by many scientists – philosophers, physicists) and is valid the excluded middle law, we still have determinism because in that structure some formulas (e.g. α → HF α) are deterministic. Prior (See [7]) give branching time idea, in which future has alternatives whereas past has not got them.

actual future

Figure 1:

From all possible future alternatives only one is realized which is called actual future. This conception of time as solution of the problem of determinisn has opponents. Yourgran maintains (See [9]), that if we choose actual future, then one branch is staying and we return to linear order. Another way to solving this problem can be creation of tense logical system and rejection of the excluded middle law (See [8]). Therefore we can acknowledge that tense logic and intuitionistic propositional logic are proper utils to describe future events from indeterministic point of view.

Some remarks about intuitionistic tense logic

The system T_{m}

The system T_{m} is the tense logic system based on intuitionistic propositional logic. The tense-logical propositional language 𝔏 consists of: propositional letters (p_{1}, p_{2}, p_{3}....), unary connectives (¬, F, G, P, H), binary connectives (∧, ∨, →), parentheses. Tense operators are defined in the usual way:

F – “at least once in the future” G – “it is always going to be that case” P – “at least once in the past” H – “it has always been that case” T_{m} contains an axiom system of intuitionistic propositional logic (A1-

A10), tense logical axioms (H1-GD’), rules Modus Ponens (MP) and the tense-logical rules (RH and RG) For all α, β, γ ∈ 𝔏 :

A1) α → (β → α) A2) (α → β) → {[α → (β → γ)] → (α → γ)} A3) [(α → γ) ∧ (β → γ)] → {(α ∨ β) → γ} A4) (α ∧ β) → α A5) (α ∧ β) → β A6) α → [β → (α ∧ β)] A7) α → (α ∨ β) A8) β → (α ∨ β) A9) (α ∧ ¬α) → β A10) (α → ¬α) → ¬α

Tense-logical axioms:

H1) H (α → β) → (Hα → Hβ) G1) G (α → β) → (Gα → Gβ) H1’) H (α → β) → (P α → P β) G1’) G (α → β) → (F α → F β) H1”) (Hα → P α) ∨ Hβ G1”) (Gα → F α) ∨ Gβ H2) α → HF α G2) α → GP α H2’) P Gα → α G2’) F Hα → α HD) P α → ¬H¬α GD) F α → ¬G¬α HD’) ¬P α → H¬α GD’) ¬F α → G¬α

Tense-logical rules:

RH: to infer Hα from α RG: to infer Gα from α

The axioms H1’,H2’,G1’,G2’ are theorems of minimal tense logic K_{t} (based on classical logic) (See [6]). In T_{m} system we can not construct proofs of these formulas because the considered system is based on intuitionistic logic (we not accept the principle of the excluded law, double negation law and other law of classical logic).

Semantics

Let T be any nonempty set. A time T is an ordered couple ⟨T, R⟩, where R is a binary relation (earlier-later) on T.

Let V be a function mapping points t ∈ T to subsets V (t) of the set of propositional letters.

Let F be nonempty class of such functions. 𝔐_{(T ,F)} denotes {⟨T, R, V ⟩ : V ∈ F}.

Let ≤ be a relation between elements of 𝔐_{(T ,F)} defined as follows: ⟨T, R, V_{1}⟩ ≤ ⟨T, R, V_{2}⟩ iff for each t ∈ T : V_{1}(t) ⊆ V_{2}(t). The relation ≤

is reflexive and transitive.

Let us consider three-element time structure showed on Figure 2.

t^{1}  t^{2}  t^{3} V_{1}(t_{1})  V_{1}(t_{2})  V_{1}(t_{3})  V_{2}(t_{3}) V_{2}(t_{1})  V_{2}(t_{2}) p s  q r  vu  p s qr w  zv p q

Figure 2:

Let m_{1} = ⟨T, R, V_{1}⟩ , m_{2} = ⟨T, R, V_{2}⟩. Analysing the situation showed on Figure 2. we conclude that in this case (accordingly to definition of relation ≤) it does not holds m_{1} ≤ m_{2}, because for point t_{1} we have that V_{1} (t_{1}) is not included in V_{2} (t_{1}).

For three-element time structure showed on Figure 3 it holds m_{1} ≤ m_{2}.

t^{1}  t^{2}  t^{3} V_{1}(t_{1})  V_{1}(t_{2})  V_{1}(t_{3})  V_{2}(t_{3}) V_{2}(t_{1})  V_{2}(t_{2}) p s q r  vu  p s qr w  zv p q

Figure 3:

Remark For m ∈ 𝔐_{(T ,F)} by m^{∗} we shall mean any m_{1} ∈ 𝔐_{(T ,F)} such that

m ≤ m_{1}.

𝔐_{(T ,F)} is called a model based on time T . For a model 𝔐_{(T ,F)}, a point t ∈ T and m ∈ 𝔐_{(T ,F)}, a tense-logical formula α, the so-called ‘truth definition’ explains what it means for α to be true in 𝔐_{(T ,F)} at [t, m]

Definition: 𝔐_{(T ,F)} ⊧ α[t, m] is defined through the clauses:

1) 𝔐_{(T ,F)} ⊧ p[t, m] iff p ∈ V (t).

2) 𝔐_{(T ,F)} ⊧ ¬α[t, m] iff for any m^{∗} ∈ 𝔐_{(T ,F)} holds 𝔐_{(T ,F)} ⊭ α[t, m^{∗}]

3) 𝔐_{(T ,F)} ⊧ (α ∨ β) [t, m] iff 𝔐_{(T ,F)} ⊧ α[t, m] or 𝔐_{(T ,F)} ⊧ β[t, m]

4) 𝔐_{(T ,F)} ⊧ (α ∧ β) [t, m] iff 𝔐_{(T ,F)} ⊧ α[t, m] and 𝔐_{(T ,F)} ⊧ β[t, m]

5) 𝔐_{(T ,F)} ⊧ (α → β) [t, m] iff for any m^{∗} ∈ 𝔐_{(T ,F)} holds 𝔐_{(T ,F)} ⊭ α[t, m^{∗}] or 𝔐_{(T ,F)} ⊧ β[t, m^{∗}]

6) 𝔐_{(T ,F)} ⊧ F α[t, m] iff ∃t_{1}, tRt_{1}, such that 𝔐_{(T ,F)} ⊧ α[t_{1}, m]

7) 𝔐_{(T ,F)} ⊧ Gα[t, m] iff ∀t_{1}, tRt_{1} holds 𝔐_{(T ,F)} ⊧ α[t_{1}, m]

8) 𝔐_{(T ,F)} ⊧ P α[t, m] iff ∃t_{1}, t_{1}Rt, such that 𝔐_{(T ,F)} ⊧ α[t_{1}, m]

9) 𝔐_{(T ,F)} ⊧ Hα[t, m] iff ∀t_{1}, t_{1}Rt holds 𝔐_{(T ,F)} ⊧ α[t_{1}, m]

𝔐_{(T ,F)} ⊧ α[t, m] (α is true in 𝔐_{(T ,F)}) iff for any t ∈ T and any m ∈ 𝔐_{(T ,F)} : 𝔐_{(T ,F)} ⊧ α[t, m].

T ⊧ α (α is true in time T ) iff it is true in 𝔐_{(T ,F)} for any F.

⊧ α (α is a tautology of the minimal intuitionistic tense logic) iff it is true in T , for any T .

It is easy to check that holds:

Lemma 1

If for some t and m holds 𝔐_{(T ,F)} ⊧ α [t, m] then for any m^{∗} holds 𝔐_{(T ,F)} ⊧ α [t, m^{∗}]

Lemma 2

If for some t and m holds 𝔐_{(T ,F)} ⊧ P α [t, m] then for any m^{∗} holds 𝔐_{(T ,F)} ⊧ P α [t, m^{∗}]

proof

Let us assume that for some t and m (where m = ⟨T, R, V ⟩) holds 𝔐_{(T ,F)} ⊧ P α [t, m]. Then there is t_{1} such that t_{1}Rt and holds 𝔐_{(T ,F)} ⊧ α [t_{1}, m] . Hence α ∈ V (t_{1}). Take any m^{∗} (where m = ⟨T, R, V^{∗}⟩). Because (from definition ≤ and Remark) for any m^{∗} holds V (t_{1}) ⊆ V^{∗} (t_{1}) then we have, that α ∈ V^{∗}(t_{1}). Then 𝔐_{(T ,F)} ⊧ α [t_{1}, m^{∗}]. Because t_{1}Rt then 𝔐_{(T ,F)} ⊧ P α [t, m^{∗}] .□

Lemma 3

If for some t and m 𝔐_{(T ,F)} ⊧ Hα [t, m] then 𝔐_{(T ,F)} ⊧ Hα [t, m^{∗}] proof Let us assume that for some t and m (where m = ⟨T, R, V ⟩) holds

𝔐_{(T ,F)} ⊧ Hα [t, m]. Then for any t_{1} such that t_{1}Rt holds 𝔐_{(T ,F)} ⊧ α [t_{1}, m]. Let us take any t_{1} such that t_{1}Rt. Then α ∈ V (t_{1}). Because for any m^{∗} we have that for any t holds V (t) ⊆ V^{∗} (t), then from definition of include relation α ∈ V^{∗} (t_{1}). However t_{1} was any such that t_{1}Rt, then for any t_{1} such that t_{1}Rt holds 𝔐_{(T ,F)} ⊧ α [t_{1}, m^{∗}]. Hence 𝔐_{(T ,F)} ⊧ Hα [t, m^{∗}] .□

The following facts showing that all the axioms are true in any model 𝔐_{(T ,F)} and the rules preserve validity.

F H1) For any 𝔐, t and m holds 𝔐_{(T ,F)} ⊧ H (α → β) →

(Hα → Hβ) [t, m]

proof

Let us assume that for a certain 𝔐, t and m: 𝔐_{(T ,F)} ⊭ H (α → β) → (Hα → Hβ) [t, m]. Then there is m_{1}, m ≤ m_{1} such that 𝔐_{(T ,F)} ⊧ H (α → β) [t, m_{1}] and 𝔐_{(T ,F)} ⊭ (Hα → Hβ) [t, m_{1}]. Hence for some m_{2} such that m_{1} ≤ m_{2} holds 𝔐_{(T ,F)} ⊧ Hα [t, m_{2}] and 𝔐_{(T ,F)} ⊭ Hβ [t, m_{2}]. Then for any t_{1} such that t_{1}Rt we have that 𝔐_{(T ,F)} ⊧ α [t_{1}, m_{2}] and there is t_{2}, t_{2}Rt that we have 𝔐_{(T ,F)} ⊭ β [t_{2}, m_{2}]. At t_{2} we have that (1) 𝔐_{(T ,F)} ⊧ α [t_{2}, m_{2}] and (2) 𝔐_{(T ,F)} ⊭ β [t_{2}, m_{2}]. From 𝔐_{(T ,F)} ⊧ H (α → β) [t, m_{1}] we have that for any t_{3} such that t_{3}Rt holds 𝔐_{(T ,F)} ⊧ (α → β) [t_{3}, m_{1}]. Hence from the definition of implicity we have that for any m_{1}^{∗} holds 𝔐_{(T ,F)} ⊭ α [t_{3}, m_{1}^{∗}] or 𝔐_{(T ,F)} ⊧ β [t_{3}, m_{1}^{∗}]. Thus it is in contradiction with (1) and (2). □

F H1’) For any 𝔐, t and m holds 𝔐_{(T ,F)} ⊧ H (α → β) →

(P α → P β) [t, m]

proof

Let us assume that for a certain 𝔐, t and m: 𝔐_{(T ,F)} ⊭ H (α → β) → (P α → P β) [t, m]. Then there is m_{1}, m ≤ m_{1} such that 𝔐_{(T ,F)} ⊧ H (α → β) [t, m_{1}] and 𝔐_{(T ,F)} ⊭ (P α → P β) [t, m_{1}]. Hence for some m_{2} such that m_{1} ≤ m_{2} holds 𝔐_{(T ,F)} ⊧ P α [t, m_{2}] and 𝔐_{(T ,F)} ⊭ P β [t, m_{2}]. Thus (1) there is t_{1}, t_{1}Rt that we have 𝔐_{(T ,F)} ⊧ α [t_{1}, m_{2}] and (2) there is not t_{2}, t_{2}Rt such that 𝔐_{(T ,F)} ⊧ β [t_{2}, m_{2}]. From 𝔐_{(T ,F)} ⊧ H (α → β) [t, m_{1}] we have that for any t_{3} such that t_{3}Rt holds 𝔐_{(T ,F)} ⊧ (α → β) [t_{3}, m_{1}]. From definition of implicity we have that for any t_{3} such that t_{3}Rt and for any m_{1}^{∗} holds 𝔐_{(T ,F)} ⊭ α [t_{3}, m_{1}^{∗}] or 𝔐_{(T ,F)} ⊧ β [t_{3}, m_{1}^{∗}]. Thus it is in contradiction with (1) and (2). □

F H1”) For any 𝔐, t and m holds 𝔐_{(T ,F)} ⊧ [(Hα → P α) ∨ Hβ] [t, m] proof Suppose that for a certain 𝔐, t and m: 𝔐_{(T ,F)} ⊭ [(Hα → P α) ∨

Hβ] [t, m]. Then (1) 𝔐_{(T ,F)} ⊭ (Hα → P α) [t, m] and (2) 𝔐_{(T ,F)} ⊭ Hβ [t, m]. From (1) we have that there is m^{∗}, such that (3) 𝔐_{(T ,F)} ⊧ Hα [t, m^{∗}] and (4) 𝔐_{(T ,F)} ⊭ P α [t, m^{∗}]. Then we have from (4) that there is not element t_{1}, t_{1}Rt such that 𝔐_{(T ,F)} ⊧ α [t_{1}, m^{∗}]. If there is t_{1}, t_{1}Rt then by (3) we have 𝔐_{(T ,F)} ⊧ α [t_{1}, m^{∗}] and we have a contradiction (3) and (4). Hence there is not element t_{1} such that t_{1}Rt ( t is the first element of the set T). Then we have that 𝔐_{(T ,F)} ⊧ Hβ [t, m]. Thus it is in contradiction with (2). □

F H2) For any 𝔐, t and m holds 𝔐_{(T ,F)} ⊧ α → HF α [t, m] proof Assume that for a certain 𝔐, t and m we have: 𝔐_{(T ,F)} ⊭ α →

HF α [t, m]. Then there is m^{∗} such that (1) 𝔐_{(T ,F)} ⊧ α [t, m^{∗}] and (2) 𝔐_{(T ,F)} ⊭ HF α [t, m^{∗}]. From (2) we have that there is t_{1}, t_{1}Rt such that 𝔐_{(T ,F)} ⊭ F α [t_{1}, m^{∗}]. Thus it is in contradiction with (1) because from (1) we have that for any t_{1}, t_{1}Rt holds 𝔐_{(T ,F)} ⊧ F α [t_{1}, m^{∗}] .□

F H2’) For any 𝔐, t and m holds 𝔐_{(T ,F)} ⊧ P Gα → α [t, m] proof Suppose that for a certain 𝔐, t and m we have: 𝔐_{(T ,F)} ⊭ P Gα →

α [t, m]. Then there is m^{∗} such that (1) 𝔐_{(T ,F)} ⊧ P Gα [t, m^{∗}] and (2) 𝔐_{(T ,F)} ⊭ α [t, m^{∗}]. From (1) we have that (3) there is t_{1}, t_{1}Rt such that 𝔐_{(T ,F)} ⊧ Gα [t_{1}, m^{∗}]. Then we have that for any t_{2}, t_{1}Rt_{2} holds 𝔐_{(T ,F)} ⊧ α [t_{2}, m^{∗}]. Thus it is in contradiction with (2) . □

F HD) For any 𝔐, t and m holds 𝔐_{(T ,F)} ⊧ P α → ¬H¬α [t, m] proof Suppose that for a certain 𝔐, t and m we have: 𝔐_{(T ,F)} ⊭ P α →

¬H¬α [t, m]. Then there is m_{1}, m ≤ m_{1} such that (1) 𝔐_{(T ,F)} ⊧ P α [t, m_{1}] and (2) 𝔐_{(T ,F)} ⊭ ¬H¬α [t, m_{1}]. From (1) we have that there is t_{1}, t_{1}Rt such that (3) 𝔐_{(T ,F)} ⊧ α [t_{1}, m_{1}] and from (2) we have that for some m_{1}^{∗} holds (4) 𝔐_{(T ,F)} ⊧ H¬α [t, m_{1}^{∗}] . From (3) and Lemma 1 we have that for any m_{1}^{∗} holds (5) 𝔐_{(T ,F)} ⊧ α [t_{1}, m_{1}^{∗}]. From (4) we have that (6) for any t_{2}, t_{2}Rt holds 𝔐_{(T ,F)} ⊧ ¬α [t_{2}, m_{1}^{∗}]. Thus is contradiction with (5) and (6). □

F HD’) For any 𝔐, t and m holds 𝔐_{(T ,F)} ⊧ ¬P α → H¬α [t, m] proof (The proof is similar to F HD)

Tense logical rule RH writen in other words preserves validity.

F RH) If for any t and m holds 𝔐_{(T ,F)} ⊧ α [t, m] then holds 𝔐_{(T ,F)} ⊧ Hα [t, m]

proof

Suppose that for any t and m holds 𝔐_{(T ,F)} ⊧ α [t, m]. Then for any t_{1}Rt and m holds 𝔐_{(T ,F)} ⊧ α [t_{1}, m]. Hence for any t and m we have 𝔐_{(T ,F)} ⊧ Hα [t, m] .□

The proofs for the axioms G1-GD’ and rule RG are analogous.

Some theorems can be proved in K_{t} (See [6]) and T_{m}:

T1: (Gα ∨ Gβ) → G (α ∨ β) proof

1) α → (α ∨ β) − A7

2) β → (α ∨ β) − A8

3) G [α → (α ∨ β)] − RG, 1

4) G [β → (α ∨ β)] − RG, 2

5) G [α → (α ∨ β)] → [Gα → G (α ∨ β)] − G1

6) G [β → (α ∨ β)] → [Gβ → G (α ∨ β)] − G1

7) Gα → G (α ∨ β) − 3, 5, MP

8) Gβ → G (α ∨ β) − 4, 6, MP

9) {[Gα → G (α ∨ β)] ∧ [Gβ → G (α ∨ β)]} → [(Gα ∨ Gβ) → G (α ∨ β)] − A3

10) (Gα ∨ Gβ) → G (α ∨ β) − 7, 8, 9, MP.□

T2: (Hα ∨ Hβ) → H (α ∨ β) proof (analogous to T1)

T3: (F α ∨ F β) → F (α ∨ β) proof

1) α → (α ∨ β) − A7

2) β → (α ∨ β) − A8

3) G [α → (α ∨ β)] − RG, 1

4) G [β → (α ∨ β)] − RG, 2

5) G [α → (α ∨ β)] → [F α → F (α ∨ β)] − G1′

6) G [β → (α ∨ β)] → [F β → F (α ∨ β)] − G1′

7) F α → F (α ∨ β) − 3, 5, MP

8) F β → F (α ∨ β) − 4, 6, MP

9) {[F α → F (α ∨ β)] ∧ [F β → F (α ∨ β)]}

→ [(F α ∨ F β) → F (α ∨ β)] − A3

10) (F α ∨ F β) → F (α ∨ β) − 7, 8, 9, MP.□

T4: (P α ∨ P β) → P (α ∨ β) proof (analogous to T3)

In T_{m} we can prove the following theorems in a similar way, too:

T5: G (α ∧ β) ↔ (Gα ∧ Gβ)
T6: H (α ∧ β) ↔ (Hα ∧ Hβ)
T7: F (α ∧ β) → (F α ∧ F β)
T7: P (α ∧ β) → (P α ∧ P β)

Time with different temporal order

If we would like to describe time with different temporal order from intuitionistic point of view we have to add to the set of axioms a formulas which will be express corresponding properties of relation R. The considered system is a minimal system of intuitionistic tense logic (no condition was imposed upon R).

Reflexive time

If we wish to describe reflexive time we must add the axioms R1) Gα → α R1’) α → F α

to the axioms for T_{m}. We call the new system T_{m}^{R} and we show, that the new axioms are valid in all tense structures, where relation R has a property reflexivity. Let us consider R1 axiom. Let us take any 𝔐, t and m such that R is reflexive. Suppose that holds 𝔐_{(T ,F)} ⊧ Gα [t, m]. Then we have that (1) for any t_{1} such that tRt_{1} holds 𝔐_{(T ,F)} ⊧ α [t_{1}, m] . From reflexivity of R we have that tRt. Hence by (1) 𝔐_{(T ,F)} ⊧ α [t, m] .□

It is easy to check that if the new axiom is a tautology then relation R has a property reflexivity. Suppose that Gα → α is a tautology and R is not reflexive. Take 𝔐, t and m such that 𝔐_{(T ,F)} ⊭ α [t, m] and for any t_{1}, tRt_{1} holds 𝔐_{(T ,F)} ⊧ α [t_{1}, m]. Let t be element such that not tRt. Then we have that 𝔐_{(T ,F)} ⊧ Gα [t, m] and 𝔐_{(T ,F)} ⊭ α [t, m]. Hence 𝔐_{(T ,F)} ⊭ (Gα → α) [t, m]. Thus is contradiction that the formula Gα → α is a tautology. □

Symmetry time

Similarly to reflexive time if we wish to make our temporal order symmetry we add the axiom

R2) Gα → Hα to the axioms of T_{m}. We call the new system T_{m}^{S}. The new axiom is valid in all tense structures, where relation R has a property symmetry.

Let us take any 𝔐, t and m such that R is symmetry. Suppose that holds 𝔐_{(T ,F)} ⊧ Gα [t, m]. Then we have that for any t_{1} such that tRt_{1} holds 𝔐_{(T ,F)} ⊧ α [t_{1}, m]. From property of symmetry of R we have that t_{1}Rt. Then for any t_{1} such that t_{1}Rt holds 𝔐_{(T ,F)} ⊧ α [t_{1}, m]. Hence 𝔐_{(T ,F)} ⊧ Hα [t, m] .□

If the new axiom is valid in all tense structures, then the relation R has a property of symmetry. Suppose that Gα → Hα is a tautology and R is not symmetry. Take 𝔐, t, t_{1} and m such that (1) tRt_{1}, (2) not t_{1}Rt, (3) 𝔐_{(T ,F)} ⊧ α [t_{1}, m] , (4) for any t_{2}, tRt_{2} holds 𝔐_{(T ,F)} ⊧ α [t_{2}, m] and (5) for any t_{3}, t_{3}Rt holds 𝔐_{(T ,F)} ⊭ α [t_{3}, m].

Then (6) 𝔐_{(T ,F)} ⊧ Gα [t, m] by (4). On the other hand from (5) we have (7) 𝔐_{(T ,F)} ⊭ Hα [t, m]. Thus we have 𝔐_{(T ,F)} ⊭ (Gα → Hα) [t, m] by (6) and (7).

Thus is contradiction that the formula Gα → Hα is a tautology. □

Transitive time

The real time seems to be transitive. Let us consider a situation: X was born earlier that Y and Y was born earlier that Z. For all it is obvious, that X was born earlier than Z. If we wish to make our tense logic system to description of time with transitive temporal order we add the axiom

R3) Gα → GGα  or  R3’) F F α → F α

to the axioms of T_{m}. We call the new system T_{m}^{T r}. The new axioms are valid in all tense structures in which relation R has a property transitivity. Let us consider R3’ axiom.

Let us take any 𝔐, t and m such that R is transitive. Suppose that holds 𝔐_{(T ,F)} ⊧ F F α [t, m]. Then we have that (1) there is t_{1}, tRt_{1} such that holds 𝔐_{(T ,F)} ⊧ F α [t_{1}, m]. Then there is t_{2},t_{1}Rt_{2} such that holds (2) 𝔐_{(T ,F)} ⊧ α [t_{2}, m]. Because R is transitive we have that (3) tRt_{2}. Then 𝔐_{(T ,F)} ⊧ F α [t, m] by (2) and (3). □

If the axiom R3’ is valid in all tense structures, then the relation R is transitive.

Suppose that F F α → F α is a tautology and R is not transitive. Take 𝔐, t_{0}, t_{1}, t_{2} and m such that (1) t_{0}Rt_{1}, (2) t_{1}Rt_{2}, (3) not t_{0}Rt_{2},

(4) 𝔐_{(T ,F)} ⊧ α [t_{2}, m] , (5) for any t, t_{0}Rt holds 𝔐_{(T ,F)} ⊭ α [t, m]. Then 𝔐_{(T ,F)} ⊧ F F α [t_{0}, m] by (1),(2) and (4). On the other hand from (5) we have 𝔐_{(T ,F)} ⊭ F α [t_{0}, m]. In consequence we have that 𝔐_{(T ,F)} ⊭ (F F α → F α) [t_{0}, m]. Thus it is in contradiction with the assumption.□

Dense time

If our system is to describe time in with dense temporal order, we add the axiom

R4) GGα → Gα or R4’) F α → F F α to the axioms of T_{m}. We call the new system T_{m}^{D}. The new axioms are valid in all tense structures in which relation R is dense. Let us consider R4’ axiom.

Suppose that for some 𝔐, t and m holds 𝔐_{(T ,F)} ⊭ F α → F F α [t, m] and R is dense. Then there is m_{1}, m ≤ m_{1} such that (1) 𝔐_{(T ,F)} ⊧ F α [t, m_{1}] and (2) 𝔐_{(T ,F)} ⊭ F F α [t, m_{1}]. Then (3) there is t_{1}, t_{1}Rt such that (4) 𝔐_{(T ,F)} ⊧ α [t_{1}, m_{1}]. From (2) we have that (5) there is not t_{2}, tRt_{2} 𝔐_{(T ,F)} ⊧ F α [t_{2}, m_{1}]. Since R is dense we have that (6) there is t_{3} such that tRt_{3} ∧ t_{3}Rt_{1}. Let us take t_{3} satisfying (6). Because t_{3}Rt_{1} we have (7) 𝔐_{(T ,F)} ⊧ F α [t_{3}, m_{1}] from (4). Thus since t_{3} has a property tRt_{3}, we have a contradiction by (5) and (7).

If the axiom R4’ is valid in all tense structures, then the relation R is dense.

Suppose that F α → F F α is a tautology and R is not dense. Take 𝔐, t_{0} and m such that (1) t_{0}Rt_{1}, (2) there is not t_{2} such that t_{0}Rt_{2} and t_{2}Rt_{1}, (3) 𝔐_{(T ,F)} ⊧ α [t_{1}, m] , (4) for any t, t_{1}Rt holds 𝔐_{(T ,F)} ⊭ α [t, m]. Then 𝔐_{(T ,F)} ⊧ F α [t_{0}, m] by (1), and (3). From (4) and (2) we have 𝔐_{(T ,F)} ⊭ F F α [t_{0}, m]. In consequence we have that 𝔐_{(T ,F)} ⊭ (F F α → F α) [t_{0}, m]. Thus it is in contradiction with the assumption.□

Time without start point

We make our temporal order without start point by adding the axiom R5) Hα → P α

to the axioms of T_{m} instead of H1” axiom.We call the new system T_{m}^{wS}. The new axiom is valid in all tense structures in which relation R has not the minimal element.

Suppose that R has not the minimal element and assume that for some 𝔐, t and m holds 𝔐_{(T ,F)} ⊭ (Hα → P α) [t, m]. Then there is m_{1,}m ≤ m_{1} such that (1) 𝔐_{(T ,F)} ⊧ Hα [t, m_{1}] and (2) 𝔐_{(T ,F)} ⊭ P α [t, m_{1}]. Then from (1) we have that (3) for any t_{1}, t_{1}Rt holds 𝔐_{(T ,F)} ⊧ α [t_{1}, m_{1}]. From (2) we have that (4) there is not t_{2}, t_{2}Rt such that 𝔐_{(T ,F)} ⊧ α [t_{2}, m_{1}]. Since R has not the minimal element we have that for any t there is t_{3} such that (5) t_{3}Rt. Let us take t_{3} satisfying condition (5). Then by (3) we have 𝔐_{(T ,F)} ⊧ α [t_{3}, m_{1}]. Hence we have a contradiction by (4).□

If the axiom R5 is valid in all tense structures, then the relation R has not the minimal element.

Suppose that Hα → P α is a tautology of and the relation R has the minimal element. Let us take 𝔐, t_{0} and m and such that (1) t_{0} is the minimal element. Then for any t_{1} such that t_{1}Rt_{0} holds 𝔐_{(T ,F)} ⊧ α [t_{1}, m]. Then we have 𝔐_{(T ,F)} ⊧ Hα [t_{0}, m] and from (1) we have that 𝔐_{(T ,F)} ⊭ P α [t_{0}, m]. Hence we have that 𝔐_{(T ,F)} ⊭ (Hα → P α) [t_{0}, m]. Thus is contradiction with the assumption.□

Time without end point

We make our temporal order without end point by adding the axiom

R6) Gα → F α

to the axioms of T_{m} instead of G1” axiom.We call the new system T_{m}^{wE}. The new axiom is valid in all tense structures in which relation R has not the maximal element.

Suppose that R has not the maximal element and assume that for some 𝔐, t and m holds 𝔐_{(T ,F)} ⊭ (Gα → F α) [t, m]. Then there is m_{1,}m ≤ m_{1} such that (1) 𝔐_{(T ,F)} ⊧ Gα [t, m_{1}] and (2) 𝔐_{(T ,F)} ⊭ F α [t, m_{1}]. Then from (1) we have that (3) for any t_{1}, tRt_{1} holds 𝔐_{(T ,F)} ⊧ α [t_{1}, m_{1}]. From (2) we have that (4) there is not t_{2}, tRt_{2} such that 𝔐_{(T ,F)} ⊧ α [t_{2}, m_{1}]. Since R has not the maximal element we have that for any t there is t_{3} such that (5) tRt_{3}. Let us take t_{3} satisfying condition (5). Then by (3) we have 𝔐_{(T ,F)} ⊧ α [t_{3}, m_{1}]. Hence we have contradiction by (4).□

If the axiom R6 is valid in all tense structures, then the relation R has not the maximal element.

Suppose that Gα → F α is a tautology of and the relation R has the maximal element. Let us take 𝔐, t_{0} and m and such that (1) t_{0} is the maximal element. Then for any t_{1} such that t_{0}Rt_{1} holds 𝔐_{(T ,F)} ⊧ α [t_{1}, m]. Then we have 𝔐_{(T ,F)} ⊧ Gα [t_{0}, m] and from (1) we have that 𝔐_{(T ,F)} ⊭ F α [t_{0}, m]. Hence we have that 𝔐_{(T ,F)} ⊭ (Gα → F α) [t_{0}, m]. Thus it is in contradiction with the assumption.□

It is easy to check in a similar way, that if we wish to make our temporal orders linear, we add the axioms:

(F α ∧ F β) → [F (α ∧ β) ∨ F (F α ∧ β) ∨ F (α ∧ F β)] (linear future) (P α ∧ P β) → [P (α ∧ β) ∨ P (P α ∧ β) ∨ P (α ∧ P β)] (linear past) to the axioms of T_{m}.

References

[1] Burges J. P, Logic and Time, “The Journal of Symbolic Logic”, vol. 44, Nr 4

[2] Dumnet M., Elements of intuitionism, Clarendon Press, Oxford, 1977 [3] Goldblatt R., Logic of time and Computation, Moscow, 1992

[4] Kotarbiński T., The problem of the existence of the future, “The Polish review”, vol. 13, 1968

[5] Łukasiewicz J., On determinism, “The Polish Review”, vol. 13, 1968 [6] McArtur R. P., Tense Logic, Dordrecht, 1976

[7] Prior A. N., Past, Present and Future, Clarendon Press, Oxford, 1967 [8] Trzȩsicki K., Intuitionism and Indeterminism, Woleński J. Philosophi-

cal Logic in Poland, Kluwer Academic Publisher, 1994

[9] Yourgran P., On the logic of indeterminist time, “The Journal of Philosophy”, vol. 82, 1985