Leibniz' Law of Identity

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 )

Temporal Logic "D" (or "DX")

That makes sense to me -- but hold that thought, and go read this lightning talk I gave on Temporal Logic:

    http://www.yak.net/d/

(Actually let's call that DX: D with the neXt (tomorrow) operator.)

Modal Logics

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   with ◻ for F:     ∀x. ∀y. (x = y) --> (◻(x) = ◻(y))   False   with ⚪ for F:     ∀x. ∀y. (x = y) --> (⚪(x) = ⚪(y))   False

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.)

Dualities:

Duality of ◻ and ◇:

    ◻a ≡ ¬◇¬a

    ◇a ≡ ¬◻¬a

In DX, you can define ◻ and ◇ recursively using Tomorrow ⚪:

    ◻a ≡ a ∧ ⚪(◻a)

    ◇a ≡ a ∨ ⚪(◇a)

Axioms

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

Prior & Bull's D

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)

Extending Temporal Logic D or DX:

Past operators as well as Future operators ( past◻ = it always was the case; past◇ = it once was the case )

Reals instead of Integers: Intervals of time on the number line of reals

Since and Until operators

Combine with other modal logics

Partially ordered Time (instead of totally ordered), which leads to

Branching Time: a favorite: the past is fixed, one future is "current" (our temporal ◻ and ◇ refer to it), but other futures are possible.

Mixed Space and Time (Minkowski spacetime)

Time Travel (Back to the Future)

Polish Notation

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).

Example:

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

For Education

I've tried teaching DX to a few kids, and they get it pretty quickly.

You don't need to understand to understand numbers, geometry, etc.

But I forgot to explain to my niece that OR can mean BOTH, so she missed a puzzle.

Kids can explain their informal (intuitive) "proofs" why certain expressions are equivalent.

For Hacking

Computer Science (Temporal & Modal Logic is often taught in CS Grad School these days. Search YouTube for Temporal or Modal Logic for many lessons in Computer Science)

Distributed Systems (Very important to reason about time, what guarantees hold eventually or forevermore.)

e.g. Gerard Holzmann used temporal logic in his protocol model checker "spin" [says Tom Duff].

Artificial Intelligence (to reason about what is possible or necessary, what is permitted or forbidden, what might be or will be)

(But John McCarthy concluded: For really doing AI, Modal Logic is not enough.)

Degrees of Separation

Temporal Logic was invented by Arthur Prior (based on Modal Logic)

whose student who studied D was Robert A Bull

whose advisor for his second thesis was Michael Dummett

who won the prize in Philosophy of Science named for Imre Lakatos

who had famous arguments about Philosophy of Science with Paul Feyerabend

which was the name of a band lead by David Dault

who made all the YAK.NET t-shirts for The Yak which is led by Henry Strickland

who just taught Modal Logic to YOU

^Z