WARNING: Summaries are generated by a large language model and may be inaccurate. We suggest that you use the synopsis, short and long summaries only as a loose guide to the topics discussed. The model may attribute to the speaker or other participants views that they do not in fact hold. It may also attribute to the speaker views expressed by other participants, or vice versa. The raw transcript (see the bottom of the page) is likely to be a more accurate representation of the seminar content, except for errors at the level of individual words during transcription.

Model theory explores the relationship between formal proofs and truth, connecting formalism and mathematics. It uses a first order language of one sort, one constant, one function symbol and no relation symbols to attribute meaning to objects. Natural deduction proof systems are used to demonstrate the uniqueness of group identity and interpretations consist of a domain, functions and relations. The Ax-Grothendieck Theorem and Lowenheim-Skolem Theorem are examples of applications of model theory which connect abstract ideas and practical constructions.

Model theory explores the relationship between formal proofs and truth, connecting the two universes of formalism and the platonic universe of mathematics. Syntax, language or logic is the tether between the two worlds, allowing access to the concept of truth in the platonic universe. Will and Billy are discussing the importance of storytelling in philosophy, foundations and mathematics, and Will has been working hard on a proof of the Ax-Grothendieck theorem. This camping-like campfire moonlit forest experience is intended to be a cozy and approachable place to learn about foundations.

A first order language consists of one sort, one constant, one function symbol and no relation symbols. It is used to attribute mathematical meaning to objects and can be treated as a mathematical object itself. Function symbols have an arity and a type, while relation symbols have an arity but no type. Variables have the type of the variable, while function application has the type of the function symbol. Formulas are constructed inductively using terms and relation symbols, and also using quantification, conjunction, implication and negation. An example of a first order theory is the first order language of groups which consists of one sort, the constant zero, the function symbol plus and the axioms x + 0 = x and x + y + z = x + z + y.

The language of building groups is interpreted as a set with function symbols representing functions. Natural deduction is a proof system which allows for the deduction of a conclusion from two premises. It is distinguished by its use of superscripts to denote discharged hypotheses, where an assumption can be made and then later confirmed in the proof. Billy has written a natural deduction proof to demonstrate the uniqueness of group identity, which is important to be able to read proofs like these.

An interpretation of a first order language consists of a domain, functions and relations for each symbol, and an evaluation which assigns variables an element of the domain. Terms are interpreted by applying the evaluation to the variable and predicates are interpreted by applying the evaluation to the arguments. Quantifiers are used to express logical statements and a model is an interpretation where all the axioms of a first order theory evaluate to one for all evaluations. Equality is interpreted as the interpretation of one argument being equal to the other, bottom is interpreted as zero and a junction is interpreted as one if and only if the interpretation of both arguments is equal to one.

Equality is used in two different ways in mathematics, a syntactic formation rule that combines terms to form a formula and a platonic world concept that states if an interpretation is provably equal to another in a first order theory, it evaluates to one. Ambient mathematical truths can be interpreted in different ways and topos theoretic approaches can provide more illumination. The right theory can be lifted from the left theory to explain what is sufficient grounds to deduce that the thing on the left is equal to one. This is done by writing down s equals t in the first order theory of sets, a shorthand for a logical statement, which implies that the two sets are equal.

The Ax-Grothendieck Theorem states that any algebraic closure of a finite field is a finite field, and is proven using the Lowenheim-Skolem Theorem. This theorem states that all first-order theories of algebraically closed fields of different characteristics are complete. The X Growth Index Theorem states that if a polynomial, f, is injective from n copies of the complex numbers to n copies of the complex numbers, then it is also surjective. This is proved by reducing the statement to a simpler case by proving it in the case of non-zero characteristic. Model theory is a field which connects abstract philosophical ideas and practical mathematical constructions.

The theme of the new experience is a camping-like campfire moonlit forest, intended to be a cozy and approachable place to learn about foundations. It is reflective of the activity of doing mathematics and reasoning, like a conversation at night around a campfire - reflecting on activities of the day, making arguments rigorous, and telling stories. Will has been working hard on a proof of the Ax-Grothendieck theorem, and both Billy and Will wish to explore and talk about the importance of storytelling in philosophy, foundations and mathematics.

Model theory is the relationship between formal proofs and truth. It is the starting point for discussing what truth is. There are two universes: the world of formalism and the platonic universe of mathematics. Inside the platonic universe is the concept of truth, which is accessed via formalism. Syntax, language or logic is the tethering between the two worlds. Model theory is the core topic of the lecture, exploring the relationship between formal proofs and truth.

A first order language consists of a set of sorts, a set of function symbols and their associated arity. This language is used to attribute mathematical meaning to and can be treated as a mathematical object itself. This can be applied to algebraic geometry and used to create a formal theory. The speaker then presents a perspective on this sentence and provides an ultimate perspective on the ideas introduced.

