A Tarski's 'Decision method for elementary algebra & geometry' (parts 1 & 2, contd.)

0:00 Thank you. Thank you. All right. We'll start with Coria's general introduction and historical discussion. Then Ricky will speak about Tarski's extension of Sturm's algorithm. And by then it will be time for a break. After the break, I will speak about the Tarski text, and when I'm done, there'll be some sort of informal general discussion.

2:30 I have four parts in my little talk, the first one I shall say a little bit about the edition of the text. Secondly, I shall report on Tarski's own historical remarks. Third, Fourth, I shall say something about Tarski's Sturzes of Sturm's theorem, and fourth, I shall sketch some connection between Tarski's text and Artin Schreier's theory. Then first, as Tarski wrote many times, the main results of his papers were found in 1930. Thus they belong to the Polish period of his activity. We know that Tarski's lifetime may be divided in some parts. In the first one, Tarski was teaching at Farsar University and leading a logical seminar, attended by many distinguished Polish logicians. In 1939, Tarski went to America. He was invited by Prime to give a lecture at Harvard University. But after the lecture, Tarski did not go back to Poland because of the war. and after two or three years of professional instability, he got a firm position at Berkeley University.

5:00 There he spent the rest of his life gathering around him a great number of outstanding logicians. The results contained in the paper of 1951 were first mentioned in print in Tarski's 1931 paper, written in French, sur les ensembles définissables de nombre réel, and published in Fundamenta Mathematicae and the machine can be found on pages 233-234. The second machine was made in the English version of the Wahrheitsbegriff in the formalisierten This servant mansion was made in the note 2 of the first Ruja edition of the collection collected the collection of some important paper written by Tarski. In this note too, Tarski wrote that he had occupied himself in the years 1926-1928 with the structural description of all complete systems of a given theory, and he gave as examples what he called arithmetics of real numbers, geometry of straight lines, theory of order, theory of groups, etc. etc. His traits that report on his results were made in the seminar exercises between 1926 and 1929. By this information repeated many times by Tarski, we have to understand

7:30 that Tarski's completeness results on the elementary algebra and elementary geometry were found before Gödel's completeness results on the first-order predicate calculus in 1930, and before Gödel's incompleteness result on the first-order theory of arithmetic of integrals, theorem 1931. It lasted nine years before Tarski came to write down the results he found in 1930. Why? I don't know exactly. Maybe we can find some information in the intellectual biography written by Solomon and Anita Fefferman, but I must confess that I have not yet the time to read it. I have the book at home. In 1939, the first English version, embodying those results was prepared for publication in Paris. It was planned to be published by Hermann, the edition Hermann, in the series Actuality Scientific Industrial, but this version remained unpublished, once again because of the war. The title was The Completeness of Elementary algebra and geometry. And again, nine years later, McKinsey, one of Tarski's colleagues in France, who was professor at Stanford University, prepared a new version, different from the original one, in its approach and also in its content, to some extent also in its content.

10:00 This new version was first published in 1948 with the support of the RAND Corporation. The reprint is what we have to read, the version of 1951, it has some changes in the introduction, some new bibliographical references, and a few supplementary notes in this second revised version. As an example, I could show four references that were lurking in the original edition and were added by Tarski in the second version. We have to remark that Herbrand, a text which was published in 1930, was not mentioned in the first edition of the text. Some references are laid aside. It's not very important to say which one. Trotsky insisted that in his preface, he wrote that the reprint took into account the remarks made by Hengen, Rose and van der Verden. We know that the editorial work was done by Solomon Feffermann and Frederick Thomson. As Tarski confirmed in his 1951 preface, the new version reflected the interest which the Rand Corporation found in these results. The focus has been shifted to the decision problem from that of completeness. A more systematic presentation of the decision

