Modal logics were created so we can express ideas like the following
without having to use quantifiers and variables:
 For all time, at some time, never, ...
 For all future time, at some time in the past...
 X wants ... to be true.
 At all places....
 In all possible worlds...
 In some worlds...
 It is impossible...
 In all subsystems....
 As long as other subsystems don't do X this system will do Y.
These ideas are called modes.
There are a large number of logics that attempt to model them.
They date back to
Aristotle (of course). These early thinkers rapidly realized that
the meaning of "at some time, the sky will fall" depends on
whether the future is predetermined or full of possibilities.
The different models of time and different modes
of expression came under intense formal study
in the twentieth century for three reasons: (1) to find a
logic where "if _ then _" behaved more intuitively, (2) because
the modal system were there, and (3) because they looked as if they
might be useful in thinking about complex computerized systems.
My interest is in computerized systems so these notes have some examples
of modal logics designed to talk about their behavior.
When computerizing complex high risk situations we need to be very
clear about what we are asking for. If we want the system to exhibit some
property in every possible state, and for all time, then
we don't want it merely, at all time, to have the option of
fulfilling the property sometimes. English is not very good at expressing
such distinctions. Studying modal logics uncovers the halfadozen
different ways we may want a piece of software to have a property.
Some modal logics make it easy to calculate whether the logical behavior
of a piece of software (a model) satisfies its requirements.
Notice that it is useful to be able to reason about time varying
properties of complex computerized systems. Indeed checking that
software fits such properties has uncovered some difficult
to find bugs in real software. However the normal notation
is somewhat clumsy and so there has been research on graphic
notations ( GIL:
[ citation.cfm?id=192218.192226&coll=portal&dl=ACM&idx=J790&part=transaction&WantType=transaction&title=ACM%20Transactions%20on%20Software%20Engineering%20and%20Methodology%20%28TOSEM%29&CFID=1643654&CFTOKEN=8691090 ]
and Buchi automata (
[click here if you can fill this hole]
)). A tabular form might also work well.
[click here if you can fill this hole]
Philosophers are interested in Modal Logics because they are not well understand, and
indeed have interesting problems.
The modalities based on the Propositional Calculus (see PROPOSITION below)
are not problematic. For example you can get a simple extension
that lets you talk about "all possibly computations" without having
to have any quantified variables: "for all x....".
But when quantifiers and equality are introduced as well as
modalities, some
interesting things can occur. In particular there is a loss of
referential transparency: you can no longer substitute equals for
equals. Euclid can not be trusted with hopes, wants, and beliefs.
For example in the mode of "wanting things to be true":
Hamlet may want the person behind curtains dead, but he does
not want Polonius to die, even though Polonius is the person
hiding behind the curtains.
Another bad effect of combining modes and quantifiers
is that some expressions become ambiguous
[FittingMendelsohn98]
because modes have no explicit scope or variables. The standard
MATHS notation has predicates and quantifiers and so
the standard approach to modes in the MATHS notation is to
treat them explicitly as quantifiers. This sacrifices
simplicity on the altar of accuracy. Thus instead of
being able to write
[]p
one must write
for all t:Time(p(t)).
This is longer but more precise. The precision is only
important if p(t) includes other variables and quantifiers.
However MATHS permits operators to operate on predicates
like p above as well as on Boolean propositions so we could
define
For P:Time>@, always(P) ::= for all t:Time(P(t)).
and get the appearance of a modal logic within the MATHS system.
I will demonstrate this below  see SIMPLE_TEMPORAL_LOGIC for details.
Michael Jackson's recent work has another approach for mapping temporal modes
into the lower predicate calculus.
This seems to be the approach taken to modeling time in the
SUMO ontology:
[ logic_8_Natural_Language.html#SUMO ]
[ Browse.jsp?kb=SUMO&term=time ]
This approach has been taken further by introducing a token
that identifies events which links them to Places and Times, see
[ Eventtoken reification for spatialtemporal modes ]
below
The traditional presentation of a logic is to:
 Describe the syntax of the well formed formula.
 Describe the axioms and derivation rules.
 Present a semantic model using formal mathematics
Garson, James, "Modal Logic", The Stanford Encyclopedia of Philosophy
(Winter 2001 Edition), Edward N. Zalta?(ed.), URL =
<http://plato.stanford.edu/archives/win2001/entries/logicmodal/>
[ http://plato.stanford.edu/entries/logicmodal/ ]
(philosophical but thorough).
Animations of several logics with instructions in Dutch:
[ http://plato.stanford.edu/entries/logicmodal/ ]
(Easier to figure out than you might think...)
The Wikipedia
[ Modal_logic ]
is pretty reliable on Modal logic.
Any more?
[click here if you can fill this hole]
The following are just to illustrate how I would approach
constructing modalities within my MATHS system.
They are not in the standard MATHS rules, but you can include them in your work by using
.See http://csci.csusb.edu/dick/maths/logic_9_Modalities.html#SIMPLE_TEMPORAL_LOGIC
for example
The MATHS approach is:
 Define a syntax and semantics using MATHS.
 Derive useful and interesting properties and rules.
The following are some samples of modal propositional logics.
 SIMPLE_TEMPORAL_LOGIC::=following,
Net
We start with presuming that there is such a thing as Time. Ot to be precise
that there is a set of times we can call "Time".
 Time::Sets=given.
We assume time is an ordered:
 POSET(Time, strict=>before, inverse=>after).
Note. Sun Feb 27 10:47:13 PST 2011.
I have just changed the above assertion so that after is no longer the strict_inverse
of before. This means that for all Time t is t after t. Also for no Time t is t before t.
 (1)t after t.
We are interested in expressions that map Time into true and false values:
 P::=@^Time.
The propositions P are statements that are true or false at particular times:
`The sun is shining`
`It is raining`.
If we supply a time then we assume that we can be sure that a proposition
is either true or false at that time. So, suppose
Net
 p:=it is raining,
and
 today:Time,
then
 p(today) = today it is raining.
(End of Net)
Note.
The above presumes that we can be definite about the state of our
propositions at any given time. Other temporal logics do not
make this assumption.
We can define Boolean operations on such propositions:
 not:: P>P = map[p:P}(map[t:Time](not p(t)).
not p is true at any time p is false and vice versa.
 and:: infix(P,P,P) = map[p,q:P](map[t:Time](p(t) and q(t) ),
p and q at time t iff p is true at t and q is true at t.
 or:: infix(P,P,P) = map[p,q:P](map[t:Time](p(t) or q(t) ),
p or q at time t iff either p is true at t or q is true at t.
 For p,q, if p then q::= ((not p) or q ),
At time t ((if p then q is true) iff ( q is true or p is false) ).
At time t (if p then q is true) iff at time t( q is true or p is false).
So, for example
not(`It is raining` and `The sun is shining`).
Then add the modal operator everafter:
 everafter:: P>P= for all Time t where t after (_) ( p(t) ),
that indicates that the proposition is always true, now and for ever after.
For example
everafter `sun shines in San Bernardino`.
Define sometime as a modal operator:
 sometime:: P>P= for some Time t where t after (_) ( p(t) ),
indicating that at some time now or later the proposition is true.
For example
sometime `it rains in Manchester`.
We can rapidly show:
 (sometime, everafter, not) (T1): sometime = not everafter (not).
 (everafter, sometime) (T2): For p:@^Time, if everafter(p) then sometime(p).
 (everafter, sometime) (T3): If p=Time+>true then everafter p and sometime p.
Notice this intuitive interpretation of the combined modality:
 everafter sometime =(_) is true infinitely often,
eternal recurrence.
Also notice we have a special modal implication:
 p being true everafter leads to q being true later.
This behaves in like the normal if_then_ in PC or LPC.
It is defined like this:
 For p,q:P, p~~>q::P = everafter( if p then sometime q),
at any time, if p is true then at some time after that q will be true.
So, for example, if p is true now and p~~>q, then, sometime (soon?) q will be true.
(End of Net
SIMPLE_TEMPORAL_LOGIC)
The SIMPLE_TEMPORAL_LOGIC makes few assumptions about the structure of time.
Here I introduce the assumption that time is a sequence of discrete instants, one, after another,
and with every instant just before the next one.
Each time would be followed by another time. Hence we can talk about a
property being true in the next instant as well as for all time or at some
future time.
 SIMPLE_DISCRETE_TEMPORAL_LOGIC::=following,
Net
We start by importing all the formulas, assumptions, and theorems
of the simple logic. Then we add assumptions that restrict time
to being discrete.
  (STL): SIMPLE_TEMPORAL_LOGIC.
(Includes the previous logic here).
 next:: TimeTime, maps one Time into a unique next Time, and each
Time t1 has a single previous Time t2 such that t1 = next t2.
  (discrete): for all t1,t2:Time, t1 after t2 iff t1 = next^(0..*) t2.
 (1) (STL0): next(t) after t.
I could use the 'prime' notation:
 For all Time t, t' ::= next(t).
For example to talk about the weather:
tomorrow = today'.
We introduce a modal operator next_time that maps a temporal property one
instance into the future:
 For p:P, next_time(p)::= map[t](p(next (t))).
 (next_time)next_time = map[p] (p o next).
We can then show properties like
 (above) (nn): not next_time = next_time not.
 (above) (sn): sometime next_time = next_time sometime.
 (above) (an): everafter next_time = next_time everafter.
 (above) (ns): if next_time p then sometime p.
 (above) (en): if ever_after p then next_time p.
 (above) (nand): next_time(p and q) = (next_time p) and (next_time q).
To take this further we would add a special Time 0, with the properties
 For all t, t after 0,
and
 For no t, t before 0.
So that
 sometime p = p(0) or sometime next_time p,
 everafter p = p(0) and everafter next_time p.
(End of Net
SIMPLE_DISCRETE_TEMPORAL_LOGIC)
. . . . . . . . . ( end of section Simple Temporal Logics) <<Contents  End>>
Linear temporal logic(
LTL
) is a popular language for verifying properties of
complex safetycritical systems. It can be used as part of the SPIN tool
to describe requirements. A language called Promela is used to describe how
the system evolves. SPIN verifies that the Promela model of the system
satisfies the requirement.
LTL expressions express constraints or properties of infinite sequences called paths. An expression applies to a set sequences if and only if it applies to the whole sequence.
TableName  Symbols  Example  Meaning  Pattern


property  p,q,r  p  true at start of sequence  p,?,?,?,...

and, or, not  /\,\/,  p/\q  PC  

always  G,[]  []p  For all future time p  p,p,p,p,p,p...

sometime  F, <>  <>p  At some future time p  p,p,p,p,p,...

next  X, ()  ()p  In the next instant p  ?,p,...

until  U  (p U q)  q becomes true and before then p is always true.  p,p,p,p,q,...

Options

weak until  W  (p W q)  p is always true or at least until q is true.

release  R  (p R q)  = not(not p U not q)

(Close Table)
See
[ Linear_temporal_logic ]
on the Wikipedia
[HavelunddLowryPenix01]
. . . . . . . . . ( end of section Linear Temporal Logic) <<Contents  End>>
This is a popular logic for proving properties of nondeterministic
concurrent programs and circuits. It assumes time is discrete: each state
is followed by anther state at the next interval of time. It does not
assume that each state is followed by a only one state. Thus, suppose
that the current state can be followed by states a, b, and c and that
p is true in all of these states, but q is true in only state b then
we can assert that AX p(all next) and EX q(exists next). We can not
assert AX q since q is not true in All neXt states. Here is
an informal picture of the semantics of CTL, followed by a more
formal presentation.
Here is a graphic summary: Black nodes are where p is true, white nodes where it is false and
grey nodes where we don't care.
 CTL::=following,
Net
Source
[HuthRyan00]
 w::=wff, from PC.
Add the following operators.
 AX::w>w=all next.
 EX::w>w=some next.
 AG::w>w=all possibilities forever, on all paths....
 EG::w>w=some possibility forever, there is an infinite path....
 AF::w>w=all possibilities sometime, what ever path there comes a time when....
 EF::w>w='some possibility sometime, it is possible that it beomes true on some path sometime...
 AU::w><w>w=always until,  AU(p,q) requires q to be true at some time and p true at all previous times.
 AW::w><w>w=weak always until,  does not require q to be true, but if it is (at some future time) then p must be true up until that time, and if q is never true, then p must
be true for ever.
(Thanks to Alejandro Hernandez who sent me note1 below)
 EU::w><w>w=sometime until.
The semantics is in terms of a model M and a state s
of that model.
The Model M has states, a next relationship, and
a labeling relation that maps states into sets
of propositions. This is used to define satisfaction:
that in the model, starting at the state, the formula is
true.
 MODEL::=
Net{
 States::@Sets.
 next::@(States, States).
  (nodeadstate): for all s:States( next(x)<>{} ).
 Wff::Propositions.
 label::States>Wff.
 For s:States, Paths(s)::@#States={p:# States. p[1]=s and for all (s,s'):p (s next s')}.
 satisfies::States><wff>>@.
 satisfies(someState, someFormula) ∈ {false, true}.
satisfices::wff>@States = map[p]{s:States. satisfies(s,p)}.
 satisfices(someFormula) = for each wff p, the set of states s where s satisfies p
 satisfies(s, p) iff p in label(s).
 satisfies(s, not p) iff p not in label(s).
 satisfies(s, p and q) iff (p in label(s) and q in label(s)).
 satisfies(s, p or q) iff (p in label(s) or q in label(s)).
 satisfies(s, AX(p)) iff for all s':next(s)(satisfies(s',p)).
 satisfies(s, EX(p)) iff for some s':next(s)(satisfies(s',p)).
 satisfies(s, AG(p)) iff for all P:Paths(s)(P ==> satisfices(p)).
 satisfies(s, AF(p)) iff for all P:Paths(s)(P and satisfies(p)).
 satisfies(s, EG(p)) iff for some P:Paths(s)(P ==> satisfices(p)).
 satisfies(s, EF(p)) iff for some P:Paths(s)(P and satisfies(p)).
 satisfies(s, AU(p,q)) iff for all P:Paths(s), some i:1..#P1(satisfies(P[i+1], q) and P[1..i] ==> satisfices(p)).
 satisfies(s, EU(p,q)) iff for some P:Paths(s), some i:1..#P1(satisfies(P[i+1], q) and P[1..i] ==> satisfices(p)).
 AW(p, q)::=not EU( not q, (not p and not q)).
}=::
MODEL.
TableMATHS  Text


and


or


not


AU(p,q)  A[p U q]

EU(p,q)  E[p U q]

AW(p,q)  A[p W q]

(Close Table)
Note. The GIFs of the logic symbols above were downloaded from
Michael Huths excellent web site at
[ http://www.cis.ksu.edu/~huth/lics/ ]
for the "Logic in Computer Science" text book authored with
Mark Ryan.
The Simple Model Verifier (SMV) has a different notation:
TableMATHS  SMV


and  &

or  

not  !

AU(p,q)  A[p U q]

EU(p,q)  E[p U q]

(Close Table)
Certain interesting and/or useful properties follow
from the MODEL.
As a rule the future includes the present:
 if p then EF(p).
 if p then EG(p).
Universality implies existence
 if AG(p) then EG(p).
 if AF(p) then EF(p).
 if EG(p) then EF(p).
 ...
Until X implies X at some time:
 AU(p,q) = AW(p, q) and AF(q).
  (dm1): not o AF = EG o not.
  (dm2): not o EF = AG o not.
  (dm3): not o AG = EF o not.
  (dm4): not o EG = AF o not.
  (dmx): not o EX = AX o not.
  (auaf): AF = AU( true, (_) ).
  (euef): AF = EU( false, (_) ).
The following look like recursive or inductive definitions:
  (agx): AG = (_) and AX AG(_)).
  (egx): EG = (_) and EX EG(_)).
  (afx): AF = (_) or AX AF(_)).
  (efx): EF = (_) or EX EF(_)).
  (eux): EU = (2nd) or ((1st) and EX EU( (1st), (2nd) )) ).
 EU(p,q)= q or ( p and EX EU(p,q).
  (aux): AU = (2nd) or ((1st) and AX AU( (1st), (2nd) )) ).
