Talk Abstracts

Jineon Baek (KIAS): “수학 연구에 쓰이는 공리들은 얼마나 당연한가?”

수학적 명제를 증명함으로서 우리는 이 명제가 절대적 진리라는 생각을 갖게 된다. 특히 대학교에서 증명을 배우면서 우리는 수학적 귀납법, 귀류법, 선택 공리 등 증명에 쓰는 몇가지 공리들을 당연하게 받아들이게 된다. 하지만 이 공리들이 정말 당연할까? 부정까지는 아니더라도, 이것들을 한번쯤은 의심해보고 때로는 공리계가 다른 수학을 생각해보는 것도 충분히 흥미로울 수 있다.

Il Young Jeong (UNIST): “Fraïssé Classes and the First-Order Limit Property”

We investigate first-order properties of finite structures arising from a Fraïssé class K in a finite relational language. For each n, we consider the uniform probability distribution on the set of n-element structures in K, and study the existence of limiting probabilities for first-order sentences as n→∞. We prove that K satisfies the first-order limit property if and only if the probabilities of all finite conjunctions of extension axioms converge. This framework isolates extension axioms as the fundamental objects governing asymptotic logical behavior and motivates further study of the zero–one property and the generic zero–one law.

Hyoyoon Lee (Sogang University): “Model theoretic approaches to Szemerédi’s regularity lemma”

Szemerédi’s regularity lemma is a fundamental theorem in combinatorics and has found applications in many areas. Since the seminal 2014 result of Malliaris and Shelah on the stable regularity lemmas, this line of work has been further refined and generalized by many model theorists and combinatorialists. In this talk, I will give a brief introduction to Szemerédi’s regularity lemma for an audience without a background in combinatorics, and explain how model theory has been connected to it.

Min Cheol Seo (Sungkyunkwan University): “Mathematical Structuralism and the Univalent Foundations”

Mathematicians and formalisation practitioners routinely treat isomorphic structures as “the same”, yet our standard foundations do not. In set theory, different reductions of arithmetic (von Neumann, Zermelo, etc.) disagree on sentences like “1 ∈ 3”, even though they are equally good models of the Peano axioms. In proof assistants, different encodings of N, or different implementations of groups and categories, are handled as distinct unless we explicitly transport along isomorphisms. These are all instances of the so-called Benacerraf Problem: if there are many mutually isomorphic realisations, what—if anything—are the mathematical objects over and above the structure?

In philosophy, mathematical structuralism is the thesis that mathematical objects are positions in abstract structures that exist independently of their set-theoretic or computational realisations. Representations related by isomorphism are equally good instantiations of the same ante rem structure; facts that vary across such instantiations are not genuinely about that structure.

This viewpoint imposes a constraint on foundations: identity at the foundational level should track structural equivalence, not encoding. The Univalent Foundations (Homotopy Type Theory and the Univalence Axiom) is a live attempt to meet this demand: Types form ∞-groupoids, equality is given by paths, and univalence identifies equality of types with their equivalence. In this talk, I will explain this picture and contrast it with familiar set-theoretic (ZF(C)) and categorical foundations (ETCS).

Eunsuk Yang (Jeonbuk National University): “Towards universal logic: Some examples”

In this presentation, I introduce some examples of general logic, which can be regarded as examples for universal logic. First, as logics based on implications I recall a class of logics called implicational tonoid logics and relational semantics introduced by Yang and Dunn (2021), and related representations introduced by Yang (2025). Second, as basic substructural (fuzzy) logics I introduce substructural logic systems without identity called here residuated monotone (semilinear) logics and their matrix semantics.

Taeyoung Yoon (Seoul National University): “분리논리: 프로그램의 안전성에 대한 형식 논증 체계”

이 발표에서는 명령형(imperative) 프로그래밍 언어에 대해 논증하기 위한 형식 논리 체계인 호어 논리(Hoare logic)와, 그 진화형인 분리논리(Separation logic)에 대해 다룬다. 전산학에서는 상태가 있는(stateful) 프로그램이 안전하고 믿을만 하다는 사실을 논증하기 위한 연구가 지속되어 왔고, 그 결과 탄생하고 발전한 분리논리는 운영체제와 분산 시스템 등을 포괄하는 복잡한 동시성 프로그램까지 검증할 수 있을 정도로 성숙했다. 몇 가지 예제를 통해 분리논리의 핵심을 개괄하고, 이를 통해 논리학이 전산학에서 어떻게 응용되는지를 보이고자 한다. 마지막으로는 분리논리에서 예언자 변수(prophecy variable)의 쓰임새를 개선하는 연구와 인공지능의 활용 가능성에 대해서 간단히 소개하려고 한다.