12:30 method brought to the fore the theoretical possibility of constructing a decision machine. One has to stress the qualifying theoretical. It is indeed known that the complexity of the imaginary theory of renumber is at least exponential. In 1967, the 1939 set of proofs was reproduced in a restricted number of copies, namely 100 by the Institut Blaise Pascal in Paris. René de Posselle, Director of this Institut, made this reproduction possible, financially possible, and Paulette Février took care of the actual process of reproduction. The French translation of this original version is available in the set of the collected papers edited by Gilles Gaston Granger under the title logic, semantic, metamathematique and published in 1974 in Paris. Thus we have the possibility to compare the different versions of the paper the original one focused on the completeness problem, and the second one focused on the decision method. Starsky defines the decision method for a class K of sentences as the method by means of which, given any sentence F, one can always decide in a finite number of steps whether in K. He considers the case when K is a class of true sentences of some theory. Let us recall that the theory is a set of axioms plus the set of the consequences of this axiom. Everyone

15:00 Everyone knows that a theory is said elementary when the sentences of the theory can be written in the first-order language of predicate calculus, involving only one variable. Tarski called Elementary Algebra, an Elementary Theory of Rhin Numbers. That is, variables represent real numbers. We have constants denoting the individual numbers, such as 0 and 1. We have more further symbols denoting the algebraical operation. multiplication, and division, and R denoting the relation, equality, and greater than, and we have further symbol denoting logical constant, as you know. Thus the language established by Tarski is the following. We don't use variables standing for arbitrary sets or sequences nor for arbitrary functions of real numbers. Thus, sentences of this theory are a combination of equations and inequalities involving real numbers and using the logical means of first-order predicate calculus. In his introduction, now I am coming to my point two, in his introduction...

17:30 So because you use the word of language and the word that we use now in modern theory, But when would this terminology be found in which we would be called by Tarski's text? In this kind of notation? This kind of notation? It looks more or less... What we do now when we define the language in classical model theory, but... This line does not stand exactly in Tusky's text. The ID, but this... For example, in the... For us, it is not for the reference, but for many pages, it is for the... And he explains in one of his notes, he explains with details, but he did not use exactly this expression. For example, the system of elemental algebra in the paper, it would be like, for the six pages, it would explain what is formula, what is free, what is free. And he is not saving, he explains how he shall use different kinds of letters, Greek letters representing arbitrary terms and so on, and Greek capitals will be used to represent arbitrary formulas and so on, but we don't have exactly that. You can see some of these ideas already in Hilbert's lectures in Gertigen in the early

20:00 1920s. They were so much in the air that it's very hard to pinpoint the place and time and crystallize in the way we use them today. There are some huge differences because for Eurbet, the meta-language has to be as restricted as possible. So for Eurbet to put all the real numbers in the meta-language is something impossible. It has no sense. For Tarski, you can put all what you want in the meta-language. That's a good difference. That's true. Tarski is no longer in a foundational point of view, so he don't care to have a meta-language as restricted as possible. No, that's perfectly true. But it's also true that the restricted formalism involving specific languages and theories you find very much in the Hilbert's program. Even the word metamathematics, which Tarski uses, though he uses it in a more expansive way than Hilbert did, but he takes the work from Hilbert. He takes the work from Hilbert. He changes his meaning. Now I am coming to my point too, and gave some comments on Tarski's own historical remarks. First of all, Tarski's traces that the importance of the decision problems for the rule of mathematics and for various mathematical theories was expressed by Hilbert. Actually, Hilbert and Ackermann, Grundzuge der Theoretischen Logik, Chapter 3, considered the decision problem as the main task of metamathematics. I have made a translation of what it is said in German. Mathematical logic can do better than just thinking and making precise the language by By formalizing the modes of inference, one can hope to achieve a systematic, let us say

22:30 numerical, treatment of logical formulas in the way of the theory of equations in algebra. We may compare with the note 5 of the first version of Tarski. There he wrote, Tarski wrote, the knowledge of the mathematical logic required for reading the present work can can be obtained from the book Hilbert Ackermann. But it is surprising, in the 1951 version, the Grundsuggethe, Theoretischen Logik, did not appear anymore in the references. The references are the same, I think. I don't have the version of 48. I have the version Yes, but Blaise Pascal is the reproduction of the 9th, 39th version, yes. I wanted just to remark that this reference, which was very important for Tarski's first version, disappeared in the final version. It was replaced by Hilbert Bernays. But Hilbert Berners was already cited in the first version. Oh, it was? I am sure. Yeah, it was Grenade in 1930.

