\input stf
\def\NieparzystyHead{\line{\hfill\HeaderFont\vphantom{/S}Some remarks about intuitionistic tense logic}}
\def\ParzystyHead{\line{\HeaderFont\vphantom{/S}Dariusz Surowik\hfill}}

\startpageno=109
\pageno=\startpageno

\pu\pu\pu

\pretolerance=10000

\lasta Dariusz Surowik\\

\t SOME REMARKS ABOUT\\
\lastt INTUITIONISTIC TENSE LOGIC\\

\font\frakFont=eufm10 scaled\magstephalf
\font\msbm=msbm10 scaled\magstephalf
\font\msam=msam10 scaled\magstephalf
\def\frak#1{\hbox{\frakFont #1}}
\def\mathcal#1{{\cal #1}}
\def\textbf#1{{\bf #1}}
\def\textit#1{{\it #1}}
\def\nvDash{\hbox{\kern1mm\msbm\char50\kern1mm}}
\def\Box{\hbox{\msam\char3}}
\def\ppu{\vskip.5\baselineskip}



\rbezpu 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.


\r 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 {\it ``p is true''},
$F(p)$ means {\it ``p is false''}
and $N(p$) means {\it ``p is necessary''}.
Then if we accept the
principle of the causality and the principle of the bivalency we have that:

\smallskip
\item{1)}$T(p)\rightarrow N(p)$ -- the principle of the causality
\smallskip
\item{2)}$F(p)\rightarrow N(\neg p)$ -- the principle of the causality
\smallskip
\item{3)}$T(p)\vee F(p)$ -- the principle of bivalency
\smallskip
\item{4)}$N(p)\vee N(\neg p)$ by 1,2,3 and
$\alpha \rightarrow \gamma,\beta \rightarrow \delta,\alpha \vee \beta
\over
\gamma \vee \delta$

\smallskip

Then if we accept the principle of the causality and the law of the excluded
middle we have that:

\smallskip
\item{1)}$T(p)\rightarrow N(p)$ -- the principle of the causality
\smallskip
\item{2)}$T(\neg p)\rightarrow N(\neg p)$ -- the principle of the causality
\smallskip
\item{3)}$T(p)\vee T(\neg p)$ -- the law of the excluded middle
\smallskip
\item{4)}$N(p)\vee N(\neg p)$ by 1,2,3 and
$\alpha \rightarrow \gamma,\beta \rightarrow \delta,\alpha \vee \beta
\over
\gamma \vee \delta$
\smallskip


The formula $N(p)\vee N(\neg 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. $\alpha \rightarrow
HF\alpha$) are deterministic. Prior (See~[7])
give branching time idea, in which
future has alternatives whereas past has not got them.

\pu
%\vbox to 0pt{\line{\hskip15mm \special{em:graph rys08-01}\hfill}\vss}
\vbox to 0pt{\line{\hskip106mm \special{em:graph rys08-1o}\hfill}\vss}
\pu
\line{\hskip108mm actual\hfill}
\line{\hskip108mm future\hfill}
\pu\pu\pu\pu\pu\pu
\vskip-2mm
\centerline{Figure 1:}
\pu

From all possible future alternatives only one is realized which is called
{\it 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.


\rbezpu The system $T_m$\\

The system $T_m$ is the tense logic system based on intuitionistic
propositional logic. The tense-logical propositional language $\frak{L}$
consists of: propositional letters ($p_1,p_2,p_3....$), unary connectives
($\neg,F,G,P,H$), binary connectives ($\wedge,\vee,\rightarrow $),
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 {\it Modus Ponens} (MP)
and the tense-logical rules (RH and RG)

\vfill

\noindent For all $\alpha,\beta,\gamma \in \frak{L}:$

{
\def\iiii #1 #2\par{\itemitem{#1}#2\par\smallskip}

\smallskip

\iiii A1) $\alpha \rightarrow \left( \beta \rightarrow \alpha \right) $

\iiii A2) $\left( \alpha \rightarrow \beta \right) \rightarrow \left\{ \left[
\alpha \rightarrow \left( \beta \rightarrow \gamma \right) \right]
\rightarrow \left( \alpha \rightarrow \gamma \right) \right\} $

\iiii A3) $\left[ \left( \alpha \rightarrow \gamma \right) \wedge \left( \beta
\rightarrow \gamma \right) \right] \rightarrow \left\{ \left( \alpha \vee
\beta \right) \rightarrow \gamma \right\} $

\iiii A4) $\left( \alpha \wedge \beta \right) \rightarrow \alpha $

\iiii A5) $\left( \alpha \wedge \beta \right) \rightarrow \beta $

\iiii A6) $\alpha \rightarrow \left[ \beta \rightarrow \left( \alpha \wedge \beta \right)\right] $

\iiii A7) $\alpha \rightarrow \left( \alpha \vee \beta \right) $

\iiii A8) $\beta \rightarrow \left( \alpha \vee \beta \right) $

\iiii A9) $\left( \alpha \wedge \neg \alpha \right) \rightarrow \beta $

\iiii A10) $\left( \alpha \rightarrow \neg \alpha \right) \rightarrow \neg \alpha $

}


\vfill

\noindent {\it Tense-logical axioms:}

\def\\ #1 #2 \\ #3 #4 \\{\smallskip\line{\hbox to0.5\hsize{\indent \hbox to 11mm{#1\hfill}#2\hfill}\indent\hbox to 11mm{#3\hfill}#4\hfill}}


\\
\textbf{H1)}
$H\left( \alpha \rightarrow \beta \right) \rightarrow \left(H\alpha \rightarrow H\beta \right)$
\\
\textbf{G1)}
$G\left( \alpha \rightarrow \beta \right) \rightarrow \left( G\alpha \rightarrow G\beta \right) $
\\

\\
\textbf{H1')}
$H\left( \alpha \rightarrow \beta \right) \rightarrow \left(P\alpha \rightarrow P\beta \right) $
\\
\textbf{G1')}
$G\left( \alpha \rightarrow \beta \right) \rightarrow \left( F\alpha\rightarrow F\beta \right) $
\\

\\
\textbf{H1'')}
$\left( H\alpha \rightarrow P\alpha \right) \vee H\beta $
\\
\textbf{G1'')}
$\left( G\alpha \rightarrow F\alpha \right) \vee G\beta $
\\

\\
\textbf{H2)}
$\alpha \rightarrow HF\alpha $
\\
\textbf{G2)}
$\alpha \rightarrow GP\alpha $
\\

\\
\textbf{H2')}
$PG\alpha \rightarrow \alpha$
\\
\textbf{G2')}
$FH\alpha \rightarrow \alpha $
\\

\\
\textbf{HD)}
$P\alpha \rightarrow \neg H\neg \alpha$
\\
\textbf{GD)}
$F\alpha \rightarrow \neg G\neg \alpha $
\\

