Changun Department of Energy

ihnz

So, definitely from last time, specifically we were

trying to establish

the credibility of the weekpoints.

We are proceeding by induction over proofs.

And we have discharged, I believe,

one of the rules, which was the axiom rule.

And maybe one additional one, but the one of the negation

rules, I think.

So, anybody giving this a thought?

You will have noticed that there's an exercise like this on the new sheet, so I'm insisting so much.

I've got the feeling that the gentleman in front of me...

This time we'll just have one person doing the writing and the thinking at the same time.

We already discussed and tried and laughed.

So, I'm going to continue with...

We have both of them.

Okay, both of them and the axiom rule.

Okay, then we'll just do the negation rule.

So, I'll continue with the main axiom.

So, we have all the last step words, lying, negation, left, right, so we have come up, crying, come up, not dying, but...

So, we know that this is the right rule.

So, an induction hypothesis, that came up on V, we have come up with the right rule.

And by trying the negation left rule, we can now say that...

That has to be right rule.

So, we have negation right rule.

So, we have...

This time we have not die on the other side.

Over here.

Before we have...

We can again, this is the right rule.

And using our induction rule hypothesis, we can again say that gamma, chi, gamma phi, the data prime is the right rule.

We can again use the right rule to visualize gamma, chi, phi, the data prime.

Right.

Is everybody happy with this, in particular with the whole start of proof?

So, that's the principle that we have in induction hypothesis.

So, what was the beginning of the induction?

Right. So, I mean that the principle behind all this is that we regard proofs as a data structure and we do structural induction over this data structure.

So, here we, I mean, basically we regard a new rule in the proof tree, such as this one, as being composed of a rule application like this to another proof tree or in the case of the right rule to two other proof trees.

And basically the induction principle is assuming that the proof trees right above our roots satisfy our elective plane, in this case, the admissibility of a weakening rule, show that the root itself also satisfies our plane.

Slightly more naively, we just do induction over proof length, right. So, this thing here has a properly shorter proof than this because it appears in the proof of this.

So, we can, the induction hypothesis saying for anything that has a shorter proof than our current goal, we can apply the induction hypothesis.

All right. And the principle, of course, that you're asked to use in the proof of admissibility of the contraction rule, which is on the sheet, is exactly the same, right.

So, everything, I mean, you can almost copy it now, right. So, I mean, the structure of the proof is entirely the same.

Right. So, let's summarize the sheet again. So, there's, I believe, one exercise in the beginning where you're asked to just prove some sequence in the system, of course, not semantically, but by providing a sequence style proof in using the rules that we've given.

Then secondly, there's an exercise where you're asked to show that a proof search fails and you're asked to do it in a special way because there's an additional question asking you what are the refuting evaluations that you get out of the failed proof search.

And we want all refuting evaluations that there are. There aren't so terribly many. I mean, to be quite precise, there are two. And we want to get them out of the proof search.

That means we basically be as brute force as possible in the proof search. So, even if you already know that the proof search fails because you have pursued one branch arriving to something that you must prove but that isn't provable,

and thereby, of course, obtaining a refuting evaluation, you're nevertheless asked to do all the remaining branches in the proof tree because you need to find the other valuation.

Okay, then there's one thing about derivable rules. We haven't done an example of a derivable rule because what derivable rules are, well, we could do a derivable rule, so let's do one derivable rule just to be on the safe side here.