Function symbols in a first order language have an arity and a type, while relation symbols have an arity but no type. There is a countably infinite set of variables, and terms are constructed inductively using variables and function symbols. Formulas are constructed inductively using terms and relation symbols, and also using quantification, conjunction, implication and negation. Terms have types, and variables have the type of the variable, while function application has the type of the function symbol.

A first order language consists of one sort, one constant, one function symbol and no relation symbols. A first order theory is a first order language, along with a collection of formulas which are the axioms of the theory. An example of a first order theory is the first order language of groups which consists of one sort, the constant zero, the function symbol plus and the axioms x + 0 = x and x + y + z = x + z + y.

A first order language of building groups is used to describe a set of axioms and formulas. To map these onto genuine mathematical meaning, the language is interpreted as a set, with function symbols representing functions. This is the formalism part of a diagram that also includes meaning, proof and truth. Proof is the simplest possible concept, being a sequence of sentences inside the language that follow a set of predetermined rules for valid deduction.

A proof system is a way of witnessing relationships between collections of premises and conclusions. An example of such a relationship is the for all elimination rule, which states that if a statement is true for all values of a variable, then the statement is true. Natural deduction is a type of proof system, and Billy has written a natural deduction proof to demonstrate the uniqueness of group identity. It is important to be able to read proofs like these, and the lecturer will go through it carefully.

Natural deduction is a system of logic which allows for the deduction of a conclusion from two premises. The natural deduction system is distinguished by its use of superscripts to denote discharged hypotheses. This means that an assumption can be made, and then if a conclusion is reached later in the proof which confirms the assumption, it can be discharged. An example of this is seen in the transcript, where an assumption is made that b times c is equal to e, and then later in the proof it is shown that this is true. This allows for the substitution of b times c for a in the conclusion.

An interpretation of a first order language consists of a set (the domain) and a function and relation for each respective symbol. An evaluation is also required, which is a choice of where the variables of the language go.

Evaluation is a function from a set of variables to a domain, which is used to interpret terms and formulas in a first order language. Variables are parameterized by a single sort and evaluation assigns each variable an element of the domain. Terms are interpreted by applying the evaluation to the variable and predicates are interpreted by applying the evaluation to the arguments. Equality is interpreted as the interpretation of one argument being equal to the other, bottom is interpreted as zero and a junction is interpreted as one if and only if the interpretation of both arguments is equal to one.

Quantifiers are used to express logical statements in first order theories. The interpretation of an existentially quantified formula is equal to one if there exists an element in the domain such that when the valuation forces x to be mapped to that element, the formula evaluates to one. Similarly, for all quantified formulas, the interpretation is equal to one if for all elements in the domain, the formula evaluates to one when the valuation forces x to be mapped to that element. A model is an interpretation where all the axioms of a first order theory evaluate to one for all possible evaluations.

Equality is used in two different ways in the board. The first is a syntactic formation rule that states two terms, s and t, can be combined to form a formula s is equal to t. The second is a platonic world concept that states if an interpretation is provably equal to another interpretation in the theory of sets then it evaluates to one. This definition of equality is provably equal inside a first order theory and is taken as the definition of truth.

Ambient mathematical truths can be interpreted in different ways, such as by experimentally verifying them with the scientific method. First order theories can be used to describe more abstract theories, such as those existing in complex topoi. This can be done by interpreting the theorem theories into other theories, allowing for more powerful and sophisticated approaches. This topos theoretic approach is helpful in understanding these theories as it can provide more illumination.

The speaker suggests that the right theory can be lifted from the left theory in order to explain what is sufficient grounds to deduce that the thing on the left is equal to one. It is asserted that the right is an assertion of a concept of the domain of objects, and that there is no ambient means of deduction of that fact. It is suggested that the syntactic proof is constructed by writing down s equals t in the first order theory of sets, which is a shorthand for a logical statement. It is argued that there is more to the picture than just inferring the existence of the proof tree, and that it feels like the statement has been made that the two sets are equal.

X Growth Index Theorem states that if a polynomial, f, is injective from n copies of the complex numbers to n copies of the complex numbers, then it is also surjective. The proof assumes that this is false and that there is a finite proof tree, pi, which disproves the statement. By looking at pi, it is possible to reduce the statement to a simpler case by proving it in the case of non-zero characteristic, which is easier because it can be appealed to finiteness of the underlying field.

