Aug 13, 2026 · 1 hr 3 min · 15 segments
The Hidden History of Logic: Jan von Plato on Gödel, Gentzen & Bernays Your support helps us keep these conversations going! If you’d like to contribute, you can buy us a coffee here…
Jan von PlatoGuest
Thorsten AltenkirchHostDeniz SarikayaHost
In Helsinki, you-- every philosophy student used to know what natural deduction is.
Anyway, so natural deduction is just you-- The basic feature is that the, uh, that, uh, mathematical inference begins with assumptions.
Now, in natural deduction, uh, the process from the assumptions to the conclusion that you want to have is, uh, not guide-- not formally l- as well guided as in sequent calculus.
In sequent calculus, so you have a formal notation in which, uh, you write the assumptions at the left as a list, and then you write an arrow, which you read like from the left side follows.
Um, then you can, uh, analyze the assumptions into components and the conclusion into components.
And so this means that you do a kind of a root first construction or a formal proof that this is quite nicely supported.
And then if you arrive at, uh-- So these things are called sequence, in which you have at the left a list of formulas, at the right y- you have the conclusion.
And, uh, you-- if-- in this analysis, if you arrive at sequence in which you have, uh, the assumption-- one assumption is equal to the conclusion, then, then you are, you are finished with that, um, that branch of proof search.
So this can be now read that fr- from the assumptions at the left of the arrow, the conclusion at the right follows.
And then Gentzen generalized this so that you have a number of cases at right also.
So the left-- at the left you have assumptions, and the-- at the right you have cases, and you say that the-- these are the cases under this, and these are the assumptions.
The propositional calculus is such that the, the proof search is like deterministic and terminating and has all sorts of nice properties.
And you also see why it is a complete calculus, because it's, uh, very, very closely, uh, related to semantics.
This is called implication introduction, and the temporary assumption A is closed here.
Then on the other hand, if you have either assumed or proved A implies B, if you have also assumed or proved A, then you can infer B.
In Helsinki, you-- every philosophy student used to know what natural deduction is.
Anyway, so natural deduction is just you-- The basic feature is that the, uh, that, uh, mathematical inference begins with assumptions.
Now, in natural deduction, uh, the process from the assumptions to the conclusion that you want to have is, uh, not guide-- not formally l- as well guided as in sequent calculus.
In sequent calculus, so you have a formal notation in which, uh, you write the assumptions at the left as a list, and then you write an arrow, which you read like from the left side follows.
Um, then you can, uh, analyze the assumptions into components and the conclusion into components.
And so this means that you do a kind of a root first construction or a formal proof that this is quite nicely supported.
And then if you arrive at, uh-- So these things are called sequence, in which you have at the left a list of formulas, at the right y- you have the conclusion.
And, uh, you-- if-- in this analysis, if you arrive at sequence in which you have, uh, the assumption-- one assumption is equal to the conclusion, then, then you are, you are finished with that, um, that branch of proof search.
So this can be now read that fr- from the assumptions at the left of the arrow, the conclusion at the right follows.
And then Gentzen generalized this so that you have a number of cases at right also.
So the left-- at the left you have assumptions, and the-- at the right you have cases, and you say that the-- these are the cases under this, and these are the assumptions.
The propositional calculus is such that the, the proof search is like deterministic and terminating and has all sorts of nice properties.
And you also see why it is a complete calculus, because it's, uh, very, very closely, uh, related to semantics.
This is called implication introduction, and the temporary assumption A is closed here.
Then on the other hand, if you have either assumed or proved A implies B, if you have also assumed or proved A, then you can infer B.
The rest of this transcript — segmented and speaker-labeled, so you land on the exact moment something was said
Search every transcript — by keyword, by phrase, or by meaning, across every show Radar indexes
Trends — what is surging across podcasts, measured against its own baseline
Alerts — when a name you follow appears in a newly indexed episode
No account is needed to search Radar.
