aboutlogic #18 | The Hidden History of Logic: Jan von Plato on Gödel, Gentzen & Bernays

00:00:00: I trained myself for about one year in reading Goethe.

00:00:04: There are like five or six people who read it today, three of them know about Logic and they're like my research group.

00:00:11: so... Can you train an AI to read that?

00:00:18: Hello everybody!

00:00:19: Welcome to our newest episode of About Logic And we were very happy that Jan von Plato accepted our invitation because he was many Heads in the logic community is a logician himself, worked on intuitionistic logic.

00:00:34: And he's not only the expert on Gensen I would say it like that but also the expert of Goethe.

00:00:42: so we hope to have lovely window into this story Of Logic his an ERC grantee and based in Helsinki.

00:00:52: So thank you very much for joining us.

00:00:54: Thank You For The Invitation.

00:00:56: i look forward To A Nice Discussion

00:00:59: Yes, so I'm also happy to see you again after we met recently in Gothenburg.

00:01:07: So my first question or my first suggestion is... ...to talk about, obviously as an expert on the history of logic.

00:01:18: and when people today tell us a story of lodging in the nineteen thirties it often comes out like there's this Hilbert Girdel-Genson camp and there is intuitionism as a separate camp.

00:01:32: But from your historical perspective, what was actually happening in this period?

00:01:38: And what do modern readers most often misunderstand about

00:01:42: it?".

00:01:42: I think as concerns formal logic role of Hilbert's not seen the proper light.

00:01:53: Hilbert wasn't an elderly university baron who did not do actual formal work in logic, no very much at least.

00:02:03: Then he hired Paul Bernice in seventeen or eighteen.

00:02:08: Bernice moved to Göttingen and I side with Richard Zack over where you want put it that the logical work of getting in school was done by Bernice.

00:02:26: have now the second REC Advanced Grant and one of the topics is Bernice lecture courses in Göttingen.

00:02:33: There are two lecture courses, One is twenty-seven The other one is twenty nine to thirty.

00:02:41: His student Erwin Engeler told me that poor Al was a hopeless lecturer.

00:02:47: so That may be reason why he wrote down all his lectures for last word in Goebbelsberger short and same as Gödelius'.

00:02:55: So I plan to publish these lectures by Werner Nice, and then everyone will see who did what in logic.

00:03:01: And so that's one thing... Well Hilbert of course gave the general direction of the Hilbert-Kruhe theory—that is correct but formal work was done by Werners nice students.

00:03:17: The other thing He was committed to intuitionistic methods in metamathematics, like for the end of forty-two.

00:03:38: It's very clear about this in his short hand notes that these are the methods which should be used.

00:03:46: In fact there is a well known dictum by Goedels That our method presupposes a kind of Platonism that doesn't satisfy any critical mind, as he said on the last day in nineteen thirty-three.

00:04:01: It was published in ninety five.

00:04:03: Now people have been wondering how can you put this together with the mathematical realist girdle?

00:04:11: I found the first version of this essay which is quite clear and even says what the methods are that they're acceptable.

00:04:18: They are like finitistic method extended intuitionistic or constructive things, so that's another aspect of this.

00:04:31: Now Gensen was also a constructivist.

00:04:37: he had just one idea which is all the things have to be developed on the basis of potential infinity.

00:04:45: well it means you cannot apply the law of excluded middle to infinite totality.

00:04:51: So That Was His Only Intuitionistic component.

00:04:56: This is now about the Hilbert-Gerdl-Genzen line that you mentioned.

00:05:02: Okay, can we have a bit more... so Girdel's incompleteness theorem came before and influenced obviously?

00:05:14: How much did they actually meet?

00:05:16: Did he discuss this to find out what was their interaction between Girdle and Genzen?

00:05:24: Gerdl Gensen was studying in Berlin from thirty to thirty-one.

00:05:31: Von Neumann had heard about incompleteness at the famous Königsberg meeting of September, nineteen thirties and also afterwards.

00:05:40: Gerdel went to Berlin And then he held a lecture course on Hilbert's Beweistheorie And there he explained the incompleteness theorem and second incompletence that he independently discovered.

00:05:55: Now, some of the contents are known because Jacques Herbrand was sitting in audience writing letters to his friends explaining these things... ...and I am pretty sure Gensen is also sitting here as well!

00:06:10: So then even one place in the Gensen notes which i think Makes sense only if he had been listening to for a moment.

00:06:19: So that was the first thing.

00:06:20: and then in thirty-two He decided too as he said cleared the situation with the consistency of arithmetic situation was what Gerdl's theorem had provoked.

00:06:36: And so, that was his aim.

00:06:39: They met only once and that was in mid December.

00:06:43: Thirty nine.

00:06:47: Gerdel was arranging his escape from Europe and he was in Berlin,

00:06:51: for

00:06:52: that purpose.

00:06:53: And then also held on the way a guest lecture in Göttingen and requested Gensin to be there.

00:07:00: so they discussed I think two or three days this had profound effect of Gerdels work in Princeton.

00:07:13: The functional interpretation was, I think inspired by this meeting.

00:07:20: I may say something quite spectacular which is that in Gensen's paper you find the Curry-Howard correspondence

00:07:31: for

00:07:32: natural deduction directly... ...the page has been preserved as the type lambda calculus rules of implication introduction and elimination.

00:07:43: Then he says the rest of rules are on another page, but that's lost.