25:00 Then, Tarski mentions different results found before 1930 or 1948, and they are well known. There are the result of Levenheim, 1915, for the first-order predicate calculus, the result of Post, 1921, Post gave a proof of the validity of the true table method. The result of Langroth, 1927, Langroth gave a decision method for an elementary theory of linear order, and this result was, I think, very important for Tarski. Tarski said that he and his colleagues were studying this work, this work of Langford in the years 1926, 1928 in his seminar at Warsaw University. He mentioned Pressburger results on the elementary theory of arithmetic involving only the addition. And we may remark, as Tarski himself said, that all these results found before 1940 concern logical theories or give a purely logical decision method. Tarski in his 1951 version gives two examples of a decision method for a mathematical theory and in the two examples the method is itself mathematical. The first one is Euclid's algorithm and the second one is Strom's theorem which permits

27:30 I think it's now time to come to my point three, Ricky will say much more about that, I just want to say some words on Sturm's theorem as the decision method and quantifier elimination. Tarski's original contribution was first to show that Sturm's method of constructing some specific functions called Sturm's chain related to an algebraic equation f of x equals zero degree in amounts to prove the existence of an elementary criterion for this equation solution to have exactly k real solution, k less than n, naturally. In other words, Vtarsky stressed that with Sturm's theorem we have a purely algebraical criterion in which we don't use any quantifier. In the language he established, we can then express this criterion by a sentence which has no quantifier. Such a criterion is obtained is obtained by constructing a certain finite sequence of systems, each consisting of finitely many equations and inequalities which involve the coefficient of f the x. Noticing that

30:00 That task he was led to extend Sturm's theorem to arbitrary systems of equations and inequalities in many unknowns, this is the theorem 31 in the 1951 version, and that explains how he He put the symbol greater than among the undefinable symbols of the language he had established. We can mention Tarski's source for Strom's theorem, how he knew Strom's theorem. them. The main sources are Heinrich Weber Lerbeau of algebra and the paper of Karl in the Encyclopädie der Mathematischen Wissenschaften. There are the two main references cited in the first version. Later, in the second version, he mentions, briefly, but he mentions Sturm's original paper. It is in the note 12, page 52. And we may add that in an abstract published in the Journal of Symbolic Logic, number 4, page 176, Tarski underlined the fact that He submitted Sturm's theorem to double analysis, analyzing on one side its mathematical content and on the other side the logical structure that led him to push to the fore the altered structure of the field of real numbers. Tarski himself insisted on the mathematical content of this decision method.

32:30 Actually, as we said, he was one of the three or maybe four logicians who gave a decision method for a mathematical theory. Tarski underlines the difference between Pressburger's and Scholem's method on one part and his Presburger and Scolham treated pieces of mathematical theories artificially selected and having a restricted mathematical content. Tarski considered a comprehensive theory of real numbers, which is nearly the familiar theory of working mathematicians. In pages 3 and 4 of his introduction, we can read the following. If we compare the theories treated in this monograph, it has elementary algebra and geometry with the other theories mentioned above for which decision methods have been found. We see at once that although the logical structure in both cases is indeed equally elementary, the theories investigated here have a considerably richer mathematical content. It would be possible to mention numerous problems which can be formulated in these theories and which played in the past an important role in the development of mathematics. In the solution of these problems, and in general in the development of the theories considered, a great variety of modes of inference have been applied, some of them of a rather intricate nature, to mention only one example, the proof of the theorem that the triangle is isocel if the bisectors of two of its angles are congruent. Thus, the fact that there exists a universal decision method for elementary algebra and geometry could hardly have been regarded as a foregone conclusion.

35:00 The second remark Tansky made in a note of his paper, he insisted, he thought that it It was the first to consider the case of finding a criterion for the solvability in the real domain of a system of inequalities without equations. In fact, we can say that Fourier, in his Analyse des equations determines, 1831, was in search of a criterion for the solvability in the real domain of a system of equations and inequalities. But Fourier did not have the time to develop his ideas, and it seems that Tarski ignored Fourier's work. Now, point 4, the connection with Artin Schreier theory. As we have said, Tarski stressed many, many times that he elaborated his decision method in the years 1926-1928. We know that Artin Schreier's paper was published in 1926 and constituted chapter 11 of Van der Werden Modern Algebra, which was published in 1930. Further, However, the second edition of Modern Algebra, published in 1937, was cited as a source book of algebra in Tarski's original version, which is in the Note 7. But this original version made no use of Artin Schreier's results. And even in the 1951 version, Artin Schreier's results are explicitly mentioned only in the notes, namely notes 9, 15, and in the supplementary note 7.

