Title:
======
Change Logic (!)
Abstract:
=========
"Change Logic" is a work in progress. By now, it has a philosophical foundation, a clear syntax
and intuitive semantics, and a powerful algebra of machines to effectively distinguish the
according model sets. A thorough survey of its design and logic is currently under way. But in
this presentation we emphasize the difference between Temporal Logic and Change Logic and the
thesis, that a natural logic of dynamic events and processes is no longer a department of modern
Modal Logic.
(A) Syntax and Semantics
========================
1. Syntax
The primitive components of change-logical formulas CFm(A) are the propositional formulas PFm(A)
on a given set A of atoms and it has the usual boolean constructions (negation, con- and dis-
junction etc.). But there are no modal operators. Instead, the one and only specific change-
logical construction is a (kind of) concatenation of formulas. This is the formal generalization
of a sequencing or tuple of propositional formulas, which reads as "f_1, then f_2,
then, ..., then f_n". Very much like "chronologies" or "logs", a succession of static events or
observations, where the order of this sequence reflects the order of the events.
2. Models
As in temporal logic, models are built upon propositional models PMod(A), i.e. functions of type
A->{0,1}. But there, a temporal model is a Kripke model, a function of type T->PMod(A), where T
is a temporal structure or "flow of time", i.e. the set T with some binary relation. Instead, and
again according to the log paradigm, change logical models CMod(A) are simply tuples
of propositional models. They are not built on a TIME structure T, they are entirely determined by
the CHANGE of the events.
3. The model relation |=
The model relation m|=f between a change model, say m= and a chronology formula
f= is defined as what we call the "corresponding sequentialization" of the
propositional model relation, which is a general operation that turns binary relations between
sets S and T into binary relations between the tuple sets S* and T*. In our case, m|=f is true,
if there is a "co(rrespondingly)-equal" mutation m' of m, i.e. a tuple equal to m, but with
arbitrary repetitions of the components, say m'=. And there must be a
co-equal version f' of f, say f'=, so that m' and f' have the same
length, namely 6, and the propositional model relation holds component-wise: m_1|=f_1, m_2|=f_1,
m_2|=f_2, m_2|=f_3, m_3|=f_3 and m_4|=f_3. We will see that this change-logical model relation is
the very natural correspondence we intuitively try to construct when we match real events to
(chronologically told) stories. As one consequence, the model class for each change formula f
is "repetition-invariant" in the sense that m|=f iff m'|=f, for each co-equal m' of m.
And that is correct indeed: repetitions don't change anything, and only changes make a difference!
(B) Automata theory
===================
As there are certain types of machines for certain kinds of formal languages, there is also a
"change automaton" for each change-logical formula. Also, for each logical constructor (negation,
conjunction, etc.) there is an according operation on change automata, all together making an
algebra of change automata. Currently (March 30, 2012), this algebra has pretty much taken shape
and a formal text is on its way to explain all this in detail, soon.
(C) Next step
=============
By taking a closer look, the algebra of change automata is not only suitable as an operational
semantics for change formulas. In fact and in turn, it induces a generalization of the syntax,
which turns the set of formulas into a Turing-complete programming language. The abstract version
of our automata in general have two basic sets: a set of "names" and a set of "values". For use
in logic, in particular, the value set is PMod(A), and the name set is the propositional model
set PMod(A'), as well. But change logical formulas are only built on top of "value forms" PFm(A)
and we can add the "name forms" PFm(A') to the syntax. (There is a certain similarity here to
"Hybrid Logic", that augments Modal Logic by extending the language with "nominals".)
Keywords:
=========
Philosophy of Time
Change Logic
Temporal Logic
Dynamic Logic