1
00:00:02,340 --> 00:00:09,030
Well, welcome to the second lecture on Alan Turing on compute ability and intelligence,

2
00:00:09,030 --> 00:00:16,110
though in fact, Alan Turing will hardly feature in this lecture. I think he just scrapes onto the last slide.

3
00:00:16,110 --> 00:00:27,320
Today, we're mainly focussing on girdles theorem, the incompleteness theorem and the impact that that had on David Hilbert programme.

4
00:00:27,320 --> 00:00:34,620
So we've got a picture of Hilbert, a picture of girdle and worth knowing that in my lecture today,

5
00:00:34,620 --> 00:00:42,450
I'm going to be basing what I say quite a lot on Nagel and Newman's classic presentation of girdles theorem,

6
00:00:42,450 --> 00:00:46,380
the book Girdles Proof and Dates from, I think, the 1950s.

7
00:00:46,380 --> 00:00:50,850
I found it very interesting as an undergraduate. Well worth reading.

8
00:00:50,850 --> 00:00:58,650
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,

9
00:00:58,650 --> 00:01:05,160
but obviously much quicker to get through it in sort of 30 minutes or so.

10
00:01:05,160 --> 00:01:13,860
It's really an ingenious proof and was of huge importance for the development of

11
00:01:13,860 --> 00:01:20,110
logic and philosophy of maths and essential background to what Turing is doing.

12
00:01:20,110 --> 00:01:31,380
OK, so this is just a recollection of a slide from the last lecture Hilbert programme, his ambitions to establish mathematics on a solid,

13
00:01:31,380 --> 00:01:42,360
provably consistent foundation of axioms from which all mathematics can be deduced by logical reasoning.

14
00:01:42,360 --> 00:01:47,370
And coupled with that, the incidence problem.

15
00:01:47,370 --> 00:01:59,340
The aim to have a decision procedure which will tell us for any formula, any proposition that suitably expressed within the appropriate notation.

16
00:01:59,340 --> 00:02:07,800
Is there a proof for it or not? So let's pull these three notions aside.

17
00:02:07,800 --> 00:02:18,510
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,

18
00:02:18,510 --> 00:02:23,250
never lead to any contradiction. We've got completeness.

19
00:02:23,250 --> 00:02:28,780
All mathematical truths should in principle be dead useable from those axioms.

20
00:02:28,780 --> 00:02:32,370
Okay, so this isn't a matter of practically being able to do it.

21
00:02:32,370 --> 00:02:37,560
I mean, obviously, there's an infinite number of mathematical truths, so we're never going to be able to deduce them all.

22
00:02:37,560 --> 00:02:48,510
But the idea is that we should know that any mathematical truth should in principle be trusted, useful decide ability.

23
00:02:48,510 --> 00:02:55,050
There should be a clearly formulated procedure which is such that given any statement of mathematics,

24
00:02:55,050 --> 00:03:01,800
it can definitively establish within a finite time whether or not that statement follows from the given axioms.

25
00:03:01,800 --> 00:03:09,540
So those are three clearly separate claims for desiderata.

26
00:03:09,540 --> 00:03:12,990
Now you can think about these sorts of notions,

27
00:03:12,990 --> 00:03:22,800
either syntactically or semantically so semantically you'd be thinking in terms of truth and meaning syntactically.

28
00:03:22,800 --> 00:03:27,960
We're talking about formal relationships between the formulae.

29
00:03:27,960 --> 00:03:34,380
So we don't worry when we're doing syntactic treatments about what the formulae mean.

30
00:03:34,380 --> 00:03:39,480
We treat the proof rules in terms of we've got a formula of this structure.

31
00:03:39,480 --> 00:03:45,600
Another formula of this structure and we've got some rule which enables us to combine them together.

32
00:03:45,600 --> 00:03:50,460
For example, we might have one formula which is of the form p.

33
00:03:50,460 --> 00:03:58,230
Another one is of the form P Arrow, Q P implies Q, and therefore we can deduce Q.

34
00:03:58,230 --> 00:04:08,230
That is a syntactic relationship within those formulae and we can understand that in in that way without worrying about the semantics.

35
00:04:08,230 --> 00:04:14,670
Okay. So we've got a system of axioms which are formulae which have a particular structure.

36
00:04:14,670 --> 00:04:24,390
We've got rules, the rules of predicate logic by which we can deduce one formula from another purely in terms of the syntactic

37
00:04:24,390 --> 00:04:32,850
structure and a consistent system is one in which it is never possible starting from those axioms,

38
00:04:32,850 --> 00:04:39,870
applying the rules to prove both the proposition p and its negation, not P.

39
00:04:39,870 --> 00:04:45,930
OK, fair enough. You should not be able to deduce any contradiction.

40
00:04:45,930 --> 00:04:51,300
A complete system is one in which it's always possible either to proof p or to

41
00:04:51,300 --> 00:04:56,610
prove not p for any proposition p that is expressed both within the system.

42
00:04:56,610 --> 00:05:04,850
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

43
00:05:04,850 --> 00:05:11,930
system that are express if you like coherent propositions for each such proposition.

44
00:05:11,930 --> 00:05:16,280
It should be possible either to prove it or its negation.

45
00:05:16,280 --> 00:05:30,710
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.

46
00:05:30,710 --> 00:05:32,660
So they're closely related.

47
00:05:32,660 --> 00:05:41,450
And notice that these can be understood syntactically quite independently of whether or not the axioms are true and the rules are valid.