37:30 I shall say briefly some of the content of these three notes. Note 9. Tarski observed that one may replace the classical intermediate value theorem, that is the theorem that every continuous function of a real variable which is positive at one point and negative at another point, of a bounded interval must vanish at some point in between. We may replace this classical theorem by the two following axioms we have learned yesterday. The first one, every positive Rhin number has square root. And the seventh, every polynomial of odd degree has a root. 0. And we know that the conjunction of 1 and 2 is equivalent to say that R is reclosed. Note 15 is important from the historical point of view because it contains the comment in which Tarski expresses the famous transfer principle. Tarski notices, indeed, that any real close field in Artichreier's sense satisfies all the action listed for the element territory of real numbers as he established it. In particular, the element territory of real close field is complete and decidable, just like the element territory of real numbers. Here, complete means means that every elementary synthesis which holds in one wheel-closed field holds in every wheel-closed field. Or we can also say that any elementary definable property which belongs to one wheel-closed field belongs also to any other wheel-closed field.

40:00 The Expiration Transfer Principle The expression transfer principle is not in Tarski's text, as far as I know. This expression was first used by Abraham Robinson in his contribution to the International Congress of Mathematicians in Cambridge, Massachusetts in 1950. We can find it in the first volume of Robinson's selected papers, page 5. And now, the supplementary note 7. In the second revised edition of 1951, Tarski comes again to the transfer principle. He points out that the transfer principle, he did not call it so, but he points out that this principle extends to a comprehensive class of properties which are not elementarily definable, i.e., which are not expressible in the first-order language for the order field of real numbers. Assume we have such a property P, for which we have a specific proof in one particular real-closed field, then P holds in every real-closed field, proof is not transferable. We know many examples. Various theorems originally established for

42:30 the field of real numbers, such as Rawls theorem or Sturm's theorem, were proved using essentially the continuity of the field of real numbers, but these theorems proved also for continuous function from air to air have in the Tarskis language for elementary algebra a purely algebraical counterpart, that is, Sturm, for instance, Sturm's property or Rol's property is expressible for polynomials and can be proved without using the continuity property of polynomials. Thus, Strom's property or Rohr's property is satisfied in any real-plus field. In conclusion on the transfer principle, we may say that this principle gives a concrete content to a remark, Tarski made at least twice, and in our text on page 3 of the introduction. He is writing there, it is important to realize that only the nature of the concepts involved and not the character of the means of proof determines reader for instance the geometrical term is a sentence of elementary geometry. You can maybe read the whole paragraph. For instance, the statement that every angle can be divided into three congruent angles is an elementary sentence in our sense. Some of us have your question and in this case, some others have different numbering.

45:00 Which one? Ah, Persepol, c'est la periche? For me, three. For me, three, ah, four. Should I continue? Yes, thank you. For instance, the statement that every angle can be divided into three congruent angles sentence in our sense, and of course a true elementary sentence, despite the fact that the usual proofs of this statement make essential rules of the action of continuity. On the other hand, the general notion of constructivity by roll and compass cannot be defined in elementary geometry, and therefore the statement that an angle in general cannot be tri-sected by roll and compass is not an elementary sentence, although we can express in elementary geometry the facts that say an angle of 30 degree cannot be dissected by 1, 2, 3, so on, or in general any fixed number of applications of roles and companies. I mean, just when Starsky made the difference between the nature of a concept and the means of proving this concept within the system, he established at first glance we cannot understand what he had in mind. But I think one way to understand that is simply to think on the transfer principle because the transfer principle is indeed a principle which permits to transfer the content without transferring necessarily the proof of this context. transferable, we cannot transfer it, but the contact, the contact is true, is valid when

