To install click the Add extension button. That's it.

The source code for the WIKI 2 extension is being checked by specialists of the Mozilla Foundation, Google, and Apple. You could also do it yourself at any point in time.

4,5
Kelly Slayton
Congratulations on this excellent venture… what a great idea!
Alexander Grigorievskiy
I use WIKI 2 every day and almost forgot how the original Wikipedia looks like.
Live Statistics
English Articles
Improved in 24 Hours
Added in 24 Hours
Languages
Recent
Show all languages
What we do. Every page goes through several hundred of perfecting techniques; in live mode. Quite the same Wikipedia. Just better.
.
Leo
Newton
Brights
Milds

Proof calculus

From Wikipedia, the free encyclopedia

In mathematical logic, a proof calculus or a proof system is built to prove statements.

YouTube Encyclopedic

  • 1/3
    Views:
    184 329
    65 481
    44 790
  • Proof of Fundamental Theorem of Calculus
  • Product rule proof | Taking derivatives | Differential Calculus | Khan Academy
  • Proof of the Product Rule from Calculus

Transcription

Let's say that we've got some function f that is continuous, continuous on the interval a to b, so let's try to see if we can visualize that. So, this is my y axis, that's my y axis. This right over here. I want to make it my t axis. We'll, we'll use x a little bit later so I'll call this my t axis. And then let's say that this right over here is the graph of, y is equal to f of t. Y is equal to f of t. And we are saying that it is continuous on the interval from a to b. So this is, t is equal to a. This is t is equal to b. So we are saying that it is continuous. It is continuous over this whole interval. Now, for fun, let's define a function capital F of x, and I will do it in blue. Let's define capital F of x as equal to the definite integral from a. From a as a lower bound to x to x, of, f of t, of f of t, of f of t dt, where x is in this interval, where. Where a is less than or equal to x is less than or equal to b or that's just another way of saying that x is in this interval right over here. Now when you see this you might say oh, you know, the definite integral just has to do with differentiation and anti-derivatives and all that, but we don't know that yet. All we know right now. Is that this area under the curve f between a and x. So between a and let's say this right over here, this right over here is x. So f of x is just, is just. This area, this area right over here. That's all we know about it. We don't know if it has anything to do with antiderivatives just yet. That's what we're going to try to prove in this video. So, just for fun, let's take the derivative of f, and we're gonna do it just using the definition of derivatives and see what that what we get when we take the derivative using the definition of derivatives. So we would get, so the derivative, f prime of x, well, this definition of derivatives, it's a limit as delta x approaches 0 of capital F of x plus delta x minus F of x, all of that. All of that over delta x. This is just the definition of the derivative. Now, what is this equal to? Well let me rewrite it using these integrals right up here. This is going to be equal to. This is going to be equal to the limit, the limit as delta x approaches 0 of. What's f of x plus delta x? Well put x in right over here. You're gonna get the definite integral from a to x plus delta x of f of t. Dt and then from that you are going to subtract. You are going to subtract. This business, f of x, which we've already written as the integral from a, the deft integral from a to x of f of t, dt. And then all of that is over delta x. All of this is over, all of this is over delta x. Now what is this represent? Remember, we don't know anything about definite integrals is somehow dealing with something with an anti-derivative and all that. We just know this, this is another way of saying the area under the curve f between a and x plus delta x; so it's the area under the curve f, between a and x plus delta x, x plus delta x. So, it's this entire area. It's this entire area. Right over here. So that's this part. We already know what this blue stuff is. This blue stuff, in that same shade of blue. So, this blue stuff right over here. This is equal to all of this business. We've all ready shaded this in. It's equal to all of this business right over here. So if you were to take all of this green area which is from a to x plus delta x and subtract out this blue area which is exactly what we are doing in the numerator, what are you left with? Well, you're going to be left with. You're going to be left with, what color have I not used yet? Maybe I will use this pink color. Well no, I already used that. I'll use this purple color. You're going to be left with this area. You, you're going to be left with this area right over here. So what's another way of writing that? Well another way of writing this area right over here, is the definite integral between x and x plus delta x. Of f of t, of f of t, dt. So we can rewrite this entire expression. The derivative of capital F of x, this is capital F prime of x. We can rewrite it now as being equal to the limit as delta x approaches 0. This I can write as 1 over delta x. Times the numerator. The numerator, we have already figured out that the numerator, the green area minus the blue area is just the purple area. Which is an, an another way of solving is denoting that area is this expression right over here. So 1 over delta x times a definite integral from x to x plus delta x of f of t. F of t, dt. Now this expression is interesting. This might look familiar from the mean value theorem of definite integrals. The mean value theorem of definite intervals tells us, so the mean, mean value theorem of definite. Definite integrals. Definite integrals tells us, there exists, there exists a c in, in the interval, so I could, a c. Where. I'll write it this way. Where a is less than or equal to c, which is less than. Or, actually let me make it clear. The interval that we now care about is between x and x + delta x, where x. Where x is less than or equal to c, which is less than or equal to x + delta x. Such that, such that the function evaluated at c, the function evaluated at c: so let me draw that c. So there's a c some place over here. So if I were to take the function evaluated at the c. So that's f of c right over here. So if I were to take the function evaluated at c, which would essentially be the height of this line, and I multiply it times the base, this interval, if I multiply it times the interval, and this interval is just delta x. X plus delta x minus x is just delta x. So if we just multiply the height times the base. Times the base, that this is gonna be equal to the area under the curve. It's going to be equal to the area under the curve, which is the definite integral from x to x plus delta x, x to x plus delta x. F of t, f of t, dt. This is what the mean value theorem of integrals tells us. If f is a continuous function, there exists a c in this interval between our two endpoints, between our two end points where the function of value of the c is essentially, you can view it as the mean height. And if you take that mean value of the function, and you multiply it times the base. You're going to get the area of the curve. Or another way of rewriting this you could say that f of c, there exists a c in that interval where f of c is equal to 1 over delta x. I'm just dividing both sides by delta x. Times the definite interval from x to x plus delta x. F of t dt. And this is often viewed as the mean value of the function over the interval. Why is that? Well this part right over here, this part right over here gives you the area, and then you divide the area by the base and you get the mean height. Or another way you could say it is if you were to take the height right over here. Multiply it times the base, you get a rectangle that has the exact same area as the area under the curve. Well, this is useful, because this is exactly what we got as the derivative of f prime of x. So there must exact a c, such that, such that f of c is equal to this stuff, or we can say that the limit. And let me re-write all of this in a new color. So there exists, there exists a c in the interval x to x plus delta x. Where, where f prime of x, which we know is equal to this, we can now say is now equal to the limit. As delta x approaches 0, and instead of writing this we know there's some c that's equal to all of this business, of f of c. Now we're in the home stretch. We just have to figure out what the limit as delta x approaches 0 of f of c is, and the main realization is this part right over here. We know that c is always sandwiched in between x and x plus delta x, and intuitively you could tell that, look, as delta x approaches 0 as this delta x as this green line, as this green line right over here moves more and more to the left. As it approaches this, as it approaches this blue line, as it approaches this blue line the c has to be in between so the c is going to approach x. So we know intuitively. We know intuitively c approaches x as delta x, delta x approaches 0 or another way of saying it is f of x is going to approach f of x as delta x, as delta x approaches 0. So intuitively we can say that this is going to be equal to f of, this is going to be equal to f of x. Now you might say, okay that's intuitively, but we're kind of working on a little bit of a proof here, Sal. Tell me, let me know for sure that x is going to approach c. Don't just do this little thing where you drew this diagram and it makes sense that c is gonna have to get closer and closer to x. And if you want that then you can just resort to the squeeze theorem. And to resort to the squeeze theorem you just have to view c as a function of delta x. And it really is. Depending on your delta x, cs gonna be further to the left or to the right possibly, and so I can just rewrite this expression as x is less than or equal to c as a function of delta x. Which is less than or equal to x plus delta x. So now you see that c is always sandwich in between x and x plus delta x. But whats the limit of x as delta x approaches 0? Well x isn't dependent on delta x in anyway so this is just going to be equal to x. Whats the limit of x plus delta x, as delta x approaches 0? Well as delta 0 approaches 0 this is just going to be equal to x. So if this approaches x, as delta x approaches 0 and it's less than this function, and if this approaches x as delta approaches 0 and it's always greater than this. Then we know from the squeeze theorem or the sandwich theorem. That the limit as delta x approaches 0 of c as a function of delta x. Is going to be equal to, is going to be equal to x as well. It has to approach the same thing as that and that is. It is sandwiched in between. And so that's the slight we we resort to the sandwich theorem. It is a little more rigorous. To get to this exact result. As delta x approaches 0 c approaches x. If c is approaching x then f of c is going to approach f of x and then we essentially have our proof. F is a continuous function. We defined f in this way, capital F in this way, and we were able to use just the definition of the derivative to figure out that the derivative of capital F of x is equal to, is equal to, is equal to f of x. And once again, why is this a big deal? Well, it tells you that if you have any continuous function f, and that's we assume, we assume that f is continuous over the interval, there exists some function. There exists a function, you can just define the function this way is the area under the curve, between, between some endpoint, or the, the beginning of the interval and sum x. If you define a function in that way, the derivative of this function is going to be equal to your continuous function. Or another way of saying it is, that you always have an anti-derivative. That any continuous function has an anti-derivative. And so it's a couple of cool things. Any continuous function has an anti-derivative. It's gonna be that capital, its' going to be that capital F of x. And this is why it's called the fundamental theorem of calculus. It ties together these two ideas. And you have differential calculus. You have the ideas, you have the idea of a derivative. And then, in integral calculus, you have the idea of an integral. Before this proof, all we viewed an integral as is the area under the curve. Is, it was just literally a notation to say the area under the curve. But now we've been able to make a connection. That there's a connection between the integral and the derivative. Or a connection between the integral and the anti-derivative. In particular so it connects all of calculus together in a very, very, very powerful, and we're so used to it now and, and now we can say almost in a somewhat obvious way but it wasn't obvious. Remember, we always think of integrals as somehow doing an anti-derivative but it wasn't clear. If you just viewed an integral as only an area you would have to go through this process and say wow, no it's connected, it's connected to the process of taking a derivative.

