Well, welcome to the second lecture on Alan Turing on compute ability and intelligence,
though in fact, Alan Turing will hardly feature in this lecture. I think he just scrapes onto the last slide.
Today, we're mainly focussing on girdles theorem, the incompleteness theorem and the impact that that had on David Hilbert programme.
So we've got a picture of Hilbert, a picture of girdle and worth knowing that in my lecture today,
I'm going to be basing what I say quite a lot on Nagel and Newman's classic presentation of girdles theorem,
the book Girdles Proof and Dates from, I think, the 1950s.
I found it very interesting as an undergraduate. Well worth reading.
If you want to know more about this, I'm going to be going through the proof at the same sort of level as they do,
but obviously much quicker to get through it in sort of 30 minutes or so.
It's really an ingenious proof and was of huge importance for the development of
logic and philosophy of maths and essential background to what Turing is doing.
OK, so this is just a recollection of a slide from the last lecture Hilbert programme, his ambitions to establish mathematics on a solid,
provably consistent foundation of axioms from which all mathematics can be deduced by logical reasoning.
And coupled with that, the incidence problem.
The aim to have a decision procedure which will tell us for any formula, any proposition that suitably expressed within the appropriate notation.
Is there a proof for it or not? So let's pull these three notions aside.
We've got consistency. So the set of axioms, the things from which we start to think formulae that we take for granted should be provably consistent,
never lead to any contradiction. We've got completeness.
All mathematical truths should in principle be dead useable from those axioms.
Okay, so this isn't a matter of practically being able to do it.
I mean, obviously, there's an infinite number of mathematical truths, so we're never going to be able to deduce them all.
But the idea is that we should know that any mathematical truth should in principle be trusted, useful decide ability.
There should be a clearly formulated procedure which is such that given any statement of mathematics,
it can definitively establish within a finite time whether or not that statement follows from the given axioms.
So those are three clearly separate claims for desiderata.
Now you can think about these sorts of notions,
either syntactically or semantically so semantically you'd be thinking in terms of truth and meaning syntactically.
We're talking about formal relationships between the formulae.
So we don't worry when we're doing syntactic treatments about what the formulae mean.
We treat the proof rules in terms of we've got a formula of this structure.
Another formula of this structure and we've got some rule which enables us to combine them together.
For example, we might have one formula which is of the form p.
Another one is of the form P Arrow, Q P implies Q, and therefore we can deduce Q.
That is a syntactic relationship within those formulae and we can understand that in in that way without worrying about the semantics.
Okay. So we've got a system of axioms which are formulae which have a particular structure.
We've got rules, the rules of predicate logic by which we can deduce one formula from another purely in terms of the syntactic
structure and a consistent system is one in which it is never possible starting from those axioms,
applying the rules to prove both the proposition p and its negation, not P.
OK, fair enough. You should not be able to deduce any contradiction.
A complete system is one in which it's always possible either to proof p or to
prove not p for any proposition p that is expressed both within the system.
I mean, notice here we're restricting P to what? We call well-formed formulae formulae that are correctly formed within the syntax of the
system that are express if you like coherent propositions for each such proposition.
It should be possible either to prove it or its negation.
If it's to be a complete system, so consistency means you can't prove both Panopto p completeness means you can prove either p or not p.
So they're closely related.
And notice that these can be understood syntactically quite independently of whether or not the axioms are true and the rules are valid.
In other words, prove that truth preserving.
OK, now suppose we were able to achieve what Hilbert desired a consistent and complete system of arithmetic with true axioms and valid rules.
In that case, any arithmetical proposition would be provable within that system if and only if it is true.
So with the syntactic treatment, we can ignore issues of semantics, truth and and so on.
But if we combine that with actually achieving an axiom system in which the the axioms are true ones and we've got a complete system for arithmetic,
then we have achieved what Hilbert wanted. OK.
So incomes, girdle and all the spoils the party,
his first incompleteness theorem is that in any true and hence consistent axiomatic theory
sufficiently rich to enable the expression and proof of basic arithmetic propositions.
So the kinds of arithmetic propositions that we want to be true in three times four equals 12.
Seven is a prime number.
It will be possible to construct an arithmetical Proposition G as such that neither g nor its negation is provable from the given axioms.
So he shows how to construct a Formula G, which is neither provable nor its negation provable.
Therefore, the system must be incomplete.
And moreover, it follows from the reasoning that girl gives on the assumption that the system is indeed true,
that all the axioms are true, that G must in fact be a true statement of arithmetic.
So you can see this raises interesting philosophical questions because from girdles reasoning,
we seem to be able to get to a true statement, which however we know to be unprovable.
And although we're not going to go into that in this lecture,
we will come back to this somewhat later when we talk about issues arising from Turing's 1950 paper.
This has provoked a lot of philosophical discussion.
OK, so I'm going to use G written thus for this formula, and we're going to see how we get to that.
So first, a quick overview of the proof strategy.
It's a very mind-bending proof. It's very satisfying.
In many ways. It's ingenious, but it can be extremely confusing when you first come across it.
So there will be a certain amount of repetition in this lecture, which I hope you'll find helpful.
So let's look at the proof strategy first.
We're going to devise a systematic method for assigning a girdle number to every formula and every sequence of formulae that are expressive,
all within the theory. So if we take any Formula F, the F is just some well-formed formula within our system.
We're going to find a way of assigning a number to it, and I'm going to use that font with a G.
That's going to represent the girdle number of a particular form. We'll see how to do that on the next slide.
So every formula will have a corresponding number. Then we're going to express logical relationships between formulae and between
sequences of formulae in terms of mathematical relationships between the total numbers.
So suppose we've got a sequence of Formula X that two has a girdle number and suppose Sequence X is a proof of Formula F,
so a proof consists of a sequence of formulae. You know where each formula in the list is validly reached from earlier formulae in the list?
Or is an axiom, and where a sequence of formulae is a proof of some Formula F,
there will be some mathematical relationship, some arithmetical relationship between the corresponding girdle numbers.
OK. So every formula has its go to number. Every sequence of formulae has its girdle number,
and there will be some arithmetical relationship between those girdle numbers that holds
if and only if the corresponding sequence is in fact a valid proof of the given formula.
So I'm going to be using this predicate hit proof GTS.
That will mean that is an assertion that the sequence which has this goal number is actually a valid proof of the formula that has this girl then.
OK. OK, then what are we going to do?
Is devise a mathematical Formula G, which, according to this method,
is true if and only if there is no sequence s, which yields a valid proof of itself.
And this formula will be of the form.
It is not the case that there is an X such that X is the girdle number of a sequence, which is a valid proof of the formula with this girdle number.
OK, I'll go through that again and then. But.
Proof GSA chief says the sequence of formulae with this girdle number is a valid proof of the formula with this goal number,
so X is a valid proof of that. What this formula correspondingly says is it is not the case that there is some number X such that X is
the girdle number of a sequence which provides a valid proof of the formula with that girdle number.
In other words, formula big. Got that? OK.
So we are going to devise such a formula and we will see from that that girdles theorem follows.
Okay, so let's see what the total numbering is, and you are going to see that we very quickly get into humungous numbers.
And if you had any thought of applying girdles theorem, you know, but actually doing the working out on a computer.
Good luck to you because what you're going to have to do at a very early stage is find some way of dealing with these absolutely humongous numbers.
So we're not talking about practicality here. We're talking about a theoretical result.
As I've said, I'm going to mainly follow Nagler Newman's presentation.
I think it's particularly clear it also has the virtue that if you have any difficulty with what I say here, you can go to that book and and get more.
OK. So girls proof encode statements about mathematical relationships, e.g. that some sequence of formulae provides a valid proof of some Formula F.
It encodes those relationships as formulae within arithmetic, and that involves, as we've said, assigning a girdle number.
And I've said, I'm using this notation girdle number to each formula.
So here's how we construct a girdle number for formula.
Well, first of all, we've got some constant symbols to deal with.
We've got knocked or arrow existential quantifier equals zero s s means successor, right?
So S0 is one the successor of zero. So that's going to give us all our natural numbers and open bracket, close bracket and comma.
Now you can see that each of those has been assigned a number. So, for example, s has been assigned the number seven.
And you can see that just straightforwardly in sequence.
OK, then we've got numerical variables and we want to have a potentially infinite number of numerical variables.
But let's just suppose the first one, the x y z.
We're going to assign the number 11 to X and you might think eleven, that's just because it's the next number after 10.
Yes, but it's a bit more to it than that, because why are we going to go to 13 Z?
We're going to go to 17 and variables after that, we're going to go up the prime numbers, right?
So we are going in the sequence of infant of prime numbers.
You may be aware that there is an infinite number of primes, so we're not going to run out of primes.
On the other hand, the gaps between them get bigger in general as we go larger.
So these numbers, if we have a lot of variables, could get quite big.
So intentional variables and variables, if you like the standard propositions, will have girdle numbers the same exact squared.
All right. So eleven squared, thirteen squared, 17 squared and predicate variables, we'll have golden numbers that accuse of the primes.
Got it! Incidentally, there's nothing particularly magical about doing it this way.
All right. There are lots of different ways in which you could set up good numbers.
But the crucial point is that they are uniquely decode of all that.
The way the girdle number is provided for any formula or sequence of formulae means that if you have the number,
you can uniquely decode it to the initial formula.
You're never going to have to formulae having the same girdle number. That's why we're using prime numbers here because of prime number decomposition.
Okay, so we've got girdle numbers for the individual symbols, and now we can work out the girdle number for a formula.
So here is a formula. There is an X such that X is the successor of Y Y.
You notice here, by the way, is a free variable. We don't have it. It's not within a quantifier that worry about that.
You'll see there's an important reason why I've done that. Let's just look at that formula and work out its girdle number.
Okay, so underneath each symbol, I've written the girdle number of that symbol.
You can see the first variable X is 11 Y, it's the next prime 13.
OK, so now what we do.
We take the first prime number, which is two, and we raise it to the power of the first symbol in the Formula two to the fourth.
We take the second prime number, which is three, and raise it for the power of the second girdle.
The second symbol in the form 11, we take the third prime number, which is five,
and raise it to the power of the total number of the first of the formula. And so.
You get the idea. So don't be confused by as it were the first time, here are the 13 there, that 13 is becoming the power of 17.
And this 13 is there because that's the one two three four five six prime number, and it is both being raised to the power of the sixth.
The double number of the six symbol in the form. Got it. And then we're multiplying all that together.
You can see already we have got a humungous number.
OK. That's just a formula. What about a sequence of formulae?
Well, if you've got a sequence formula, you do the same kind of thing. You raise two to the power of the first formula.
Three for the power of the second and so on. And you multiply those all together and thus you get a good little number for the sequence of formula.
All right. We are very quickly getting to numbers, which it's hard even to write down your name, let alone calculate with it.
OK. Now, the crucial point is I mentioned each formula or sequence,
a formula has a unique hurdle number, and no true formula can have the same girl number.
If you think about how it's created from multiplying all these prime numbers together,
if you take any girdle number, any legitimate girdle number and break it down into its prime factors,
you can mechanically work out where it comes from, whether it was a sequence, a formula or a formula or symbol, and what those were.
Okay, that makes it feasible to use girdle numbers as proxies for those formulae in expressing their properties in the relations between them.
And we're going to see a function called sub that holds when one formula is a substitute, an instance of another.
So we're going to reason about the logical properties of formulae and proofs in terms of the arithmetical relationships between their girdle numbers.
All right. We're going to use their girdle numbers as proxies as things that we use instead of the formulae themselves.
OK. Now let's look at one of these relationships.
Okay. Here's a formula. There is an X such that X is the successor of Y, and there's it's girdle number.
OK. And you can see that 17 has been raised to the power of 13 because 13 is the girdle number of y y is a free variable.
We can imagine substituting a particular numeral in place of Y.
So X x zero is the successor of the successor is zero.
In other words, two. So that's a numeral or perhaps an expression for a particular number.
Now imagine we substitute that in place of Y.
So we get this instead of that. So Y has been replaced with S s zero.
And you can see that that has a certain effect on the girdle number of the formula.
That was the goal, the number of that formula.
Now we instead of having 17 race the power 13, we've got 17 race for the power of seven for the first at 19 race,
the power of second, seven for the second best in 23 race for the power six, which is the total number of zero.
So, OK, so there is a certain mathematical relationship between that formula.
The good, the number of that formula and the total number of that form, you could in principle express this as an arithmetic function.
So we've taken the formula that has that goal number within it,
we have substituted the variable that has that girdle number 91 by the numeral expression for the number two.
OK. Now notice this is not the girdle number of that.
This is the number of which that is the new rule.
OK, that all of these red things are numbers.
This substitution has yielded formula, the formula with that total number, namely that forms of that.
Is that OK? So we've actually got a relationship between four numbers here, the girl number of the original formula, the girl number of the variable,
the the actual number whose numeral is being substituted and the girdle number of the resulting formula from the substitution.
OK. Do you agree there is an interesting and rather complicated arithmetical relationship between these?
Let's call that. So the submarine substitution, right?
So the girdle number of the resulting formula is some of the go to number of the original formula.
The bigger the number of the battery will be substituted and the number whose numeral is substituted.
OK. And I'm not telling you what that function sub is.
And this is the bit where I'm asking you to take something on trust. And you know, if you were doing a maths course on Girdles Theorem,
which would probably last a whole term and you know you'd be in your third year of a maths degree or something,
you would learn how to beat, we can be assured that there is such a well-defined function.
Right? I'm not going to do that. I'm going to ask you to take it on trust that there is a well-defined function
that could in principle be defined that would pin down what this relationship is.
I hope you can see it's at least plausible because if you look back here,
you can see that there are systematic changes in the formula when you make the substitution.
Imagine working out some clever arithmetic, a way of expressing that everyone happy with that.
Yeah. OK. So like I say, I'm not giving you a complete presentation of girls theorem, of course, because I'm leaving out these gory details.
But if we can take that for granted, pretty much everything else will follow.
OK. I mean that and similar things.
So subbies and arithmetical function, which has three inputs it takes the girdle number of a formula containing a free variable.
It takes the girdle number of that variable, a number, for example, to whose numeral is to be substituted for that variable.
So that one to three inputs here.
And given these inputs, subfields the girdle number of the formula resulting from substitution of the variable with the numeral, which is that one.
OK. So I've spent some time on the the sub formula.
We'll see. It plays a very important role in girls proof. Bear in mind, other other such functions could be expressed as well.
Subbies just one example of the kind of manipulation that we commonly do on formulae substituting a numeral for a variable when we do that.
We've got this sub function, which expresses the corresponding relationship between the girdle numbers of the formulae,
but you could have lots of other possible operations on formulae, which could also be expressed in terms of the girdle numbers of the formerly.
OK. So I said sub is arithmetically a complicated function, but it is well-defined and could be spelt out in detail.
Again, I'm asking you to take that on trust. OK.
So if Y is a formula containing why, which has go to number 13 and F and is the corresponding formula in which Y is substituted by the numeral for N,
so remember N is actually a number, but the substitution is the numeral gets substituted.
Then we have the girdle number of f n is sub g of x y comma 13 comma here.
OK, that's just expressing what we've already seen. Right, but with more generality rather than a specific case.
OK, now imagine that we spell out this function.
So. We spell that out in gory arithmetical detail.
All right. So we've got some complicated expression which expresses function sub in terms of its three inputs, which we'll call here ABC.
Yeah. Now imagine that we write out that expression and we put y in place of ANC.
So wherever we got C in this complicated expression, we put y wherever we've got a in this complicated expression, we put y.
So we've still got an a valid expression or a a well-formed expression, but with a variable y put in place of ANC.
And then imagine that we put the team in place of B.
This yields a complicated but provably possible arithmetical expression, which we can write like that.
So the crucial point here is that when you see some ADC think this is shorthand for
some complicated formula that's got a b and C A's B's and seised in that right.
Now imagine that exactly the same complicated formula, except that we've got y in place of ANC and 13 in place of B.
Do you agree? If one is possible, the other is. Yeah.
OK. So that's going to play a role soon.
So when you see this, you know, expressions with sub, just remember this is shorthand for some very complicated arithmetical stuff.
Right? OK, so these are relatively simple function.
It's not that simple, but it's relatively simple,
but girdle also showed it's possible to define a far more complicated arithmetic formula a corresponding to the net.
A mathematical statement that a sequence of formulae s corresponds a proof to a
proof of Formula F a will be arithmetically true if and only if s indeed proves f.
OK, so here I'm asking you to take something rather bigger on trust.
But suppose you have a sequence of formulae, which is in fact a valid proof of some conclusion concluding formula.
I'm saying there is some arithmetical relationship between the girdle number of the sequence and the girdle number of the conclusion.
Yeah, such that that arithmetical relationship will hold if and only if the sequence is in fact a valid proof of the conclusion.
Let's use proof a as shorthand. All right. So proof B that is an assertion, right?
This is this is not now a function. This is not yielding some value.
Well, it yields a Boolean value. It's true or false. Alright.
Proof a b is saying the sequence of formulae with girdle number eight is in fact a valid proof of the formula that has go to number B.
Everyone happy that same kind of thing is sub. I'm hiding a lot of arithmetical complication just in a single shorthand.
Just by the way, if you read Nigel in human, they use them rather than proof that I think it's easier, they're more intuitive to use proof.
Now, the crucial point, if this is all being done properly, is that we have a truth preserving correspondents.
The arithmetical formula proof AB, you remember that is an arithmetical formula.
It's not a statement of matter mathematics. It is an arithmetical relationship between A and B.
But we've done the arithmetic in such a way. We we we formulated this in such a way that given our particular formal system, whatever it is,
this arithmetical relationship holds if and only if the appropriate syntactic
relationships hold between the sequence of formula formulae and the conclusion.
It really is syntactically a valid proof that all right.
But this is an arithmetical statement, not a metal mathematical statement,
but the correspondence has been worked out in such a way that this arithmetical statement will be
true if and only if the met a mathematical statement that this is a make a mathematical statement.
The sequence of formulae with girdle number eight is a proof of the formula with good no.
B is also true. Everyone happy.
This is this is the crucial point, there's a correspondence being set up by some ingenious mathematics in such a way that this mathematical
relationship between A and B holds if and only if we do have a correct syntactic proof from of one a formula,
we get a No. B via a sequence of formulae with girl No.
OK. So to establish whether or not the sequence of formulae with girdle number A is in fact a valid proof of the formula, this girl no.
C it suffices to establish whether or not the numbers ANC yield a true equation when substituted to give the arithmetic formula.
Proof a c so we can use the arithmetical relationship as a proxy for the mettam mathematical relationship.
OK, is everyone happy so far?
Yeah, it's it's a bit mind-boggling because we're we're working on two levels.
We've got the meta mathematics things like, you know, is one thing a proof of another.
We've got the arithmetical relationship between the girdle numbers and the point is that that arithmetical relationship is being set up
in such a clever way that it exactly mirrors the met in mathematical relationships and obviously the the real core arithmetical core.
If your mathematical core of girdles theorem is showing that that can be done and I've kind of glossed over that.
OK, now consider this arithmetic or formula.
It is not the case that the sequence of formulae with to number A is in fact a proof of the formula good and number B.
I'm, of course, giving you that the meta mathematical variant actually remember this isn't a complicated arithmetic statement.
All right. And this is saying it's not the case that this complicated arithmetical relationship holds.
It corresponds to the mathematical statement that the sequence of formulae with girl number eight is not a proof of the formula with the number B.
OK, now let's go to this more complicated one.
It is not the case that there is an X such that the proof relationship holds between X and whatever number that is.
Now we've come across that, OK? But remember, just remember, that is a very complicated arithmetic function.
But it has a particular value. So this is saying there is no x such that that relationship holds,
and that corresponds to the statement that there is no proof of the formula with that.
The right. OK. This is it does get a little bit mind bending.
This is the sort of thing where having a slightly tenuous grasp of it while I'm going through the lecture is not a problem, right?
As long as you get the general feel for what's going on.
It's something that very much rewards going back and reading through the stuff carefully because we've got a lot of very highly abstract ideas here.
But everything you need to understand this is down here. And as I say, you might find Nagel and Newman useful if you want more.
The crucial point is to remember that when we look at that, when we look at this, we are talking about arithmetical expressions, right?
But there are arithmetical expressions which which happen to have been cooked up within
the system in such a way that they correspond to meta mathematical claims about proof.
And so. Okay. Oh, yeah, just one other thing, by the way.
Nagel and Newman use it, use an old style, universal quantifier and so on.
I've replaced that with the existential quantifier because I know that's more familiar to you.
OK. OK, so let's let's look at this formula here.
Remember, again, that's an arithmetical formula. It corresponds to the meta mathematical statement that there exists no sequence
of formulae that constitutes a proof of the formula that has that good or no.
In other words, that formula.
Is not proven now, I've said the precise identity of that formula will obviously depend on the value that substituted for way,
if you right, that's that's a mathematical expression that has a y y in there.
So the the actual value that the yields will depend on what you substitute for, why it's got a very free variable sitting in that.
But at any rate, the meaning of that expression is clear, even though, as it were,
the formulas in which it's applying is not clear until you've made that substitution.
OK. But now look at that formula that that very formula,
think of that as a formula and suppose that has the girdle no end, it must have some girdle, no agreed.
We haven't calculated what it is. We can't calculate what it is because that's horrendously complicated expression.
And it's going to involve prime not, you know, very high prime numbers raised very high powers.
Right. It's going to be pretty humongous, but it has a girdle. No.
Yeah. Suppose that girdle number is in.
Okay. This is where it gets really clever. So the girl number of that formula is in, we don't know what it is.
I mean, we know there is an end, but it's absolutely huge. Now consider this formula.
Now you can see that she's coming back. Consider this formula.
That notice is that formula with end substituted in place of Y, where N is the girl number of that formula, whatever that is.
Got it! OK, now notice that this formula here is Formula G is itself the formula that we obtain from the girls.
The formula with girl number N i.e. that formula there if we substitute Y by the numeral for N.
Hence, the girdle number of this formula here, the blue one is, in fact, that.
Because sub, remember subbies, this clever function that has been devised in such a way that it has this property.
You get a formula with a certain girdle number that has a free why there you
replace it with a numeral four and you get a good little number with that.
So you get a formula with that girl number. OK, now look at that last line.
You can see there's something really funny going on there.
Really clever because we've now got a formula which kind of asserts the non-approved ability of a formula with a certain girdle number,
and it turns out that the very good number is there.
OK, so here we are, here's our our big our girdle formula,
so that arithmetical formula corresponds to the that's a mathematical statement
that there exists no sequence of formula that constitutes a proof of the formula.
With that goes a number. All right. There is no x such that X is the girl number of a sequence of formula, which constitutes a proof of the formula.
That girl got it. But that double number, that that number is in fact bigger than the number of g itself.
By the way, it's been constructed. So, gee, that statement corresponds to the metre mathematical statement itself is unprovable.
It's pretty mind. We've got a statement there, which is an arithmetical statement,
but by the way that the correspondence between the arithmetic and the measurement method mathematics has been set up.
This effectively asserts the unimproved ability of itself.
OK, so the arithmetic of Proposition G encodes the statement that G itself is unprovable.
Again, I'm I'm trying to keep a distinction here between the arithmetical statements and the meta mathematical statements.
But when I say that one encodes the other, I mean, they have this correspondence that's being set up.
So the arithmetical Proposition G encodes the statement that G itself is unprovable within the formal system chosen.
So if G were false, then it would follow that G was not unprovable.
If G encodes the statement that it is unprovable, then if it's false, it's not unprovable.
And if it's not unprovable, that means it must be provable in the system.
And if the system is a correct axiomatic system, arithmetic g would have to be true.
Remember, Gurnal is reasoning about the system, which we assume to be have true consistent axioms from which basic arithmetic follows.
So if she were false, we'd have a contradiction. If she is false, then she has to be provable.
And if the system is is, it is a consistent, complete basis for arithmetic, then that would mean she was true.
So if she is false, she is true. So it can't be false, must be true. But remember that Gene codes the statement that it itself is unprovable.
So if it's true, then it is both true and I'm provable.
OK, let's go through that again, using a little bit of symbolism to help bring out the structure because of the way that the encoding is set up,
the correspondence between the arithmetic and the maths mathematics. We have the gene is true if and only if G is unprovable because G kind of
asserts its own unproved ability and it follows from that that if it is false,
then G is provable, right? If it's true, it's provable if and only if it's unprovable.
So if it's not true, it's not unprovable.
Therefore, it must be provable.
But if G is provable and the system provides a faithful and consistent representation of arithmetic, then gene must be true.
So if we string those two implications together, we've got a few false things provable.
But if it's provable, then it's true. So G can't be false.
We get a contradiction of genes. False must be true.
But if it's true, it's unprovable out there because it encodes the statement that it is unprovable.
So our system, if it is a consistent and correct axiomatic zation of arithmetic,
cannot be complete for G will then be a true statement of arithmetic that cannot be proven.
Right. Yeah, it's ingenious, isn't it?
OK, so that's girdles there. It's a profound bit of metaphor mathematics.
It had an absolutely seismic impact in the philosophy of maths.
Remember that that Hilbert not very long before had announced his programme and here was girdle showing actually that it couldn't be achieved.
But notice that it doesn't solve all of the problems or it doesn't settle the questions with regard to all of held its programme.
It shows that any consistent axiomatic system of arithmetic will leave some arithmetical truths unprovable.
So if you have a system that is consistent and correct basic arithmetic, it cannot be complete.
But that doesn't mean that the shadings problem, the decision problem is thereby solved because there might be.
Even though there are true statements that are not going to be provable within the system,
there might be some effectively computable decision procedure,
which would infallibly, in a finite time, reveal whether any given Proposition P is or is not provable, right?
It might be that there are some propositions that are provable and some that aren't provable,
but you might be able to work out some decision procedure for whether a proposition lies in the provable set or the not provable set.
So that's the tribunal's problem. Now notice does this work effectively computable?
Where does that come from?
Well, here is a perfect procedure for discovering whether any arithmetical proposition is or is not provable from a given set of axioms.
Ask God. Well, OK, if that's if that's if there is a God and you've got a hotline to God and God is infallible, then that might work.
But we know that that doesn't count right when we're looking for a decision procedure.
We're not going to allow anything that's magical or that relies on, you know, completely unexplained intuition.
And you know, I ask John Newman, he's a genius unit.
No, that's not going to do.
We need to have a procedure that we can pin down and specify precisely so that's where the issue of effective compute ability comes in.
In order to make sense of the decision problem, we need to have a conception of what counts as an effectively computable procedure.
And that is where Turing comes in.
And effectively computable procedure is supposed to be one that can be performed by systematic application of clearly specified rules.
OK.
You can't just appeal to your local deity or genius, and it should not require any inspirational leap, spontaneous intellectual insights or whatever.
It's got to be precisely specified. So to find the limits of effective computer ability,
we need to devise a way of encompassing all possible mechanical methods of inference in order to even address the decision problem.
Remember the problem of deciding, given any formula? Is this provable or not?
We need to have a conception of what counts as a legitimate, provable proving method and effectively computable method.
And that's how Alan Turing came to invent what's now known as the Turing machine.
The Turing machine is Alan Turing's fantastically successful attempt to pin down what counts as an effectively computable procedure,
and we'll be going onto that next time. I strongly advise, particularly those of you who are studying this for your course,
start seriously on the Pixelbook Go through the Turing proof along with my lectures.
I mean, you might find it good to try the relevant chapters before the lecture,
or possibly to read them immediately after to consolidate what you've got through.
That is what we will be starting on next time. All right.
See you then.