47:30 the theory, the theory is complete, naturally. And that is all that I wanted to say. What I'm going to do is give an outline of Tarski's extension of Sturm's theorem. I'd also like to call attention to how it's related to the whole thing. This is not in Tarski, and basically I've learned from Marie-Francoise, as most of what I've learned was at the subject. So, can I erase this? Yes, of course. As we know, Sturm's Theorem tells us, for a univariate polynomial, how to calculate the number of roots, the number of real roots that it has, and the extension that we want if I have two polynomials P and Q, I would like to be able to count the number of roots of P at which Q is positive and the number of roots of P at which Q is negative. And the reason why once you've done that, you know, I mean once you've done that in a way that you calculated in terms simply of the coefficients of P and Q and things that you calculate from them and basically all you have to calculate in term I mean the Sturm sequence is a value you take the successive remainders in the Euclidean algorithm and you look at there the signs of the leading coefficients at well the signs of leading coefficients and whether the polynomials, even degree or odd degree, determines the signs of minus infinity and plus infinity.

50:00 And once we know that, first, we can calculate, well, we know the coefficients, and so we can calculate that sequence directly, and from the signs of that sequence, we know the number of roots. This will be answered in exactly the same way. What does this have to do with quantifier elimination? quantifier elimination is essentially the statement that the projection of a semi algebraic set is semi algebraic in other words I'm starting with a semi algebraic set which is simply the union of what is called basic semi algebraic So, I have essentially the union of things in the form P1 to PL is 0, and I have other polynomials Q1 to QM which are at various signs, greater than 0, less than 0. And now first, what I want to do is reduce this practically to the case, to the simple case of where I have just one polynomial. In other words, suppose I consider the semi-algebraic set P equals zero where P is a single polynomial and Q is positive. Anything like this is simply an intersection of things like this. and any semi-algebraic set is a union of such things. So, once I answer this question, I'm looking at the question, there exists an X such that P is 0 and Q is 0, as Q is greater than 0, say. This, if I'm looking at the number of, I have a bunch of variables, Y1 to YL, and x. I want to eliminate the quantifier there exists. It's just a matter of deciding whether or not there's an x which has this property. So all I have to do is be able to answer this question in the same way that Sturm's theorem answers the question, how many roots? And the

52:30 The way this is done is to make a connection to, well, what's up there is called the Cauchy index of, say, P over Q, and what the Cauchy index of P over Q, yes, I can't hear you. Q over P. What difference does it make you think? No, P plays a special word in your decision. What? P plays a special word in your decision. Oh, that's true, sure. Okay. No, but this is not the Q and P that I have here. What's in the name? It's, uh... So, P upon P. The point is that I have the quotient of two polynomials. I'm looking at a rational function. And you look at the graph of the rational function, it has a variety of vertical asymptotes. And where it can jump from plus infinity to plus infinity, from minus infinity to plus infinity, or all of those combinations. And basically, this is going to be the number of jumps, and I may have it backwards as the refund source points out, in the number of jumps from minus infinity to plus infinity minus the number of jumps from plus infinity to minus infinity. I'm very curious to know the whole origin of this notion, because this is essentially counting, it's essentially In fact, I'm probably going to get this wrong. If I look at P prime P, Q over P prime P, just by an examination, upside down. Okay. Right. So if I look at P... D minus Q divided by D. Sorry. If I look at this rational function and examine the changes assigned, I'm calculating essentially the number of roots of P where Q is negative, minus the number of roots of P with Q is positive so I'm answering the question which are as a strong query for Q positive say this for for Q with respect

55:00 to the polynomial P this is the number of roots of P with Q is negative minus the number of roots of P, something like that. So that if I can calculate the Cauchy index in general, I have the answer to the whole problem. And the, so the, I want, I want to show that this is essentially the Sturm sequence of P divided by Q. In other words, I say, I divide P by Q, get the negative remainder, and I, and I, and I continue. So the main result is that this is calculated by the Sturm sequence which permits me to calculate the Sturm query which permits me to count the number of places where p is zero and the number where q is positive, and then we're all done. Now, I don't know, you want me to do more than this, yes? I was imagining you were... Okay. Well, I will try, but I think done again. It's also clear that I just have to do this for a univariate polynomial, because when I do it for a univariate polynomial, what I'll wind up with are, in other words, I'm looking at the polynomial in the y's and the x's as polynomials in x. So P is something of the form an x to the n plus blah blah, where the a's are polynomials in the y's.