00:07:48: The essential thing is there.

00:07:49: so we had read Church lambda calculus in thirty six and that was his reaction.

00:07:54: So I guess he must have explained these things together.

00:08:01: So

00:08:02: do you mention already again since Consistency proof right?

00:08:07: Of arithmetic?

00:08:08: this is absolute not So the audio analysis of arithmetic.

00:08:16: And so would you say this is a continuation of Hilbert's program?

00:08:20: I mean, to ask...

00:08:22: It's exactly that kind of continuation that Gerdl was looking for when he in these thirty-three lectures said that there's system A, System A sort of finiteistic and then you should extend it by constructed principles under the transfinite induction in Gentsen would be exactly that kind of a thing.

00:08:51: You have like a primitive recursive system, but when you add the trans-finite inductions so thats your metamathematical assumption.

00:09:03: So this fits exactly Gödel's sort.

00:09:08: what he said things should Like.

00:09:14: yeah.

00:09:15: So a very naive question on this and if it's not too broad to To have an answer.

00:09:22: so the image you drew was something where all these big actors of logic were to some extent constructivists or Intuitonistically at least.

00:09:34: well first, maybe they even believed in themselves.

00:09:40: classical division, they are the classical mathematicians and they're the intuitionists.

00:09:45: That's nothing that existed back then or was it just...

00:09:49: Well this is of course Hilbert's influence that the foundations on mathematics should be sort-of absolutely certain whatever he said.

00:10:01: And then he said that finiteistic methods are like Of course you can make errors but in principle clear then that you have made an error but it's sort of absolutely reliable, in some sense.

00:10:15: In which any counting is reliable.

00:10:20: and to extend because of Gerdl's theorem That was the framework for foundational work.

00:10:28: Then how other mathematicians reacted these things are another matter.

00:10:38: Genshin was trying to be very careful.

00:10:42: I think he made sociological moves or something like in the thirty-sixth paper, He uses classical logic even though if you study carefully at work You see that that Classical logic is no way.

00:11:00: essentially can just leave out excluded middle and all things go through Intuitionistically.

00:11:06: but then maybe The average reader that he was thinking of would think this is suspicious because there's a Broward guy in the story.

00:11:18: So, it used to be like sociology.

00:11:21: I mean... I wasn't... I mean, Hilbert and Browar had some argument right?

00:11:26: The Grundladenstreit did not influence Hilbert position or his position as students.

00:11:36: well when Haythin formalized into Shinnistic logic in nineteen thirty and he got the letter of congratulations from Bernice.

00:11:44: And Bernice wrote then also that I too did this thing in twenty-five after Rao's visit to Göttingen, and i did it so that addition system of axioms that you see in the Grundlag and the Mathematik, which have groups for each connective on quantifier.

00:12:08: But this was nothing to publish for Hilbert's assistant.

00:12:13: I don't know if he just didn't want to irritate Hilbert or otherwise thought it is not worth publishing.

00:12:21: He had other results like... In the twenty-nine lectures There's no finite system of valuations.

00:12:28: so that would exactly correspond to what you can prove in intuitionistic logic.

00:12:33: This is Gerdl's result from thirty-two, that intuitionistic logical is not the manual logic.

00:12:38: So nothing to publish.

00:12:39: but then if you look at about page forty Of The Grundlag and their Mathematique That came out in thirty four It was full of praise of Brower.

00:12:51: Healbert never even looked At the book...that for sure because he would have gotten a heart attack if you had seen that his book is praising Brower to Beyond All Limits.

00:13:05: Okay, but Beniz was very strange... ...because like he was like a very devoted servant to Hilbert.

00:13:16: and on the other hand then.. ..he gave course in set theory and that's also preserved.

00:13:25: And then in the later firties, he did this series of articles... ...and published a book on what is called Gödel Bernays' Set Theory.

00:13:34: You could actually strike the name of Gödel because... ...Bernice explained to Gödel what the axioms are.

00:13:41: People like to say Gödel Bernais.

00:13:44: So he had this set theory as well.

00:13:46: somehow He could live with double nature, Hilbertian formalist and someone who does axiomatic set

00:14:02: theory.

00:14:02: Okay so the Spanish... I mean we are usually when we say that Gensen introduced both natural reduction in secret calculus.

00:14:13: but how is this related to what Bernays was doing?

00:14:18: So Bernais was explaining what are called Hertz systems in the thirty to thirty-one lectures, no.

00:14:27: What was it?

00:14:27: Yeah... No twenty nine to thirty lectures where I think Genson were sitting.

00:14:34: Heard systems have sequence but they just like what you know called weakening and then he had a kind of simultaneous cut.

00:14:44: so he has stack of left premises in cut And Then You Had Just One Right Premise And Genson.

00:14:52: There was then a problem in these Hertz systems and that became Gensen's first work, but he did it at thirty-one.

00:14:59: And this is where he limited the stack... ...in the left premise of the Syllogism rule of Hertz to one.

00:15:08: Then you get the standard cut rule so now we can permute the order of cuts etc.

00:15:14: So I had this result when they did that on thirty-two.

00:15:17: This clearly either he was listening for lectures Or then Bernice had explained him all the details.

00:15:25: So he did that, but in the beginning of thirty-two... ...he started to figure out his sort of response to Gerdel's incompleteness and the task was to formalize mathematical proofs And for this he invented natural deduction which is a fairly good state by September thirty two.

