% A basic ingredient of tense logic is described by the following
% (ephemeral) template:
defThAs( 'Tense'( F, P, Tense ), [
defAs( @(Tense), F ),
->(['RAbs'(Q)],subseteq( Q, dagger( opp( F ), circ( P, Q ) ) )),
subseteq( setminus( circ( F, opp( R ) ), circ( F, opp( Q ) ) ),
circ( F, setminus( Q, R ) ) ) % the latter is valid
]).
% first-order translation of the conclusion of the inference rule
% and of the other (logically valid) ingtredient of the above template
% are, respectively:
% X Q _ -> (ALL y)( X F y -> (EXISTS v)(y P v -> v Q _) )
% X F Y & ~ Y R Z & (FORALL w)(X F w -> w Q Z) -> (EXISTS v)(X F v Q Z & ~ v R z)
% The above template is used twice to characterize the mutually symmetric
% properties of past and future:
% Axioms of minimal tense logic (p1=past, p2=future):
'Tense'(p2,p1,future).
% "if Q presently holds, it will henceforth be true
% that Q held in the past"
'Tense'(p1,p2,past).
% "if Q presently holds, it always held till now that Q
% would eventually be true"