Model theory is an interesting field which bridges the gap between abstract philosophical ideas and practical mathematical constructions. In this lecture, the professor discussed the proof of the Ax-Grothendieck Theorem, which states that any algebraic closure of a finite field is a finite field. The proof relies on the Lowenheim-Skolem Theorem, which states that all first-order theories of algebraically closed fields of different characteristics are complete. This proof highlights the potential of model theory in connecting abstract and practical mathematics.

so um welcome welcome to the new the new experience the new world for foundations um so yeah i just want to say a few things maybe explain the theme a little bit um and and how i think it sort of relates to foundations so as you can see it's kind of a camping like campfire moonlit forest uh kind of theme uh what does that have to do with foundations um like a very simple reason i don't know i just kind of wanted it to be a more cozy approachable uh place to learn about foundations but but more than that uh i guess i have to explain like for me when when i'm reading a proof or listening in a lecture i often get uh like distracted by a like i hear some interesting piece of uh logical deduction some interesting argument or construction that uh doesn't necessarily reflect or like uh is not like explained by previous foundations that have been uh like served to me before and i sort of ponder how i can make like such a thing uh like rigorous or like explain something carefully rather than just making a wavy argument and this kind of uh sort of reflection to me is kind of evocative of the kind of conversation you might have uh like at night around a campfire with some friends i don't know reflecting on on the activities of the day what you did what you could do better um and and also telling stories and i think uh this is all uh reflective of the activity of doing mathematics and reasoning and thinking carefully and uh yeah reflecting on the reasoning what we do and what it sort of uh what that reveals about this activity uh of mathematics so um so yeah that's that's the idea i hope that sort of speaks to you in some way um and so will so while i've been preparing this world uh will has been working very hard on uh this proof of uh explaining the proof of the axe groth and dick conjecture oh sorry uh theorem um and so yeah take it away will thanks billy just adding my little two cents there i think that the theme of storytelling and storytelling in no i mean in no condescending way whatsoever is very important when it comes to philosophy and when it comes to foundations and therefore mathematics and this is something that i wish to uh explore and talk about more as this series goes on but that was also reflective of the world around us which is something that billy and i spoke about and that's something i really liked as well so the idea of a campfire and you have night time out camping the idea of telling stories um but meaningful stories stories that help us understand who we are where we are why

are we here etc i think that all relates to philosophy extremely closely okay today's lecture is going to start with the bold question what is truth and i'm going to be extremely biased in the description that i give today towards tasking truth he came up with everything that you're going to well i came up with the model theory that i'm going to present today but the starting point and i'm going to talk very amateurly about philosophy in just one moment uh the following is not quoting some famous book or some famous philosopher instead this is just me as my understanding as to what we do when we do mathematics and we when we write it down and when we talk about it to each other and i want to use this as a starting point for our conversations on the topic of what truth is so i would say that there are at least two relevant universes when we perform mathematics we have the world of formalism inside which exists the notion of proof and then next to it or beside it or identical to it there are many different opinions that you can form would be what i'm going to and yeah i'm like name dropping plato here but i don't think plato haven't discussed anything like this but the platonic universe of mathematics which is where the mathematics exists so i might write down let's x be a topological space but in my opinion that marking of the x that i write down on the page that finger itself is not the topological space that i'm talking about but instead it is some kind of symbol that denotes the real topological space but what is that real topological space where is it where does it exist well the answer to that question is what i'm drawing here is a circle it's this platonic world where we have the theoretical objects that exist in some sense and those are the objects that we talk about when we perform theoretical mathematics and we access them via formalism so inside the platonic universe of mathematics is the concept of truth and then what we have is a tethering between these two worlds which is syntax or language or logic there's a lot of different labels that you can give to this arrow here so in fact i'm going to write one down that didn't mention i'm going to say at the very least there's model theory here which is going to be the core topic of today's lecture and the way that i want us to be thinking about it today is in exactly this way it is the relationship between the formal proofs that we write down and the truth that exists out there in some very hard to define way

okay so the goal is to understand the language that we use to describe mathematics and for today this is going to be first order theories and then i also want to talk about the meaning of those sentences and the proofs that i write down and this is going to be the models now at the end of the lecture i'm going to come back to this and present a completely ultimate perspective that you could give to everything that i've introduced so far so i've been very philosophical i've been very vague i've just been saying to myself i want to understand the universe and i want to use finite language in order to do it but what happens if i go ahead and treat that formalism that i wrote down as itself a mathematical object well i will be able to squeeze out a surprising application of this theory invented here to algebraic geometry but i'm going to come back to that and the statements i've made so far about looking at what we've done as a mathematical object in its own right and using it as an application the perspective that i have on that um that sentence is going to be described in more detail later on in this lecture but to begin with we're just going to consider this concept of having formalism and proof on one hand and then platonic mathematics and truth on the other and see if we can create a formal theory out of it okay do i need to move over here for the orb yeah okay so dan do i have reason to believe that the correct boards are being recorded now these two blank ones yep oh you can't hear me no i can't hear you but i can i heard you say that ah every time i use my ipad i get the voice chat covering the board how do i get the chat to go away okay there we go okay that's what i'm writing so long by the way so i fixed it so i can move on okay i'm going to quickly recall the concepts of first order languages and first of all the uh this is going to be quite hard and fast we covered this very slowly back in uh back in the first season of this seminar series i'll write everything important down and please ask me questions if you want me to explain anything more thoroughly but all that i'm doing here is writing down the rules of the naked empty meaningless language that we're allowed to write down when we which we then want to attribute mathematical meaning to so recall that we have this concept of first order languages and these consists these consist of a set of sorts a b c etc we have a set of function symbols and these have an associated arty so this isn't i'm getting horrible feedback from