00:15:52: Then around January or so, thirty-three he had a full Proof of normalization for intuitionistic natural deduction from predicate logic.

00:16:03: Yeah But then it didn't get the true four classical logic and he thought its It doesn't hold them.

00:16:09: He invented sequent calculus to have an analogous result for classical.

00:16:14: I see

00:16:17: one can see from his notebooks quite clearly how how he came to Sequent Calculus.

00:16:22: It was when he wanted to translate between natural deduction and axiomatic logic, so an axiomatic logic as you have it in the Hilbert Ackerman book.

00:16:36: by the way Hilbert Dackeman's books were written very nice.

00:16:45: So Wilfried Sieg has done a lot of work on... In the introduction to this one-thousand page volume, he says that chapters I to X of Hilbert Ackermann are based on Bernice's typewriter and manuscript.

00:17:01: And a couple of pages later he said, chapter eleven through fifteen is now based on Bernais' Typewriter and Manuscripts.

00:17:07: That was the whole book!

00:17:09: Then he says why is Ackerman there?

00:17:11: He's more like a textual editor... My guess is that Bernaiss wasn't satisfied with his treatment.

00:17:20: logic in the Hilbert Ackerman which is based on Russell's axiomatics with just negation and disjunction, universal quantifier.

00:17:30: And existential quantifier because they wanted to have prenex normal form.

00:17:35: that's handy for two quantifiers anyway.

00:17:37: so I think Berners would've want you see a book where groups of axioms.

00:17:43: but it was great luckful logic that this Hilbert Akkermann Book was published as airbrand read and his reaction was to do all the results in logic.

00:17:53: And Gerdl read it on May or the summer of twenty-eighth, without Hilbert Ackermann there would not have been Erbrand's work nor neither Gerdel's work.

00:18:03: so... In the end that is a good thing!

00:18:07: So anyway now how did I get into this?

00:18:09: Yes about natural deduction.

00:18:13: When Genson did this natural deduction as sequence calculus then finished his thesis late May, thirty-three.

00:18:22: Bernice had been fired from his position in April and the reason was that he was non-Aryan That is sort of correct terminology at this time.

00:18:36: And he also finished the Grundlag and Mathematics.

00:18:39: so He did not read Gensen's thesis At that

00:18:44: time.

00:18:46: I mean Wildred somehow went was then officially presenting sort of the thesis.

00:18:53: But, in thirty-four when I read it he gave a lecture series called Grundzüge des logik kalkius like outline over logical calculus.

00:19:04: in Zurich in thirty four years and there he goes through natural deduction but i'm a bit disappointed at that presentation later... He worked on sequence calculs but they're like fifties and sixties And there's some good results which show that he had been talking about the details with Gets.

00:19:25: So, what you were

00:19:26: just saying is sort of reflects this usual.

00:19:31: so views and natural reduction as a right proof calculus for intuitionistic logic and sequence calculus fits better with classical logic.

00:19:44: This was Gensen's view

00:19:48: A very short interlude because on this channel we haven't had so much proof theory.

00:19:53: and would you mind giving like a Very rough idea of the small syntactic side of things.

00:19:58: And maybe We also already mentioned to cut rule which is I mean, they're very special rules.

00:20:04: So just speak for our audience.

00:20:07: If that is so then those who don't know these things will not pass.

00:20:11: my first class in logic In Helsinki Every philosophy student used to know what natural deduction is.

00:20:22: Anyway, so natural deductions just... The basic feature that mathematical inference begins with assumptions and you move from the assumptions towards their conclusion.

00:20:39: Now in Natural Deduction ...the process From the Assumptions To a Conclusion That You Want Have Is Not to Guide Not Formally as well-guided, in sequence calculus.

00:20:52: In sequence calculus you have a formal notation where the assumptions at left are listed and then you write an arrow which you read from the left side follows And on the right side is your conclusion.

00:21:09: Then you can analyze the assumption into components.

00:21:16: So this means that you do kind of a root-first construction or formal proof, and it is quite nicely supported.

00:21:25: And then if you arrive at... so these things are called sequences in which the left list of formulas on the right have the conclusion.

00:21:37: In this analysis when you arrive to sequence where there's an assumption One assumption is equal to the conclusion, then you are finished with that branch of full search.

00:21:54: And this can be generalized... This could now be read from assumptions at left arrow and conclusions on right follows.

00:22:01: Then Gentsen generalizes it.

00:22:03: so there's a number cases in the right also.

00:22:07: At the left you have assumptions and at the right case.

00:22:12: These are the cases under these, and they're assumptions.

00:22:15: So that makes for a very effective classical logical calculus.

00:22:20: The propositional calculus is such that proof searches like deterministic and terminating has all sorts of nice properties And you also see why it is complete calculus because It's really closely related to semantics.

00:22:40: In intuitionist logic usually one just have one formula the right, what else can I say.

00:22:49: Now yes okay then normalization in natural deduction.

00:22:52: so let's say that you assume A and then you infer B. now you are allowed to conclude a implies b. this is called implication introduction And the temporary assumption A is closed here.

00:23:06: Then on the other hand if you have either assumed or approved a implies B. If you also assumed or proved A. Now if you do this one after the other, so first to introduce A implies B and then you eliminate it.

00:23:23: Then what remains is that there's a path from A to B And then continue from B. So you can compose these parts but leave out the A implies b formula which is kind of locally longest formula.