48
00:05:41,450 --> 00:05:46,160
In other words, prove that truth preserving.

49
00:05:46,160 --> 00:06:02,120
OK, now suppose we were able to achieve what Hilbert desired a consistent and complete system of arithmetic with true axioms and valid rules.

50
00:06:02,120 --> 00:06:10,250
In that case, any arithmetical proposition would be provable within that system if and only if it is true.

51
00:06:10,250 --> 00:06:19,040
So with the syntactic treatment, we can ignore issues of semantics, truth and and so on.

52
00:06:19,040 --> 00:06:31,820
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,

53
00:06:31,820 --> 00:06:38,280
then we have achieved what Hilbert wanted. OK.

54
00:06:38,280 --> 00:06:43,860
So incomes, girdle and all the spoils the party,

55
00:06:43,860 --> 00:06:52,410
his first incompleteness theorem is that in any true and hence consistent axiomatic theory

56
00:06:52,410 --> 00:06:58,380
sufficiently rich to enable the expression and proof of basic arithmetic propositions.

57
00:06:58,380 --> 00:07:06,810
So the kinds of arithmetic propositions that we want to be true in three times four equals 12.

58
00:07:06,810 --> 00:07:09,360
Seven is a prime number.

59
00:07:09,360 --> 00:07:20,550
It will be possible to construct an arithmetical Proposition G as such that neither g nor its negation is provable from the given axioms.

60
00:07:20,550 --> 00:07:31,320
So he shows how to construct a Formula G, which is neither provable nor its negation provable.

61
00:07:31,320 --> 00:07:34,500
Therefore, the system must be incomplete.

62
00:07:34,500 --> 00:07:40,620
And moreover, it follows from the reasoning that girl gives on the assumption that the system is indeed true,

63
00:07:40,620 --> 00:07:47,520
that all the axioms are true, that G must in fact be a true statement of arithmetic.

64
00:07:47,520 --> 00:07:55,380
So you can see this raises interesting philosophical questions because from girdles reasoning,

65
00:07:55,380 --> 00:08:03,510
we seem to be able to get to a true statement, which however we know to be unprovable.

66
00:08:03,510 --> 00:08:06,630
And although we're not going to go into that in this lecture,

67
00:08:06,630 --> 00:08:16,920
we will come back to this somewhat later when we talk about issues arising from Turing's 1950 paper.

68
00:08:16,920 --> 00:08:20,970
This has provoked a lot of philosophical discussion.

69
00:08:20,970 --> 00:08:29,940
OK, so I'm going to use G written thus for this formula, and we're going to see how we get to that.

70
00:08:29,940 --> 00:08:36,270
So first, a quick overview of the proof strategy.

71
00:08:36,270 --> 00:08:41,220
It's a very mind-bending proof. It's very satisfying.

72
00:08:41,220 --> 00:08:48,060
In many ways. It's ingenious, but it can be extremely confusing when you first come across it.

73
00:08:48,060 --> 00:08:54,510
So there will be a certain amount of repetition in this lecture, which I hope you'll find helpful.

74
00:08:54,510 --> 00:08:56,800
So let's look at the proof strategy first.

75
00:08:56,800 --> 00:09:05,940
We're going to devise a systematic method for assigning a girdle number to every formula and every sequence of formulae that are expressive,

76
00:09:05,940 --> 00:09:15,630
all within the theory. So if we take any Formula F, the F is just some well-formed formula within our system.

77
00:09:15,630 --> 00:09:22,140
We're going to find a way of assigning a number to it, and I'm going to use that font with a G.

78
00:09:22,140 --> 00:09:27,810
That's going to represent the girdle number of a particular form. We'll see how to do that on the next slide.

79
00:09:27,810 --> 00:09:38,640
So every formula will have a corresponding number. Then we're going to express logical relationships between formulae and between

80
00:09:38,640 --> 00:09:44,490
sequences of formulae in terms of mathematical relationships between the total numbers.

81
00:09:44,490 --> 00:09:54,930
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,

82
00:09:54,930 --> 00:10:04,290
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?

83
00:10:04,290 --> 00:10:13,110
Or is an axiom, and where a sequence of formulae is a proof of some Formula F,

84
00:10:13,110 --> 00:10:20,670
there will be some mathematical relationship, some arithmetical relationship between the corresponding girdle numbers.

85
00:10:20,670 --> 00:10:26,520
OK. So every formula has its go to number. Every sequence of formulae has its girdle number,

86
00:10:26,520 --> 00:10:33,180
and there will be some arithmetical relationship between those girdle numbers that holds

87
00:10:33,180 --> 00:10:42,960
if and only if the corresponding sequence is in fact a valid proof of the given formula.

88
00:10:42,960 --> 00:10:49,520
So I'm going to be using this predicate hit proof GTS.

89
00:10:49,520 --> 00:11:02,270
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.

90
00:11:02,270 --> 00:11:06,870
OK. OK, then what are we going to do?

91
00:11:06,870 --> 00:11:10,650
Is devise a mathematical Formula G, which, according to this method,

92
00:11:10,650 --> 00:11:18,630
is true if and only if there is no sequence s, which yields a valid proof of itself.

93
00:11:18,630 --> 00:11:21,030
And this formula will be of the form.

94
00:11:21,030 --> 00:11:32,880
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.

95
00:11:32,880 --> 00:11:36,410
OK, I'll go through that again and then. But.

96
00:11:36,410 --> 00:11:46,880
Proof GSA chief says the sequence of formulae with this girdle number is a valid proof of the formula with this goal number,