Overview

A proof system includes the components:[1][2]

A formal proof of a well-formed formula in a proof system is a set of axioms and rules of inference of proof system that infers that the well-formed formula is a theorem of proof system.[2]

Usually a given proof calculus encompasses more than a single particular formal system, since many proof calculi are under-determined and can be used for radically different logics. For example, a paradigmatic case is the sequent calculus, which can be used to express the consequence relations of both intuitionistic logic and relevance logic. Thus, loosely speaking, a proof calculus is a template or design pattern, characterized by a certain style of formal inference, that may be specialized to produce specific formal systems, namely by specifying the actual inference rules for such a system. There is no consensus among logicians on how best to define the term.

Examples of proof calculi

The most widely known proof calculi are those classical calculi that are still in widespread use:

Many other proof calculi were, or might have been, seminal, but are not widely used today.

Modern research in logic teems with rival proof calculi:

See also

References

  1. ^ Anita Wasilewska. "General proof systems" (PDF).
  2. ^ a b c "Definition:Proof System - ProofWiki". proofwiki.org. Retrieved 2023-10-16.
This page was last edited on 23 October 2023, at 14:02
Basis of this page is in Wikipedia. Text is available under the CC BY-SA 3.0 Unported License. Non-text media are available under their specified licenses. Wikipedia® is a registered trademark of the Wikimedia Foundation, Inc. WIKI 2 is an independent company and has no affiliation with Wikimedia Foundation.