00:23:45: This is called a step of normalization, and Gensen showed then that all derivations in intuitionistic natural deduction for predicate logic convert to normal form.

00:23:58: And the most essential property of a normal form is what you call subformular properties.

00:24:03: so all formulas are sub-formulas as open assumptions or conclusions.

00:24:13: Now this gives decidability for into-synistic propositional logic.

00:24:18: But then, for predicate logic you have to allow that if we have like for all x fx than any instance is a sub formula.

00:24:28: so with quantifiers do you have an infinity of sub formulas and That's actually one way.

00:24:34: looking at the absence over decision method for predicated logic You can find ever new instances.

00:24:42: Now, Genshin wanted to do like this that he includes arithmetic in the system of natural reduction.

00:24:50: And when you assume there's a derivation from zero it no one equals two way.

00:24:55: at that time they didn't count zero They started with one.

00:24:59: So if we have a derivate on one equal as two.

00:25:02: If then you had normal derivation and easily see There is not normal derivates over an atomic formula Zero equals One.

00:25:11: So his aim was to prove the consistency of that arithmetic.

00:25:15: But then he realized, well... ...the normalization proof is kind-of finiteistic It's a finitary algorithm And so this isn't compatible with Gödel's incompleteness theorem.

00:25:29: What he did?

00:25:30: This was like January or maybe February.

00:25:33: thirty three.

00:25:36: He made an emergency solution invented sequence calculus, and then he presented the thesis about pure logic.

00:25:46: Natural reduction in sequence calculus for pure classical and intuitionistic logic.

00:25:51: so that was his sort of emergency solution for finishing a PhD.

00:25:56: And I see you wanted to do already consistent job.

00:26:00: arithmetic.

00:26:00: Yes That is the original aim of thirty two and there's a first record of their rule system for natural deduction from September and it still has a rule of induction.

00:26:14: So you have some property F, as one has this property.

00:26:23: then the other premise is the derivation that if X has the property than the successor or X had the property And conclusion is that an arbitrary term has the properties That was in natural deduction system to prove normalization for this thing.

00:26:40: But now the trouble, of course is that you cannot restrict formulas in these induction rules beforehand if you do it and get some system

00:26:55: of arithmetic.

00:26:58: Yes?

00:27:00: So...

00:27:01: You explained this normalization curve which I mean was a step into reduction force by elimination.

00:27:07: So as we now know, this is specifically the petal law of lambda calculus.

00:27:13: But I guess that was only realized in much data right?

00:27:16: No, Gentsen... As i said.. In thirty-eight he wanted to prove the consistency analysis and functional hierarchy over ordinals.

00:27:31: so assume given the constructive ordinals then if you have like A implies B, there are some function in the hierarchy over the ordinals that transforms the ordinal and realizes A into an ordinal that realises B. Then when you do implication introduction then you do lambda abstraction do implication elimination, we do functional application.

00:28:02: And he writes all these down and the terms are nicely written in a blue pencil next to formulas just like you do if you type lambda calculus in natural reduction style.

00:28:14: so exactly that way The aim was defined.

00:28:20: So he clearly knew steps of normalization Just mean you have an abstraction and then, in the new You have an application over the abstraction.

00:28:35: And then even than you just compute the value by substituting The argument.

00:28:41: so he saw clearly that normalization is the same as their computation of oven Application into into a normal form.

00:28:54: So that was.

00:28:56: But he didn't tell anyone.

00:28:57: He didn't talk about the normalization proof to any one.

00:29:01: it happened that This was quite some story In two thousand and five.

00:29:07: I was in Munich as a Humboldt fellow, and then I traveled to Erlangen where German University professor philosophy had Gensens manuscripts That he had gotten from Gensen's history.

00:29:21: so like four hundred pages of gentses manuscripts.

00:29:26: So I went there and was able to study them.

00:29:29: And so, i found a hundredth version of Gensen's doctoral thesis... ...and it contained this absolutely detailed proof of normalization for Intuitionistic predicate logic some fourteen pages.

00:29:47: How?

00:29:47: This is Doug Pravitz great result when I came back home then found Doug and explained this matter.

00:29:56: He took it extremely well.

00:29:59: Now what not when I talk about him?

00:30:00: I'll tell you that last week, I was in Stockholm.

00:30:03: There was a celebration of dark profits ninety years.

00:30:08: he Was there also very fresh and I was giving a talk About the development of natural deduction.

00:30:16: then they're also recollected this event.

00:30:19: so So this result was like hidden from thirty-three to two thousand and five.

00:30:27: And it was the original of these particular pieces with the Bernice papers, had just folded this pile of papers that had the panwritten doctoral thesis.

00:30:39: then he had written sort of diagonally over it concept from Hagenzen sketches of Mr.

00:30:49: Gensen.

00:30:50: now actually I will show make some published notes do you see?

00:30:58: So,

00:31:00: said from the seller Gerhard Gensen shortened notes on logic and foundations of mathematics.

00:31:06: This book is two thousand seventeen and it contains an English translation of The Doctor of Feces with the normalization proof And many other things.

00:31:19: Yes so uh...the title It's like this Folders about one and a half centimeters each.

00:31:32: Selected such papers in the summer of forty-four, left them on a family summer place... ...on the island of Rügen in the Baltic Sea.

00:31:40: And then some of these papers it's written Actually I can read from German here.