57:30 And when I calculate the remainder sequence, to evaluate the signs of this produces inequalities about an and successive remainders. statements of the form A, N, positive or negative, and other polynomials and the Ys. So that whether or not the sequence produces an answer, yes, there is an X. I mean, what do I have to know? I simply have to know that there is a place where P is positive. And that's expressible as a statement that a certain sequence of polynomials have a value or not, not a value but a sign that produces the correct answer or not. Now, the key thing then is to prove that the index of Q over P is equal to the storm chain for p over q, in other words, for q over p, simply dividing q by p, and taking the negative, what? So I'm taking the Sturm sequence of p divided by q. And, I mean, this essentially follows from two lemmas. The first lemma, in other words, once this is established, the whole theorem is done. Now, the two numbers, I mean, just, we take one step. I divide Q by P. First, I can also

1:00:00 assume, without laws of generality, that P and Q are relatively prime. Just divide out their greatest common voice. Yes? You don't mean that the pushing deck is equal to the sequence? I'm sorry, I can't hear you. You don't mean that the pushing deck is equal to the sequence? Is it? No, no, no. It's equal to the number of variation. The number of sign variations of the sigmas. Okay. So let's write Q as AP plus R. So the first remainder is R, and I want basically by induction to see what's going on. You're going to get dividing Q by P. Thank you, Shalella. I'm going off. I'm dividing Q by P. I don't know. No, you are dividing. You get the Gaussian vector of Q over P by dividing P by Q. No, no, no, no, no. It's the bottom equation. You should reverse the P again. Thank you. I count them a little to correct me. So, the first observation is that the variation of, one second, so Q over So the variation in the Sturm sequence for P and Q is almost the same as the variation in this term sequence of PQ and minus R. That's the first step. And now it's simply a matter of writing down whether I have to add a one or not, depending upon the first

1:02:30 in the first step. I don't think it's worth going through a detailed case in Emesis. And then there's one other lemma, which I don't, so this is the first lemma, and the second lemma, which I don't remember, I have to consult my computer to write it down. Do you remember, Now, if you look at the gauching length of Q over P and the gauching length of minus R divided by Q, and the gauching length of minus R divided by Q, the correction term will be the same as the variation. Okay, and then it's just a matter of comparing. There's a plus, one, or a minus, and the whole will be the same. Right, in both places, and that essentially tells you the whole story, by induction on the length of the sequence. May I say, as far as I know, the culture in Dexter was written later than Sturmstheor. Oh really? 31, 31, 1831. Oh, you mean this theorem was written? By whom? Cauchy's work came later than Strom's theorem. Ah, and when the Sturm's theorem? because I'm expecting the 12th century in the 1899, without proof, but the... No, still not in the 1899. The theorem is... ... on the... How did it say? 1899? 1799. No, no. Dulletin de Ferrisac, in Dulletin de Ferrisac. It was known, it was well known, since 1829. Oh, since 1829, I see.

1:05:00 Atra, as I know, Cauchy's theory was published in my paper of 1831. So this is Sturr, 1829. Yes, Sturr. And Cauchy in 1831, published essentially this year. Yes, and Cauchy, Marshall, so explicitly. How was the truth by Cauchy then? Sturmsbrook. How do I have to take this? Here we have Joseph Ebert and the doubt proof. And then in 1835 we have the complete proof and the general way. And what did Cauchy do in 1831? What you are talking about. Yes, yes, yes. No, no, no. Cauchy will be finding in two ways. So I have a question. Because I... So then what Tarski is doing is continuing this Cauchy-Invest approach, but in order to conclude the number of groups of P, that P is positive, by taking this prime Q as a numerator, as you mentioned. And this, I was not able to identify whether it is done somewhere before Parsi himself.

1:07:30 Because Parsi himself is saying that he was unable to locate his previous term. And at some point I thought it was not invested, but when I looked at the paper, I just found the usual machine that was invested. No. As far as I remember, counting with inequalities you cannot find in Silverstone. But that means you have a company inside of several girls, which wash it in the mouth. I don't think you can choose right from the portions to it. Thank you very much. I think well there's about 20 minutes So I thought I would use that before looking at the text proper to give an imaginative reconstruction of what I imagined went on at the seminar in Warsaw where the method of elimination of quantifiers was being discussed and developed. But to put it another way, Ricky was letting us look at it from the point of view of the algebra working out. I want to look at it from the point of view of the logic working in, and how to get to starting with the logic where one is led to look at that kind of algebraic question.