97
00:11:46,880 --> 00:11:57,830
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

98
00:11:57,830 --> 00:12:05,120
the girdle number of a sequence which provides a valid proof of the formula with that girdle number.

99
00:12:05,120 --> 00:12:11,330
In other words, formula big. Got that? OK.

100
00:12:11,330 --> 00:12:20,090
So we are going to devise such a formula and we will see from that that girdles theorem follows.

101
00:12:20,090 --> 00:12:28,280
Okay, so let's see what the total numbering is, and you are going to see that we very quickly get into humungous numbers.

102
00:12:28,280 --> 00:12:36,200
And if you had any thought of applying girdles theorem, you know, but actually doing the working out on a computer.

103
00:12:36,200 --> 00:12:45,590
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.

104
00:12:45,590 --> 00:12:50,450
So we're not talking about practicality here. We're talking about a theoretical result.

105
00:12:50,450 --> 00:12:53,600
As I've said, I'm going to mainly follow Nagler Newman's presentation.

106
00:12:53,600 --> 00:13:03,350
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.

107
00:13:03,350 --> 00:13:14,480
OK. So girls proof encode statements about mathematical relationships, e.g. that some sequence of formulae provides a valid proof of some Formula F.

108
00:13:14,480 --> 00:13:24,140
It encodes those relationships as formulae within arithmetic, and that involves, as we've said, assigning a girdle number.

109
00:13:24,140 --> 00:13:28,790
And I've said, I'm using this notation girdle number to each formula.

110
00:13:28,790 --> 00:13:33,260
So here's how we construct a girdle number for formula.

111
00:13:33,260 --> 00:13:36,200
Well, first of all, we've got some constant symbols to deal with.

112
00:13:36,200 --> 00:13:47,450
We've got knocked or arrow existential quantifier equals zero s s means successor, right?

113
00:13:47,450 --> 00:13:59,540
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.

114
00:13:59,540 --> 00:14:07,310
Now you can see that each of those has been assigned a number. So, for example, s has been assigned the number seven.

115
00:14:07,310 --> 00:14:11,390
And you can see that just straightforwardly in sequence.

116
00:14:11,390 --> 00:14:17,630
OK, then we've got numerical variables and we want to have a potentially infinite number of numerical variables.

117
00:14:17,630 --> 00:14:21,710
But let's just suppose the first one, the x y z.

118
00:14:21,710 --> 00:14:30,680
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.

119
00:14:30,680 --> 00:14:35,840
Yes, but it's a bit more to it than that, because why are we going to go to 13 Z?

120
00:14:35,840 --> 00:14:42,590
We're going to go to 17 and variables after that, we're going to go up the prime numbers, right?

121
00:14:42,590 --> 00:14:45,620
So we are going in the sequence of infant of prime numbers.

122
00:14:45,620 --> 00:14:51,350
You may be aware that there is an infinite number of primes, so we're not going to run out of primes.

123
00:14:51,350 --> 00:14:55,170
On the other hand, the gaps between them get bigger in general as we go larger.

124
00:14:55,170 --> 00:15:00,170
So these numbers, if we have a lot of variables, could get quite big.

125
00:15:00,170 --> 00:15:10,160
So intentional variables and variables, if you like the standard propositions, will have girdle numbers the same exact squared.

126
00:15:10,160 --> 00:15:22,010
All right. So eleven squared, thirteen squared, 17 squared and predicate variables, we'll have golden numbers that accuse of the primes.

127
00:15:22,010 --> 00:15:27,860
Got it! Incidentally, there's nothing particularly magical about doing it this way.

128
00:15:27,860 --> 00:15:32,990
All right. There are lots of different ways in which you could set up good numbers.

129
00:15:32,990 --> 00:15:38,270
But the crucial point is that they are uniquely decode of all that.

130
00:15:38,270 --> 00:15:46,130
The way the girdle number is provided for any formula or sequence of formulae means that if you have the number,

131
00:15:46,130 --> 00:15:49,760
you can uniquely decode it to the initial formula.

132
00:15:49,760 --> 00:16:00,740
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.

133
00:16:00,740 --> 00:16:07,250
Okay, so we've got girdle numbers for the individual symbols, and now we can work out the girdle number for a formula.

134
00:16:07,250 --> 00:16:16,250
So here is a formula. There is an X such that X is the successor of Y Y.

135
00:16:16,250 --> 00:16:21,830
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.

136
00:16:21,830 --> 00:16:30,320
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.

137
00:16:30,320 --> 00:16:36,550
Okay, so underneath each symbol, I've written the girdle number of that symbol.

138
00:16:36,550 --> 00:16:43,490
You can see the first variable X is 11 Y, it's the next prime 13.

139
00:16:43,490 --> 00:16:47,290
OK, so now what we do.

140
00:16:47,290 --> 00:16:57,580
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.

141
00:16:57,580 --> 00:17:03,970
We take the second prime number, which is three, and raise it for the power of the second girdle.

142
00:17:03,970 --> 00:17:10,660
The second symbol in the form 11, we take the third prime number, which is five,

143
00:17:10,660 --> 00:17:18,710
and raise it to the power of the total number of the first of the formula. And so.

144
00:17:18,710 --> 00:17:28,860
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.

145
00:17:28,860 --> 00:17:38,960
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.

146
00:17:38,960 --> 00:17:45,020
The double number of the six symbol in the form. Got it. And then we're multiplying all that together.