00:31:47: Then i give translation.

00:31:49: So its this Here only a few things can be used.

00:31:55: Then it says, Seite one sixty-one to one ninety eight außer babela.

00:32:06: So in the basement is the work on Habilschrift.

00:32:11: so think of all things unimportant or repeated In the cellar.

00:32:18: here are only Things that could Be useful.

00:32:22: and The other One then Says That that these pages, one sixty-one to one ninety eight in the cellar except for a couple of pages.

00:32:31: And this was... These were the pages in which one finds hundreds and versions of Gensen's habilitationshift with which he finished on September thirty nine before his military service published in forty three Which establishes ordinal proof theory as field of study.

00:32:53: Now, this just means that the other pages have been preserved.

00:32:59: They continue directly to the habilitationshift by about as much of a published part.

00:33:10: The published parts are like twenty pages and it's four chapters or four sections.

00:33:18: And the unpublished continuation is another maybe four sections, maybe thirty pages or something.

00:33:26: This is now being... The work on this manuscript has been done by Daniel Misselbeck-Wessel in Munich so he's a DFT grant for that.

00:33:43: there will be two more Genseng books when Daniel has finished one of the proof theory into shynistic arithmetic and to these ones belongs continuation of the paper that established ordinal proof theory.

00:33:59: And then another one is... it's like WA, this like Wiederspros-Feyheit analysis.

00:34:06: so consistency of analysis That's another two hundred pages.

00:34:09: So these books will be published in next few years.

00:34:16: Daniel was originally planning to become part my new ERC project but he got this one.

00:34:23: when it's finished, he will come to my group.

00:34:27: So there is good hope and we also hope that against and uses the Kare-Howard correspondence in this proof here of intuitionist charismatic.

00:34:39: so would be nice to see it in action.

00:34:44: these are great resources.

00:34:47: may I ask a little bit about the process from the documents to these books.

00:34:54: I mean, how does this historical work feels like?

00:34:59: So the Genshin was born in nineteen oh nine and so there was in nineteen twenty five reform of short-term competing shorthand schools in Germany.

00:35:12: And then the German parliament issued a decree by which it became forbidden the associations for these Lagabers, Berger and Schultz-Eschry and two others.

00:35:29: They had to agree on a unified shorthand.

00:35:32: so they made compromises and came with this called Einheitliche Kurzschrift Unified Shorthand.

00:35:37: that's still taught.

00:35:39: there are people who read it.

00:35:44: So this German professor was doing the transcriptions but he never sort of finished anything.

00:35:50: I got some of the transcripts from him.

00:35:53: There was Helmut Schwichtenberg's secretary who knew it, and I just commissioned transcriptions.

00:36:00: And then I trained myself to control the correctness of the transcription so that there is a raw transcription in the words... ...and figured out what the sentences are and translated into English.

00:36:16: Now some people say why don't you publish German originals?

00:36:20: To this I have to say Shorten is a thing in itself, and there's no German original.

00:36:28: There was the German reading of shortens... ...and an English reading.

00:36:33: I sometimes do directly English from the shortened.

00:36:37: So anyway so i had this sort of passive reading on their unified shorten.

00:36:41: but then when started with Gerdl who has been tolder to use the Gabelsberg system.. ..then I just decided to forget the Unified and trained myself for about one year in reading Gader.

00:36:57: There are like five or six people who read it today, three of them know about logic and they're like my research

00:37:05: group.

00:37:06: so... Can you train an AI to read?

00:37:10: If that were possible I would be the first one do with now some.

00:37:20: It would be part of the subject called handwriting recognition.

00:37:28: Handwriting recognition of handwritten addresses in letters, when you have a list over few hundred possible street names has had some eighty percent success.

00:37:43: now replace the few hundred street names with like one hundred thousand or whatever German words of fifty thousand, twenty thousand say twenty thousand German words in shorthand.

00:38:03: So there's something called like a people who are experts on this field.

00:38:08: they think it is a paradox that to read a word handwritten you would have know the letters.

00:38:15: To read the letter you will need to know the word.

00:38:17: so go into circles.

00:38:21: well maybe But once ordinary handwriting has been cleared then the next step would be short-term.

00:38:31: I have, once a research application turned down because one guy from certain country in Central Europe wrote that all of this should be done in AI.

00:38:45: Now you can take someone who applies for funding For an idiot Who never thought about these possibilities In eight

00:38:53: or

00:38:53: ten years.

00:38:54: or else you can think that maybe these people know what they are doing and I don't.

00:39:00: So, but i got the secondary rc luckily.

00:39:04: well...I was prepared also..i just thought this is not viable.

00:39:07: yeah maybe someday there's some people who would like to try yes?

00:39:14: I would like move on to a very slightly different topic And this is sort of association with Goethe philosophy.

00:39:23: as playgroundism I mean, Girdel obviously engaged with intuitionism in the dialectic interpretation and negative translation.

00:39:33: And so on.

00:39:34: how does this fit together?

00:39:35: Yes!

00:39:36: So i will be giving a talk on the first of June in Oxford about Girdle and Intuitionism.

00:39:51: Rudolf Karnapp wrote down discussions he had with Goethe and Goetle said that he is an intuitionist, a formalist.

00:39:59: And then... He says that he came to think about incompleteness because of Brauer's talk in Vienna.

00:40:07: It was provoked through the thought that mathematics cannot be formalized completely by Brauer talking Vienna.

