Gödel's Incompleteness Theorems: An Informal Introduction to Formal Logic

[00:00:10]you are a blacksmith in a faraway land while others work with iron or bronze you work with magic and your swords are prized throughout the land for their supernatural abilities one day a knight visits you he places a heavy bag of gold coins upon the counter and asks can you make me a sword that can kill all of my enemies of course you reply for this is easily done can you make me a sword that can kill only my enemies and no other living thing there is nothing simple you reply then make me a sword that can kill all of my enemies and only my enemies so that i will not harm a hair on any allies head during battle and with that he departs you toil at your forge every day for three months shaping the blade weaving arcane forces into the metal and exercising any imperfections until eventually you are left with a magnificent weapon when the knight returns you place the sword down before him he examines it then satisfied gives you the remainder of your payment before mounting his horse and riding away you never see him again yet as he leaves a tremor of nervousness passes through you for you know that the sword you have made for him can either kill all of his enemies or kill only his enemies but not both worse still without calling upon magic beyond your control there is no way to determine which 4. while mustering administering the magic imbued within the blade a prophecy revealed itself to you a prophecy older than time written in the language of reality which states that any magic sword of this kind must necessarily create its own downfall for there exists someone in the world be they man woman or otherwise who if they are your enemy cannot be killed by your sword and if they can be killed by your sword then they are not your enemy [Music] part 0 introduction [Applause] you don't have to be logic ian to watch this video wait sorry you don't have to be a logician to watch this video as long as you're interested and you have a baseline familiarity with mathematics you should be able to get something from this there will be logic involved quite a lot of it at some points but when that happens i'll do my best to include both technical and higher level descriptions of the material so that everyone can get something out of it you also don't need to watch this video all in one go i'm quite aware of its length but everything in here needs to be in here for us to appreciate the conclusion for that reason i've broken it up into chapters so feel free to stop and start as you like i won't hold it against you this video as the title card would suggest is about a rather esoteric field of mathematics called formal logic i'll talk at great length later about what exactly that is but for now it's just the fighters to say that it's probably the most abstract discipline in all of mathematics and for that reason even professional mathematicians might find a gulf between their regular work and the stuff i'll be talking about indeed it's so abstract that it actually strays closer to becoming philosophy of points in that we are analyzing modes of thought and how humans are likely to conceptualize arguments there is actually a whole discipline of logic called philosophical logic which aims to analyze logic from a philosophical perspective but for now given that this is the summer of maths exposition we'll be sticking to a mathematical treatment of logic except for right at the end when i might indulge in a little philosophical speculation because no one can stop me i've also included the patent-pending matte punk danger meter which will appear periodically throughout the video to tell you how tough the going's gonna be it goes all the way from dark green meaning hopefully not too bad to read meaning weapons grade mathematics i hope to stay out of the red zone for as long as possible but regrettably there will be some valiances into it because this is some heavy stuff we're dealing with this video will be a slow burn and we'll be making several detours along the way i would encourage you to watch the entire thing especially if this is your first introduction to logic because everything will be in play by the end and i think you'll like the conclusion a question i get asked surprisingly often is what 0.5 what is pure maths good for right yeah because if you're an engineer or a politician or a journalist or something else then the work you do has a tangible effect on reality engineers build things politicians represent people in democratic power structures or at least they're supposed to and journalists distill complex ideas down into digestible products for general consumption when i tell people i'm a mathematician they often assume correctly in my case that i study pure mathematics but what exactly is pure mathematics well to paraphrase one of my favorite books of all time a pure mathematician is someone who goes to their office sits down at their desk and spends all day thinking about the question what is three while this isn't strictly true at all it captures quite well the distance between pure mathematics and some of the more applied disciplines like fluid dynamics information theory or statistics all of which definitely have pure aspects to them but it's fairly obvious how they can be applied to the real world in a way that pure mathematics can't so what good is pure mathematics you know thinking about numbers all day what good's that gonna do i can think of several possible responses to this question only one of which includes a swear word they range from the practical to the uber geeky i think we'll start with the practical answer to adapt to monty python quote aside from architecture transport networks agriculture modern medicine manufacturing automation communication and the internet what's pure maths ever done for us much of the applied mathematics which is directly useful is grounded in centuries of pure mathematics research to give but one example modern day cryptography which is what allows you to shop online without your credit card information being stolen simply would not exist without the pioneering number theory work of g.h hardy a man who once said quote no discovery of mine has made or is ever to make directly or indirectly for good or ill the least difference to the world without him we wouldn't have facebook or amazon or apple or also pure maths isn't just about numbers this is more of a nitpick than an actual response but it's common to conflate pure maths with number theory when in reality number theory is just a small part of the much broader field of pure mathematics which also includes things like abstract algebra analysis set theory subjects where the appearance of numbers tends to be met with surprise and or suspicion moving to the geekiest side of things the fact that mathematics is such a good model of reality poses a super interesting question is reality maths in the opening of this video i indirectly called mathematical theorems prophecies older than time written in the language of reality itself but is this true is the universe maths or is maths just a model we've created to describe the universe in other words is mathematics created or discovered there's far too much behind this question for me to unpack here so i'll shelve it for now but maybe give it some thought i've been thinking about it for years and i still can't find a good answer either way understanding mathematics is key to understanding the way the world is pure maths and all the study of mathematics as a philosophical concept is called meta mathematics and it's here in these hallowed lands where mathematics and philosophy walk hand in hand that we first brush up against our hallowed logic part one axiomatic systems what is an axiom an axiom is something we assume to be true which we can use to deduce other things an axiomatic system is then any mathematical field which has axioms perhaps the earliest known example of an axiomatic system was the geometry created by euclid in the 300 bces he attempted to pin geometry down into as few statements as possible and use those statements to show every other geometric property from them euclid's axioms were as follows the first axiom is that a line can be drawn from any point to any other point axiom two a line can be extended to infinity axiom three a circle can be drawn with the same length as a line segment axiom four all right angles are the same axiom five if two lines are drawn which intersect a third in such a way that the sum of the inner angles on one side is less than two right angles then the two lines inevitably must intersect each other on that side if extended far enough now the fifth axiom caused euclid quite a bit of trouble and in the intervening centuries many people tried to get rid of the fifth axiom because it seemed unwieldy and unnecessary and it wasn't in keeping with the elegant beauty of the first four and eventually people realized that we don't need the fifth axiom you can't prove it from the other four but there's no reason to assume it you can if you want assume the opposite and as soon as people realized that whole new fields of geometry opened up called non-euclidean geometries perhaps the two most famous examples of non-euclidean geometries are elliptic geometries and hyperbolic geometries elliptic geometry is the geometry of a sphere instead of the fifth axiom we say that if two of light if two lines in elliptic geometry are perpendicular to a third then those two lines must intersect a consequence of this is that a sum of angles in a triangle will always be greater than 180 degrees it's used a lot in planes and gps and anything where you're having to deal with 3d spheres or ellipses whatever hyperbolic geometry on the other hand is very weird lines curve away from each other instead of running parallel to each other and this means that the sum of angles and triangles are always less than 180 degrees always less than 180 degrees this has a lot of really interesting uses in special relativity for example but it doesn't very accurately describe the real world so we never really come across it i think i have a diagram that can explain it um let me just move everything out of the way quickly yeah okay there we go so around the time people began to realize that euclid's axioms were malleable in some sense there was a big drive for formalism we had the analysis gang of viastros koshi and bolzano we had group theory being studied by arbo and galwa and so people began to ask can we do the same for arithmetic that is is there a single set of axioms from which we can derive every single truth of arithmetic and the answer was very complicated in order to answer this mathematicians were going to need new and much more powerful tools the way mathematics was conceived of in the academic sphere was about to change forever and with that i think it's finally time we get formal part two formal logic who said that despite my appearance formal logic is called formal because it deals with laws of form i.e the structure of arguments rather than the content of the arguments to give an example of this when i was a kid i had a jumper from next which had the logo across the chest the letters n e x t and my mum used to point at the letters each letter in turn and say n e x t then one day when we were out walking we walked past a stop sign an english stop sign that says s-t-o-p on it and i pointed at the stop sign at each of the letters in turn and said n e x t and my mum looked at me with a glint in her eye and said what a dumb ass of course she didn't really my mum's lovely instead she realized that i picked up on the form of the sign the four-letter pattern rather than the actual content of the letters of that pattern and formal logic is about studying those kinds of patterns formal logic can be thought of as an attempt to find every kind of argument and break them down into their forms as you can imagine there are many many many many many many many many many many many many many many many many many many many many many many many many many different kinds of argument and so logicians have come up with a series of tricks to help them find each one and we're going to look at some of those tricks in this video we'll start with perhaps the simplest idea of a logical argument that of a b reasoning so the idea is that if we have a and we have a implies b then we get b an example of this might be it is raining if it is raining then i will get wet therefore i will get wet don't be intimidated by the fact that we're using letters to represent sentences by the way in the example i gave before the letter a stood in for it is reigning and b stood in for i will get wet because we're only interested in the form of each argument we want to generalize as much as we can and the way we do that is by taking abstract sentence symbols in this case letters and letting them stand in for specific sentences in an argument thinking in these terms gives rise to 2.1 propositional logic can you guys hear that too anyway interruptions aside yes we get a system called propositional logic or zeroth order logic propositional logic arose as a way to deal with arguments whose constituent sentences can't be broken down any further so it is raining for example i will get wet both of these cannot in our argument be broken down any further than themselves however the sentence if it is raining then i will get wet may be broken down further by use of a connective if then is an example of what's called a binary connective it's called binary because it has two input values in our case the input values are it is raining and i will get wet putting these together we get if it is raining then i will get wet there are other kinds of connectives as well let's think about the slightly more complicated case i am late to work my boss has not had her coffee if i am late to work and my boss has not had her coffee then i will be shouted at therefore i will be shouted at another example of a connective is ore we could just as easily say if i am late to work or my boss has not had her coffee i will get shouted at therefore i will leave my job it's not a valid argument i don't know why i said that for now i think it's time we start to formalize properly so let's move over to the whiteboard and i'll start laying out the good stuff the system we define here is going to be based on gerhard genson's system of natural deduction it consists of four sets oh and i'm sure some of you are wondering why it says hoopla here the answer is i have tried so hard to rub this off but it's not coming so for now we are stuck with hoopla logic anyway hoopla logic consists of four sets one a set sorry talk to the microphone one a set of propositional symbols these are our a b c d e f g uh the letters we are using to represent individual sentence fragments the ones that i said earlier can't be broken down any further we're never going to need more than 26 of them but if you do here's how you do it you're right a one bottom index one a two bottom index two a three and so on so in our earlier argument it is raining and i will get wet are both represented by propositional symbols but we're not dealing with their meaning yet we are only considering the symbols meaning will come later trust me next up we have our set of connectives these express relationships between sentences and we give each one its own special symbols so we don't have to write out each word in full each time now in logic we like to represent abstract sentences by greek letters so these are our propositional symbols but sentences are something slightly different because they include connectives again we're going to rigorously define sentences in a moment but for now for now all you need to consider is basically we can put propositional symbols in in place of them and we'll go from there hey it's me from the future here to say i made a huge mistake when i recorded this part which was i started to talk about meaning now we don't want to talk about meaning yet so i've edited out all the parts of me talking about meaning this means the next section is going to be a little jagged but hopefully everything will come to light eventually okay cool we have and symbol or implies if and only if and not this only takes one sentence as an argument whereas the others take two this means that this is what's known as a unary connective whereas these four are all binary connectives next we have our set of axioms as discussed earlier these are things we assume to be true for the sake of the system we don't actually have any axioms in this system because the axioms are kind of given to us by the inference rules for certain connectives this is kind of a technical detail so i'm going to gloss over it here because it's not hugely relevant all that matters is that we have an empty axiom set for this system and finally fourth and sexiest we have the inference rules if the propositional symbols and the connectives are the lego bricks of logic then these are the instruction manual they tell us how we can combine sentences together by adding or removing connectives there are too many for me to list on this board so as i keep saying i'm going to put them on screen now and you can pause and read them at your leisure some of them get pretty technical so don't blame me if you don't want to engage that's fine you won't need to know specific details of the inference rules for the system to enjoy the rest of this video so have at it if you like [Music] when these four sets combine their powers they form what is called a deductive system or somewhat confusingly i've also seen it referred to as a logic logic refers to the broad overarching field a logic refers to a specific instance of sets of these things but i think that's fairly uncommon terminology i just quite like it but we're not quite done yet because we still don't have a way to reliably generate sentences we do this using three rules number one every propositional symbol is a sentence number two if phi and psi are sentences then so are all of these so basically you can put two sentences on either side of a binary connective and you'll always get a sentence and three most important rule of all nothing else is a sentence not even the life sentences defined in this way are often called well-formed formulae which is often abbreviated to wff which i'm going to pronounce as woof finally a proof of a sentence phi in our system consists of a set of woofs psi naught psi 1 psi 2 dot dot all the way up to psi n for some number n such that psi n is equal to phi the sentence we want to be proved and every worth in the set is either an axiom an assumption which is something we take to be true for the sake of the proof or can be deduced logically from other members of that set using the rules of inference provided oh that was quite a bit of work wasn't it if you glazed over slightly don't worry i'll go through an example to show you what i mean let's take the theory with connective and axioms a and b and inference rule if phi and psi are sentences then so is phi and psi it's a standard introduction rule for and using this if we assume c can we deduce a and b and c yes we can here's how first we take from our axioms a then we take from our axioms b then we can join them using our rule of inference to a and b then we take c from the assumptions at the start of our proof and can join that with our a and b to get a and b and c however with the same assumption we can't prove a and b and d as d is neither an axiom of the system nor an assumption we make similarly a and b or c can't be proved because or is not a connective we've specified we can use you might wonder why we chose the connectives we did earlier and not a different set basically it's because we wanted a system that would mirror how we think about logic in real life in our day-to-day lives we use connectives like and or if then very frequently maybe not in specifically those ways and we use a lot of other connectives which are very similar to them but these are the connectives which underpin the way humans think about logic to be sure it would definitely be possible to come up with systems of logic using other connectives in fact it's possible to come up with systems of logic which use only one connective which are able to prove everything that you can prove in our system and that's really interesting but we won't be talking about it here natural deduction is a system which emphasizes understandability over economy and as such it has a few more connectives than we strictly need i think now is a good time to introduce a key concept in the field of formal systems that of consistency a theory is inconsistent if there is a well-formed formula phi for which both phi and not phi can be derived within the theory a theory is consistent if it is not inconsistent we like consistent theories because there's a little thing called the principle of explosion which says that if there is a sentence such that both it and its negation can be proved then you can prove any sentence you like within that system it's called the principle of explosion because everything will blow up in your face a consequence of this is that a theory is consistent if and only if there is a well-formed formula which cannot be proved there only needs to be one typically there are more but there only needs to be one our example theory from earlier is consistent because we were able to show that a and b and d cannot be proved despite it being well formed this is an important equivalence to make so store it away and we'll return to it later doors closing indeed my favorite formal theory is the hilbert system it has two connectives not and implication three axioms on screen and one inference rule which says that if phi and phi implies psi then psi this is called modus ponens meaning method of placing usually gets abbreviated to mp for implies the helbet system can prove everything that natural deduction can and vice versa but the fact that there's only one inference rule makes the hilbert system really cool for proving things in particular for the mathematicians among you proofs by induction get really simple when you only have one inductive case to consider whereas in natural deduction there are i think something like 12 inference rules and you have to consider every single case it gets grueling if you're trying to do inductive proofs in natural deduction so from now on if i have to do a proof which i may not actually have to i can't remember in the video script but if i do i'm only going to bother proving things for the implication case because natural deduction and the hilbert system are equivalent so we only need to consider the implication case for the programmers among you the hilbert system is like c to natural deductions python much more difficult to understand but once you're familiar with it it's very quick phew i'm glad that's over although aristotelian syllogisms are statements of the form all x are y a is x therefore a is y the most famous example of this is all men are mortal socrates is a man therefore socrates is mortal but we can't do that in propositional logic all men are mortal formalizes a propositional sentence a socrates is a man propositional sentence b therefore socrates is mortal propositional sentence c so we would have to say that a and b together imply c which is not a valid argument in propositional logic we need to upgrade our logic which means no no no i don't want to go back part 2.2 predicate logic all right let's get it over with predicate logic is like propositional logic but better whereas with predicate logic we could only consider worths in their entirety using propositional logic you're allowed to break down formulae into their constituent parts predicate logic is also called first order logic i think i forget to say this in this section of the video and then from the end of this part onwards i only ever call it first order logic so just to clear up any confusion predicate logic also called first order logic they're the same thing well i don't even get a suit this time basically all of the definitions of propositional logic carry over the major difference is that we introduce a concept called arity which is a word i adore i love the word arity the arity of a predicate is the number of variables it admits but what's a predicate and what's a variable these are very good questions and one which i should probably have started with remember how propositional logic had proposition symbols which stood for whole sentences like it is raining and i will get wet well in predicate logic we upgrade these to admit variables which are terms with no fixed meaning so for example you could have a predicate symbol p of x which we might notate p1 of x to indicate that it has an arity of one this might be interpreted as something like x has property p if we want to be very general a specific case of this could be x is a dog or x has a father or x is mortal similarly we could have b3 of x y and z which would be a predicate symbol with three variables which would mean that x y and z have property b or more accurately xyz has property b because there's a technical detail here which is order matters to discuss why this is the case i'm going to have to talk briefly about interpretations this will really come back later in the video for now i'm mostly just saying it to make a point and the point is that the order in which your variables sit in the predicate symbol matters so let's define p of x and y to be a binary predicate which we can interpret as meaning x is greater than y in this case it's fairly obvious to see why we might like order to matter in predicate symbols because if order doesn't matter then p of x and y would be equivalent to p of y and x and if we want to interpret p as x is greater than y then that would mean x is greater than y is equivalent to y is greater than x so in order for the logic that we're about to build to make sense it has to be such that the order of variables within predicate symbols matters to make explicit something i've been hinting at the arity of a predicate symbol is then the number of variables within it or if you like the number of letters that follow it that means p of x is a one erry symbol b of x y z is a three arry symbol and our propositional symbols from earlier are not arry predicate symbols because they admit no variables in this way you can think of the predicate symbols as being a natural extension of the class of propositional symbols if that's your thing in addition to this we have quantifier symbols now these are the scary looking logic symbols that you always see when you open textbooks but they're really not that bad once you've met them and are familiar with them if you've gone out for drinks a few times maybe i don't know held their hand in a public place they're really not that bad the two that we have here are for all and there exists upside down a and upside down e respectively or i guess backwards a no upside down a backwards e for all x p x can be understood to mean every x has property p there exists an x such that px can be understood as some x has property p if a variable is under the influence of a quantifier symbol we say that that variable is bound otherwise we say that it is free for example the predicate symbol that is currently on screen is bound in x and y and free in z alternatively z is free x and y are bound we also introduce constant symbols which can take the place of variables within predicates these are like specific terms as opposed to the more general idea of variables we haven't yet given the meaning as i keep saying but what we can do is we can replace general variables with specific constants so for example px can be transformed into pa but pa means specifically that a has property p whereas p of x means x has property p where x is not defined as a specific thing another way to think about it is that p of x has one free variable whereas p of a has no free variables another thing you'll commonly see in formulations of first order logic are so-called function symbols function symbols take variables to constants and actually constants are a special kind of function symbol but that's a bit technical and i won't get into it here the idea is in mathematics functions represent a rule which take one number to another number function symbols in logic work much the same way where you take a variable and you transform it into another kind of variable which we can interpret like a constant once again i know i keep saying it but hopefully this will all make more sense once we see examples the formation rules for quantifiers are relatively easy if you have a predicate symbol which is free in x then you can slap a quantifier symbol on the front so you can have for all x p of x and there exists x such that p of x that is how you form them anything like that is well formed you're also allowed to do this even if the predicate symbol does not contain the variable you are quantifying over so for all y p of x is a well-formed formula what it means well that's up for discussion really but the point is that it's well formed this also works for propositional symbols which if you'll remember are predicate symbols with arity zero you can say for all x p again doesn't really mean much but you're allowed to do it with these new tools we can now formalize our socrates argument let p of x mean x is a man and q of x mean x is mortal we'll then let a stand in for socrates the argument then becomes for all x p x implies q x p a therefore q a we've dabbled a bit with meaning here but i'd just like to illustrate to you an example of a valid argument in predicate logic if you want some good material on the topic i've got some books on screen that you might enjoy this might feel a little bit rushed to you and to be honest that's because it is predicate logic is fascinating and a really fun thing to go and do some reading about yourself but in order to get across the points in this video i've had to restrict it only to things that are relevant to my proof of the girdle theorems which is really fish's proof which is really ross's proof but either way i'm not going to be able to give this subject the fair shake it deserves i'd love to come back to it one day and maybe give a proper series on what exactly predicate logic holds in store for those of us who want to study it but for now i think it's time we just moved on and i will refer to and clarify things as they come up see you on the other side everything we've talked about so far has been dealing with the syntax of formal languages the the so-called symbol shuffling or symbolic calculus if you're fancy aside from my examples we haven't tried to give anything meaning yet or even to try and work out when arguments are true or false in order to do that we'll need a method to determine whether sentences are true or false which means it's time for part three syntax and semantics it's time for semantics models and valuations semantics give meaning to sentences which is done in the form of a structure structures have four parts logic seems to like fours you have a set of objects called the domain these are the allowable values for variables but they can be anything we like you also have an interpretation of each endplace function as an ordered n-tuple that's an ordered set of n elements of the domain mapping them to a single element of the domain we also then have an interpretation of any n-place non-function predicate as being a set of ordered n-tuples of elements of the domain and finally we have an interpretation of each constant symbol as corresponding to a specific element of the domain this is a technical formal definition of a structure if you don't follow the specifics that's completely fine you don't need to i've mostly just included this for the hell of it having created a structure we then perform a valuation on it which assigns truth values i.e true or false to each predicate the idea behind this is we want to know whether certain predicates are true for a given set of inputs using our example from earlier let's take the two place predicate symbol p x y to mean x is greater than y and then we'll take the domain one two and three we could think of p as being a set of ordered pairs which satisfy the relation is greater than so in our specific case p would be given by 2 1 3 1 and 3 2 because in each of those ordered pairs the first element is greater than the second hence they satisfy the predicate p and we can choose to define the predicate p in terms of this relation if we so wish a predicate is true if and only if the input values are within the allowable set of input values so for example p of 2 1 is true because 2 is greater than 1 whereas p 1 2 is false because 1 is not greater than 2. we can define other predicates this way too over the same domain the numbers 1 2 and 3. let's define q to be 1 1 2 1 and 2 3. then q 2 1 would be true because 2 1 is in the set of q whereas q 1 3 would be false because 1 3 is not in the set q there's no special interpretation of q and maths like there was of p i created it just to be a reminder that what we're dealing here is very general and captures a lot of things that don't directly correspond to familiar mathematical objects from there you can evaluate more complicated expressions by considering the connectives they contain if phi and psi are both true then phi and psi must also be true but if psi is false then phi and psi must also be false however phi or psi will be true these connectives behave in the same way they do in ordinary language we codify this in logic by using something called a truth table for example the truth table for or shows us that phi or psi is false only in the case where both phi and psi are false of note here is the truth table for implies it's only false in the case where a truth proves a falsehood you might wonder why the bottom two entries evaluate as true well it's our old friend the principle of explosion again in a new and improved form if you assume a falsehood you can prove anything therefore if phi is false then the expression automatically evaluates as true evaluating quantified predicates isn't much harder say you want to work out the truth value of for all x px the way you do this is to look at every element of the domain and see if px is true or equivalently if x is in the set assigned to p by the structure if so for all x p x is true if not it's false there exists an x such that p x works the same way where so long as there's one element of the domain in the set p then you're good to go for example if we set p as x plus 1 equals 2 then over the domain of integers there exists an x such that p x is true but for all x p x is false an interesting aside here is that certain works have the same truth tables despite being made of different connectives take not phi and not psy if we put the truth table for not phi or psi beside it we see that they're the same if this happens we say that the sentences are functionally equivalent another example of truth functionally equivalent worths are phi implies psi and not phi and not psi although we can't use truth tables for quantifiers a similar relationship holds for there does not exist an x such that p of x and for all x not p of x in essence we can push the not sign into the expression and change the quantifier this will become important later using ideas like this it's possible to formalize certain parts of math such as group theory within first order logic since we can interpret predicates however we like it usually isn't very useful to prove general things about all predicates more interesting things start to happen if we assume certain statements and only look at structures in which those statements are true these statements as well as the things you can derive from them are called a theory a theory a model of a theory is any structure in which all of the statements in that theory are true hence we arrive at the notion of an axiomatic system assume axioms and see what happens in other words around and find out you [ __ ] around with theories and find out with models if this is hard to get your head around hang on a bit and we'll look at an example in a little while while you're constructing a theory you're allowed to define certain special predicates with desirable quantities and these predicates can be assigned their own unique symbols for ease of interpretation the extra symbols used by a model are called its signature these aren't standard symbols of first order logic but we can use them in place of instances of symbols of first order logic for example let's take the predicate a of x and y and assume that a of x and x is always true if we also have that whenever x and y satisfy a then phi equals phi prime for any sentence phi where phi prime is obtained from replacing every occurrence of x in phi with y then a is what's known as logical equality this represents the idea that if a of x and y holds then whenever x shows up we can replace it with y and the truth values of whichever sentences we've put it in will stay the same it's the formal counterpart to the mathematical idea of the equals sign and a of x and y is often notated as either x equals dot y or simply x equals y the dot is meant to make it clear that this is just another predicate symbol be it one with some special qualities i'm gonna stick to the undotted version also from now on i'm going to invoke x equals y with this being understood as a special symbol of first order logic with the above axiom taken for granted bear in mind that these are models of maths and are different from actual maths there may be many different models which satisfy a given set of axioms also the syntax is common to all of first order logic it's the semantics which makes the models work syntax and semantics are two completely different things most of the time sometimes foreshadowing is relatively obvious now i'd like to introduce two important logical participles soundness and completeness from now on when i talk about a theory proving something what i mean is it can be proved in first order logic with the axioms of the theory as assumptions a theory that is sound has the property that anything it can prove is true within any model of that theory in most theories inconsistency implies unsoundness as both phi and not phi cannot be true a theory proving both of them means that the theory has proved something false which is capital b bad there are theories in which this isn't necessarily true and those theories are super interesting but they're a bit beyond the scope of this video completeness on the other hand is a property of an entire logic it states that if a sentence is true in every model of a theory then the sentence can be proved from that theory we'll call this definition semantic completeness as it deals with only the semantics or truth values of sentences there is another definition which we'll get to in a moment you might recognize these from the opening of the video but i'd say just slow down we'll get there when we get there it's really easy to make a sound theory in predicate logic it turns out that if you assume no axioms the resulting theory is sound i'll put the proof on screen but the details don't really matter all that matters is it's very easy to make sound theories it's also very easy to make a complete theory take as an axiom phi and not phi for any sentence phi the principle of explosion tells us that from this we can derive anything we like including all true sentences of course we get all the false ones as well but completeness doesn't say anything about false sentences all that matters is we can capture all the true ones it's malicious compliance this is why the blacksmith says of course and there is nothing simpler at the beginning of the video because of course you can create sound theories and there is almost literally nothing simpler than creating a consistent one the difficulty comes if you want to find theory that is both sound and complete and as it turns out both propositional and predicate logic are sound and complete this is not an easy thing to prove and indeed the completeness of first order logic was only first proved midway through the 20th century by a certain mr kurt girdle so if both propositional and predicate logic are sound and complete where does incompleteness come into it well remember how i mentioned there's another definition of completeness well here it is it's called syntactic completeness and it states that for every well-formed formula phi either phi or not phi can be proved within a theory and it's this property that arithmetic is unfortunately lacking having finally acknowledged what this video is about we're now going to take a hard left and start talking about something completely different part four plus i paradoxes [Music] the word paradox like a lot of words has several different but similar meanings you have linguistic paradoxes which occur when language pulls traits on us for example the following is a linguistic paradox nothing is better than eternal happiness a ham sandwich is better than nothing therefore a ham sandwich is better than eternal happiness you have scientific paradoxes which are when observations are made which contradict existing theories such as alba's paradox if there are billions upon billions of stars in the night sky then why aren't we being blinded by starlight in every direction and you have the kind of paradoxes we're interested in the logical paradoxes these are statements which logically contradict themselves in some way perhaps the most famous logical paradox is the liar paradox [Applause] that was easy i'll be honest we can render this in propositional logic as simply p implies not p as if the sentence is true p then the sentence is false not p assuming p we derive not p by modus ponens and so by the principle of explosion our theory is inconsistent as we can derive everything this shows us that you can't derive the liar paradox in a consistent theory one could make the argument that the liar paradox is the only true logical paradox and all other logical paradoxes are just different statements of that one paradox imagine a hairdresser who cuts the hair of only the people that don't cut their own hair should she cut her own hair if so then she cuts her own hair and so by her logic she cannot cut her own hair but if not she does not cut her own hair and so she may cut her own hair this is called russell's paradox and once again it comes down to p implies not p in this case p is the barber cuts her own hair except when russell found it it was lurking in the depths of set theory and he was too late to save it pouncing and devouring one gotlob frega we also have quine's paradox is false when it follows itself being quoted is false when it follows itself being quoted this is a sentence which cannot be true as if it is true then it must be false since it has the structure which it asserts makes it false you might feel like this is closer to being a linguistic paradox and you're not wrong but quene's words echo through the proof of the incompleteness theorems in surprising ways so it's worth mentioning here all three of these paradoxes arise due to self-reference the liar paradox directly asserts its own falsehood russell's paradox disallows certain kinds of sets and quine's paradox mirrors its own internal structure to give rise to a contradiction finally let's look at something which claims to be a paradox and see if it really is this is richard's paradox which is spelt richard but pronounced richard because he was a frog right down in the list every english phrase which unambiguously defines an arithmetic property for example is divisible by only itself and one would be on the list as would is the sum of three cubes but apple incorporated would not be on the list if we number the list it may be the case that the number of a property has that property for example if is an even prime was the second member of that list then it would have the property it expresses since 2 is an even prime whereas if is divisible by 5 was the third member of the list then it would not have that property since three is not divisible by five call numbers which don't have the property assigned to them are richardian in my earlier examples three would be richardian but two would not be now as being richardian as a property of integers it belongs on the list if k corresponds to the property is richardian then is k richardian if so by definition it is not if not then by definition it is is this a liar paradox again well not quite you see i slipped something past you i deceived you you fools why did you think you could trust me i am loki goddess of being a richardian is not an arithmetic property of integers it is a meta-mathematical property and so should not be listed at all you can think of it this way two plus two equals four is an arithmetic truth but the word represented by the symbol two contains three letters is not two is richardium is closer to the second than the first as it describes the property of two which cannot be expressed in arithmetic and so we can't count it among the arithmetic properties hence we can use the word meta-mathematical is richardian is a property about mathematics rather than of mathematics the greek word meta as in metaphor means above or over and in that sense being richardian is a property over arithmetic rather than in arithmetic if we were to expand the list of allowed statements to include meta-mathematical things like israe chardian then we open the door to all kinds of trouble including an infinite chain of false statements one of which must be true but what if there was a way to make israeli into an arithmetic property then it would have to appear on the list and some version of richard's paradox would apply in order to do that one would have to show that meta mathematical properties of numbers could correspond to arithmetic properties but how part five what happens when you give numbers numbers do you remember when we first met it wasn't long ago we'd both been invited to the same party by different people and as we sat alone at the bar our eyes locked i could tell you were interested but neither of us were willing to make the first move until finally i leaned over to you and over the humming throb of the music whispered did you know that you can formalize certain areas of mathematics using theories and models of first order logic at the beginning of the 20th century a mathematician by the name of david hilbert of hilbert's system fame wanted to go one step further he wanted to find a complete formalization of all of mathematics he wondered if you could find a finite set of axioms from which every single mathematical truth would follow to this end he founded hilbert's program which aims to do exactly that find some way to represent mathematics in terms of a formal language for which rules could be provided to generate proofs beginning in 1910 bertrand russell and alfred north whitehead published a three-volume work called principia mathematica which aimed to satisfy hilbert's program by laying out a complete and rigorous formalization of the very basics of mathematical thought we will find out in a moment whether or not russell and whitehead were successful in their aim to formalize all of mathematics and whether hilbert's program was indeed concluded with their work but for now let's turn our attention to a relatively small part of mathematics namely arithmetic when girdle was working the closest thing he had to a complete set of axioms for arithmetic the field of maths associated with positive whole numbers being manipulated by elementary operations were the piano axioms these simple statements of logic seemed as though they might be comprehensive enough to allow us to derive every arithmetic truth the axioms are pretty dry which is why in order to spice things up a little i've decided to rank them but before we get into that i need to set the scene as we'll be meeting some familiar symbols in new contexts piano arithmetic uses all of the standard symbols of first order logic plus four special ones less than or equal to plus times and successor the less than or equal to symbol is a predicate as discussed earlier whereas the successor is a unary function which means it takes one input and points to one element of the domain and plus and times are both binary functions which means they take two inputs and point to one element of the domain strictly speaking we don't need custom symbols for them as their properties will be defined in the axioms we could if we wanted simply notate them p f1 f2 and f3 respectively but it's easy to understand what the axioms mean when they're filled in with familiar symbols plus we aren't breaking any rules by doing it so why not we also have one constant symbol which we notate a zero bar the idea behind this is that we're giving zero bar properties of zero but in order to distinguish it from the number zero we add the bar over the top to reinforce that it is in fact still a symbol it's a bit like the dot over the equals sign from earlier reminding us that this is just a symbol and any properties it may have will be given in the axioms rather than inherent to the object itself it's axiom time baby that's so stupid we are going to rank the 13 piano axioms 30 30 13 13 piano axioms some formulations often have fewer some formulations of them have more i've split them up into 13 for the purposes of making it very clear what each axiom is doing and i will be ranking them based on more or less just how i feel about them there's no rhyme or reason to this except for number one which has been chosen for a very specific reason now before i begin i should explain the three different colors if i'm writing in red i'll either be defining the properties of the zero symbol or of the greater than or equal to symbol hi future me here in the editing bay just to say that i mean the less than or equal to symbol apologies for any confusion caused i'm gonna get it right from here on out i promise you also i only realized that the whiteboard wasn't in focus after i'd finished filming everything i really can't be bothered to go back and film it all again so instead i'm going to edit clean versions of each axiom on screen as they're introduced in the video which should hopefully make things easier to understand back to the video if i'm writing in black i will be defining the properties of the addition symbol and if i'm writing in blue i will be defining the properties of the multiplication symbol got that okay let's hit the road with the very bottom of the list crashing into last place in number 13 we have this property of the less than or equal to symbol which says that if x is less than or equal to y it is also the case that either x is y or the successor of x is less than or equal to y so this is basically just allowing for the equals sign the the lower line in the symbol if we didn't have this axiom then we could define it to simply be the strictly less than symbol but because of this equals clause here we get the less than or equal to symbol instead what's next in at number 12 we have this property of the successor function which i forgot to add to my key but we're going to lump in in black with the and symbol this basically says that if the successor of a number is equal to the successor of another number then those two numbers are the same it's a fairly standard property of equality and we define it here to give some rigor to the successor function and to equality this is mostly a workhorse axiom we've yet to get to anything really interesting i think so let's move on to number 11.