147
00:17:45,020 --> 00:17:50,310
You can see already we have got a humungous number.

148
00:17:50,310 --> 00:17:55,410
OK. That's just a formula. What about a sequence of formulae?

149
00:17:55,410 --> 00:18:00,870
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.

150
00:18:00,870 --> 00:18:09,150
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.

151
00:18:09,150 --> 00:18:19,890
All right. We are very quickly getting to numbers, which it's hard even to write down your name, let alone calculate with it.

152
00:18:19,890 --> 00:18:27,150
OK. Now, the crucial point is I mentioned each formula or sequence,

153
00:18:27,150 --> 00:18:34,110
a formula has a unique hurdle number, and no true formula can have the same girl number.

154
00:18:34,110 --> 00:18:38,820
If you think about how it's created from multiplying all these prime numbers together,

155
00:18:38,820 --> 00:18:44,970
if you take any girdle number, any legitimate girdle number and break it down into its prime factors,

156
00:18:44,970 --> 00:18:55,050
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.

157
00:18:55,050 --> 00:19:03,600
Okay, that makes it feasible to use girdle numbers as proxies for those formulae in expressing their properties in the relations between them.

158
00:19:03,600 --> 00:19:10,110
And we're going to see a function called sub that holds when one formula is a substitute, an instance of another.

159
00:19:10,110 --> 00:19:23,820
So we're going to reason about the logical properties of formulae and proofs in terms of the arithmetical relationships between their girdle numbers.

160
00:19:23,820 --> 00:19:32,070
All right. We're going to use their girdle numbers as proxies as things that we use instead of the formulae themselves.

161
00:19:32,070 --> 00:19:39,540
OK. Now let's look at one of these relationships.

162
00:19:39,540 --> 00:19:45,420
Okay. Here's a formula. There is an X such that X is the successor of Y, and there's it's girdle number.

163
00:19:45,420 --> 00:19:56,190
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.

164
00:19:56,190 --> 00:20:01,440
We can imagine substituting a particular numeral in place of Y.

165
00:20:01,440 --> 00:20:05,730
So X x zero is the successor of the successor is zero.

166
00:20:05,730 --> 00:20:12,600
In other words, two. So that's a numeral or perhaps an expression for a particular number.

167
00:20:12,600 --> 00:20:17,640
Now imagine we substitute that in place of Y.

168
00:20:17,640 --> 00:20:23,700
So we get this instead of that. So Y has been replaced with S s zero.

169
00:20:23,700 --> 00:20:28,320
And you can see that that has a certain effect on the girdle number of the formula.

170
00:20:28,320 --> 00:20:30,870
That was the goal, the number of that formula.

171
00:20:30,870 --> 00:20:39,650
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,

172
00:20:39,650 --> 00:20:47,140
the power of second, seven for the second best in 23 race for the power six, which is the total number of zero.

173
00:20:47,140 --> 00:20:55,920
So, OK, so there is a certain mathematical relationship between that formula.

174
00:20:55,920 --> 00:21:07,250
The good, the number of that formula and the total number of that form, you could in principle express this as an arithmetic function.

175
00:21:07,250 --> 00:21:14,480
So we've taken the formula that has that goal number within it,

176
00:21:14,480 --> 00:21:24,650
we have substituted the variable that has that girdle number 91 by the numeral expression for the number two.

177
00:21:24,650 --> 00:21:28,490
OK. Now notice this is not the girdle number of that.

178
00:21:28,490 --> 00:21:33,480
This is the number of which that is the new rule.

179
00:21:33,480 --> 00:21:38,570
OK, that all of these red things are numbers.

180
00:21:38,570 --> 00:21:45,830
This substitution has yielded formula, the formula with that total number, namely that forms of that.

181
00:21:45,830 --> 00:21:55,040
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,

182
00:21:55,040 --> 00:22:05,090
the the actual number whose numeral is being substituted and the girdle number of the resulting formula from the substitution.

183
00:22:05,090 --> 00:22:12,950
OK. Do you agree there is an interesting and rather complicated arithmetical relationship between these?

184
00:22:12,950 --> 00:22:20,220
Let's call that. So the submarine substitution, right?

185
00:22:20,220 --> 00:22:32,240
So the girdle number of the resulting formula is some of the go to number of the original formula.

186
00:22:32,240 --> 00:22:38,070
The bigger the number of the battery will be substituted and the number whose numeral is substituted.

187
00:22:38,070 --> 00:22:43,110
OK. And I'm not telling you what that function sub is.

188
00:22:43,110 --> 00:22:50,460
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,

189
00:22:50,460 --> 00:22:55,980
which would probably last a whole term and you know you'd be in your third year of a maths degree or something,

190
00:22:55,980 --> 00:23:02,190
you would learn how to beat, we can be assured that there is such a well-defined function.

191
00:23:02,190 --> 00:23:06,750
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

192
00:23:06,750 --> 00:23:11,400
that could in principle be defined that would pin down what this relationship is.

193
00:23:11,400 --> 00:23:14,940
I hope you can see it's at least plausible because if you look back here,

194
00:23:14,940 --> 00:23:20,550
you can see that there are systematic changes in the formula when you make the substitution.

195
00:23:20,550 --> 00:23:27,480
Imagine working out some clever arithmetic, a way of expressing that everyone happy with that.

196
00:23:27,480 --> 00:23:38,580
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.

197
00:23:38,580 --> 00:23:44,070
But if we can take that for granted, pretty much everything else will follow.