somebody's feedback from somebody's bending metal in the background yeah and a wild animal at the same time okay so the function symbols have an arity oh sorry the function symbols have an arity and they also have a type so the notation that i've written down here represents an arrow tn function of type b and then we have a set of relation symbols as well and these have an arity but they do not have a type okay and then we also assume the existence of a countably infinite set of variables for every sort well denote this capital v a for the variables of saute okay and then given the first order language i can construct the terms and the formulas the terms are the easy one so all the variables are terms and then i define the rest of the terms inductively so if i have terms t1 of type a1 up to tn of type a n and i have a function symbol with the right arrow t and the right types inside the domain then i can construct f of t1 up to tn and this is going to be a term of type b okay the formulas are what we can say about the terms so the terms are the objects of the language and then the formulas and the statements we can make about them so if i have terms and a relation symbol where the arrow ts and the types line up then r of t1 up to tn is a formula i also have equality of terms so the states went t1 is equal to t2 t2 is a formula and i need t1 and t2 to have the same type i've got two special formulas which are going to be false and true and these are thought of as the constantly false proposition or the constantly false formula and the constantly true formula okay there are more but i'm moving on to the next board i can also inductively construct formulas from other formulas say given phi and psi formulas i also have phi conjunction psi oh sorry that's this junction and then phi conjunction psi phi implies psi and negation phi are all formulas and then i also have quantification so i'm going to have universal quantification and existential quantification so there exists x of type a phi and for all x of type a phi where x is a variable okay i'm going to say two more sentences and i'm going to pause and look at these definitions and make a few comments about them so just hold on for one more minute if you feel a little bit lost it's just important to realize that terms have types and in the variable case it's the type of the variable and in the function application case it's the type of the function symbol i did mention that there but the important part is that formulas don't

have types but they do have free variables and then terms also have free variables but in in terms every variable is a free variable so it's not really that um interesting the the important part with the free variables is how they work with the quantifiers here so i'll write down the important statement that the free variables of their exists x of type a phi is equal to the set of three variables of all x type a phi which is equal to the three variables of phi set minus this variable which has become bounded by the quantifier and then i'm just going to boldly claim that the rest of their definitions of the free variable sense are obvious more than happy to write any of them down if anyone would like like me to okay that's a very hard and fast introduction to first all the languages does anybody have any questions about that okay so maybe like wait can you hear me yeah i can hear you do you want an example or something complex formula with some yeah saying all i can give you yeah well i can do maybe even one better so i can give you the first order language of groups so the first order language maybe i'll do a billion groups has one source let's call it a and we have one function symbol missions plus and this goes from a squared to a so i'm not being consistent with my notation there right but i think it's pretty clear what i mean so a times a to a and then i have no relation symbols and a definition that i haven't given you so far is what a first order theory is so i've defined the first order language but the first order theory is simply a first order language along with a collection of formulas inside of that language and the way that we think about that is that those formulas are the axioms of that theory right so for the first order language of a million groups i've done that's it whereas for the first order theory of groups i also have to write down the axioms of a million groups so uh remember that i have an infinite set accountable infinite set of variables for every sort right here i only have one sort and so therefore x y z is completely unambiguous these all have to be variables of type a so this is equal to x plus y plus z and then what else do we need x plus zero is equal to x i guess i need to tell you what zero is so let me put another function symbol in and this one is going to be of arity zero which is actually allowed so another way to think about that is they're the constants of the language but you don't need to define constants inside first order theories they sorry