00:40:16: Then he did his little results on intuitionistic logic.

00:40:21: In thirty-five he decided that there's nothing to be done in... Well, why don't I now show the girdle books we have produced and then i will tell all these things while i do it.

00:40:42: So this is now chronological.

00:40:46: This was in nineteen twenty.

00:40:49: Can mathematics be proved consistent?

00:40:52: all the notes about incompleteness in Gerdod.

00:40:56: And, uh... The interesting thing is that Gerdor's first approach was to define a truth predicate for higher-order logic or for Principia Mathematica and then have a meta theorem which says that all provable result—all theorems of Principia Matematica are true.

00:41:19: And then you do the Gerdl sentence which says that I am unprovable.

00:41:23: If it is provable, if

00:41:24: true.".

00:41:25: Then he met von Neumann and suggested... ...that we should do an imprimative recursive arithmetic.

00:41:32: So Gerdler rewrote his essay on the concept of truth….

00:41:37: …and even the word Truth was not mentioned once in the paper.

00:41:43: That's what is now considered to be Tarski's approach too!

00:41:47: to like semantic approach to incompleteness.

00:41:49: That was Gerdel's original approach, so that the main thing about this is from twenty-one it's only in German.

00:42:02: could Gerdels not its sensor quantum machine?

00:42:04: This is done by Tim Letten and Oliver Parsons.

00:42:06: So Tim is one of the readers over the short hand.

00:42:12: This is a...Gerner wrote down three hundred and forty remarks on foundations of quantum mechanics in first half of thirty five.

00:42:23: And then he said that quantum mechanic shows that Kant was right, but the Dean Amzig you can never have.

00:42:31: because if you have a quantum mechanical system and then you have measurement apparatus by von Neumann's analysis of their measurements situation when they interact become superposition state from a quantum mechanical superposition, you can project the pure state of the object system.

00:42:52: So that's sort of transcendental and so... That is an idealistic view of physics.

00:42:59: And then he says it's same in mathematics that Russell's paradox shows.

00:43:09: any universal set that contains all things is paradoxical.

00:43:15: And he says, this is just like classical physics which gives a sort of complete objective picture over the world.

00:43:22: But that's sort of contradictory.

00:43:25: So

00:43:26: He

00:43:27: decided to leave logical foundations.

00:43:29: but then he gave a lecture course in the summer of thirty five on On logic and there you also covered set theory.

00:43:38: so then here found Found ideas about proving their independence of the axiom, and decided that would be a better bet.

00:43:48: So Goethe had a career problem.

00:43:51: he was suffering from giving lectures.

00:43:54: He suffered greatly from it his notebooks showed.

00:43:57: And then he was a pacifist and anti-militarist and of course anti Nazi.

00:44:05: so he could see no future in

00:44:07: Europe.

00:44:12: clear feeling is that he thought, well now I will prove the independence of a continuum hypothesis and axiom of choice.

00:44:19: And then i would get to job in

00:44:20: America.".

00:44:21: This actually happened because In thirty-seven years he had the consistency proofs from Neumann then sold it.

00:44:30: so that was... Now third book also by Tim Lehten Gerdas notes from Vienna in thirty-seven to thirty eight.

00:44:44: There's the last breath of The Vienna Circle, he is writing down the meeting protocols on what it called the Zilsel circle and all sorts interesting things anyway.

00:44:57: so now this is Gerdal book of twenty two.

00:44:59: This was easy.

00:45:01: It´s a Princeton lecture on intuitionism.

00:45:03: that I did with Maria Hemen until i was in my group gonna get this lecture course In which she explained in detail their girdle functional interpretation.

00:45:15: now the aim with that Interpretation was to extend it to analysis and prove the consistency of analysis In twenty two.

00:45:24: I published

00:45:25: a

00:45:25: little book each year a good old book chapters from girls unfinished book on foundational research in mathematics.

00:45:32: So there's this Highting book from thirty-four, it's about just seventy pages on Mathematische Grundladenfelsung.

00:45:40: It covers intuitionism and proof theory.

00:45:45: And Goethe was supposed to write about logicism and logical calculus and so on.

00:45:50: He never finished his part... ...and it was believed that he didn't get anywhere.

00:45:54: But I was able to reconstruct his chapters when we published this book.

00:46:01: Then the big thing we did, Gödel book of this will take some time.

00:46:05: Gödel Book of twenty three Resultate Grundlag and results on foundations And This is with Maria.

00:46:11: also Goedel wrote from nineteen forty to forty two down results in logic and foundation she considered be finished?

00:46:21: And it's a three hundred and sixty eight pages and one hundred and twenty six theorems numbered.

00:46:29: Sixty percent Is about set theory.

00:46:32: Aki Kanamori has written an essay about them.

00:46:35: One fourth is about intuitionistic logic, so it contains for example a syntactic proof of the converse of Gödel's result of thirty-three in which he shows how to translate intuitionistic formulas into formulas about provability and a suitable model logic.

00:46:56: Then he conjectured that you can also go from modal logic to intuitionistic logic, and now we do it in detail.

00:47:04: There's a special issue of this Resultate Grundlagen book... It is the latest in the journal Logiket Annaliese.

00:47:12: So there are four articles about these books.

00:47:17: Now then This is Gerdl book of twenty-four Portrait Of Jan Gerdel Education First Step first steps in logic, the problem of completeness.