198
00:23:44,070 --> 00:23:48,090
OK. I mean that and similar things.

199
00:23:48,090 --> 00:23:55,200
So subbies and arithmetical function, which has three inputs it takes the girdle number of a formula containing a free variable.

200
00:23:55,200 --> 00:24:04,680
It takes the girdle number of that variable, a number, for example, to whose numeral is to be substituted for that variable.

201
00:24:04,680 --> 00:24:08,490
So that one to three inputs here.

202
00:24:08,490 --> 00:24:17,850
And given these inputs, subfields the girdle number of the formula resulting from substitution of the variable with the numeral, which is that one.

203
00:24:17,850 --> 00:24:22,140
OK. So I've spent some time on the the sub formula.

204
00:24:22,140 --> 00:24:32,160
We'll see. It plays a very important role in girls proof. Bear in mind, other other such functions could be expressed as well.

205
00:24:32,160 --> 00:24:44,790
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.

206
00:24:44,790 --> 00:24:52,650
We've got this sub function, which expresses the corresponding relationship between the girdle numbers of the formulae,

207
00:24:52,650 --> 00:25:03,540
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.

208
00:25:03,540 --> 00:25:10,860
OK. So I said sub is arithmetically a complicated function, but it is well-defined and could be spelt out in detail.

209
00:25:10,860 --> 00:25:15,840
Again, I'm asking you to take that on trust. OK.

210
00:25:15,840 --> 00:25:27,720
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,

211
00:25:27,720 --> 00:25:34,590
so remember N is actually a number, but the substitution is the numeral gets substituted.

212
00:25:34,590 --> 00:25:41,880
Then we have the girdle number of f n is sub g of x y comma 13 comma here.

213
00:25:41,880 --> 00:25:50,580
OK, that's just expressing what we've already seen. Right, but with more generality rather than a specific case.

214
00:25:50,580 --> 00:25:57,360
OK, now imagine that we spell out this function.

215
00:25:57,360 --> 00:26:06,130
So. We spell that out in gory arithmetical detail.

216
00:26:06,130 --> 00:26:18,220
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.

217
00:26:18,220 --> 00:26:28,810
Yeah. Now imagine that we write out that expression and we put y in place of ANC.

218
00:26:28,810 --> 00:26:37,930
So wherever we got C in this complicated expression, we put y wherever we've got a in this complicated expression, we put y.

219
00:26:37,930 --> 00:26:51,790
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.

220
00:26:51,790 --> 00:26:57,640
And then imagine that we put the team in place of B.

221
00:26:57,640 --> 00:27:05,170
This yields a complicated but provably possible arithmetical expression, which we can write like that.

222
00:27:05,170 --> 00:27:10,540
So the crucial point here is that when you see some ADC think this is shorthand for

223
00:27:10,540 --> 00:27:16,120
some complicated formula that's got a b and C A's B's and seised in that right.

224
00:27:16,120 --> 00:27:23,560
Now imagine that exactly the same complicated formula, except that we've got y in place of ANC and 13 in place of B.

225
00:27:23,560 --> 00:27:27,670
Do you agree? If one is possible, the other is. Yeah.

226
00:27:27,670 --> 00:27:32,380
OK. So that's going to play a role soon.

227
00:27:32,380 --> 00:27:40,730
So when you see this, you know, expressions with sub, just remember this is shorthand for some very complicated arithmetical stuff.

228
00:27:40,730 --> 00:27:46,810
Right? OK, so these are relatively simple function.

229
00:27:46,810 --> 00:27:49,780
It's not that simple, but it's relatively simple,

230
00:27:49,780 --> 00:27:57,190
but girdle also showed it's possible to define a far more complicated arithmetic formula a corresponding to the net.

231
00:27:57,190 --> 00:28:02,590
A mathematical statement that a sequence of formulae s corresponds a proof to a

232
00:28:02,590 --> 00:28:11,830
proof of Formula F a will be arithmetically true if and only if s indeed proves f.

233
00:28:11,830 --> 00:28:15,640
OK, so here I'm asking you to take something rather bigger on trust.

234
00:28:15,640 --> 00:28:28,180
But suppose you have a sequence of formulae, which is in fact a valid proof of some conclusion concluding formula.

235
00:28:28,180 --> 00:28:36,850
I'm saying there is some arithmetical relationship between the girdle number of the sequence and the girdle number of the conclusion.

236
00:28:36,850 --> 00:28:49,120
Yeah, such that that arithmetical relationship will hold if and only if the sequence is in fact a valid proof of the conclusion.

237
00:28:49,120 --> 00:28:54,530
Let's use proof a as shorthand. All right. So proof B that is an assertion, right?

238
00:28:54,530 --> 00:29:01,660
This is this is not now a function. This is not yielding some value.

239
00:29:01,660 --> 00:29:04,840
Well, it yields a Boolean value. It's true or false. Alright.

240
00:29:04,840 --> 00:29:16,930
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.

241
00:29:16,930 --> 00:29:26,680
Everyone happy that same kind of thing is sub. I'm hiding a lot of arithmetical complication just in a single shorthand.

242
00:29:26,680 --> 00:29:37,360
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.

243
00:29:37,360 --> 00:29:44,590
Now, the crucial point, if this is all being done properly, is that we have a truth preserving correspondents.

244
00:29:44,590 --> 00:29:50,060
The arithmetical formula proof AB, you remember that is an arithmetical formula.

245
00:29:50,060 --> 00:29:56,980
It's not a statement of matter mathematics. It is an arithmetical relationship between A and B.