inside first order languages they can just be rit zero function symbols okay um i don't need to say that zero plus x is equal to x because uh these are billing groups so i'll write uh community everything just one moment but i also mean there exists y such that x plus y is equal to zero and then lastly x plus y is equal to y plus x okay so this example kind of has everything for you we've got these formula we've got these axioms just formulas and start the first order theory sorry inside the first order language of the building groups i'm shoving them at the top and the idea is that this doesn't have meaning yet so the next the next point of the talk is to say how can we map these etchings on the board onto genuine mathematical meaning and it's kind of obvious how we won't do that right we just interpret everything so i'm going to take this a i'm going to think about it as a set i'm going to take these function symbols i'm going to think about as a function and i'm going to see whether these hold and that sentence see whether these hold that's where the philosophical muck exists okay so i mean yeah that it's probably worth pointing out that like when you write down uh terms of type or like terms f uh colon a1 times a2 up to a n to b that like so that looks like like the notation you would write for like to say that f is a function there but that's purely notation here it's really just a list of sorts a1 up to a and then b but clearly it's evocative of like the thing that you interpret it as so when we say we've got first order billionaire first order logic sorry the language the first little language of a billion groups when you at plus colon a times a to a uh that's a pure formalism but like what you're about to go into is that it's of course interpreted as the function which we would notate like that that takes in pairs of a's and produces an a okay so what we've described so far is this part of the diagram that i during the start say formalism and if you remember there was arrow arrow there was meaning and then there was proof and truth okay so let me just briefly remind you the notion of proof that billy and i at least are using but there are many different possibilities for this part so we just do the dumbest thing that you could possibly think of right like what's a proof gonna be i have a language well the proof is going to be a sequence of sentences inside that language which follow a set of rules which i decide a priori count as valid deduction right

so you and i might philosophically disagree as to what deductions are allowed and aren't allowed and these are all those famous arguments lie for example do you believe in the epsom of choice do you believe in the law of excluded middle do you believe in the law of contradiction etc um of of though of explicit contradiction sorry um but it doesn't matter because whatever you believe we can all get together and make a decision a priori as to which deduction rules we will allow and then we can just do mathematics inside that system right and then everybody's happy presumably but i don't want to write out all of the natural deduction rules for you now because it takes a long time so instead billy wrote this gorgeous natural deduction proof i i must say i'm most impressed right on the uh first board so maybe i'll walk back over there to move the camera and also we can all have a quick look at it okay so it's really important that you're able to read proofs like these and yes this is this is a proof we've got the statement down the bottom uniqueness of group identity so please ask me a question if you're confused about this but i'll go through it very carefully right at the top and then i'll get more vague as i head down the bottom so when we start off yeah yeah before you get i think you haven't mentioned like i guess the like you said uh you can take any proof system that like does whatever like the uh i think you need to mention that like the the common uh face that all these like the thing that whatever proof system use has to achieve is that it declares some relationship between uh collections of premises and conclusions um so and like the the way this tree is set up is it represents one of those relationships but uh like if you have another proof system it should also have some sense of relationship between uh collections of premises and conclusions and uh so a proof system is just a thing that witnesses those relationships and this is a kind of witness okay so an example of one of these relationships that we have a prior i've decided this valid is this one up here which is the for all elimination rule so the way that we read this first sentence is well it's easy to read for all w it's the case that a times a is equal to a right you can see that w doesn't appear inside the formula but that's fine because what fall elimination does is it says if we know that this statement is true and it's a for all so it's a statement of the of the type for all variable statement

then i can i can pick any sorry yeah yeah so yeah yeah yeah i know it's very weird but it's totally legit right like this is one of the weird things about first order theory like keep in mind i didn't even have a for all right so earlier i wrote x plus zero is equal to x and that was my axiom right so you don't even need a for all if you don't i can just go ahead and be a free variable the reason why is because interpretations range over all um evaluations but yes all right so yes i agree that it's it's clear out you just put this whole w here um but for the experts it doesn't actually matter but yes anyway so now we can substitute this free variable a in so that's just saying what for all you know says that's what we understand it to be and that's the point so a priori we have decided on this deduction rule as being valid where if you have a for all you can remove the for all and substitute a free variable in okay and then you can continue reading the proof right so now we have an equals elimination and this takes in two premises and then gives you a conclusion so here we know that a times e is equal to a and then we're assuming here that if b times c was equal to e well if that's true then that's true but the point is we can just go ahead and substitute b times c in for a that's what the rule equals elimination permits us to do right and so if we do that we just get this conclusion here which is just a times e with a substituted as b times c and then you continue right so the double lines here mean that there are a few emitted steps because these things get pretty big and ugly pretty easily but we're just appealing to associativity there in order to get the brackets over onto the left then we can do another equals elimination and then away we go one thing that's worth mentioning are these superscripts here this is a very special feature of the natural deduction it's a very important difference between the natural deduction system and other systems of logic and you can see that it's pertaining to discharged hypotheses so let me explain what that means in english if we go up to this hypothesis here then you can see that we just introduced that as an assumption we just said if it's true that b times c is equal to the e then what can we do with that right and the reason why we're allowed to do that is because if we come down the proof and look at this part then we're appealing to the axiom that there always exists a multiplicative inverse right so there exists a z such that b times n is equal