TBD
(End of Net
CTL)
Similar second order predicates are defined in
[ logic_41_HomogenRelations.html#Paths and Trajectories ]
and
[ maths/math_71_Auto...Systems.html#Discrete_Dynamic_System ]
o this site.
Any suggestions?
[click here CTL in Practice if you can fill this hole]
 CTL_PATTERNS::= See http://www.cis.ksu.edu/santos/specpatterns/ctl.html.
. . . . . . . . . ( end of section Computational Tree logic) <<Contents  End>>
The following comes from a paper that summarizes the conclusions
of 20 years research into a modal logic for talking about
stepbystep computations
[ LichtensteinPnueli00 ]
that describes the PTL and proves lots of results both within
PTL and about PTL.
 PTL::=Propositional_Temporal_Logic.
 Propositional_Temporal_Logic::=following,
Net
 wff::Syntax, well formed formula of the PTL.
 PROPOSITIONS(simple_proposition=>wff).
 next::wff>wff.
 prev0::wff>wff.
 until::infix(wff).
 since::infix(wff).
 prev::= not prev0 not.
 eventually::= true until (_).
 once::= true since (_).
 henceforth::= not eventually not.
 sofar::= not once not.
 p waitingfor q::=(henceforth p) or (p until q).
 p backto q::=(sofar p) or (p since q).
 p entails q::=henceforth(if p then q).
 p equiv q::=henceforth( p iff q).
  (F0): if henceforth p then p.
  (F1): next not p equiv not next p.
  (F2): next(if p then q)entails(if next p then next q).
  (F3): henceforth(if p then q)entails(if henceforth p then henceforth q).
  (F4): if henceforth p then henceforth next p.
  (F5): if p entails next p then p entails henceforth p.
  (F6): p until q equiv (q or (p and next (p until q))).
  (F7): p until q entails eventually q.
  (P1): prev p entails prev0 p.
  (P2): prev0(if p then q )entails if prev0 p then prev0 q.
  (P3): if henceforth p then henceforth prev0 p.
  (P4): (p since q)equiv(q or(p and prev(p since q)) ).
  (P5): prev0 false.
  (M8): p entails next prev0 p.
all tautologies and inference rules in PROPOSITIONS are inherited along with modus ponens.
The original paper
[ LichtensteinPnueli00 ]
proves many theorems that hold in this logic.
[click here if you can fill this hole]
(End of Net
Propositional_Temporal_Logic)
 PTL_MODEL::= following,
Net
 S::Sets.
 interpretation::=propositions>@S, the set of states in which (_) is true.
 computation::=Nat0 > S.
 model::=computation><interpretation.
 triple::=computation><interpretation><Nat0.
 satisfies::@(triple,wff).
 ( (s,I,j) satisfies true) and not ( (s,I,j) satisfies false).
 for P:proposition( (s,I,j) satisfies P iff s[] in I(P)).
 ...
 ( (s,I,j) satisfies p until q) iff for some k:j.. ((s,I,k) satisfies q and for all i:j..k1 ((s,I,i) satisfies p)).
 ( (s,I,j) satisfies next p) iff (s,I,j+1) satisfies p).
 ( (s,I,j) satisfies prev0 p) iff j=0 or j>0 and (s,I,j1) satisfies p).
 ( (s,I,j) satisfies p since q) iff for some k:0..j ((s,I,k) satisfies q and for all i:k+1..j ((s,I,i) satisfies p)).