246
00:29:56,980 --> 00:30:07,960
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,

247
00:30:07,960 --> 00:30:14,590
this arithmetical relationship holds if and only if the appropriate syntactic

248
00:30:14,590 --> 00:30:19,540
relationships hold between the sequence of formula formulae and the conclusion.

249
00:30:19,540 --> 00:30:24,340
It really is syntactically a valid proof that all right.

250
00:30:24,340 --> 00:30:31,660
But this is an arithmetical statement, not a metal mathematical statement,

251
00:30:31,660 --> 00:30:36,610
but the correspondence has been worked out in such a way that this arithmetical statement will be

252
00:30:36,610 --> 00:30:42,250
true if and only if the met a mathematical statement that this is a make a mathematical statement.

253
00:30:42,250 --> 00:30:46,930
The sequence of formulae with girdle number eight is a proof of the formula with good no.

254
00:30:46,930 --> 00:30:51,890
B is also true. Everyone happy.

255
00:30:51,890 --> 00:31:01,970
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

256
00:31:01,970 --> 00:31:14,060
relationship between A and B holds if and only if we do have a correct syntactic proof from of one a formula,

257
00:31:14,060 --> 00:31:19,310
we get a No. B via a sequence of formulae with girl No.

258
00:31:19,310 --> 00:31:27,410
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.

259
00:31:27,410 --> 00:31:37,130
C it suffices to establish whether or not the numbers ANC yield a true equation when substituted to give the arithmetic formula.

260
00:31:37,130 --> 00:31:48,550
Proof a c so we can use the arithmetical relationship as a proxy for the mettam mathematical relationship.

261
00:31:48,550 --> 00:31:53,120
OK, is everyone happy so far?

262
00:31:53,120 --> 00:31:57,550
Yeah, it's it's a bit mind-boggling because we're we're working on two levels.

263
00:31:57,550 --> 00:32:02,200
We've got the meta mathematics things like, you know, is one thing a proof of another.

264
00:32:02,200 --> 00:32:11,110
We've got the arithmetical relationship between the girdle numbers and the point is that that arithmetical relationship is being set up

265
00:32:11,110 --> 00:32:21,280
in such a clever way that it exactly mirrors the met in mathematical relationships and obviously the the real core arithmetical core.

266
00:32:21,280 --> 00:32:30,490
If your mathematical core of girdles theorem is showing that that can be done and I've kind of glossed over that.

267
00:32:30,490 --> 00:32:35,560
OK, now consider this arithmetic or formula.

268
00:32:35,560 --> 00:32:45,550
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.

269
00:32:45,550 --> 00:32:54,550
I'm, of course, giving you that the meta mathematical variant actually remember this isn't a complicated arithmetic statement.

270
00:32:54,550 --> 00:33:01,150
All right. And this is saying it's not the case that this complicated arithmetical relationship holds.

271
00:33:01,150 --> 00:33:11,290
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.

272
00:33:11,290 --> 00:33:16,570
OK, now let's go to this more complicated one.

273
00:33:16,570 --> 00:33:30,280
It is not the case that there is an X such that the proof relationship holds between X and whatever number that is.

274
00:33:30,280 --> 00:33:40,060
Now we've come across that, OK? But remember, just remember, that is a very complicated arithmetic function.

275
00:33:40,060 --> 00:33:51,620
But it has a particular value. So this is saying there is no x such that that relationship holds,

276
00:33:51,620 --> 00:33:59,900
and that corresponds to the statement that there is no proof of the formula with that.

277
00:33:59,900 --> 00:34:05,570
The right. OK. This is it does get a little bit mind bending.

278
00:34:05,570 --> 00:34:16,040
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?

279
00:34:16,040 --> 00:34:18,680
As long as you get the general feel for what's going on.

280
00:34:18,680 --> 00:34:28,100
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.

281
00:34:28,100 --> 00:34:36,350
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.

282
00:34:36,350 --> 00:34:44,420
The crucial point is to remember that when we look at that, when we look at this, we are talking about arithmetical expressions, right?

283
00:34:44,420 --> 00:34:49,640
But there are arithmetical expressions which which happen to have been cooked up within

284
00:34:49,640 --> 00:34:56,420
the system in such a way that they correspond to meta mathematical claims about proof.

285
00:34:56,420 --> 00:35:00,650
And so. Okay. Oh, yeah, just one other thing, by the way.

286
00:35:00,650 --> 00:35:04,730
Nagel and Newman use it, use an old style, universal quantifier and so on.

287
00:35:04,730 --> 00:35:09,990
I've replaced that with the existential quantifier because I know that's more familiar to you.

288
00:35:09,990 --> 00:35:16,440
OK. OK, so let's let's look at this formula here.

289
00:35:16,440 --> 00:35:24,360
Remember, again, that's an arithmetical formula. It corresponds to the meta mathematical statement that there exists no sequence

290
00:35:24,360 --> 00:35:33,660
of formulae that constitutes a proof of the formula that has that good or no.

291
00:35:33,660 --> 00:35:37,490
In other words, that formula.

292
00:35:37,490 --> 00:35:50,720
Is not proven now, I've said the precise identity of that formula will obviously depend on the value that substituted for way,

293
00:35:50,720 --> 00:35:57,140
if you right, that's that's a mathematical expression that has a y y in there.

294
00:35:57,140 --> 00:36:06,710
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.