to e so if we had such a z for example c then what would we be able to do with it well we would be able to write out this top part of the proof then we'll be able to write out this part of the proof okay but we need some coherent way of annotating when we've performed some kind of substitution like that so the proper term is discharged once we've discharged some hypothesis we need to reference which hypothesis it is that we've discharged or else the proof would be the notation would be ambiguous okay so that's what these superscripts mean does anybody have any questions about proof trees natural deduction or the way that we're going to understand the concept of proof inside this lecture all right let's continue so now for the new stuff we did cover this last time but that lecture got lost to the effort somehow so if you're somebody watching this online in sequence with the uh proof of girdle's first and completeness theorem then oh no it wasn't that was it it was the proof of girdle's completeness theorem then this is the part that you need in order to understand that um but the previous stuff you would have already watched okay to the people that are in the present day what we're doing here is we're going to interpret these formal sentences that we've defined and we're going to come up with a systematic way of doing that okay so let's make some definitions let l be your first order theory do i need a theory no let's just start with the language so let l be a first order language and i'm going to assume for simplicity here that the first order language i'm working with has only got one sort and indeed that's the only case that will be required for the expert in big theorem anyway okay so let me give myself more space we define an interpretation of l to consist of a set i of a so the so the of a here is reflecting that it's just straight to the sort so let me label my sort so we're assuming that l has got a single sort and we're assuming that that slot is labeled a and then part of an interpretation is a set i of a and this is the domain and then for each function symbol we interpret it as a function and then no surprises here for each relation symbol a relation but we'll denote our relations using a the characteristic function of the relation so this is a predicate you might you might know it as okay uh and that's it i believe yes that's it and then on top of this we will need an evaluation which is a choice of where the variables inside our language go so

i've told you where all of the big pieces go but we need to look at the particular choices the possible particular choices of variables evaluation over l in the set d so these things can exist outside the context of an interpretation although i will only be using it inside that context so d here will be arbitrary but later it's going to be i of a for some interpretation a okay is just a function from the set of variables to d right so remember that i told you earlier that to every sort we have an associated countably infinite collection of variables and they were parameterized by the sorts but there's only one sort here so i can just go ahead and write v and evaluation is just a function from that set of variables into the domain so it's a choice of what these variables represent right and then once you have an uh an interpretation you can then extend the interpretation to all of the terms and all of the formulas inside your first order language so extend two terms in the following way interpretation sub new oh i guess i need to keep it all precise here so nu now is going to be set in the um domain of the interpretation so v is a valuation over l or i guess it's of l over the interpretation of a okay so how to interpret the variables well we've got our evaluation sitting there so it's just going to be equal to the evaluation of x right which is some element of the interpretation of a so hopefully this is making sense the way that we interpret the function terms that's going to be the interpretation of our function so now this truly is a function applied to the following arguments which are true arguments so this is an inductive definition okay and that's it for terms and then we can extend to formulas as well and these are going to be predicates as well so the interpretation with respect to new of a relation i guess i was using lowercase r earlier up to t n is equal to one if and only if the interpretation of r when applied to the interpretations of its arguments is equal to one okay and then we have similar clauses for all of the other inductive clauses in the definition of what a formula is so we had equality let's see for the one if and only if these all news by the way they kind of look like odds but they're new uh only interpretation of s is equal to the interpretation of t interpretation of t is one the interpretation of bottom is zero interpretation of this junction is equal to one if and only if the interpretation of phi equals one or the interpretation of psi

equals one conjunction we require both of them whoa for implication is that the antecedent is evaluating to zero or the consequent is evaluating to one okay now if you tuned out because you thought that was boring tuned back in the quantifiers are a little bit weird so the interpretation of there exists x such that phi this is equal to one if and only if there exists d inside the interpretation of a such that the interpretation of nu when we force x to get mapped to d of phi is equal to one right so this is notation that i haven't introduced i've just gone ahead and used it but the point is nu is evaluation so it's some function from the set of variables to the domain right so in particular it maps x to some element it might map it to d but it might not okay and then what happens here is that the interpretation of the existentially quantified formula is even the one even only if there exists some d if i um amolgamate my valuation to force it to send x to d so it doesn't send x to nu of x anymore it throws that away and sends it to d instead so that's a new valuation if under that valuation phi uh gets mapped to one okay so we're just saying that there exists some element inside the domain where if we had to find our valuation to send x to that element then we get a formula that maps to one okay and fall is similar but you just put for all instead so for all the an element of i of a such that i knew x maps to d of phi equals one okay and then a model is going to be an interpretation where all of the axioms of your first order theory get mapped to one for all possible evaluations new so i'll write that up in a second but this is another good place to pause and again i invite you to ask the questions that you might be scared to ask like there's a lot of this that is weird right like for example why is this so heavily baked into set theory right and why is why is this considered deep i mean seriously look at these definitions i of uh of this junction is equal to one if this or this i think somebody i don't know if it was gerard but somebody said this is um definition via stuttering like the definition of or is all and the definition of and is and right um that wouldn't be a fair uh way to describe this because i haven't defined and in that way i've defined conjunction in that way uh but i can i can i can try to answer any questions even even ones like that that's all it all seems kind of dead obvious right yeah but keep in mind you're from the world that's i don't know but what i mean by that is