(End of Net
PTL_MODEL)
can show that PTL is sound and complete for PTL_MODEL.
. . . . . . . . . ( end of section Propositional Temporal Logic) <<Contents  End>>
 INTERVAL_LOGIC::=
Net{
Source: Hansen Ravn and Rischel 91
[HansenRavnRischel91].
Boolean expressions (predicates) are interpreted as describing the set of times when the formula are true. Hence interval functions and durations.
 Note: (a..b) = open interval ={x. a<x<b},
 a..b=closed interval={x. a<=x<=b},
 [a..b)=half open interval={x. a<=x<b},
 (a..b]=half open interval={x. a<x<=b},
 Times::= Real.
Interval functions
 intervals::=Times)>@.
duration(p)(b..e) ::=measure{x:b..ep}, or equiv integral(x,b,e,if(p,1,0)).
length(b..e)=be=duration(x in b..e)
 duration_predicate(p)::=\ceiling(p) ::=
 map[i](duration(p)(i)=length(i)>0)
 A;B::=map[i]for some m:i(true./A==>b..m and true./B==>m..e)
 eventually(A)::=map[i](true;A;true),
 always(A)::=not o eventually(A) o not.
...
[click here if you can fill this hole]
}=::
INTERVAL_LOGIC.
. . . . . . . . . ( end of section Interval Logic) <<Contents  End>>
Trio is a modal logic that has been used to reason about complex time dependent properties of computerized system. It has a large number of modes corresponding to tenses. All derived form one simple one by using quantification over time.
[GargantiniMorzenti01]
[Federetal94a]
 TRIO::=following