\\
\textbf{HD')}
$\neg P\alpha \rightarrow H\neg \alpha$
\\
\textbf{GD')}
$\neg F\alpha \rightarrow G\neg \alpha $
\\

\vfill

\noindent Tense-logical rules:

\smallskip

\\
\textbf{RH}:
to infer $H\alpha $ from $\alpha $
\\
\textbf{RG}:
to infer $G\alpha $ from $\alpha $
\\

\eject


The axioms \textbf{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).


\r Semantics\\

Let $T$ be any nonempty set.
A time $\mathcal{T}$ is an ordered couple
$\left\langle T,R\right\rangle$,
where $R$ is a~binary relation
(earlier-later) on~$T$.


Let $V$ be a function mapping points $t\in T$ to subsets $V\left( t\right)$
of the set of propositional letters.

Let $\mathcal{F}$ be nonempty class of such functions.
$\frak{M}_{\left(\mathcal{T},\mathcal{F}\right)}$
denotes
$\left\{\left\langle T,R,V\right\rangle:V\in\mathcal{F}\right\}$.

Let $\leq$ be a relation between elements of
$\frak{M}_{\left(\mathcal{T},\mathcal{F}\right)}$
defined as follows:

$\left\langle T,R,V_1\right\rangle \leq \left\langle T,R,V_2\right\rangle$
iff for each
$t\in T:V_1(t)\subseteq V_2(t)$.
The relation $\leq$ is reflexive and transitive.

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

\pu

%%\vbox to 0pt{\line{\hskip0mm \special{em:graph rys08-02}\hfill}\vss}
\vbox to 0pt{\line{\hskip126mm \special{em:graph rys08-2o}\hfill}\vss}
\mpu
\vbox to0pt{
\offinterlineskip
\def\t #1.#2.#3...{\vbox to0pt{\vskip#2mm\line{\hskip#1mm $#3$\hss}\vss}}

\t  16.-4.t_1...
\t  61.-4.t_2...
\t 105.-4.t_3...
\t   1.16.V_1(t_1)...
\t  46.16.V_1(t_2)...
\t  89.16.V_1(t_3)...
\t 115.16.V_2(t_3)...
\t   2.47.V_2(t_1)...
\t  46.47.V_2(t_2)...
\t  9.25.p...
\t  7.32.s...
\t 18.29.q...
\t 15.34.r...
\t 26.27.v...
\t 28.35.u...

\t 63.29.p...
\t 67.32.s...
\t 62.34.q...
\t 62.43.r...
\t 71.42.w...

\t  98.29.z...
\t 98.38.v...
\t 107.34.p...
\t 110.39.q...

\vss}
\pu\pu\pu\pu\pu\pu\pu\pu\pu\pu\pu
\centerline{Figure 2:}

\vfill

Let $m_1=\left\langle T,R,V_1\right\rangle,m_2=\left\langle
T,R,V_2\right\rangle$.
Analysing the situation showed on \textbf{Figure~2}.
we conclude that in this case (accordingly to definition of relation
$\leq$) it does not holds
$m_1\leq m_2$, because for point $t_1$ we have that
$V_1\left( t_1\right) $ is not included in $V_2\left( t_1\right)$.

\pu\pu

\eject

For three-element time structure showed on \textbf{Figure~3} it holds
$m_1\leq m_2$.

\pu
%\vbox to 0pt{\line{\hskip0mm \special{em:graph rys08-03}\hfill}\vss}
\vbox to 0pt{\line{\hskip126mm \special{em:graph rys08-3o}\hfill}\vss}
\mpu
\vbox to0pt{
\offinterlineskip
\def\t #1.#2.#3...{\vbox to0pt{\vskip#2mm\line{\hskip#1mm $#3$\hss}\vss}}

\t  16.-4.t_1...
\t  61.-4.t_2...
\t 105.-4.t_3...
\t   1.15.V_1(t_1)...
\t  46.15.V_1(t_2)...
\t  89.15.V_1(t_3)...
\t 115.15.V_2(t_3)...
\t   0.51.V_2(t_1)...
\t  46.47.V_2(t_2)...
\t 12.25.p...
\t  9.32.s...
\t 18.29.q...
\t 15.34.r...
\t 28.27.v...
\t 28.37.u...

\t 63.29.p...
\t 67.32.s...
\t 62.34.q...
\t 62.43.r...
\t 71.42.w...

\t  98.29.z...
\t 98.38.v...
\t 107.34.p...
\t 110.39.q...

\vss}
\pu\pu\pu\pu\pu\pu\pu\pu\pu\pu\pu
\centerline{Figure 3:}

\vfill

\textbf{Remark}

For $m\in \frak{M}_{\left( \mathcal{T},\mathcal{F}\right) }\,\,\,$by $m^{*}$
we shall mean any $m_1\in \frak{M}_{\left( \mathcal{T},\mathcal{F}\right) }$
such that $m\leq m_1$.

\pu

$\frak{M}_{\left( \mathcal{T},\mathcal{F}\right) }$ is called a model based
on time $\mathcal{T}$. For a model $\frak{M}_{\left( \mathcal{T},\mathcal{F}%
\right) }$, a point $t\in T$ and $m\in \frak{M}_{\left( \mathcal{T},\mathcal{%
F}\right) }$, a tense-logical formula $\alpha $, the so-called \textit{%
`truth definition}' explains what it means for $\alpha $ to be \textit{true
in} $\frak{M}_{\left( \mathcal{T},\mathcal{F}\right) }$ \textit{at} $\left[
t,m\right] $

\pu

\textbf{Definition:}

$\frak{M}_{\left( \mathcal{T},\mathcal{F}\right) }\models \alpha [t,m]$ is
defined through the clauses:

{
\def\iiii #1 #2\par{\smallskip\itemitem{#1}#2\par}

\iiii 1) $\frak{M}_{\left( \mathcal{T},\mathcal{F}\right) }\models p[t,m]$
 iff
 $p\in V(t).$

\iiii 2) $\frak{M}_{\left( \mathcal{T},\mathcal{F}\right) }\models \neg \alpha[t,m]$
 iff
 for any $m^{*}\in \frak{M}_{\left( \mathcal{T},\mathcal{F}\right) }$ holds $\frak{M}_{\left( \mathcal{T},\mathcal{F}\right)}\nvDash \alpha [t,m^{*}]$

\iiii 3) $\frak{M}_{\left( \mathcal{T},\mathcal{F}\right) }\models \left( \alpha \vee \beta \right) [t,m]$
 iff
 $\frak{M}_{\left( \mathcal{T},\mathcal{F}\right) }\models \alpha [t,m]$ or $\frak{M}_{\left( \mathcal{T},\mathcal{F}\right) }\models \beta [t,m]$

\iiii 4) $\frak{M}_{\left( \mathcal{T},\mathcal{F}\right) }\models \left( \alpha \wedge \beta \right) [t,m]$
 iff
 $\frak{M}_{\left( \mathcal{T},\mathcal{F}\right) }\models \alpha [t,m]$ and $\frak{M}_{\left( \mathcal{T},\mathcal{F}\right) }\models \beta [t,m]$

\iiii 5) $\frak{M}_{\left( \mathcal{T},\mathcal{F}\right) }\models \left( \alpha \rightarrow \beta \right) [t,m]$
 iff
 for any $m^{*}\in \frak{M}_{\left( \mathcal{T},\mathcal{F}\right) }$
 holds\hfill\break
 \indent\kern39mm
 $\frak{M}_{\left( \mathcal{T},\mathcal{F}\right) }\nvDash \alpha [t,m^{*}]$
 or
 $\frak{M}_{\left( \mathcal{T},\mathcal{F}\right) }\models \beta [t,m^{*}]$

\iiii 6) $\frak{M}_{\left( \mathcal{T},\mathcal{F}\right) }\models F\alpha [t,m]$
 iff
 $\exists t_1,tRt_1,\,$such that $\frak{M}_{\left( \mathcal{T},\mathcal{F}\right) }\models \alpha [t_1,m]$

\iiii 7) $\frak{M}_{\left( \mathcal{T},\mathcal{F}\right) }\models G\alpha [t,m]$
 iff
 $\forall t_1,tRt_1\,\,$holds $\frak{M}_{\left( \mathcal{T},\mathcal{F}\right) }\models \alpha [t_1,m]$

\iiii 8) $\frak{M}_{\left( \mathcal{T},\mathcal{F}\right) }\models P\alpha [t,m]$
 iff
 $\exists t_1,t_1Rt,\,$such that $\frak{M}_{\left( \mathcal{T},\mathcal{F}\right) }\models \alpha [t_1,m]$

\iiii 9) $\frak{M}_{\left( \mathcal{T},\mathcal{F}\right) }\models H\alpha [t,m]$
 iff
 $\forall t_1,t_1Rt\,\,$holds $\frak{M}_{\left(\mathcal{T},\mathcal{F}\right) }\models \alpha [t_1,m]$

}


\pu

%\medskip

$\frak{M}_{\left( \mathcal{T},\mathcal{F}\right) }\models \alpha [t,m]$
($\alpha $ is true in $\frak{M}_{\left( \mathcal{T},\mathcal{F}\right) }$) iff
for any $t\in T$ and any $m\in \frak{M}_{\left( \mathcal{T},\mathcal{F}%
\right) }:\frak{M}_{\left( \mathcal{T},\mathcal{F}\right) }\models \alpha
[t,m]$.

\eject

$\mathcal{T}\models \alpha $ ($\alpha $ is true in time $\mathcal{T}$) iff
it is true in $\frak{M}_{\left( \mathcal{T},\mathcal{F}\right) }$ for any $%
\mathcal{F}$.

$\models \alpha $ ($\alpha $ is a tautology of the minimal intuitionistic
tense logic) iff it is true in $\mathcal{T}$, for any $\mathcal{T}.$


\pu

It is easy to check that holds:

\pu

\textbf{Lemma 1}

If for some $t$ and $m$ holds $\frak{M}_{\left( \mathcal{T},\mathcal{F}%
\right) }\models \alpha \left[ t,m\right] $ then for any $m^{*}$ holds $%
\frak{M}_{\left( \mathcal{T},\mathcal{F}\right) }\models \alpha \left[
t,m^{*}\right] $

\pu

\textbf{Lemma 2}

If for some $t$ and $m$ holds $\frak{M}_{\left( \mathcal{T},\mathcal{F}%
\right) }\models P\alpha \left[ t,m\right] $ then for any $m^{*}$ holds $%
\frak{M}_{\left( \mathcal{T},\mathcal{F}\right) }\models P\alpha \left[
t,m^{*}\right] $

\textbf{proof}

Let us assume that for some $t$ and $m$ (where $m=\left\langle
T,R,V\right\rangle $) holds $\frak{M}_{\left( \mathcal{T},\mathcal{F}\right)
}\models P\alpha \left[ t,m\right] $. Then there is $t_1$ such that $t_1Rt$
and holds $\frak{M}_{\left( \mathcal{T},\mathcal{F}\right) }\models \alpha
\left[ t_1,m\right].\;$ Hence $\alpha \in V(t_1)$. Take any $m^{*}$ (where $%
m=\left\langle T,R,V^{*}\right\rangle $)$.$ Because
(from definition $\leq$ and Remark)
for any $m^{*}$ holds $V\left( t_1\right) \subseteq V^{*}\left( t_1\right)
$ then we have, that $\alpha \in V^{*}(t_1).$ Then $\frak{M}_{\left(
\mathcal{T},\mathcal{F}\right) }\models \alpha \left[ t_1,m^{*}\right] $.
Because $t_1Rt$ then $\frak{M}_{\left( \mathcal{T},\mathcal{F}\right)
}\models P\alpha \left[ t,m^{*}\right].\Box $

\pu

\textbf{Lemma 3}

If for some $t$ and $m$ $\frak{M}_{\left( \mathcal{T},\mathcal{F}\right)
}\models H\alpha \left[ t,m\right] $ then $\;\frak{M}_{\left( \mathcal{T},%
\mathcal{F}\right) }\models H\alpha \left[ t,m^{*}\right] $

\textbf{proof}

Let us assume that for some $t$ and $m$ (where $m=\left\langle
T,R,V\right\rangle $) holds $\frak{M}_{\left( \mathcal{T},\mathcal{F}\right)
}\models H\alpha \left[ t,m\right] $. Then for any $t_1$ such that $t_1Rt$
holds $\frak{M}_{\left( \mathcal{T},\mathcal{F}\right) }\models \alpha
\left[ t_1,m\right] $. Let us take any $t_1$ such that $t_1Rt.$ Then $\alpha
\in V\left( t_1\right)$. Because for any $m^{*}$ we have that for any $t$
holds $V\left( t\right) \subseteq V^{*}\left( t\right) $, then from
definition of include relation $\alpha \in V^{*}\left( t_1\right) $. However
$t_1$ was any such that $t_1Rt,$ then for any $t_1$ such that $t_1Rt$ holds $%
\frak{M}_{\left( \mathcal{T},\mathcal{F}\right) }\models \alpha \left[
t_1,m^{*}\right]$. Hence $\frak{M}_{\left( \mathcal{T},\mathcal{F}\right)
}\models H\alpha \left[ t,m^{*}\right].\Box $

\pu

The following facts showing that all the axioms are true in any model $\frak{%
M}_{\left( \mathcal{T},\mathcal{F}\right) }$ and the rules preserve validity.

\pu

\textbf{F}\_\textbf{H1)} For any $\frak{M},t$ and $m$ holds $\frak{M}%
_{\left( \mathcal{T},\mathcal{F}\right) }\models H\left( \alpha \rightarrow
\beta \right) \rightarrow \left( H\alpha \rightarrow H\beta \right) \left[
t,m\right] $

\textbf{proof}

Let us assume that for a certain $\frak{M},t$ and $m$: $\frak{M}_{\left(
\mathcal{T},\mathcal{F}\right) }\nvDash H\left( \alpha \rightarrow \beta
\right) \rightarrow \left( H\alpha \rightarrow H\beta \right) \left[
t,m\right]$. Then there is $m_1,m\leq m_1$ such that $\frak{M}_{\left(
\mathcal{T},\mathcal{F}\right) }\models H\left( \alpha \rightarrow \beta
\right) \left[ t,m_1\right] $ and $\frak{M}_{\left( \mathcal{T},\mathcal{F}%
\right) }\nvDash \left( H\alpha \rightarrow H\beta \right) \left[
t,m_1\right]$. Hence for some $m_2$ such that $m_1\leq m_2$ holds $\frak{M}%
_{\left( \mathcal{T},\mathcal{F}\right) }\models H\alpha $ $\left[
t,m_2\right] $ and $\frak{M}_{\left( \mathcal{T},\mathcal{F}\right) }\nvDash
H\beta \left[ t,m_2\right]$. Then for any $t_1$ such that $t_1Rt$ we have
that $\frak{M}_{\left( \mathcal{T},\mathcal{F}\right) }\models \alpha \left[
t_1,m_2\right] $ and there is $t_2$, $t_2Rt$ that we have $\frak{M}_{\left(
\mathcal{T},\mathcal{F}\right) }\nvDash \beta $ $\left[ t_2,m_2\right]$. At
$t_2$ we have that \textbf{(1)} $\frak{M}_{\left( \mathcal{T},\mathcal{F}%
\right) }\models \alpha $ $\left[ t_2,m_2\right] $ and \textbf{(2)} $\frak{M}%
_{\left( \mathcal{T},\mathcal{F}\right) }\nvDash \beta $ $\left[
t_2,m_2\right]$. From $\frak{M}_{\left( \mathcal{T},\mathcal{F}\right)
}\models H\left( \alpha \rightarrow \beta \right) \left[ t,m_1\right] $ we
have that for any $t_3$ such that $t_3Rt$ holds $\frak{M}_{\left( \mathcal{T}%
,\mathcal{F}\right) }\models \left( \alpha \rightarrow \beta \right) \left[
t_3,m_1\right]$. Hence from the definition of implicity we have that for
any $m_1^{*}$ holds $\frak{M}_{\left( \mathcal{T},\mathcal{F}\right)
}\nvDash \alpha $ $\left[ t_3,m_1^{*}\right] $ or $\frak{M}_{\left( \mathcal{%
T},\mathcal{F}\right) }\models \beta $ $\left[ t_3,m_1^{*}\right]$. Thus
it is in contradiction with \textbf{(1)} and\textbf{\ (2)}. $\Box $

\pu

\textbf{F\_H1')} For any $\frak{M},t$ and $m$ holds $\frak{M}_{\left(
\mathcal{T},\mathcal{F}\right) }\models H\left( \alpha \rightarrow \beta
\right) \rightarrow \left( P\alpha \rightarrow P\beta \right) \left[
t,m\right] $

\textbf{proof}

Let us assume that for a certain $\frak{M},t$ and $m$: $\frak{M}_{\left(
\mathcal{T},\mathcal{F}\right) }\nvDash H\left( \alpha \rightarrow \beta
\right) \rightarrow \left( P\alpha \rightarrow P\beta \right) \left[
t,m\right]$. Then there is $m_1,m\leq m_1$ such that $\frak{M}_{\left(
\mathcal{T},\mathcal{F}\right) }\models H\left( \alpha \rightarrow \beta
\right) \left[ t,m_1\right] $ and $\frak{M}_{\left( \mathcal{T},\mathcal{F}%
\right) }\nvDash \left( P\alpha \rightarrow P\beta \right) \left[
t,m_1\right]$. Hence for some $m_2$ such that $m_1\leq m_2$ holds $\frak{M}%
_{\left( \mathcal{T},\mathcal{F}\right) }\models P\alpha $ $\left[
t,m_2\right] $ and $\frak{M}_{\left( \mathcal{T},\mathcal{F}\right) }\nvDash
P\beta \left[ t,m_2\right]$. Thus \textbf{(1)} there is $t_1$, $t_1Rt$ that
we have $\frak{M}_{\left( \mathcal{T},\mathcal{F}\right) }\models \alpha $ $%
\left[ t_1,m_2\right] $ and \textbf{(2)} there is not $t_2$, $t_2Rt$ such
that $\frak{M}_{\left( \mathcal{T},\mathcal{F}\right) }\models \beta $ $%
\left[ t_2,m_2\right]$. From $\frak{M}_{\left( \mathcal{T},\mathcal{F}%
\right) }\models H\left( \alpha \rightarrow \beta \right) \left[
t,m_1\right] $ we have that for any $t_3$ such that $t_3Rt$ holds $\frak{M}%
_{\left( \mathcal{T},\mathcal{F}\right) }\models \left( \alpha \rightarrow
\beta \right) \left[ t_3,m_1\right]$. From definition of implicity we have
that for any $t_3$ such that $t_3Rt$ and for any $m_1^{*}$ holds $\frak{M}%
_{\left( \mathcal{T},\mathcal{F}\right) }\nvDash \alpha $ $\left[
t_3,m_1^{*}\right] $ or $\frak{M}_{\left( \mathcal{T},\mathcal{F}\right)
}\models \beta $ $\left[ t_3,m_1^{*}\right] $. Thus it is in contradiction
with \textbf{(1)} and\textbf{\ (2)}. $\Box $

\pu

\textbf{F\_H1'')} For any $\frak{M},t$ and $m$ holds $\frak{M}_{\left(
\mathcal{T},\mathcal{F}\right) }\models \left[ \left( H\alpha \rightarrow
P\alpha \right) \vee H\beta \right] \left[ t,m\right] $

\textbf{proof }

Suppose that for a certain $\frak{M},t$ and $m$: $\frak{M}_{\left( \mathcal{T%
},\mathcal{F}\right) }\nvDash \left[ \left( H\alpha \rightarrow P\alpha
\right) \vee\right.$\break%%%%%%%%%%%%%%%%
$\left.H\beta \right] \left[ t,m\right]$. Then \textbf{(1)} $\frak{M}%
_{\left( \mathcal{T},\mathcal{F}\right) }\nvDash \left( H\alpha \rightarrow
P\alpha \right) \left[ t,m\right] $ and \textbf{(2)} $\frak{M}_{\left(
\mathcal{T},\mathcal{F}\right)
}\nvDash$\break%%%%%%%%%%%%%%%%%%%%%%%
$H\beta \left[ t,m\right]$. From
\textbf{(1)} we have that there is $m^{*}$, such that \textbf{(3)} $\frak{M}%
_{\left( \mathcal{T},\mathcal{F}\right) }\models H\alpha \left[
t,m^{*}\right] $ and \textbf{(4)} $\frak{M}_{\left( \mathcal{T},\mathcal{F}%
\right) }\nvDash P\alpha \left[ t,m^{*}\right]$. Then we have from \textbf{%
(4)} that there is not element $t_1,t_1Rt$ such that $\frak{M}_{\left(
\mathcal{T},\mathcal{F}\right) }\models \alpha \left[ t_1,m^{*}\right]$. If
there is $t_1,t_1Rt$ then by \textbf{(3)} we have $\frak{M}_{\left( \mathcal{%
T},\mathcal{F}\right) }\models \alpha \left[ t_1,m^{*}\right] $ and we have
a contradiction \textbf{(3)} and \textbf{(4)}. Hence there is not element $%
t_1$ such that $t_1Rt$ ( $t$ is the first element of the set $T$). Then we
have that $\frak{M}_{\left( \mathcal{T},\mathcal{F}\right) }\models H\beta
\left[ t,m\right]$. Thus it is in contradiction with \textbf{(2)}. $\Box $

\pu

\textbf{F\_H2)} For any $\frak{M},t$ and $m$ holds $\frak{M}_{\left(
\mathcal{T},\mathcal{F}\right) }\models \alpha \rightarrow HF\alpha \left[
t,m\right] $

\textbf{proof}

Assume that for a certain $\frak{M},t$ and $m$ we have: $\frak{M}_{\left(
\mathcal{T},\mathcal{F}\right) }\nvDash $ $\alpha \rightarrow HF\alpha
\left[ t,m\right]$. Then there is $m^{*}$ such that \textbf{(1)} $\frak{M}%
_{\left( \mathcal{T},\mathcal{F}\right) }\models \alpha \left[
t,m_{}^{*}\right] $ and \textbf{(2)} $\frak{M}_{\left( \mathcal{T},\mathcal{F%
}\right) }\nvDash HF\alpha \left[ t,m_{}^{*}\right]$. From \textbf{(2)} we
have that there is $t_1$, $t_1Rt$ such that $\frak{M}_{\left( \mathcal{T},%
\mathcal{F}\right) }\nvDash F\alpha \left[ t_1,m_{}^{*}\right]$. Thus it is
in contradiction with \textbf{(1)} because from \textbf{(1)} we have that
for any $t_1$, $t_1Rt$ holds $\frak{M}_{\left( \mathcal{T},\mathcal{F}%
\right) }\models F\alpha \left[ t_1,m_{}^{*}\right].\Box $

\pu

\textbf{F\_H2')} For any $\frak{M},t$ and $m$ holds $\frak{M}_{\left(
\mathcal{T},\mathcal{F}\right) }\models PG\alpha \rightarrow \alpha \left[
t,m\right] $

\textbf{proof}

Suppose that for a certain $\frak{M},t$ and $m$ we have: $\frak{M}_{\left(
\mathcal{T},\mathcal{F}\right) }\nvDash PG\alpha \rightarrow \alpha \left[
t,m\right]$. Then there is $m^{*}$ such that \textbf{(1)} $\frak{M}_{\left(
\mathcal{T},\mathcal{F}\right) }\models PG\alpha \left[ t,m_{}^{*}\right] $
and \textbf{(2)} $\frak{M}_{\left( \mathcal{T},\mathcal{F}\right) }\nvDash
\alpha \left[ t,m_{}^{*}\right]$. From \textbf{(1)} we have that \textbf{(3)%
} there is $t_1$, $t_1Rt$ such that $\frak{M}_{\left( \mathcal{T},\mathcal{F}%
\right) }\models G\alpha \left[ t_1,m_{}^{*}\right]$. Then we have that for
any $t_2$, $t_1Rt_2$ holds $\frak{M}_{\left( \mathcal{T},\mathcal{F}\right)
}\models \alpha \left[ t_2,m_{}^{*}\right]$. Thus it is in contradiction
with \textbf{(2) }. $\Box $

\pu

\textbf{F\_HD)} For any $\frak{M},t$ and $m$ holds $\frak{M}_{\left(
\mathcal{T},\mathcal{F}\right) }\models P\alpha \rightarrow \neg H\neg
\alpha \left[ t,m\right] $

\textbf{proof}

Suppose that for a certain $\frak{M},t$ and $m$ we have: $\frak{M}_{\left(
\mathcal{T},\mathcal{F}\right) }\nvDash P\alpha \rightarrow \neg H\neg
\alpha \left[ t,m\right]$. Then there is $m_1,m\leq m_1$ such that (\textbf{%
1)} $\frak{M}_{\left( \mathcal{T},\mathcal{F}\right) }\models P\alpha \left[
t,m_1\right] $ and \textbf{(2) }$\frak{M}_{\left( \mathcal{T},\mathcal{F}%
\right) }\nvDash \neg H\neg \alpha \left[ t,m_1\right]$. From \textbf{(1)}
we have that there is $t_1$, $t_1Rt$ such that \textbf{(3) }$\frak{M}%
_{\left( \mathcal{T},\mathcal{F}\right) }\models \alpha \left[
t_1,m_1\right] $ and from \textbf{(2)} we have that for some $m_1^{*}$ holds
\textbf{(4) }$\frak{M}_{\left( \mathcal{T},\mathcal{F}\right) }\models H\neg
\alpha \left[ t,m_1^{*}\right] $ $.$ From \textbf{(3)} and \textbf{Lemma 1 }%
we have that for any $m_1^{*}$ holds \textbf{(5)} $\frak{M}_{\left( \mathcal{%
T},\mathcal{F}\right) }\models \alpha \left[ t_1,m_1^{*}\right]$. From
\textbf{(4)} we have that \textbf{(6)} for any $t_2$, $t_2Rt$ holds $\frak{M}%
_{\left( \mathcal{T},\mathcal{F}\right) }\models \neg \alpha \left[
t_2,m_1^{*}\right]$. Thus is contradiction with \textbf{(5) }and\textbf{\
(6)}. $\Box $

\pu

\textbf{F\_HD')} For any $\frak{M},t$ and $m$ holds $\frak{M}_{\left(
\mathcal{T},\mathcal{F}\right) }\models \neg P\alpha \rightarrow H\neg
\alpha \left[ t,m\right] $

\textbf{proof}

(The proof is similar to \textbf{F\_HD})\


\pu

Tense logical rule \textbf{RH} writen in other words preserves validity.\

\pu

\textbf{F\_RH)} If for any $t$ and $m$ holds $\frak{M}_{\left( \mathcal{T},%
\mathcal{F}\right) }\models \alpha \left[ t,m\right] $ then holds $\frak{M}%
_{\left( \mathcal{T},\mathcal{F}\right) }\models H\alpha $ $\left[
t,m\right] $

\textbf{proof}

Suppose that for any $t$ and $m$ holds $\frak{M}_{\left( \mathcal{T},%
\mathcal{F}\right) }\models \alpha \left[ t,m\right]$. Then for any $t_1Rt$
and $m$ holds $\frak{M}_{\left( \mathcal{T},\mathcal{F}\right) }\models
\alpha \left[ t_1,m\right]$. Hence for any $t$ and $m$ we have $\frak{M}%
_{\left( \mathcal{T},\mathcal{F}\right) }\models H\alpha \left[ t,m\right]
.\Box $

\pu

The proofs for the axioms \textbf{G1-GD'} and rule \textbf{RG} are
analogous.

\pu

Some theorems can be proved in $K_t$ (See~[6]) and $T_m$:

\pu
\pu

\textbf{T1:} $\left( G\alpha \vee G\beta \right) \rightarrow G\left( \alpha
\vee \beta \right) $

\textbf{proof}

{
\def\iiii #1 #2\par{\smallskip\itemitem{#1}#2\par}

\iiii 1) $\alpha \rightarrow \left( \alpha \vee \beta \right) -A7$

\iiii 2) $\beta \rightarrow \left( \alpha \vee \beta \right) -A8$

\iiii 3) $G\left[ \alpha \rightarrow \left( \alpha \vee \beta \right) \right]
-RG,1 $

\iiii 4) $G\left[ \beta \rightarrow \left( \alpha \vee \beta \right) \right] -RG,2$

\iiii 5) $G\left[ \alpha \rightarrow \left( \alpha \vee \beta \right) \right]
\rightarrow \left[ G\alpha \rightarrow G\left( \alpha \vee \beta \right)
\right] -G1$

\iiii 6) $G\left[ \beta \rightarrow \left( \alpha \vee \beta \right) \right]
\rightarrow \left[ G\beta \rightarrow G\left( \alpha \vee \beta \right)
\right] -G1$

\iiii 7) $G\alpha \rightarrow G\left( \alpha \vee \beta \right) -3,5,MP$

\iiii 8) $G\beta \rightarrow G\left( \alpha \vee \beta \right) -4,6,MP$

\iiii 9) $\left\{ \left[ G\alpha \rightarrow G\left( \alpha \vee \beta \right)
\right] \wedge \left[ G\beta \rightarrow G\left( \alpha \vee \beta \right)
\right] \right\}
\rightarrow$\hfill\break%%%%%%%%%%%%%%%%%%%%%%
$\left[ \left( G\alpha \vee G\beta \right)
\rightarrow G\left( \alpha \vee \beta \right) \right] -A3$

\iiii 10) $\left( G\alpha \vee G\beta \right) \rightarrow G\left( \alpha \vee
\beta \right) -7,8,9,MP.\Box $


}

\pu

\textbf{T2:} $\left( H\alpha \vee H\beta \right) \rightarrow H\left( \alpha \vee
\beta \right) $

\textbf{proof} (analogous to T1)

\pu

\textbf{T3:} $\left( F\alpha \vee F\beta \right) \rightarrow F\left( \alpha \vee
\beta \right) $

\textbf{proof}

{
\def\iiii #1 #2\par{\smallskip\itemitem{#1}#2\par}

\iiii 1) $\alpha \rightarrow \left( \alpha \vee \beta \right) -A7$

\iiii 2) $\beta \rightarrow \left( \alpha \vee \beta \right) -A8$

\iiii 3) $G\left[ \alpha \rightarrow \left( \alpha \vee \beta \right) \right]
-RG,1 $

\iiii 4) $G\left[ \beta \rightarrow \left( \alpha \vee \beta \right) \right] -RG,2$

\iiii 5) $G\left[ \alpha \rightarrow \left( \alpha \vee \beta \right) \right]
\rightarrow \left[ F\alpha \rightarrow F\left( \alpha \vee \beta \right)
\right] -G1^{\prime }$

\iiii 6) $G\left[ \beta \rightarrow \left( \alpha \vee \beta \right) \right]
\rightarrow \left[ F\beta \rightarrow F\left( \alpha \vee \beta \right)
\right] -G1^{\prime }$

\iiii 7) $F\alpha \rightarrow F\left( \alpha \vee \beta \right) -3,5,MP$

\iiii 8) $F\beta \rightarrow F\left( \alpha \vee \beta \right) -4,6,MP$

\iiii 9) $\left\{ \left[ F\alpha \rightarrow F\left( \alpha \vee \beta \right)
\right] \wedge \left[ F\beta \rightarrow F\left( \alpha \vee \beta \right)
\right] \right\}$\hfill\break%%%%%%%%%%%%%%%%%%%%%%%%%%
$\rightarrow \left[ \left( F\alpha \vee F\beta \right)
\rightarrow F\left( \alpha \vee \beta \right) \right] -A3$

\iiii 10) $\left( F\alpha \vee F\beta \right) \rightarrow F\left( \alpha \vee
\beta \right) -7,8,9,MP.\Box $

}

\pu

\textbf{T4:} $\left( P\alpha \vee P\beta \right) \rightarrow P\left( \alpha \vee
\beta \right) $

\textbf{proof} (analogous to T3)

\pu

In $T_m$ we can prove the following theorems in a similar way, too:

\pu

\textbf{T5:} $G\left( \alpha \wedge \beta \right) \leftrightarrow \left( G\alpha
\wedge G\beta \right) $

\smallskip

\textbf{T6:} $H\left( \alpha \wedge \beta \right) \leftrightarrow \left( H\alpha
\wedge H\beta \right) $

\smallskip

\textbf{T7:} $F\left( \alpha \wedge \beta \right) \rightarrow \left( F\alpha \wedge
F\beta \right) $

\smallskip

\textbf{T7:} $P\left( \alpha \wedge \beta \right) \rightarrow \left( P\alpha \wedge
P\beta \right) $

\mpu

\r 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$).

\mpu

\r Reflexive time\\

If we wish to describe reflexive time we must add the axioms

{
\def\\ #1 #2 \\ #3 #4 \\{\line{\hbox to0.5\hsize{\indent\hbox to 11mm{#1\hfill}#2\hfill}\hbox to 11mm{#3\hfill}#4\hfill}}

\smallskip

\\
\textbf{R1)}
$G\alpha \rightarrow \alpha $
\\
\textbf{R1')}
$\alpha\rightarrow F\alpha $
\\

\smallskip
}

\noindent 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 \textbf{R1} axiom. Let us take any $%
\frak{M},t$ and $m$ such that $R$ is reflexive. Suppose that holds $\frak{M}%
_{\left( \mathcal{T},\mathcal{F}\right) }\models G\alpha \left[ t,m\right]$. 
Then we have that \textbf{(1)} for any $t_1$ such that $tRt_1$ holds $\frak{M%
}_{\left( \mathcal{T},\mathcal{F}\right) }\models \alpha \left[ t_1,m\right]
.$ From reflexivity of $R$ we have that $tRt$. Hence by \textbf{(1)} $\frak{M%
}_{\left( \mathcal{T},\mathcal{F}\right) }\models \alpha \left[ t,m\right]
.\Box $

It is easy to check that if the new axiom is a tautology then relation $R$
has a property reflexivity. Suppose that $G\alpha \rightarrow \alpha $ is a
tautology and $R$ is not reflexive. Take $\frak{M},t$ and $m$ such that $%
\frak{M}_{\left( \mathcal{T},\mathcal{F}\right) }\nvDash \alpha \left[
t,m\right] $ and for any $t_1,tRt_1$ holds $\frak{M}_{\left( \mathcal{T},%
\mathcal{F}\right) }\models \alpha \left[ t_1,m\right]$. Let $t$ be element
such that not $tRt.$ Then we have that $\frak{M}_{\left( \mathcal{T},%
\mathcal{F}\right) }\models G\alpha \left[ t,m\right] $ and $\frak{M}%
_{\left( \mathcal{T},\mathcal{F}\right) }\nvDash \alpha \left[ t,m\right]$. 
Hence $\frak{M}_{\left( \mathcal{T},\mathcal{F}\right) }\nvDash \left(
G\alpha \rightarrow \alpha \right) \left[ t,m\right]$. Thus is
contradiction that the formula $G\alpha \rightarrow \alpha $ is a tautology.
$\Box $


\mpu

\r Symmetry time\\

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

\smallskip

\textbf{R2)} $G\alpha \rightarrow H\alpha $

\smallskip

\noindent 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 $\frak{M},t$ and $m$ such that $R$ is symmetry. Suppose that
holds $\frak{M}_{\left( \mathcal{T},\mathcal{F}\right) }\models G\alpha
\left[ t,m\right]$. Then we have that for any $t_1$ such that $tRt_1$ holds
$\frak{M}_{\left( \mathcal{T},\mathcal{F}\right) }\models \alpha \left[
t_1,m\right]$. From property of symmetry of $R$ we have that $t_1Rt$. Then
for any $t_1$ such that $t_1Rt$ holds $\frak{M}_{\left( \mathcal{T},\mathcal{%
F}\right) }\models \alpha \left[ t_1,m\right]$. Hence $\frak{M}_{\left(
\mathcal{T},\mathcal{F}\right) }\models H\alpha \left[ t,m\right].\Box $

If the new axiom is valid in all tense structures, then the relation $R$ has
a property of symmetry. Suppose that $G\alpha \rightarrow H\alpha $ is a
tautology and $R$ is not symmetry. Take $\frak{M},t,t_1$ and $m$ such that
\textbf{(1)} $tRt_1$, \textbf{(2)} not $t_1Rt,$ \textbf{(3)} $\frak{M}%
_{\left( \mathcal{T},\mathcal{F}\right) }\models \alpha \left[ t_1,m\right]
, $ \textbf{(4)} for any $t_2,tRt_2$ holds $\frak{M}_{\left( \mathcal{T},%
\mathcal{F}\right) }\models \alpha \left[ t_2,m\right] $ and \textbf{(5)}
for any $t_3,t_3Rt$ holds $\frak{M}_{\left( \mathcal{T},\mathcal{F}\right)
}\nvDash \alpha \left[ t_3,m\right] $.

Then \textbf{(6)} $\frak{M}_{\left( \mathcal{T},\mathcal{F}\right) }\models
G\alpha \left[ t,m\right] $ by \textbf{(4)}. On the other hand from \textbf{%
(5)} we have \textbf{(7)} $\frak{M}_{\left( \mathcal{T},\mathcal{F}\right)
}\nvDash H\alpha \left[ t,m\right]$. Thus we have $\frak{M}_{\left(
\mathcal{T},\mathcal{F}\right) }\nvDash \left( G\alpha \rightarrow H\alpha
\right) \left[ t,m\right] $ by \textbf{(6)} and \textbf{(7)}.

Thus is contradiction that the formula $G\alpha \rightarrow H\alpha $ is a
tautology. $\Box $


\mpu

\r 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

{

\def\\ #1 #2 \\ #3 #4 \\{\line{\hbox to0.5\hsize{\indent\hbox to 11mm{#1\hfill}#2\hfill}\hbox to 11mm{#3\hfill}#4\hfill}}

\medskip

\\
\textbf{R3)}
$G\alpha \rightarrow GG\alpha \,$~~~~~~~~or
\\
\textbf{R3')}
$FF\alpha\rightarrow F\alpha$
\\

\medskip
}

\noindent to the axioms of $T_m$. We call the new system $T_m^{Tr}$. The new axioms
are valid in all tense structures in which relation $R$ has a property
transitivity. Let us consider \textbf{R3'} axiom.

Let us take any $\frak{M},t$ and $m$ such that $R$ is transitive. Suppose
that holds $\frak{M}_{\left( \mathcal{T},\mathcal{F}\right) }\models
FF\alpha \left[ t,m\right]$. Then we have that \textbf{(1)} there is $%
t_1,tRt_1$ such that holds $\frak{M}_{\left( \mathcal{T},\mathcal{F}\right)
}\models F\alpha \left[ t_1,m\right]$. Then there is $t_2$,$t_1Rt_2$ such
that holds \textbf{(2)} $\frak{M}_{\left( \mathcal{T},\mathcal{F}\right)
}\models \alpha \left[ t_2,m\right]$. Because R is transitive we have that
\textbf{(3)} $tRt_2.\,$ Then $\frak{M}_{\left( \mathcal{T},\mathcal{F}%
\right) }\models F\alpha \left[ t,m\right] $ by \textbf{(2)} and \textbf{(3)}.
$\Box$

If the axiom {\textbf R3'} is valid in all tense structures, then the relation $R$ is
transitive.

Suppose that $FF\alpha \rightarrow F\alpha $ is a tautology and $R$ is not
transitive. Take $\frak{M},t_0,t_1,t_2$ and $m$ such that \textbf{(1)} $%
t_0Rt_1$, \textbf{(2)} $t_1Rt_2,$ \textbf{(3)} not $t_0Rt_2,$ \textbf{(4)} $%
\frak{M}_{\left( \mathcal{T},\mathcal{F}\right) }\models \alpha \left[
t_2,m\right],$ \textbf{(5)} for any $t,t_0Rt$ holds $\frak{M}_{\left(
\mathcal{T},\mathcal{F}\right) }\nvDash \alpha \left[ t,m\right] $. Then $%
\frak{M}_{\left( \mathcal{T},\mathcal{F}\right) }\models FF\alpha \left[
t_0,m\right] $ by \textbf{(1),(2)} and \textbf{(4)}. On the other hand from
\textbf{(5)} we have $\frak{M}_{\left( \mathcal{T},\mathcal{F}\right)
}\nvDash F\alpha \left[ t_0,m\right]$. In consequence we have that $\frak{M}%
_{\left( \mathcal{T},\mathcal{F}\right) }\nvDash \left( FF\alpha \rightarrow
F\alpha \right) \left[ t_0,m\right]$. Thus it is in contradiction with the
assumption.$\Box $


\mpu\mpu

\r Dense time\\

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

{
\def\\ #1 #2 \\ #3 #4 \\{\line{\hbox to0.5\hsize{\indent\hbox to 11mm{#1\hfill}#2\hfill}\hbox to 11mm{#3\hfill}#4\hfill}}

\smallskip

\\
\textbf{R4)}
$GG\alpha \rightarrow G\alpha \,$~~~~~~~~or
\\
\textbf{R4')}
$F\alpha \rightarrow FF\alpha$
\\

\smallskip
}

\noindent 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 \textbf{R4'} axiom.

Suppose that for some $\frak{M},t$ and $m$ holds $\frak{M}_{\left( \mathcal{T%
},\mathcal{F}\right) }\nvDash F\alpha \rightarrow FF\alpha \left[ t,m\right]
$ and $R$ is dense. Then there is $m_1,m\leq m_1$ such that \textbf{(1)} $%
\frak{M}_{\left( \mathcal{T},\mathcal{F}\right) }\models F\alpha \left[
t,m_1\right] $ and (2) $\frak{M}_{\left( \mathcal{T},\mathcal{F}\right)
}\nvDash FF\alpha \left[ t,m_1\right]$. Then \textbf{(3)} there is $%
t_1,t_1Rt$ such that (4) $\frak{M}_{\left( \mathcal{T},\mathcal{F}\right)
}\models \alpha \left[ t_1,m_1\right]$. From \textbf{(2)} we have that
\textbf{(5)} there is not $t_2,tRt_2$ $\frak{M}_{\left( \mathcal{T},\mathcal{%
F}\right) }\models F\alpha \left[ t_2,m_1\right]$. Since R is dense we have
that \textbf{(6)} there is $t_3$ such that $tRt_3\wedge t_3Rt_1.$ Let us
take $t_3$ satisfying \textbf{(6)}. Because $t_3Rt_1$ we have \textbf{(7)} $%
\frak{M}_{\left( \mathcal{T},\mathcal{F}\right) }\models F\alpha \left[
t_3,m_1\right] $ from \textbf{(4)}. Thus since $t_3$ has a property $tRt_3,$
we have a contradiction by \textbf{(5)} and \textbf{(7).}

If the axiom \textbf{R4'} is valid in all tense structures, then the
relation $R$ is dense.

Suppose that $F\alpha \rightarrow FF\alpha $ is a tautology and $R$ is not
dense. Take $\frak{M},t_0$ and $m$ such that \textbf{(1)} $t_0Rt_1$, \textbf{%
(2)} there is not $t_2$ such that $t_0Rt_2$ and $t_2Rt_1,$ \textbf{%
(3)} $\frak{M}_{\left( \mathcal{T},\mathcal{F}\right) }\models \alpha \left[
t_1,m\right],$ \textbf{(4)} for any $t,t_1Rt$ holds $\frak{M}_{\left(
\mathcal{T},\mathcal{F}\right) }\nvDash \alpha \left[ t,m\right] $. Then $%
\frak{M}_{\left( \mathcal{T},\mathcal{F}\right) }\models F\alpha \left[
t_0,m\right] $ by \textbf{(1), }and \textbf{(3)}. From \textbf{(4)} and
\textbf{(2)} we have $\frak{M}_{\left( \mathcal{T},\mathcal{F}\right)
}\nvDash FF\alpha \left[ t_0,m\right]$. In consequence we have that $\frak{M%
}_{\left( \mathcal{T},\mathcal{F}\right) }\nvDash \left( FF\alpha
\rightarrow F\alpha \right) \left[ t_0,m\right]$. Thus it is in
contradiction with the assumption.$\Box $


\mpu

\r Time without start point\\

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

\smallskip

\textbf{R5)} $H\alpha \rightarrow P\alpha \,$

\smallskip

\noindent to the axioms of $T_m$ instead of \textbf{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 $\frak{%
M},t$ and $m$ holds $\frak{M}_{\left( \mathcal{T},\mathcal{F}\right)
}\nvDash \left( H\alpha \rightarrow P\alpha \right) \left[ t,m\right] $.
Then there is $m_{1,}m\leq m_1$ such that \textbf{(1)} $\frak{M}_{\left(
\mathcal{T},\mathcal{F}\right) }\models H\alpha \left[ t,m_1\right] $ and
\textbf{(2)} $\frak{M}_{\left( \mathcal{T},\mathcal{F}\right) }\nvDash
P\alpha \left[ t,m_1\right] $. Then from \textbf{(1)} we have that \textbf{%
(3)} for any $t_1,t_1Rt$ holds $\frak{M}_{\left( \mathcal{T},\mathcal{F}%
\right) }\models \alpha \left[ t_1,m_1\right] $. From \textbf{(2)} we have
that \textbf{(4)} there is not $t_2,t_2Rt$ such that $\frak{M}_{\left(
\mathcal{T},\mathcal{F}\right) }\models \alpha \left[ t_2,m_1\right]$.
Since $R$ has not the minimal element we have that for any $t$ there is $t_3$
such that \textbf{(5)} $t_3Rt$. Let us take $t_3$ satisfying condition
\textbf{(5)}. Then by \textbf{(3)} we have $\frak{M}_{\left( \mathcal{T},%
\mathcal{F}\right) }\models \alpha \left[ t_3,m_1\right]$. Hence we have a
contradiction by \textbf{(4)}.$\Box $

If the axiom \textbf{R5} is valid in all tense structures, then the relation
$R$ has not the minimal element.

Suppose that $H\alpha \rightarrow P\alpha \,$ is a tautology of and the
relation R has the minimal element. Let us take $\frak{M},t_0$ and $m$ and
such that \textbf{(1)} $t_0$ is the minimal element. Then for any
$t_1$ such that $t_1Rt_0$ holds $\frak{M}_{\left( \mathcal{T},\mathcal{F}%
\right) }\models \alpha \left[ t_1,m\right] $. Then we have $\frak{M}%
_{\left( \mathcal{T},\mathcal{F}\right) }\models H\alpha \left[ t_0,m\right]
$ and from \textbf{(1)} we have that $\frak{M}_{\left( \mathcal{T},\mathcal{F%
}\right) }\nvDash P\alpha \left[ t_0,m\right] $. Hence we have that $\frak{M}%
_{\left( \mathcal{T},\mathcal{F}\right) }\nvDash \left( H\alpha \rightarrow
P\alpha \right) \left[ t_0,m\right] $. Thus is contradiction with the
assumption.$\Box $


\mpu

\r Time without end point\\

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

\medskip

\textbf{R6)} $G\alpha \rightarrow F\alpha \,$

\medskip

\noindent to the axioms of $T_m$ instead of \textbf{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 $\frak{%
M},t$ and $m$ holds $\frak{M}_{\left( \mathcal{T},\mathcal{F}\right)
}\nvDash \left( G\alpha \rightarrow F\alpha \right) \left[ t,m\right] $.
Then there is $m_{1,}m\leq m_1$ such that \textbf{(1)} $\frak{M}_{\left(
\mathcal{T},\mathcal{F}\right) }\models G\alpha \left[ t,m_1\right] $ and
\textbf{(2)} $\frak{M}_{\left( \mathcal{T},\mathcal{F}\right) }\nvDash
F\alpha \left[ t,m_1\right] $. Then from \textbf{(1)} we have that \textbf{%
(3)} for any $t_1,tRt_1$ holds $\frak{M}_{\left( \mathcal{T},\mathcal{F}%
\right) }\models \alpha \left[ t_1,m_1\right] $. From \textbf{(2)} we have
that \textbf{(4)} there is not $t_2,tRt_2$ such that $\frak{M}_{\left(
\mathcal{T},\mathcal{F}\right) }\models \alpha \left[ t_2,m_1\right]$.
Since $R$ has not the maximal element we have that for any $t$ there is $t_3$
such that \textbf{(5)} $tRt_3$. Let us take $t_3$ satisfying condition
\textbf{(5)}. Then by \textbf{(3)} we have $\frak{M}_{\left( \mathcal{T},%
\mathcal{F}\right) }\models \alpha \left[ t_3,m_1\right]$. Hence we have
contradiction by \textbf{(4)}.$\Box $

If the axiom \textbf{R6} is valid in all tense structures, then the relation
$R$ has not the maximal element.

Suppose that $G\alpha \rightarrow F\alpha \,$ is a tautology of and the
relation R has the maximal element. Let us take $\frak{M},t_0$ and $m$ and
such that \textbf{(1)} $t_0$ is the maximal element. Then for any
$t_1$ such that $t_0Rt_1$ holds $\frak{M}_{\left( \mathcal{T},\mathcal{F}%
\right) }\models \alpha \left[ t_1,m\right] $. Then we have $\frak{M}%
_{\left( \mathcal{T},\mathcal{F}\right) }\models G\alpha \left[ t_0,m\right]
$ and from \textbf{(1)} we have that $\frak{M}_{\left( \mathcal{T},\mathcal{F%
}\right) }\nvDash F\alpha \left[ t_0,m\right]$. Hence we have that $\frak{M%
}_{\left( \mathcal{T},\mathcal{F}\right) }\nvDash \left( G\alpha \rightarrow
F\alpha \right) \left[ t_0,m\right]$. Thus it is in contradiction with the
assumption.$\Box $

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

$\left( F\alpha \wedge F\beta \right) \rightarrow \left[ F\left( \alpha
\wedge \beta \right) \vee F\left( F\alpha \wedge \beta \right) \vee F\left(
\alpha \wedge F\beta \right) \right] $ \textit{(linear future)}

$\left( P\alpha \wedge P\beta \right) \rightarrow \left[ P\left( \alpha
\wedge \beta \right) \vee P\left( P\alpha \wedge \beta \right) \vee P\left(
\alpha \wedge P\beta \right) \right] $ \textit{(linear past)}

to the axioms of $T_m.$


\mpu
\mpu

\r References\\

\def\\#1. #2\par{\item{[#1]}#2\par\smallskip}


\\1. Burges J. P, \textit{Logic and Time}, ``The Journal of Symbolic
Logic'', vol.~44, Nr~4

\\2. Dumnet M., {\it Elements of intuitionism}, Clarendon
Press, Oxford, 1977

\\3. Goldblatt R., {\it Logic of time and Computation}, Moscow,
1992

\\4. Kotarbi\'nski T., {\it The problem of the existence of the
future}, ``The Polish review'', vol.~13, 1968

\\5. {\L}ukasiewicz J., {\it On determinism}, ``The Polish Review'',
vol.~13, 1968

\\6. McArtur R. P., {\it Tense Logic}, Dordrecht, 1976

\\7. Prior A. N., {\it Past, Present and Future}, Clarendon
Press, Oxford, 1967

\\8. Trz\c{e}sicki K., {\it Intuitionism and Indeterminism,
Wole\'nski J.~Philo\-sophi\-cal Logic in Poland},
Kluwer Academic Publisher, 1994

\\9. Yourgran P., {\it On the logic of indeterminist time},
``The Journal of Philosophy'', vol.~82, 1985