[01:01:15]at number 11 another workhorse function defining an essential property of the less than or equal to sine which says that if x is less than or equal to y and y is less than or equal to x then x must be equal to y these are just defining standard properties of the symbols at this point again things will start to get interesting soon i promise you i'm trying to do this bit just to liven up what would otherwise be me narrating a list of axioms so uh on to number 10 number 10 is where i think we start to get some of the interesting axioms because we've now defined one of the many properties of zero which says that zero is less than or equal to every number now when i write the x here when i say all x we are quantifying over the domain of numbers or numerical symbols so what this is saying is that if x is a number then zero is less than or equal to x pretty cool property not the last we're going to see of zero for sure number nine marks the first appearance of our blue pen which says that if you multiply any number by zero the result is zero very standard property of zero cool we get to define it like this let's move on in at number eight the first appearance of the black pen defining the mirror property of zero for multiplication for zero for addition which says that if we add zero to any integer we get that same integer this is because zero is the additive identity of the group of integers what does that mean well it means that if you add it to any number you get the same number back it is identity it is it defines an identity you get the picture number seven is the final zero axiom it says that no number comes before zero we're not including negative numbers because negative numbers make life very difficult when you're trying to define arithmetic um there are there are ways to do it you can formulate group theory using a different set of axioms and use that to define inverse elements for the additive group of the integers those work as negative numbers we're not going to worry about them here for now just take it this is an axiom just take it that zero is the first number it is the first number it was there before all the others it's also interestingly the only numeral we need because we can just use the successor function iterated on itself over and over again to define any number we like but i'll talk more about that later number six the transitive property of the less than or equal to sine says that if x is less than or equal to y and y is less than or equal to z then x is less than or equal to z as well this defines what we call an ordering on the set of integers it's this property that allows the less than or equal to symbol to have all of the nice features that we expect it to have like bigger numbers should be less than smaller numbers other way around like smaller numbers should be less than bigger numbers things like that this is a very cool property very neatly defined and yeah number five either x is less than or equal to y or y is less than or equal to x has to be one of the two one of them's got to happen which one who knows all this axiom says is that one of them has to obtain this makes sense right because if we have if we have two and we have three then we can't say oh two isn't less than or equal to three but three isn't less than or equal to two by our understanding of the less than or equal to symbol one of them has to obtain this is the axiom that allows that to happen coming in at a very respectable fourth just shy of the podium still not bad at all for all x x is less than or equal to x this this makes sense two is less than or equal to two because two is equal to two equal to implies less than or equal to that conforms with our understanding i'll edit that not sound better we have arrived at the podium and immediately i'm faced with a problem because i can't decide between third and second place because they define basically the same property for addition and for multiplication correspondingly and here they are addition x plus y plus one is equal to x plus y plus one two plus three is equal to two plus two plus one likewise x times y plus one is equal to x times y plus x five times seven is equal to five times six plus five and with that there's only one axiom left or is there because in number one the pole position the gold medal we have the induction schema now this is an especially tricky axiom because it is actually an infinite set of axioms so to explain in further detail i'm going to pass you over to future me on the bed over to you while almost all of the axioms of piano arithmetic can be written in first order logic plus some extra symbols in the signature there is an exception there's a principle in mathematics called induction you know if a unary predicate of integers is true for naught and its truth for some number k implies its truth for k plus one then every positive integer satisfies that predicate the way we express that in logic requires us to assert that any predicate which obeys this rule holds for all x in our domain but we aren't allowed to quantify over predicates and first order logic so if we want to stay in the first order we need to create an infinite set of axioms one for each unary predicate which says that if it has this property or these two properties required for induction then it holds for every element of the domain you may be a bit worried that we're having to invoke infinity here but it turns out we actually don't have anything to worry about because the infinite set of axioms that we have is countable and recursively enumerable recursively enumerable simply means it can be listed by an algorithm and countable means there's a bijection between it and the natural numbers there's a great resource video on the different kinds of infinity which i'll link in the card up there the key fact of these axioms is that they use finitely many symbols and as such there are only finitely many symbols you need to use to express any proposition of arithmetic and it's this combined with many other things that allows us to break mathematics wide open as there are finitely many symbols in first order logic we can assign each symbol a unique number note that there are infinitely many ways to do this but the way we're going to do it is adapted from the lecture notes on the course i took on this material to represent symbols unique to arithmetic in this case plus times and less than or equal to we're going to use this tick operator and put it next to either the function symbol or the predicate symbol this means that plus will be rendered as f prime times will be rendered as f double prime and less than or equal to will be rendered as equals prime we might also like to have number symbols other than zero to do this we represent the number symbol n by the number symbol 0 followed by exactly n successor symbols using this it's possible to assign each collection of symbols a unique number as well by simply concatenating the numbers of the individual symbols i keep stressing this uniqueness factor because it's very important in logic that every logical theorem should have a unique way of being understood there should be no syntactic ambiguity there is a theorem of logic called the unique readability theorem which states that this is the case and we want to preserve it under our map of girdle numberings in this way every base 13 number containing no zeros corresponds to a collection of symbols of first order logic however not every collection of symbols will be well formed in the case that the string of symbols is well-formed we call the number corresponding to that string a woof number or rather i will be calling them that i don't believe this is standard terminology i'm going to be a bit sloppy with my notation and allow sentence variables to refer to both sentences and the girdle numbers of those sentences it should always be clear from context whether i'm talking about the sentence or the girdle number associated with it but where possible i'm going to take pains to make it explicitly clear which one i'm referring to in this way every woof has its own unique girdle number whether that work is true false or otherwise examples are shown on screen one final point to note is that we may wish to encode sequences of woofs the way we do this is with our hash symbol we take each woof add a hash after it and then concatenate them all together if we then take the girdle number of this the result is the worth numbers of each individual worth broken up by the girdle number of our hash symbol which otherwise will not appear in any worth this way we ensure that each girdle number of a sequence of works cannot correspond to the girdle number of a single worth for those of you keeping track at home the girl numbering map from the natural numbers to sentences of logic is injective but not surjective part 5.1 girdles first aha i knew it who are you wait you can hear me yes you aren't meant to be able to hear me i've been able to hear you this entire time no i mean you're going to edit me in later i'm recording this on a different continent to you right now that doesn't change the fact that i can still hear you but i can't hear you wait then how are you talking to me i'm following the script you gave me very meta anyway if we're done here not yet i still don't know why i can hear you katie this bit's gone on long enough why don't you ow that hurt huh so if i hit myself you feel it yeah so don't do it again you dick but if i'm following your script how did i feel that pain i don't know all right just carry on with what you were going to talk about and leave me out of it it may not be immediately obvious but girdle numberings are extremely powerful as an example let's look at a few metallurgical properties of woofs and see if we can express them using girdle numbers first of all let's consider the property the woof phi is 5 characters long there is absolutely no way to express this in only the language of first order logic however if we assign phi a girdle number then the length of phi is related to the length of the girdle number of phi which in turn is expressible as an arithmetic property of the girdle number of phi in this case that the girdle number of phi is between 13 to the power of 4 and 13 to the power of 5.