Net
 Time::@Real. Normally would be the Real numbers. Note: (a..b) = open interval ={x. a<x<b}, a..b=closed interval={x. a<=x<=b), [a,b), ...
[ Intervals in math_42_Numbers ]
 GROUP(Time, +, , 0). Implicitly assumes times are closed under addition.
 TDP::= Time>@,Time dependent predicate.
 For d:Time, F:TDP, Dist(F,d):: TBP= map[t]F(t+d).
 Dist(F,d) is true at time t if and only if F is true at time t+d.
 () (d1): for G:=Dist(F,d), all t, G(t)=F(t+d).
 (above) (d2): Dist(F,d) = F((_) + d) = F o (_+d) = (_+d); F.
 Futr(F,d)::= d>=0 and Dist(F,d).
 Past(F,d)::= d>=0 and Dist(F,  d).
 Lasts(F,d)::= for all d':(0..d) (Futr(F,d)).
 Lasted(F,d)::= for all d':(0..d) (Past(F,d)).
 Alw(F)::= for all d(Dist(F,d)).
 AlwF(F)::= for all d, d>0(Dist(F,d)).
 AlwP(F)::= for all d, d>0(Dist(F, d)).
 () (a1): AlwF(F) = for all d, d>0(Futr(F,d)).
 Until(F,G)::= for some t>0( Futr(G,t) and Lasts(F, t) ).
 Som(F)::= for some d (Dist(F,d)).
 SomP(F)::= for some d, d<0(Dist(F, d)).
 UpToNow(F)::=for some d, d>0(Lasted(F,d)).
 NowOn(F)::=for some d, d>0(Lasts(F,d)).
 Becomes(F)::= UpToNow(not F) and (F or NowOn(F)), slightly different to Federeretal?
 LastTime(F,t)::=Past(F,t) and Lasted(not F, t).
 NextTime(F,t)::= Futr(F,t) and Lasts(not F, t).
 Can define closed and half closed versions of all the above!
