|YaK:: Ramblings about Temporal Logic (Hackers 2018)||[Changes] [Calendar] [Search] [Index] [PhotoTags]|
The late Hackers Conference attendee John McCarthy teaches us Leibniz' Law of Identity:
∀x. ∀y. (x = y) --> (F(x) = F(y))
[ McCarthy 1996 ] ( http://www-formal.stanford.edu/jmc/mcchay69/node22.html )
That makes sense to me -- but hold that thought, and go read this lightning talk I gave on Temporal Logic:
(Actually let's call that DX: D with the neXt (tomorrow) operator.)
One of the reasons Modal Logics (and Temporal or Tense Logic) was difficult to get started was that it has strange operators that violate that Law of Identity.
with ◇ for F: ∀x. ∀y. (x = y) --> (◇(x) = ◇(y)) True
To me the biggest idea in Modal Logic is this:
◻R -> R -> ◇R
Generally in Modal Logic:
The ◻ implies some kind of necessity ("In all possible worlds").
The ◇ implies some kind of possibility ("In some possible world.")
(The "neXt" or "tomorrow" operator is not a part of modal logic in general.)
Duality of ◻ and ◇:
◻a ≡ ¬◇¬a ◇a ≡ ¬◻¬a
In DX, you can define ◻ and ◇ recursively using Tomorrow ⚪:
◻a ≡ a ∧ ⚪(◻a) ◇a ≡ a ∨ ⚪(◇a)
Coming up with Axioms is trickier than it seems and took years of work. There are an infinite number of systems, but some standards exist:
[S1]: Normal logic: a non-modal logic system with 6 axioms using only AND and IMPLIES.
[S2]: Add to S1: ◇(p ∧ q) -> ◇p
[S3]: Add to S1: (p -> q) -> (¬◇q -> ¬◇p)
[S4]: Add to S1: ◇◇p -> ◇p or equivalently ◻◻p -> ◻p
[S5]: Add to S1: ◇p -> ◻◇p
D is a "Diodorean" Modal Logic, that includes S4 but not S5. (Something that "will eventually be true" does not imply it will be true infinitely often.)
[S4.3] Add to S4: ◻(◻p -> ◻q) -> ◻(◻q -> ◻p)
D is S4.3. By Micheal Dummet, this also applies to D with discreet ordering of time (but not with continuous ordering):
[Dummett] ◻(◻(p -> ◻p) -> ◻p) -> (◇◻p -> ◻p)
A lot of us are familiar with Reverse Polish notation (HP calculators, FORTH, Postscript)
Arthur Prior used Polish Notation for these formulas throughout his life. I had no idea how dense it would be (cf. Unlambda).
Compare to Unlambda (Hello World): ` ``si`k``s.H``s.e``s.l``s.l``s.o``s. ``s.w``s.o``s.r``s.l``s.d``s.!``sri ``si``si``si``si``si``si``si``si`ki
(But John McCarthy concluded: For really doing AI, Modal Logic is not enough.)
|(last modified 2018-11-03) [Login]|