1:10:00 So I can imagine that to begin with, people were thinking of the languages like that of arithmetic of real numbers or the natural numbers or whatever which occur as the most obvious formalizations of usual mathematics. where you, let us say, the main connective between terms is just the equals sign. Let's not worry about order yet. Just talking about equals and the usual logical language. So suppose we have not, we have or, we have and, and we have the existential quantifier. And of course, it's well known, if you have the existential quantifier, you can also have the universal quantifier. So if you look at the most general expression, and you have variables, and for the moment, let's not worry about what the variables range over. whatever they range over, there are some logical operations which suggest themselves in a most natural way. If you look at an expression of the form where there are no quantifiers inside here, then there are some reductions themselves immediately. One of the first reductions that suggests itself is to get rid of all the negation signs. And the rules that get rid of them are the usual ones. Not P is equal

1:12:30 to P, not P and Q is the De Morgan law, and the dual that goes the other way. If you iteratively use those all the way. You end up with a not sign, if it exists at all, in front of an equation. And so, aha, now you suddenly realize that you're going to have to deal not just with equations, but within equations, this is A, unequal to B. All right, let's add unequal as another initial symbol. So it's the logical operations that suggest that right off the bat. So now we're left with a sort of polynomial expression in ands and ors of various kinds, And it's well known that distributive laws, there are distributive laws in which either operation distributes over the other one so that you can simplify in either direction, ending up with either a disjunctive normal form or a conjunctive normal form. Well, the disjunctive normal form seems particularly nice because the existential quantifier commutes with the ore. So we end up with something that looks like this. Where each alpha i is a conjunction of...

1:15:00 And each of these betas is either an equation is either an equation or an inequation. And because the existential quantifier does commute with the or, we're reduced to looking at the individual at the, I'm sorry, at the individual alpha i's, and now one is down to the bedrock of the algebra, because now what is it you're looking for? Well, you're looking to see if you can find a common solution to a finite set of equations and inequations. And note So far I haven't said anything about whether the X's are real numbers or natural numbers or whatever. That reduction just forces itself simply by using the most elementary logic, the sort of thing that, you know, is well known since Boole and Schroeder, nothing except for the quantifier, Spreger. But otherwise, this is really the most elementary sort of logical consideration. I believe that, as I understand it, it's the work of the Warsaw Seminar that led to the Pressburger procedure in which they not only ended up having to add congruence to fixed moduli in addition to equals and inequals in order to get an algorithm and get the elimination of quantifiers. If you'll permit me, I'd like to mention a direct personal experience I

1:17:30 had with all of this. Back in the dark ages of 1954, I had the idea that it would be a good idea to write a computer program for the Tarski procedure. And then because I thought that was probably too hard a thing to take as a first task, I thought I'd settle for In fact, I did. In the summer of 1954, I wrote a computer program for the Institute for Advanced Study Computer in Princeton for the Pressburger Procedure. Of course, I found that that already exhausted the resources of the computer that was available, and that the idea of actually programming Tarski was out of the question. Okay, I think now we can take a break and come back and say hello. Yeah, I have a question. In reading the biography of Staski, it says that in the Basel seminars, they were first interested by elementary geometry was the first entry point for afterwards going to elementary algebra. I don't have any comments, just the, of course imaginative reconstructions of history are often wrong. Okay, let's take a moment.

1:20:00 So there is one which is the production of Tarski and the other one which goes on the website to be printed. like the other one which was on the website. So, the machine there is on page 15. No, it's all right. In the left inch 25. Left inch 25. So, if I come up, so he is writing the formula to describe the derivative, then he's writing a formula to describe the multiplicity of the root, that's what he does, definition 17, and so forth, and then he's writing a formula which is called this phi with f, c, n of alpha, beta, which will probably seem strange at first glance, even to those acquaintances with logical symbols, which means, in fact, it's counting the number of jumps, it's looking at the number of jumps from, say, minus infinity to plus infinity, except that it does it not in terms of the jumps to the denominator, but in terms of the same thing. And then it takes the difference of the two, n equals n1 minus n2, and we see that before the condition 25. So definition 25 should be read like the Cauchy index of theta over alpha is n, and the main variable is c. I'm totally confused. I didn't know there were two manuscripts. No, it's not manuscripts. There are two versions. One version is the reproduction of the original task list paper, and the version we put on the website at the conference was re-typed from. Yes, but the number is not the same. Not on either of the pages of the current investigation. There is one for what? And in the version I'm looking at, there is no definition 25.

