Type Theory, Constructive Mathematics and Geometric Logic / Théorie des types, mathématiques constructives et logique géométrique

Collection Type Theory, Constructive Mathematics and Geometric Logic / Théorie des types, mathématiques constructives et logique géométrique

Organizer(s) Coquand, Thierry ; Negri, Sara ; Rathjen, Michael ; Schuster, Peter

Date(s) 01/05/2023 - 05/05/2023

linked URL https://conferences.cirm-math.fr/2319.html

00:00:00 / 00:00:00

1 5

On a decomposition of WKL!!

By Takako Nemoto

constructive reverse mathematics

Constructive reverse mathematics aims to decompose mathematical theorems into choice principles and logical principles. In this talk, we decompose a version of weak Koenig's lemma with a uniqueness condition called WKL!!.

Information about the video

Date of recording 01/05/2023
Date of publication 15/05/2023
Institution CIRM
Licence CC BY NC ND
Language English
Audience Researchers, Graduate Students
Director(s) Jean Petit
Format MP4

Citation data

DOI 10.24350/CIRM.V.20040803
Cite this video Nemoto, Takako (01/05/2023). On a decomposition of WKL!!. CIRM. Audiovisual resource. DOI: 10.24350/CIRM.V.20040803
URL https://dx.doi.org/10.24350/CIRM.V.20040803

Domain(s)

Logic

Bibliography

FUJIWARA, Makoto et NEMOTO, Takako. On the decomposition of WKL!!. Philosophical Transactions of the Royal Society A, 2023, vol. 381, no 2248, p. 20220010. - http://doi.org/10.1098/rsta.2022.0010

MSC codes

Last related questions on MathOverflow

You have to connect your Carmin.tv account with mathoverflow to add question

Ask a question on MathOverflow

All the collection videos

52:12

published on May 15, 2023

On a decomposition of WKL!!

By Takako Nemoto

55:38

published on May 15, 2023

New modal operators for constructive mathematics

By Ingo Blechschmidt

58:06

published on May 15, 2023

Recursive inequalities in applied proof theory

By Thomas Powell

58:27

published on May 15, 2023

Compact ordinals in HoTT/UF

By Martin Escardó

46:40

published on May 15, 2023

From axioms to synthetic inference rules via focusing

By Dale Miller

Copyright Carmin.tv 2024

Give feedback