[01:12:59]we can then express this as a woof of first order logic as shown for another example let's look at a syntactic property of phi namely the worth phi is a negation we might try something along the lines of there exists no worth phi such that psi is equal to the negation of phi but this is not allowed since we can't quantify over sentences in first order logic instead note that phi must begin with a negation symbol if it is to be a negation therefore the girdle number of phi must begin with the girdle number of the negation symbol which in this case is a one this can then be expressed as a numerical property of the girdle number of phi as shown here we've had to invoke knowledge of the length of phi but from our first example this can be demonstrated within first order logic so we don't need to worry about it too much this property may also be expressed as a woof of first order logic note that this generalizes very easily to the woof fi beginning with an arbitrary character and we can also extend it to the woof five beginning with an arbitrary collection of characters although this is a little more complicated this can generalize further to allow us to express properties of whether or not works contain certain symbols at certain locations as before we can generalize this even further to the wifi has an arbitrary collection of symbols beginning at an arbitrary position and this is extremely significant oh i get it i'm like the semantics and you're like the syntax normally the relationship only goes one way but under the right circumstances you can affect me sort of the syntax and the semantics are to a certain extent already in that relationship that's soundness and completeness but what we've shown is that we can transform the syntactic rules of the system into arithmetic rules for the girdle numbers which means we can express both syntactic and semantic claims in terms of properties of the girdle numbers i guess it's more like you're the theory and i'm the girdle numbers well i'm glad we've sorted that out can i go now yeah sure go ahead you owe me 75 pounds for this by the way you volunteered these are just a few examples of metallogical properties being converted into arithmetic properties of the girdle numbers of sentences these have been included to be illustrative they are not comprehensive and i have skimmed over a lot of detail here but i just wanted to give an overview of some applications of the girdle numberings using the techniques i've illustrated it's also possible to arithmetize the statement that a sequence of works begins with a given worth or contains a given worth in an arbitrary position in that sequence this will also be very important momentarily the natural question is then are there more properties that can be arithmetic using girdle numberings and the answer is a resounding yes there are try this one on for size x proves y i.e there is a proof of the wolf y which uses only the wolf x as an axiom i'm switching away from greek letters for my own sanity note that this is sufficient to cover all axiomatic systems including ones with multiple axioms as a set of axioms can be formed into one conjunct which can be pruned as necessary for example if the set x x1 proves y then x and x1 also proves y i'm going to take it as read that it's possible to remove conjuncts because it will make my life easier recall that we can encode the sequence x y as x y and the theory has a finite set of deduction rules in a hilbert system one which operates syntactically if we take as our axiom x then a proof of y from x is given by x hash z hash y where z is a sequence of words representing the deductive steps to get from x to y we can use our sequence begins with x and sequence ends with y from earlier to check that the sequence really does begin with x and end with y as we have a finite set of deduction rules we can also check the girdle numbers of the elements of z to make sure that they are either axioms assumptions or can be deduced from them using set deduction rules using modus ponens as an example to check if a girdle number corresponds to x implies y all you need to do is show that it begins with x ends with y and has an 8 in between we can therefore render the statements x proves y as a property of the girdle numbers of x and y this is huge and gives another sense of the power of girdle numbers as to formalize the notion of an arithmetic proof within arithmetic itself is hugely significant we'll write proves x y for the word corresponding to the assertion the sentence with girdle number x proves the sentence with girdle number y ie x proves y and for a set of assumptions s we write proves sub s x y for x proves y assuming s note that this can be true or false it's simply a statement saying x proves y it doesn't mean that x does prove y remember that we capture false statements as well as true ones with girdle numberings using this we can now state in more general terms the idea of provability and unprovability in piano arithmetic there exists an x such that proof sub p a x y means y is provable in piano arithmetic likewise for all x it is not the case that proves sub p a x y means y is not provable in pa now i said earlier we couldn't range over wolves but what we can do is range over the numbers which represent the woofs under our girdle numbering this is like the one weird trick that doctors hate except for logic also note that we can formalize the opposite of y is provable in pa by combining proves pa with z is the negation of y which we showed earlier i will notate this as proves sub pa x not y which is an abuse of notation but i do not care we also want some manner of self-reference remember that the paradoxes from earlier all relied on being able to assert things about themselves so let's define a new predicate p r sub p a x y short for proof recursion this is true when x is the girdle number of a formula x a with one free variable and y is the girdle number of a proof of x x this means that we are feeding x its own girdle number and then trying to prove it i know it's weird but go with it this self-substitution operation is also definable within piano arithmetic it simply says if the kth digit of the girdle number of a worth is equal to b then replace it with the numeral representing the girdle number of that worth we then combine it with proves sub pa to get the desired result this allows us to craft sentences which can assert things about themselves for example this statement is three characters long corresponds to the guidel number of this statement is three digits long from earlier we defined x is three digits long as a predicate zx in piano arithmetic with girdle number z and then we can consider z of z which is false we now have everything we need to formulate incompleteness and first order logic now i'm not going to be following girdle's original argument i will instead be pursuing ross's amended version of girdles and completeness theorem which makes it a little more obvious where the contradiction lies however i will just take a moment to lay out what girdle did girdle's girdle sentence expressed that it was only provable if it was false which if you'll remember is a capital b capital t bad thing this is what i was talking about at the very beginning of the video someone the girdle sentence exists who if they are your enemy true cannot be killed by your sword cannot be proved in the theory and if they can be killed by your sword can be proved in the theory then they are not your enemy false our argument is adapted from alec fisher's formal number theory and computability which is a great book and i highly recommend it to anyone who's interested in this area what we're going to do is formulate a sentence which asserts its unprovability within the theory and then adds something to it and then we're going to show that if we can prove this sentence it implies some bad things about the consistency of arithmetic it's easy to create a woof saying that x cannot be proved within pa from before for all y it is not the case that proves sub p a y x corresponds to x is not provable let's make two slight amendments to this statement let's replace proof sub pa with p r sub p a and add in this additional clause now the wolf says either x of x is not provable or there exists a proof of the converse of x of x or in other words if x of x is provable then so is not x of x let's call this worth g of x noting that it has exactly one free variable x as this is a woof it must have a girdle number let's call this girdle number lowercase g now let's take g of g and this is the sentence which breaks maths from a metallogical perspective this sentence means either this statement is not provable or you can prove the opposite of the statement intuitively you can see the contradiction if you can prove g of g then you can prove not g of g which violates the assumption of consistency however this isn't a formal proof and i can't give you a formal proof the best i can do is a neat little animation showing you fish's argument which is a little more rigorous than what i've presented but still not quite as formal as formal logic demands it's going to use everything we've talked about so far in particular the functional equivalence relations i brought up during my talk about semantics if you're interested in following along pause and stop as necessary the full proof will be on screen at the end of each section so sit back and enjoy the first incompleteness theorem [Music] foreign [Music] lord uh [Music] foreign [Music] [Applause] this is pretty bad but don't worry it gets worse before we begin one thing to note while the first section is still fresh in our minds for all x a x implies for all x a x or b x this is important because the latter half of this is the form of g of g therefore if we can prove the first half of this statement then we will have proved g of g by disjunction we showed before was that if piano arithmetic is consistent then gfg is unprovable both parts of this statement can be formalized inside of piano arithmetic using girdle numberings remember from earlier that an equivalent condition for consistency is that there is at least one well-formed formula of the language that is unprovable so let's take one equals naught as that thing and consider the formula one equals naught and x equals x this is a formula with one free variable x let's call this formula c of x with girdle number c [Music] consistency is then equivalent to saying that there is no proof of c of c within piano arithmetic which can be formalized using our proof recursion method we also have g of g as unprovable as simply for all why it is not the case that p r sub p a g of y therefore we may formalize our earlier argument as follows now let's think about what would happen if we could prove that piano arithmetic is consistent using only the axioms of piano arithmetic if this were the case we'd be able to prove the first half of our implication on screen but then we'd be able to use modus ponens to deduce the second part but from earlier notice that the second part implies g of g since we proved earlier that you can't prove g of g within piano arithmetic it follows that you can't prove the first half of the implication which means that you can't use piano arithmetic to prove that piano arithmetic is consistent to put it another way we would only be able to prove piano arithmetic is consistent if it isn't it would be remiss of me not talk a little bit about some common misconceptions about the girdle theorems for example something that's commonly said about them is that you require a system stronger than piano arithmetic to prove piano arithmetic's consistency this is not true gerhard gensen showed that piano arithmetic is consistent if you assume the consistency of another system which is no less or more powerful than piano arithmetic so when people say that piano arithmetic requires a stronger system to prove its consistency that's not quite true furthermore and this is a detail i kind of skipped over for time all the guidal theorems state is that if you have a system whose axioms can be listed algorithmically then it must be incomplete it says nothing about the completeness of systems whose axioms can't be listed algorithmically and so for that reason while hilbert's program might have failed mathematics as a whole has nothing to fear and some great things came out of hilbert's program his prokipia mathematica though flawed contributed some great ideas to the development of logic in the latter half of the 20th century so it definitely wasn't a waste of time and we certainly shouldn't set fire to it actually hang on [Music] foreign [Music] and just in case you were worried i would actually burn a copy of principia mathematica it's just this instead and although arithmetic has proved particularly difficult to formalize we have very good formalizations for other areas of mathematics for example zf set theories a melee franco set theory is very good and forms the basis for a lot of ongoing efforts in formalization and axiomatization to this day so there's absolutely nothing to worry about you can stop worrying please people stop saying maths is over maths is not cancelled cancel culture has not come for maths yet it will especially when it finds out like two of the most prominent logicians in the field were just nazis warning we are about to enter the opinion zone everything from this point onwards is merely my own opinion and you should feel free to agree or disagree with it at your leisure you have been warned one final comment just because it annoys me slightly when people do this people love to bring up the girdling completeness theorems as an example of why human brains could never be modeled by computers roger penrose has written over two books on this matter and i just don't see it like sure maybe human brains can't be simulated by a computer we may never know the chinese room argument is a great rebuttal as to why not but i don't think you can say uh just because some things in arithmetic can't be proved within finitely within um recursively enumerated axiomatized systems then human brains can't be simulated by a computer it it just it doesn't follow and like i get their arguments so for those of you who haven't read the material i'm skimming over quite a lot here people make the argument that girdles and completeness theorems show that you can't prove everything using formalized systems of arithmetic which is wrong as i've just said but we move on then people say but humans can prove metal mathematical results about formal systems therefore humans are better than computers because apparently computers can only prove things in axiomatic systems that's why algorithmically innumerable axiom sets are important because we love computers we like computers to be able to check our work and there are many many programs out there that run theories of logic on them and can tell you whether they're consistent whether they're complete whether certain things can be proved in them but i don't think you can take that to mean that human brains are necessarily something other than fuzzy biological computers but anyway i've gone off script here there are many better videos and essays and video essays about this than the one i'm currently making and this has gone on long enough already so all that remains is for me to thank everyone who's contributed to this video their names were listed at the beginning go back and check them out if you haven't already and to say thank you for sticking with me this has been the biggest thing i've ever done and i hope something comes of it even if it's not in this summer of math exposition maybe in the future i'd love to come back and talk a little bit more about formal logic so if you'd like that like subscribe leave a comment it feels weird to say this is the first time i've ever said it but um yeah i hope you enjoyed bye