So today we are going to finally start talking about some properly non-classical logic, after

this long introduction on classical proposition of alphalus and the first subject, first

major system or familial systems that we are going to talk about are modern logics.

So we will not have even the opportunity to talk or even mention all of the possible applications

or places where they appear or reappear, where invented or reinvented in computer science

area, they can be appearing various aspects of theoretical computer science.

But also in other areas, for example, linguistics, even social sciences, economy, one could even

argue that in some areas of mathematics, but this wouldn't be the most amazing mathematics.

So we will only cover some of the applications here.

But before we start suggesting where one can possibly use those formalisms, maybe let's

explain briefly what is the main idea behind them.

Maybe one should also mention that they really emerged from philosophy, so this is in fact

where, just like logic in general, so this is in fact where people start first looking

at the model system, model formalisms.

So there are two possible, at least two possible stories by which one can use to introduce

the subject.

One would be semantic and another would be syntactic.

This is not very standard way of describing it, but.

So the semantic story will be that we want to have some lightweight formalism to talk

about transition structures to specify reason about transition structures.

And the syntactic story would be simply that we want to introduce some new connectives

to the supply of those basic connectives of classical propositional logic that we have

seen so far, so conjunction, implication, bottom, well negation, negation being the

implication to bottom, something which unlike in case of predicate logic does not necessarily

have fancy binding issues like quantifiers and what not, so something which still remains

on the propositional level, but it cannot be characterized anymore by just by true and

false tables, because this was the only semantic that we really needed so far.

So the syntactic story would be extending CPL with new propositional connectives.

It can be one, it can be more, which cannot be characterized just by truth and by just

ordinary truth tables.

So the simplest possible setup and the setup which we are going to spend most of our time

on is when we have just one single unary such connective and possibly some other things

that can be syntactically defined from it, like you can define, let's say, this junction

from negation and conjunction or top using negation and bottom and so on and so on.

So the simplest possible setup, basic modal logic or basic modal signature, single unary

connective box, let's call it box.

Actually you can find all sorts of notations for all sorts of similarities, but this one

is probably most common.

And just as a remark for the time being at least, there are systems where you have whole

algebra, there are systems where you have n-ary modalities and then there are systems

where you have whole algebra where modalities themselves form a separate structure where

you can form sums of modalities, possibly intersection of modalities, transitive closures

of modalities and so on and so on.

In applications, one often considers much richer

supply of modalities possibly equipped with some algebraic structure.

For example, sums, intersections are not so common, converses, transitive closures of

modalities, but this is something that is only going to concern us much later if we

get there at all.

So if we have enough time, we will try to discuss one such formalism, so called propositional

dynamic logic which is particularly natural from computer science point of view.