That looks better.

So statistically significantly better, but not like extremely better.

Who's seen the exercises before?

None of you?

Okay.

Okay, so you did.

Okay.

Okay.

So let that be an incentive to actually toy around with Alea maybe.

You might find some of the questions that come up in Tuesday quizzes.

Okay.

We were talking about proofs.

So let's quickly recap the basics.

So we have inference rules, where an inference rule is a decidable n plus 1 area relation

of formulae.

In the simplest case, again, we're immediately going to break that definition because we're

going to put like sequence here instead of formulae.

And once we have such inference rules, we can collect them into a calculus.

A calculus then is just a collection of inference rules.

And if we have a calculus, then we can define what a proof in that calculus is.

And the formal definition of that is it's literally just a sequence of formulae such

that every formula follows from the previous one by some inference rule.

And again, that definition we're immediately going to break because nobody wants to work

with the kinds of proofs where everything is just on the basis of formulae because they

tend to get really cumbersome.

Prime examples for that are the kinds of Hilbert-style calculus.

Great for reasoning about proofs themselves.

But otherwise, basically unusable.

We're going to use this turnstile symbol to denote that some formula is provable in Calculus

C from some set of axioms T. We call it sets of axioms theories.

The one that we're going to mostly work with because it's very paradigmatic for the kind

of calculi that are actually used in computer implementations, at least when it comes to

user interactions, is the natural deduction calculus.

In particular, the kind of natural deduction calculus where the things we derive are not

formulae and the premises are not formulae, they're a sequence.

Where a sequence is basically a pair of form, a set of formulae on the left-hand side and

an actual formula on the right-hand side.

Initially we start with whatever set of axioms we work with and use that as gamma.

And then in the process of proving, we might add formulas to that context or we might remove

formulas from the context again.

And then ultimately the goal is to find a derivation of some sequence where the left-hand

side really just consists of the set of axioms that we're actually interested in and the

right-hand side actually consists of the formula that we're interested in.

Natural deduction falls into two kind of categories.

Every rule is either usually an introduction rule for some symbol or an elimination rule

for some symbol where the introduction rules tell us how do I prove a formula with that

particular symbol as its head and an elimination rule tells us if I have a formula with that

kind of head, I have a symbol, what can I do with it?

Okay, good.

We have truth introduction, straightforward, we can always prove true.