like why does it take so long to two man i'm struggling a little bit with the microphones i didn't hear alana's question can you cover it really i i don't think she finished i'm sorry i didn't think they finished a question oh really i don't know spank did you have more to add to elena okay um i think i just wanted to add that like okay there's the sort of there's confusion that might arise like relating to what you're saying in terms of uh like it's obvious why we like saying this or that but maybe i think something more important is uh there's a lot of technical details here and you might be a little confused about like what is this or that even saying and i guess my advice for that is uh like keeping track of like which parts of the board contain uh syntax which are sort of the things inside the brackets in most parts of this board like that's in that's all on the language side whereas uh yeah like that in certain parts of this board that becomes part of the like model side or the meaning side or the truth value side um yeah i think uh yeah she saying why doesn't take so long to write this out so i think i can maybe say something to value here a really good one to emphasize billy's point and it kind of tackles eleanor's question is the equality one right so look at this equality one and be very careful with the different usages of equality inside it right so this equality here is one of the formation rules of the syntax so we said earlier that if i have two formulas if i have two terms s and t then i can form the formula s is equal to t right so that's some syntactic thing sitting there and then this equality right next to it is well that's exactly my point like this is where i always want to put my finger what is that equality right this is kind of the platonic world out there so we're saying that this formula evaluates to one if and only if this thing whatever the heck it is like it's an interpretation but not in the world of syntax anymore some interpretation is equal whatever that means to this interpretation provably the same thing in the theory of sets otherwise what are you talking about yeah but then how do you define this guy right so what we're doing is there is we're saying that the definition of equality there is provably equal inside this first order theory so we've just stayed inside this formalism world and then just said that inside here exists proof and we're just going to take that as our definition of truth yeah right i think the model theory is kind of

incoherent but that's i've really understood how this is supposed to be anything but a translation from some first order theory into some other first order theory but that's not how most people think about it so that's okay yeah i do think that most people don't think about them in that way but i'm in the position where i think it's okay to i think that the concept of ambient mathematical truths that so it's kind of open to your interpretation for example you might say that these two things are equal if i can experimentally verify using the method of science to prove that they're equal to each other you see like maybe maybe it means i can observe that these two things are equal to each other no but you're not free to say that because all the things on the right hand side of your iffs need to work together consistently for what you're saying to make any sense in particular the proofs you have in the the way what you accept as proofs about the things inside your brackets on the left hand side so phi or psi for example what you allow as proofs also have to translate into things that are valid on the right hand side so you can't you know you're fairly constrained there and you're constrained in exactly the way you would be constrained as if you would have a proof system on the right-hand side which looks more or less like the one on the left-hand side uh i don't i i don't mind i think with you're kind of okay if you read it platonically or read it as another theory in which you're interpreting it and that's fine right to to have this kind of powerful theory that you're interpreting things inside of it's a risky statement to make but i'll go ahead and just for one second say that this is where the topos theoretic approach to this does in fact kind of make it more illuminating so you can interpret these first twelve theories not inside the category of sets you can interpret it into different categories where the things on the right maybe are genuinely more complicated or more powerful or more sophisticated or whatever but that's a i think that's a helpful way to think about dan's statements that you're interpreting these theorem theories into other theories so we use first order theory first order languages as a tool in order to describe more abstract theories for example things existing in complex topoi now that's a very down to earth and kind of you have a grip on it way of approaching this but i think that there's other options as well anyway you enter into dangerous