00:47:28: So this contains Gerdas' first sort of scientific and philosophical things from when he was in last class at the Lyceum.

00:47:37: And his study is how he became a logician by attending Karnab's course on axiomatics application.

00:47:51: He did that in twenty-eight and then he found the completest problem In The Hilbert Ackerman book That Carnop gave to him.

00:47:59: So, that covers those things.

00:48:01: And I still have one more book.

00:48:03: This is Gerdel's Book of Twenty Five Gerdl & Hahn.

00:48:07: It's under Gerdle & Hahn's name Mathematical Logic in Vienna.

00:48:10: so Hahn was Gerdler's mathematics professor.

00:48:13: They had a seminar in thirty One To Thirty Two and the notes Have been written down.

00:48:21: This one also contains an essay of Gerdel's about intuitionism.

00:48:26: That was his trial lecture for becoming a private consent in February, thirty-three So that's fourteen pages.

00:48:35: He published these results on intuitionistic logic and they are just like one page.

00:48:39: each article is about one page One is a bit longer And now he explains in abundant terms those results into the intellectual.

00:48:47: We found it in short-hand in the Gerdl books.

00:48:52: So that's their status now, eight Gerdel books in six years.

00:48:58: Impressive!

00:49:01: You already mentioned this.

00:49:04: for destruction of logic and Europe as a consequence obviously of World War II into terrible crimes which were committed... all the logic moved from Europe to America.

00:49:24: Impact, I mean what would have happened otherwise?

00:49:29: How would history of logic had changed if this hadn't happened as catastrophe in that

00:49:34: sense?".

00:49:36: Well... This means that Gernel would've gotten some sort of a position in Europe If not for Nazism i'm sure And Gensen as well, and maybe they would have started to collaborate... ...and give a proof of the consistency of analysis or something.

00:49:54: Now then we would've heard about Kari Howard.. ..or our fathers or grandfathers and mothers who'd have heard about Karri Howard in the forties.

00:50:04: So lots of things would be faster.

00:50:08: Well than of course this United States offered enormous resources so it became extensive In Germany, so there were no professors of logic in the third.

00:50:23: Bernice was an extraordinary professor because of Hilbert's prestige and some people had some jobs.

00:50:33: Frankel had a job doing set theory but then he moved away And maybe a couple others.

00:50:40: So The scale wasn't like that.

00:50:46: So maybe he was lucky in this sense.

00:50:54: The direction of logical research... In the states, there were cleaning.

00:50:59: Cleaning was doing things that you see from his introduction to metamathematics that he knew sequence calculus as a main tool for the book more or less.

00:51:12: And then there's Tachyoti.

00:51:14: but people who took Proof theory seriously, they were like Chrysler and Takeuti.

00:51:21: And Kleeney and Kari not so many...

00:51:28: What about church?

00:51:33: Church is hopeless!

00:51:34: I mean the introduction to mathematical logic from fifty six.

00:51:42: it says about natural deduction that psychologically interesting explanation of logic, something like this.

00:51:52: So it's just axiomatic logic and its... Axiomatic Logic is a disaster.

00:51:59: Gerdel also noticed that axiomatic logic is useless in practice because when he did his Karnapp exercises one of the exercises was to formalize arithmetic.

00:52:12: so he formalized second-order arithmetic.

00:52:16: But he wanted to formalize also proofs, but we cannot do any proofs in axiomatic logic because you would have to guess axiom instances and then just use implication.

00:52:26: So he invented on the spot linear natural reduction that she used in his derivations.

00:52:33: The longest derivations are over eighty lines And like for maybe three or four nested assumptions.

00:52:44: But then he didn't think that it's of any interest in itself, contrary to Gensi.

00:52:50: So now when... In the States of course set theory and model-theory became dominant topics.

00:53:00: so there was like maybe there was a Tarski school and a Kleeney School And the Kleeneyschools were very small Recursion Theory and Soundproof Theory Intuitionistic things.

00:53:17: Okay, so maybe that's the draw a line to today and obviously especially Genson's work has influenced lots of things like lambda calculus, Curry Howard but also these proof assistants they're using I mean like Rock or Cork and Akta and Linne.

00:53:38: So would Genson recognize proof assistance as descendants?

00:53:46: Well, I haven't thought about this.

00:53:49: So

00:53:50: what would he say?

00:53:52: There are lots of papers and results in proof theory which I think Genshin would have enjoyed to have known especially these contraction-free sepian calculator or sort the state of art.

00:54:09: well He said when he was working towards the consistency of analysis.

00:54:15: then he said that... He thinks it's just more of the same as what he has been doing in ordinal analysis, but its like a hundred pages compared to two pages.

00:54:29: So it would be kind of monstrously big thing to do.

00:54:35: whether all steps are correct is of course really complicated.

00:54:41: and whether all step are correct Crucial question which you may not be able to survey without proof assistance.

00:54:50: Yeah,

00:54:53: yeah and since we are already like close to now or maybe let me ask you one Question whether you would there's something else?

00:55:02: You would really like to tell us about.

00:55:04: I mean we haven't touched on your own work.

00:55:05: they're still into a cynistic geometry to be talked about your work on proof theory, but I guess we cannot squeeze that in this episode anymore.

00:55:15: But is there anything?

00:55:18: and yeah?

00:55:18: So i already told you the new ERC project began just few months ago.

