1 of 6 (contd.)

0:00 Good algebra, I learned. My brother is a mathematician. That's how we do it. Every time, he starts with a good one. When there's a good one, there's a good one. So yes, what does an induction do? It shows me everything from A to zero. And it gives me a way to go from high break to high break. So, to go through all the elements. And we say, I demonstrated for everyone, because I gave a method to go through them all. But be careful, it's not like that that everyone will go through all the theorems. In general, we have a prototype proof, like. And that's, I think, what's good, because you know, even in induction, what do you do about that? Well, yes, there will be the nested induction, the induction of the effect. The nested induction for which induction is used. There is no end to the fault, you have to stop it. At some point, there will be a prototype proof with a transgeneric proof. So, the geometric sense of proof. And another remark that I would like to make is that proof is a geometric structure. It is a fundamental institution that I will be able to do to introduce a range of approaches. But otherwise, I could start with some elements. Maybe I'll just put the bottom, let's say, so as not to start over with elementary logic. What are we going to do? In the second part of what I'm going to tell you next time, we're going to short-circuit Goethe's Theorem. And as I said, we took a basic logic, then there's this, then there's this. And in these traditional logic systems, we demonstrate the following thing.

2:30 As a starting point. And also, we are going to prosecute Gödel, and instead of saying, by a work of causation, it is not possible, we write directly the proofs as terms in the functional system. And this is called the language of rapidity. That is to say, I am going to associate to each proof a term. I say, if I take a hypothetical proof x, b, a, well, of course, it is a proof x, b, a. If I have a proof of theta with an a, and b a proof of a with an a, if I have a proof of a with an a with an a with an a, then b a gives me b. And then, here, I write directly in the language. If x is also a proof of a, and this gives me a proof of b, then I have a proof of this arrow. How do I do it? I don't know. It would be impossible to put them here, but I don't know. Landers B equals A plus B. So we put, from the beginning... This is a mixture of the 40 churches. We put, from the beginning, the quotations, which are the terms of these calculations. Then, as I told you, we put them in the language itself. So, you see, this is the same writing as the theoretical writing. This passage tells me that if I have the hypothetical metatheoric deduction of the axis of x equal to gb, I can directly give this theorem, 1 equal to b, in a gauge and I give a code for the proof. Let's try now to see an important passage. Suppose I have a that allows me to demonstrate b and here I have b that allows me to demonstrate c. This tells me that a equals c.

5:00 And so, I give names to these rules. This is the introduction arrow, this is the elimination arrow, and vice versa. Introduction arrow, elimination arrow. And here I used the introduction arrow, and here the elimination arrow. Y in B, C in C, it's going to be like that, but Y can't be like that, it can't be like that, it can't be like that, it can't be like that, it can't be like that, it can't be like that, it can't be like that, it can't be like that, it can't be like that, it can't be like that, it can't be like that, it can't be like that, it can't be like that, it can't be like that, it can't be like that, it can't be like that, it can't be like that, it can't be like that, it can't be like that, it can't be like that, it can't be like that, it can't be like that, it can't be like that, it can't be like that, it can't be like that, it can't be like that, it can't be like that, it can't be like that, it can't be like that, it can't So, the idea is to say, well, now I put as an axiom the big thing of replacement, of substitution done by Gödel, that is to say, I know that lambda C applied to B is equal to B instead of Y without C. One way or another, be careful, you will not find that the replacement will be related to the free variables in relation to lambda.

7:30 This is an axiom called the state axiom. It is therefore an axiom that only makes the master, as it may be, talk about these things, and great work of the lemma of the substitution of the state axiom. And what is the meaning in the mathematical sense? That is to say, I have a proof of Gramby and I can derive from any proof of Gramby a proof of C. So I give myself a general lemma that tells me that it is from him. I have a general lemma. This means that if I apply the general lemma that asks for a specific proof of B, it is the same thing as having a specific proof of C in which I replaced a specific proof of B in the face of the hypothesis. The detour by a general lemma is the same thing. However, if I give an orientation to this equality, it is a very simple passage. Since I wrote it, I have eliminated this B. I don't see it anymore. We have eliminated a pure cube, which is the passage that leads Pegamon to the center of the two corners. There will be no connections, but in the end there will be equations.