territory very quickly okay dan part of what you are like asserting is that uh like in making this definition like you were talking about lifting from the left theory to the right theory but like that's strictly in the scenario where like in presenting this we are like uh trying to explain what is sufficient grounds to like to like deduce that the like that the thing on the right on the left is equal to one there and so like how do you do that well you need some deduction in nothing on the right but i think i think like that's sort of another way to take it uh which i know you may still have problems with is that like the thing on the right is an assertion like i know i have some concept of like the domain of objects and i i don't like i can sort of have an eye a concept of saying that like the thing that s is the thing that s is is naming is the same thing as the thing that t is naming and i'm not like there's no like ambient means of deduction of that fact that's like merely just an assertion of yeah it's platonically true that's what i'm always getting what are you people even talking about i have no idea what that means okay well why don't i just do that from the beginning then i mean if you're happy with platonically true why why bother with the rest i mean it's either uh i don't know what is it when you write down s equals t in the first order theory of sets uh what do you think you're writing down you're writing down something which is a sort of shorthand for a logical statement which is for all t t and s is well for all x x and s is equivalent to x and t and that's a statement it's either it's either true or it's not uh yeah a grade but that is the construction of a syntactic proof so you've kind of written down enough etchings that make me convinced that there exists some first order natural deduction proof that fills in all these details but the point that i want to make is that there's more to the picture than that it just doesn't feel as though oh yes all i have done is inferred the existence of this proof tree whose edges are statements inside the first order theory you know it feels like you've done more than that it feels like you have shown that these two sets are equal to each other right so there is some kind of extra thing there or platonic belief in these objects that exist theoretically you believe that you've made a statement about them when you construct that syntactic argument and so that's what i think the point of this yes that's what

i think they were trying to do when they wrote it yeah that's fine i don't buy it took it i thought you might say something like that i've got one last thing that i want to write and then we can either um finish or continue discussions so let's not get too carried away okay so i did mention this approach in this surprising application to algebraic geometry so i know that i'm over time so let me do this very quickly so the x growth in the theorem states that if f is a polynomial from n copies of the complex numbers to end copies of the complex numbers and they don't need to be equal there is a polynomial so polynomial in all entries n then f injective is sufficient in order to infer that f is surjective okay so that's a statement great and the proof that we're going to present inside this series is assume this was false then we can infer that there exists some disproof of it well i need to i need to write the x growth index theorem as refers to all the statements but assuming i've done this so write phi as a first order statement and then let pi be disproved so pi proves the negation of phi and then what we do is we look at pi right and we say pi is some finite proof tree so it's a finite object so that means that there exists some oh let me put this way so there are finitely many axioms of the form one plus dot plus one is not equal to zero right so there is some characteristic that is not being applied inside the hypotheses there might be none of them right but maybe this proof uses that statement as hypotheses a hundred times but however many times it does it finitely many times right okay so that means there exists q which is prime not on this list so pi is disproof in the first order theory of algebraically closed fields of prime characteristic q so that amounts to uh i'll just say pi it's a little bit vague or whatever so play is a disproof of the corresponding statement for finite characteristics so if i took the algebraic closure of the finite field here of characteristic key then we end up with a disproof of this statement and then this statement is easy to prove that in fact is true using finiteness of fq right so we've a we've been able to reduce down to a simpler case so i'm able to uh so if i'm able to prove the actual ethernet theorem in the case of uh non-zero characteristic which is indeed easier because we can appeal to finiteness of the underlying field you know the complex numbers so the algebraic closure of um the real numbers which is not finite

whereas the algebraic closure of the finite field with cura of characteristic q is a um finite uh field and so we can appeal to that inside the argument and simplify it so the point is we're going to grab the proof as a formal object and then move it into another uh another theory and then get a contradiction like that so i think this is really interesting because we started off with a purely philosophical motivation to model theory and you know what is true for this truth etc and we ended up with just another formal construction which was able to be used in the world of mathematics again so i think this really highlights the questions where are we are we inside the world of syntax only are we inside the platonic world only are we succeeding in dancing between the two of them i don't know and i'll hope to make my opinion more sophisticated throughout the course of these lectures and i hope that you come with me thank you for listening that's the end of my time thanks no worries thanks billy for this setting the orb on fire this is cool it's thankful yeah okay thanks that's what um i don't think there's anything after this so i'll stick around for one more minute if there are any questions but people can just leave if they if they're done is there a proof of the x growth indeed theorem there must be other proofs that don't involve model theory at this point right yeah i don't think that it was first proofed using model theory in fact so i don't know the history of this proof but it's probably a good idea to learn it because that would be interesting when i looked it up on wikipedia it seemed like both axe and growth and dig had more or less the same idea and it was this idea too i don't know if growth addict formulated model theoretically but it was yep basically this argument so yeah i got the impression from the way you talked about it earlier that this was like a later observation and you could prove it model theoretically but my current impression and that's also pretty superficial just from wikipedia is that no this is the original argument well the reason why that surprised me so much and as i was saying to you in our meaning is because of the reliance on the lower lowen hype spolam theorem so if you just grant that the first order theories of algebraically closed fields of all of the different characteristics if you if you assume that all of those are complete theorem theories then it's really easy to prove this right but you need to get that statement