GargantiMorzenti also define some special types of predicates.
 Events are point based: they are true at a time but not before or after:
 Event::={F. Alw( if F then UpToNow(not F) and NowOn( not F))}.
 Interval_based_predicate::= {F. Alw(if F then (UpToNow(F) or NowOn(F)) else UpToNow(not F) or NowOn(not F)))}.
 Note: if p then q else r = (if p then q) and (if not p then r).
 Left_Continuous_Interval_Based_Predicate::={F. Alw((if F then UpToNow(F)else ` UpToNow(not F)))}.
 Right_Continuous_Interval_Based_Predicate::={F. Alw((if F then NoOn(F) else UpToOn(not F)))}.
Some TDP are more likely to exist in real systems, and about which properties are easier to prove.
For example a predicate Z defined by Past(Z, t) iff for some n:1..(t=1/n) describes an event defined to occur at an infinite number of times 1, 1/2, 1/3, ... in the near past. NonZeno predicates are
 nonZeno(F)::@ TDP = Alw( (UpToNow(not F) or UpToNow(F)) and (NowOn(not F) or NowOn(F) ).
Note the idea of a nonZeno predicate allows events to occur infinitely close to each other but excludes events that happen an infinite number of times.
Question: What about switch bounces?
 Many results are claimed to be proved in GargantiMorzenti01.
 They go on to define time dependent variables and other ideas useful for analyzing requirements.
(End of Net
TRIO)
Kripke semantics provides a uniform way to interpret
the formulas of modal logics. In normal logic we have a single
domain of discourse. To model modes we envisage a collection
of worlds, each with its own logic. These worlds are connected and one knows
about the connected ones but not the others. One mode is in all connected words
and the other is modeled by in some connected world. By
assuming various properties of the connection relationship
we can create a model of any wellknown modal logic.
[click here Kripke Semantics if you can fill this hole]
. . . . . . . . . ( end of section Kripke Semantics) <<Contents  End>>
(note1):
Hello, my name is Alejandro Hernandez, I am a research assistant at DTU,
Denmark. I have found an omission in your site about Modal Logic
, in the CTL
section. In the informal explanation of the Always Weak Until operator
(AW) you
say "does not require q to be true, but if it is (at some future time) then
p must be true up until that time", but there it is not clear the "if not"
part, which it is that p should be true always (because q never will be). I
spent a while trying to understand that (and realizing that the formal
definition in terms of the the negation of the Sometimes Until did not fit
the informal explanation), until I found another site where it is more
clear. I just wanted to tell you so if you fix it then the next person will
not spend the time I did. Sorry, and thank you very much for all that I
have learned reading your site!
 TBD::="To Be Done".
 PROPOSITIONS::= See http://www.csci.csusb.edu/dick/maths/logic_10_PC_LPC.html#PROPOSITIONS.
 POSET::= See http://www.csci.csusb.edu/dick/maths/math_21_Order.html#Posets.
 RELATIONS::= See http://cse.csusb.edu/dick/maths/logic_41_HomogenRelations.html
 GargantiMorzenti01::=following,
[GargantiMorzenti01].
 LichtensteinPnueli00::=following,
[LichtensteinPnueli00].
 Real::= See http://www.csci.csusb.edu/dick/maths/math_42_Numbers.html#Real_Numbers
 Search::= See http://auto.search.msn.com/results.asp?FORM=AS14&v=1&RS=CHECKED&srch=4&q=Modal+logic.
 Sources::= See http://groups.google.com/groups?q=temporal+logic&hl=en&selm=1993Jan27.140803.4254%40city.cs&rnum=1.
. . . . . . . . . ( end of section Modal Logic) <<Contents  End>>
Special characters are defined in
[ intro_characters.html ]
that also outlines the syntax of expressions and a document.
Proofs follow a natural deduction style that start with
assumptions ("Let") and continue to a consequence ("Close Let")
and then discard the assumptions and deduce a conclusion. Look
here
[ Block Structure in logic_25_Proofs ]
for more on the structure and rules.
The notation also allows you to create a new network of variables
and constraints. A "Net" has a number of variables (including none) and
a number of properties (including none) that connect variables.
You can give them a name and then reuse them. The schema, formal system,
or an elementary piece of documentation starts with "Net" and finishes "End of Net".
For more, see
[ notn_13_Docn_Syntax.html ]
for these ways of defining and reusing pieces of logic and algebra
in your documents. A quick example: a circle
might be described by
Net{radius:Positive Real, center:Point, area:=π*radius^2, ...}.
For a complete listing of pages in this part of my site by topic see
[ home.html ]
The notation used here is a formal language with syntax
and a semantics described using traditional formal logic
[ logic_0_Intro.html ]
plus sets, functions, relations, and other mathematical extensions.
For a more rigorous description of the standard notations
see
 STANDARD::= See http://www.csci.csusb.edu/dick/maths/math_11_STANDARD.html
 above::reason="I'm too lazy to work out which of the above statements I need here", often the last 3 or 4 statements.
The previous and previous but one statments are shown as (1) and (2).
 given::reason="I've been told that...", used to describe a problem.
 given::variable="I'll be given a value or object like this...", used to describe a problem.
 goal::theorem="The result I'm trying to prove right now".
 goal::variable="The value or object I'm trying to find or construct".
 let::reason="For the sake of argument let...", introduces a temporary hypothesis that survives until the end of the surrounding "Let...Close.Let" block or Case.
 hyp::reason="I assumed this in my last Let/Case/Po/...".
 QED::conclusion="Quite Easily Done" or "Quod Erat Demonstrandum", indicates that you have proved what you wanted to prove.
 QEF::conclusion="Quite Easily Faked",  indicate that you have proved that the object you constructed fitted the goal you were given.
 RAA::conclusion="Reducto Ad Absurdum". This allows you to discard the last
assumption (let) that you introduced.