<
<div class="span index">1</div> <span><a class="" data-remote="true" data-type="html" href="/series/species-unite">Species Unite</a></span>
Stories that change the way the world treats animals.
Player FM - Internet Radio Done Right
Checked 13d ago
two 週前 前追加した
コンテンツは Cody Roux によって提供されます。エピソード、グラフィック、ポッドキャストの説明を含むすべてのポッドキャスト コンテンツは、Cody Roux またはそのポッドキャスト プラットフォーム パートナーによって直接アップロードされ、提供されます。誰かがあなたの著作物をあなたの許可なく使用していると思われる場合は、ここで概説されているプロセスに従うことができますhttps://ja.player.fm/legal。
Player FM -ポッドキャストアプリ
Player FMアプリでオフラインにしPlayer FMう！
Player FMアプリでオフラインにしPlayer FMう！
))
Daily Deals
聞く価値のあるポッドキャスト
スポンサード
The Church of Logic
すべての項目を再生済み／未再生としてマークする
Manage series 3653028
コンテンツは Cody Roux によって提供されます。エピソード、グラフィック、ポッドキャストの説明を含むすべてのポッドキャスト コンテンツは、Cody Roux またはそのポッドキャスト プラットフォーム パートナーによって直接アップロードされ、提供されます。誰かがあなたの著作物をあなたの許可なく使用していると思われる場合は、ここで概説されているプロセスに従うことができますhttps://ja.player.fm/legal。
A podcast about logic in all its forms, going into the historical, social, mathematical and philosophical aspects of the subject.
…
continue reading
57 つのエピソード
シェア
すべての項目を再生済み／未再生としてマークする
Manage series 3653028
コンテンツは Cody Roux によって提供されます。エピソード、グラフィック、ポッドキャストの説明を含むすべてのポッドキャスト コンテンツは、Cody Roux またはそのポッドキャスト プラットフォーム パートナーによって直接アップロードされ、提供されます。誰かがあなたの著作物をあなたの許可なく使用していると思われる場合は、ここで概説されているプロセスに従うことができますhttps://ja.player.fm/legal。
A podcast about logic in all its forms, going into the historical, social, mathematical and philosophical aspects of the subject.
…
continue reading
57 つのエピソード
すべてのエピソード
×
I talk with the brilliant and charming Siva Somayyajula about structural proof theory, and the concept of harmony : what makes a logical rule "good"? It turns out there's some beautiful philosophical considerations behind that simple question. As promised during our chat; I'm going to link a few references for those who want to dig deeper: The papers that started it all: Prior, The runabout inference ticket Belnap, Tonk, Plonk and Plink The first paper (book, really) on Harmony: Dummett, The Logical Basis of Metaphysics The paper that originally inspired Siva's discussion: Zeilberger, On the unity of duality (I highly recommend the introduction to this one!). Stay logical, folks!…
We get a little philosophical with Phil Zucker (as we are wont), and ask "What even is a type?" We touch on some deep stuff about what it means to deduce, or even to know, in a mathematical sense. It takes us a bit. Here are some of Phil's notes on the subject, in his fascinating blog-of-consciousness sytle: https://www.philipzucker.com/notes/Logic/Type-theory/#what-are-types-what-is-type-theory…
I (Cody) and Phil Zucker (https://www.philipzucker.com/) have a fun chat about set theory, infinities and the Continuum Hypothesis. We start building up to the core ideas in the independence proofs, but these things take time.
We, again, talk about modal logic, taking a more syntactic approach.
I briefly chat about T. Tao's equations project , which involves building a full graph of implications for magma laws with less than 4 invocations of the operation. We talk about the cool logic facts that are used to build such a graph. A very cool play-by-play account is in the log , and all implications are explicitly or explicitly recorded via a machine-checkable proof in Lean.…
We try to give hints to answer this often asked question.
Quantifier alternation is a somewhat simple concept, but with some hidden depths! Find out what the big deal is. Now with pictures!
Andrej Bauer is our delightful guest in this long episode! We talk about intuitionistic logic, and how adopting an open minded attitude towards foundations of logic can help you discover new mathematical worlds ! Andrej has an incredible aptitude for taking complex ideas in logic and making them simple and compelling. Here are some links to know more: https://www.andrej.com/ https://math.andrej.com/ This is Part II of our episode (and the final part). A few of the works referenced in our chat: 1. The Countable Reals https://arxiv.org/abs/2404.01256 Andrej Bauer, James E. Hanson 2. On Fixed-Point Theorems in Synthetic Computability https://math.andrej.com/asset/data/recursion-theorem.pdf Andrej Bauer 3. An Invitation to Smooth Infinitesimal Analysis https://publish.uwo.ca/\~jbell/invitation%20to%20SIA.pdf John L. Bell 4. Constructive Analysis https://link.springer.com/book/10.1007/978-3-642-61667-9 Errett Bishop, Douglas Bridges 5. An introduction to fibrations, topos theory, the effective topos and modest sets https://www.lfcs.inf.ed.ac.uk/reports/92/ECS-LFCS-92-208/ Wesley Phoa 6. The Effective Topos https://www.dpmms.cam.ac.uk/~jmeh1/Research/Pub81-90/hyland-effectivetopos.pdf lJ.M.E. Hyland 7. Realizability: An Introduction to its Categorical Side https://www.amazon.com/Realizability-152-Introduction-Categorical-Foundations/dp/0444515844 Jaap van Oosten 8. Using the internal language of toposes in algebraic geometry https://arxiv.org/abs/2111.03685 Ingo Blechschmidt 9. On synthetic undecidability in Coq, with an application to the Entscheidungsproblem https://www.ps.uni-saarland.de/Publications/documents/ForsterEtAl\_2018\_On-Synthetic-Undecidability.pdf Yannick Forster,Dominik Kirst, Gert Smolka 10. Synthetic topology of data types and classical spaces https://www.cs.bham.ac.uk/~mhe/papers/barbados.pdf Martın Escardo 11. Foundations of Constructive Mathematics: Metamathematical Studies https://a.co/d/bz4zWUE Michael J. Beeson…
Andrej Bauer is our delightful guest in this long episode! We talk about intuitionistic logic, and how adopting an open minded attitude towards foundations of logic can help you discover new mathematical worlds ! Andrej has an incredible aptitude for taking complex ideas in logic and making them simple and compelling. Here are some links to know more: https://www.andrej.com/ https://math.andrej.com/ This is Part I of our episode. A few of the works referenced in our chat: 1. The Countable Reals https://arxiv.org/abs/2404.01256 Andrej Bauer, James E. Hanson 2. On Fixed-Point Theorems in Synthetic Computability https://math.andrej.com/asset/data/recursion-theorem.pdf Andrej Bauer 3. An Invitation to Smooth Infinitesimal Analysis https://publish.uwo.ca/\~jbell/invitation%20to%20SIA.pdf John L. Bell 4. Constructive Analysis https://link.springer.com/book/10.1007/978-3-642-61667-9 Errett Bishop, Douglas Bridges 5. An introduction to fibrations, topos theory, the effective topos and modest sets https://www.lfcs.inf.ed.ac.uk/reports/92/ECS-LFCS-92-208/ Wesley Phoa 6. The Effective Topos https://www.dpmms.cam.ac.uk/~jmeh1/Research/Pub81-90/hyland-effectivetopos.pdf lJ.M.E. Hyland 7. Realizability: An Introduction to its Categorical Side https://www.amazon.com/Realizability-152-Introduction-Categorical-Foundations/dp/0444515844 Jaap van Oosten 8. Using the internal language of toposes in algebraic geometry https://arxiv.org/abs/2111.03685 Ingo Blechschmidt 9. On synthetic undecidability in Coq, with an application to the Entscheidungsproblem https://www.ps.uni-saarland.de/Publications/documents/ForsterEtAl\_2018\_On-Synthetic-Undecidability.pdf Yannick Forster,Dominik Kirst, Gert Smolka 10. Synthetic topology of data types and classical spaces https://www.cs.bham.ac.uk/~mhe/papers/barbados.pdf Martın Escardo 11. Foundations of Constructive Mathematics: Metamathematical Studies https://a.co/d/bz4zWUE Michael J. Beeson…
We talk about the logic behind a powerful modern software analysis technique, Satisfiability Modulo Theories, which bridges the gap between theory and practice.
Chris Martens and Rob Simmons give their concluding remarks on this session on linear logic.
Rob and Chris are here still, to plumb the mysterious depths of linear logic!
Chris and Rob are back and explaining what linear logic is, and what it has to do with single-use soda machines.
I'm delighted to have special guests Chris Martens and Rob Simmons to talk about the fascinating world of linear logic! This is a four-parter, so strap in!
If you have only + in your logic, you do not get the Gödel curse: the full first order fragment, called Presburger Arithmetic is decidable and complete. But you're juuuust squeezing by! It turns out this innocent looking theory is quite expressive, and this expressiveness comes with a baby version of the incompleteness theorems: a lower bound on how fast you can decide statements! We explain what this means and how it comes to be.…
In this double episode, we talk about the power of arithmetic, or how simple theories simply allowing us to talk about plus and times over the integers give us the power to talk about almost anything in logic and CS. This ties in to the Incompleteness Theorems, and a trick originally devised by Gödel.…
We talk about the logical theory of Real Closed Fields, a set of axioms with a startling property.
T
The Church of Logic
We bring Phil Z back to talk about ordinal analysis, which is a technique to reduce the consistency of various logical systems to the well-foundedness property of certain ordinals, that is, the "size" of certain numbers. We explain the motivation and implications of this strategy. Part 3 of the series.…
T
The Church of Logic
We bring Phil Z back to talk about ordinal analysis, which is a technique to reduce the consistency of various logical systems to the well-foundedness property of certain ordinals, that is, the "size" of certain numbers. We explain the motivation and implications of this strategy. Part 2 of the series.…
T
The Church of Logic
We bring Phil Z back to talk about ordinal analysis, which is a technique to reduce the consistency of various logical systems to the well-foundedness property of certain ordinals, that is, the "size" of certain numbers. We explain the motivation and implications of this strategy.
We continue discussing the greatest of all math problems. We discuss why diagonalization, the greatest of all math solutions, seems helpless here.
We talk about the biggest open problem in mathematics, whether 'tis easier to discover, or to verify. It's not, we think. But we haven't discovered a proof!
We continue to talk about the BHK interpretation of proofs-as-programs, but now with the surprising observation that there is a programmatic interpretation for the Excluded Middle! It involves time travel.
Ask not what your logic can do for your computer, ask what your computer can do for your logic! We briefly touch on the BHK interpretation for first order logic, which describes how to give evidence for a proposition using programming.
T
The Church of Logic
Still chatting with Phil Zucker about interactive theorem proving, the good, the ugly, and the so darn fun!
T
The Church of Logic
I have an interactive conversation about interactive theorem provers with the funny (but wise) Phil Zucker (of https://www.philipzucker.com/). We try to break down the Why, rather than the how.
T
The Church of Logic
We discuss the proof of the second incompleteness theorem. Enough said!
T
The Church of Logic
Dominik is back! We talk about one of the most poignant theorem of mathematics, the famed 2nd incompleteness theorem.
T
The Church of Logic
We talk about modal logic, intuitionism and Kripke semantics, and what this has to do with bar hopping.
We talk about the first order logic axiomatization of Set Theory, focusing on the Zermelo Fraenkel axioms and why one might be inclined to think about sets if you care about logic (and philosophy!)
プレーヤーFMへようこそ！
Player FMは今からすぐに楽しめるために高品質のポッドキャストをウェブでスキャンしています。 これは最高のポッドキャストアプリで、Android、iPhone、そしてWebで動作します。 全ての端末で購読を同期するためにサインアップしてください。
Daily Deals
Daily Deals
Player FM -ポッドキャストアプリ
Player FMアプリでオフラインにしPlayer FMう！
Player FMアプリでオフラインにしPlayer FMう！
))