1:22:30 So this is the Cauchy index, so please. Okay. So, I don't know if you can... I actually... It's 21 in your numbering. 22... 21... 21... 21... 21... 22... It was really, it was automatically really numbered, and... But it is possible to have a good number. It is not possible to have a good number. Okay, so sorry, so apparently it's 21, they mentioned 21 and 22, you know, okay, sorry. And then, there is, later, so on my version it's on page 25, it's the discussion, the two for theorem thought, my version, but I don't know if that's, you know, if someone and the other one, why is it renumbered? I don't really understand. It is. Thank you. We should just do that. Pardon me? It happens. It happens. Okay? So if the formula that's T, let T be any variable and let T be any formula so that T of E is defined by the definition, then T of E is the formula which contains no quantifiers. That's the theorem. So inside the proof of this theorem, you have in the third paragraph of the proof, it says that if R1 is the number of proofs of alpha, R3 is the number of proofs common to alpha and beta, R3 is the difference between the number of proofs of alpha at which beta is positive and the number of proofs of alpha at which beta is negative. So it means this strong query, that was mentioned directly, is included in this task. So the idea is, if you have three information, which are how many roots of alpha, how many roots of alpha which are common to beta, and how many roots of alpha, which beta is 20 minus, how many roots of alpha, which beta is negative,

1:25:00 then you'll be able to compute the number of roots of alpha, which beta is at the given time. So at least three information you can compute by generalized terms. So this is the same text except that the numbering of theorems and definitions has been shown. Yes, and there are also two typos and something missing on the bibliography. What I was basically proposing to do is to give a close reading of some of this along with everyone. Okay, may I use this, or is that... Well, if you give me back after the... Yeah, sure. Okay, fine. That way I can be sure that everyone is... Yes, thank you. There are two things that one needs to, I think, bear in mind when reading this carefully. One is that, as Uhurya has emphasized, this was written for the Rand Corporation with the specific goal of making the actual algorithm extremely explicit, because they had this vision that this was something that might actually be useful in a computer implementation.

1:27:30 The other is that the elementary logical notions involved were sufficiently unknown to most mathematicians that the whole thing has a level of detail that, to quote a phrase that Hardy used in another context, is a little bit like missionaries preaching to cannibals. Missionaries preaching to cannibals. Arnie's reference was to his course of pure mathematics, where analysis was still, modern analysis was a rather foreign subject in England around the turn of the 20th century. He said a few words. Starting again, he would write with much more restraint. So everything is explained in gory, gory detail. The representation of any given term in the language as a polynomial in any specific one of the variables with the coefficients being terms and the remaining variables is worked out in gory detail in, I was going to say definition 10, but I'm sure this is definition 69. Oh, it's definition 9.

1:30:00 No? Yes, definition 9 and definition 12 in the redone version, definition 8 and definition 12 in the official... Let me refer to this version as the official version, and this as the revisionist version. So we have this piece of C is now defined for any term, and it's defined for, as well, for any quantifier-free formula of the language. And it's simply the trivial remark that you can expand any such term as a polynomial in any specific variable with the coefficients of the term. And he even allows himself to make such an obvious remark as, unlike the situation in algebra, it is not something to cause any particular disturbance that the leading coefficient might be a constant that evaluates the zero, which would not be counted. He makes extensive use of extended disjunctions and conjunctions, things like something or other. And I'd like to suggest that in reading those expressions, it is sometimes helpful to think of those as really being quantifiers, the extended disjunction, an existential quantifier, the extended conjunction, a universal quantifier, in which the quantifier can be represented in finite terms

1:32:30 because the quantification is over a finite range. But the mode of logical representation makes one want to say there exists and for all in understanding what it's said. Theorem 13 in the official version, which is theorem 15, version expresses this expansion in disjunctive normal form that I talked about before the break.