00:55:24: so we have Gerdl Gensen and Bernice in focus.

00:55:27: And i told you about bernice and i said that Daniel will be working with Gensen.

00:55:35: Then there's with Gerdl, so it's the as concerns logic and foundations.

00:55:40: The absolutely most important thing left in Gerdle is It's notebooks he called Arbites hefte.

00:55:48: So the first three are about set theory written in Europe like thirty eight or so but then from four to sixteen.

00:55:55: One thousand nine short hand pages He wrote down in Princeton form.

00:55:59: forty two baby early forty-three.

00:56:02: And the main topic in these Arbites have to... Well, let's say most of it has to do with intuitionism.

00:56:12: So then there is a formal theory of intuitionistic analysis based on choice sequences that are written in seven runs of text maybe hundred pages or something.

00:56:31: So Gordon's hope was to determine how many real numbers there are in this Intuitionistic theory

00:56:39: of

00:56:40: rules.

00:56:41: and then does a theory of higher order computable Functionals, and that those were Plants to act as models for the for intuitionistic analysis.

00:56:51: So you would get The consistency of analysis so it will get How Many Reels?

00:56:58: That's the original continuum problem and consistency of analysis, which are Hilbert's first-and second program.

00:57:06: Goethe failed with both these and then he got angry at Brower... ...and started I think invented this fantasy about set theoretical realism that even Solomon Pfefferman can't take it seriously.

00:57:24: And Chrysler also said that is not good But anyways.

00:57:28: So I have done the transcription and translation into English, but... ...the plan is now to try to understand the girl's results.

00:57:39: Like he has a calculus of what we call species or functions so you have finite information about the behavioural function.

00:57:48: then more information is fed in that when they have a bare space for some such for these pieces of functions And he uses this word, that they extend your information and so on.

00:58:02: So then he compares it to co-wind... I think quite exciting things.

00:58:11: maybe results nobody ever thought about.

00:58:18: This is to be expected.

00:58:20: with Gerdahl As my own work I have a good number of recent results in logic, but one result is special that comes out of Gerdl.

00:58:31: In some notes he asks what the constructively strongest formula classically equivalent to given formula?

00:58:42: And then says it's the negation normal form.

00:58:45: and after trying... He said I don't prove this!

00:58:49: Then i tried to prove for couple months.

00:58:51: they found an example.

00:58:53: Then I found out that for propositional logic, the constructively strongest formula classically equivalent to a given formula is its disjunctive normal form.

00:59:03: So you have a lemma where the disjunctive normal form of a formula intuitionistically implies this formula.

00:59:11: This is the crucial lemma.

00:59:13: and then we can show any formula which is classically equal to the given formula the disjunctive normal form of a given formula.

00:59:25: This then led to result that think about the Boolean implication lattice, or these disjunctive normal forms.

00:59:33: and then you think about hiding lattice.

00:59:36: And now I can prove that The hiding lattice adds no element inside elements inside the boolean lattice but just on top of it.

00:59:46: So with one atom You have contradiction.

00:59:48: Then you have the atom P Have the negation And then you have P or not P. That's the classical boule and lattice, by this Riga Nishimura result we have that P implies non-non-P... ...and rest of the formulas that intuitionistic logic adds are all classical tautologies.

01:00:10: So nothing inside the boule & lattice!

01:00:14: The same is true for any number of atomic formulas.

01:00:18: Classical and intuitionistic logic live a peaceful coexistence, sort of.

01:00:23: Or... Intuitionistic logic sits on the top of classical logic in this lattice-theoretic sense.

01:00:33: Now I was also able to show that because now you ask well if there is only one formula added by intuitionist logic In the case of one atom That it's not a classical tautology.

01:00:44: How many are they with?

01:00:47: two or more atoms and I was able to construct it's not the difficult construction at all.

01:00:53: So, iIwas able to construct an infinity of formulas that are not classical tautologies but they're intuitionistically inequivalent.

01:01:03: so there is an infinity on non-tautology.

01:01:05: as added.

01:01:08: this was a directly inspired by Gerdler's wrong result.

01:01:17: So now I told you something about my most recent work.

01:01:21: Good,

01:01:22: excellent!

01:01:23: Yeah so

01:01:24: much more things...

01:01:25: I have a paper about this and the paper

01:01:27: should.

01:01:28: i hope it gets published soon?

01:01:31: It goes together with the historical paper that gives The Problem And Ghetto's failed solution.

01:01:38: That's what they're doing.

01:01:40: We are publishing these here.

01:01:42: great thank you so much for this window into Your work and I mean when I was not enough to cover everything or even every branch.

01:01:53: I could easily talk for several weeks about the other things And also Bernice who's left a bit aside here, but i mentioned some of these things.

01:02:02: Okay

01:02:04: So what let us say?

01:02:05: thank you for now.

01:02:07: Thank You very much.

01:02:08: There will be plenty of opportunities to talk at meet end.

01:02:12: The world of logicians is smaller than It should be.

01:02:16: So there will be other opportunities, thank you

01:02:19: very much.

01:02:21: and for the people who can ask your questions comment below.

01:02:25: we'll link to many books that were mentioned in the description of this video so they have a look at them as well.

01:02:34: We try to reply to as many questions as possible but most often it works out for all of us.

01:02:41: so feel free.

01:02:43: And then, thanks for watching.

01:02:44: Bye

01:02:46: bye!