If you kind of tell the same story again from a little bit further away you can define things

like logical systems.

When I tell you there are certain things that are always there in a logic, that you can

write down and that's what we call a logical system, which is essentially a triple which

has a language, a class of models, something that say this is true or not, right, it has

a satisfaction relation, this is formulae, satisfied by that situation or model and that's

all you need, right, language, models, satisfaction relation, okay.

And then these things have properties and you can kind of redefine in this more general

setting, namely which covers all logics, not just propositional logic, the same words

that we've defined before.

That's kind of the formal basis we're going to use.

The thing we want to add is what we call a calculus, a set of rules which says if you

see this, you can also, if you believe this, you can also believe that.

And remember there's one interesting thing about that, this is completely independent

a priori from semantics.

You can give yourselves any kind of rules, but of course a posteriori as we've seen yesterday,

you want to give yourself a good set of rules, which is a rule that plays nice with the semantics.

But to understand what that means, plays nice with the semantics, we kind of give ourselves

arbitrary rules.

And the only things we want to have is from this, we call it a derivation relation, which

is a relation that has, that is not like the entailment relation here.

Wait, let me, like the entailment, will I ever learn?

No.

There we go.

This is the satisfaction relation, right, that has this kind of double barreled, whereas

the derivation relation, this one, is single barreled.

Here we have semantics, logical system, here we have syntax only.

And the only thing we want of this is that it be proof reflexive, meaning if I'm assuming

a then I can also prove a.

Makes sense, right?

If I'm seeing that it rains, I can derive that it rains.

If it's proof transitive, meaning I can derive a from a set of observations, think of h as

observations, and from a and another set of observations I can derive b, then from the

union of the observations I can derive b as well.

Okay, so that's kind of a progressive safety net.

You see something, you say, aha, a holds.

And you see something else and you know from that something else and a, I would be able

to conclude b, then from all the observations you have you can conclude b, it's very important.

And of course monotonic, meaning if you know more then you're not actually endangering

any conclusions.

And if we have that, we're calling that a calculus or a derivation system, and the logic

just contains these four pieces, language, models, and satisfaction relation, which is

the semantics, and the calculus.

And if we want to do the engineering, then we can write down a calculus like this in

a set of rules.

If you see everything that's above the line, you can add the stuff that's below the line.

And if anybody ever asks you why, the rule has a name, and you can say because n.

Okay, that's what a calculus is.

The nice thing about a calculus is that we have proof transitivity.

So we can actually string them together and we can get proofs.