295
00:36:06,710 --> 00:36:14,270
But at any rate, the meaning of that expression is clear, even though, as it were,

296
00:36:14,270 --> 00:36:20,390
the formulas in which it's applying is not clear until you've made that substitution.

297
00:36:20,390 --> 00:36:28,970
OK. But now look at that formula that that very formula,

298
00:36:28,970 --> 00:36:38,140
think of that as a formula and suppose that has the girdle no end, it must have some girdle, no agreed.

299
00:36:38,140 --> 00:36:45,700
We haven't calculated what it is. We can't calculate what it is because that's horrendously complicated expression.

300
00:36:45,700 --> 00:36:51,220
And it's going to involve prime not, you know, very high prime numbers raised very high powers.

301
00:36:51,220 --> 00:36:55,810
Right. It's going to be pretty humongous, but it has a girdle. No.

302
00:36:55,810 --> 00:37:03,360
Yeah. Suppose that girdle number is in.

303
00:37:03,360 --> 00:37:15,240
Okay. This is where it gets really clever. So the girl number of that formula is in, we don't know what it is.

304
00:37:15,240 --> 00:37:22,590
I mean, we know there is an end, but it's absolutely huge. Now consider this formula.

305
00:37:22,590 --> 00:37:27,270
Now you can see that she's coming back. Consider this formula.

306
00:37:27,270 --> 00:37:41,740
That notice is that formula with end substituted in place of Y, where N is the girl number of that formula, whatever that is.

307
00:37:41,740 --> 00:37:54,750
Got it! OK, now notice that this formula here is Formula G is itself the formula that we obtain from the girls.

308
00:37:54,750 --> 00:38:08,110
The formula with girl number N i.e. that formula there if we substitute Y by the numeral for N.

309
00:38:08,110 --> 00:38:22,390
Hence, the girdle number of this formula here, the blue one is, in fact, that.

310
00:38:22,390 --> 00:38:29,320
Because sub, remember subbies, this clever function that has been devised in such a way that it has this property.

311
00:38:29,320 --> 00:38:33,310
You get a formula with a certain girdle number that has a free why there you

312
00:38:33,310 --> 00:38:40,090
replace it with a numeral four and you get a good little number with that.

313
00:38:40,090 --> 00:38:45,910
So you get a formula with that girl number. OK, now look at that last line.

314
00:38:45,910 --> 00:38:50,320
You can see there's something really funny going on there.

315
00:38:50,320 --> 00:39:01,360
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,

316
00:39:01,360 --> 00:39:09,750
and it turns out that the very good number is there.

317
00:39:09,750 --> 00:39:19,800
OK, so here we are, here's our our big our girdle formula,

318
00:39:19,800 --> 00:39:24,630
so that arithmetical formula corresponds to the that's a mathematical statement

319
00:39:24,630 --> 00:39:33,240
that there exists no sequence of formula that constitutes a proof of the formula.

320
00:39:33,240 --> 00:39:42,120
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.

321
00:39:42,120 --> 00:39:54,390
That girl got it. But that double number, that that number is in fact bigger than the number of g itself.

322
00:39:54,390 --> 00:40:09,680
By the way, it's been constructed. So, gee, that statement corresponds to the metre mathematical statement itself is unprovable.

323
00:40:09,680 --> 00:40:18,440
It's pretty mind. We've got a statement there, which is an arithmetical statement,

324
00:40:18,440 --> 00:40:27,500
but by the way that the correspondence between the arithmetic and the measurement method mathematics has been set up.

325
00:40:27,500 --> 00:40:37,100
This effectively asserts the unimproved ability of itself.

326
00:40:37,100 --> 00:40:43,880
OK, so the arithmetic of Proposition G encodes the statement that G itself is unprovable.

327
00:40:43,880 --> 00:40:51,110
Again, I'm I'm trying to keep a distinction here between the arithmetical statements and the meta mathematical statements.

328
00:40:51,110 --> 00:40:57,980
But when I say that one encodes the other, I mean, they have this correspondence that's being set up.

329
00:40:57,980 --> 00:41:06,650
So the arithmetical Proposition G encodes the statement that G itself is unprovable within the formal system chosen.

330
00:41:06,650 --> 00:41:13,070
So if G were false, then it would follow that G was not unprovable.

331
00:41:13,070 --> 00:41:20,600
If G encodes the statement that it is unprovable, then if it's false, it's not unprovable.

332
00:41:20,600 --> 00:41:25,490
And if it's not unprovable, that means it must be provable in the system.

333
00:41:25,490 --> 00:41:31,490
And if the system is a correct axiomatic system, arithmetic g would have to be true.

334
00:41:31,490 --> 00:41:45,130
Remember, Gurnal is reasoning about the system, which we assume to be have true consistent axioms from which basic arithmetic follows.

335
00:41:45,130 --> 00:41:53,890
So if she were false, we'd have a contradiction. If she is false, then she has to be provable.

336
00:41:53,890 --> 00:42:02,290
And if the system is is, it is a consistent, complete basis for arithmetic, then that would mean she was true.

337
00:42:02,290 --> 00:42:11,860
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.

338
00:42:11,860 --> 00:42:17,590
So if it's true, then it is both true and I'm provable.

339
00:42:17,590 --> 00:42:31,360
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,

340
00:42:31,360 --> 00:42:40,120
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

341
00:42:40,120 --> 00:42:45,760
asserts its own unproved ability and it follows from that that if it is false,

342
00:42:45,760 --> 00:42:53,800
then G is provable, right? If it's true, it's provable if and only if it's unprovable.

343
00:42:53,800 --> 00:42:57,640
So if it's not true, it's not unprovable.

344
00:42:57,640 --> 00:43:00,040
Therefore, it must be provable.

345
00:43:00,040 --> 00:43:06,220
But if G is provable and the system provides a faithful and consistent representation of arithmetic, then gene must be true.

346
00:43:06,220 --> 00:43:12,700
So if we string those two implications together, we've got a few false things provable.

347
00:43:12,700 --> 00:43:16,570
But if it's provable, then it's true. So G can't be false.

348
00:43:16,570 --> 00:43:21,010
We get a contradiction of genes. False must be true.

349
00:43:21,010 --> 00:43:28,270
But if it's true, it's unprovable out there because it encodes the statement that it is unprovable.

350
00:43:28,270 --> 00:43:32,560
So our system, if it is a consistent and correct axiomatic zation of arithmetic,

351
00:43:32,560 --> 00:43:40,000
cannot be complete for G will then be a true statement of arithmetic that cannot be proven.

352
00:43:40,000 --> 00:43:47,210
Right. Yeah, it's ingenious, isn't it?

353
00:43:47,210 --> 00:43:55,250
OK, so that's girdles there. It's a profound bit of metaphor mathematics.

354
00:43:55,250 --> 00:44:01,100
It had an absolutely seismic impact in the philosophy of maths.

355
00:44:01,100 --> 00:44:17,100
Remember that that Hilbert not very long before had announced his programme and here was girdle showing actually that it couldn't be achieved.

356
00:44:17,100 --> 00:44:26,670
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.

357
00:44:26,670 --> 00:44:35,640
It shows that any consistent axiomatic system of arithmetic will leave some arithmetical truths unprovable.

358
00:44:35,640 --> 00:44:45,660
So if you have a system that is consistent and correct basic arithmetic, it cannot be complete.

359
00:44:45,660 --> 00:44:56,310
But that doesn't mean that the shadings problem, the decision problem is thereby solved because there might be.

360
00:44:56,310 --> 00:45:01,860
Even though there are true statements that are not going to be provable within the system,

361
00:45:01,860 --> 00:45:06,180
there might be some effectively computable decision procedure,

362
00:45:06,180 --> 00:45:15,390
which would infallibly, in a finite time, reveal whether any given Proposition P is or is not provable, right?

363
00:45:15,390 --> 00:45:20,010
It might be that there are some propositions that are provable and some that aren't provable,

364
00:45:20,010 --> 00:45:32,670
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.

365
00:45:32,670 --> 00:45:38,400
So that's the tribunal's problem. Now notice does this work effectively computable?

366
00:45:38,400 --> 00:45:41,670
Where does that come from?

367
00:45:41,670 --> 00:45:53,790
Well, here is a perfect procedure for discovering whether any arithmetical proposition is or is not provable from a given set of axioms.

368
00:45:53,790 --> 00:46:07,200
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.

369
00:46:07,200 --> 00:46:13,650
But we know that that doesn't count right when we're looking for a decision procedure.

370
00:46:13,650 --> 00:46:21,430
We're not going to allow anything that's magical or that relies on, you know, completely unexplained intuition.

371
00:46:21,430 --> 00:46:24,930
And you know, I ask John Newman, he's a genius unit.

372
00:46:24,930 --> 00:46:26,670
No, that's not going to do.

373
00:46:26,670 --> 00:46:37,920
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.

374
00:46:37,920 --> 00:46:51,270
In order to make sense of the decision problem, we need to have a conception of what counts as an effectively computable procedure.

375
00:46:51,270 --> 00:46:56,130
And that is where Turing comes in.

376
00:46:56,130 --> 00:47:04,710
And effectively computable procedure is supposed to be one that can be performed by systematic application of clearly specified rules.

377
00:47:04,710 --> 00:47:05,400
OK.

378
00:47:05,400 --> 00:47:15,510
You can't just appeal to your local deity or genius, and it should not require any inspirational leap, spontaneous intellectual insights or whatever.

379
00:47:15,510 --> 00:47:21,900
It's got to be precisely specified. So to find the limits of effective computer ability,

380
00:47:21,900 --> 00:47:30,930
we need to devise a way of encompassing all possible mechanical methods of inference in order to even address the decision problem.

381
00:47:30,930 --> 00:47:40,140
Remember the problem of deciding, given any formula? Is this provable or not?

382
00:47:40,140 --> 00:47:50,160
We need to have a conception of what counts as a legitimate, provable proving method and effectively computable method.

383
00:47:50,160 --> 00:47:54,570
And that's how Alan Turing came to invent what's now known as the Turing machine.

384
00:47:54,570 --> 00:48:06,180
The Turing machine is Alan Turing's fantastically successful attempt to pin down what counts as an effectively computable procedure,

385
00:48:06,180 --> 00:48:17,610
and we'll be going onto that next time. I strongly advise, particularly those of you who are studying this for your course,

386
00:48:17,610 --> 00:48:26,370
start seriously on the Pixelbook Go through the Turing proof along with my lectures.

387
00:48:26,370 --> 00:48:30,840
I mean, you might find it good to try the relevant chapters before the lecture,

388
00:48:30,840 --> 00:48:36,480
or possibly to read them immediately after to consolidate what you've got through.

389
00:48:36,480 --> 00:48:39,870
That is what we will be starting on next time. All right.

390
00:48:39,870 --> 00:48:40,877
See you then.