발표 초록

튜토리얼 발표

Shichang Song : Projective Fraisse limits and profinite groups

We show that the projective Fraisse limit of the class of finite groups is the free profinite group on a countably infinite set converging to 1. Also, we prove that its automorphism group has ample generics. Joint work with Sulin Hu.

초청 발표

Carl-Fredrik Nyberg Brodda : Some decision problems in finitely presented groups and semigroups

I’ll give an overview of some algorithmic problems in algebra, focussing on the word problem and membership problem. I’ll first present some recent results in the past few years by myself and coauthors (Foniqi & Gray) on the word problem for one-relation monoids, a problem that has remained open for over a century, since 1914. Using embeddings of right-angled Artin groups and trace monoids, I will show how the first known undecidability results for one-relation monoids can be proved: the rational subset membership problem can be undecidable. Finally, I’ll present some recent results by myself and Gray (East Anglia), where we fully classify which Artin groups have decidable submonoid/rational subset membership problem. This extends a result from 2007 by Lohrey & Steinberg, who classified which right-angled Artin groups have decidable membership problems.

박세원 : Real functions are continuous, continuously, computationally

In this talk, I present an axiomatization and formalization of computable analysis in constructive dependent type theory. It provides an axiomatic type of real numbers where constructive proofs from mathematical analysis are extracted to certified real-number computation programs. The axioms are sound for the realizability interpretation of dependent type theory in the category of assemblies over Kleene’s second algebra. To formalize interesting hyperspace computations, we further assume a general continuity principle from which we prove that all real functions are, in a sense, continuously continuous. This talk is based on my joint work with Michal Konečný and Holger Thies.

Javier de la Nuez González

김동우 : Reference and Analysis in Frege

I discuss Frege’s definition of number. I argue that the definition is intended to preserve the references of the ordinary number terms.

전한울 : On proof-theoretic dilator and Pohlers’ characteristic ordinals

The proof-theoretic ordinal (PTO) of a theory is a way to gauge the strength by looking at the supremum of provably well-founded recursive ordinals. There are two generalizations of the PTO: Pohlers isolated characteristic ordinals in “On the Performance of Axiom Systems,” which is the supremum of provably well-founded definable well-orders over a given Spector class. Meanwhile, Girard developed another invariant of a theory called proof-theoretic dilator that also yields PTO. In this talk, I will demonstrate proof-theoretic dilators are related to Pohlers’ characteristic ordinals.

최승락 : Formalizing intuitionistic negations in natural deduction system

This talk examines how historical intuitionists have employed the concepts of negation and contradiction in two distinct senses, focusing particularly on the works of L. E. J. Brouwer, Michael Dummett, and Neil Tennant. In doing so, it reveals that within intuitionism, the notion of contradiction has also been utilized in two different ways, especially regarding the definition of negation in terms of contradiction. Building on this historical and philosophical background, the talk argues that standard intuitionistic natural deduction systems fail to capture the full spirit of intuitionism. They do not adequately formalize the intuitionistic notion of negation and thus cannot fully represent the intuitionistic stance against the principle of excluded middle—that every meaningful statement is either true or false.

More specifically, this talk contends that the classical notion of contradiction, commonly symbolized as ⊥ (falsum), is insufficient for representing the meaning of intuitionistic negations, particularly when it comes to the concept of “prooflessness.” In the standard intuitionistic natural deduction systems, the crucial difference between “a statement not being true” and “a statement being false” collapses. To remedy these shortcomings, the talk proposes an enhanced intuitionistic natural deduction system that incorporates both the classical notion of contradiction (⊥) and a new symbol (⋏), representing an intuitionistic notion of contradiction centered on the absence of proof. By integrating ⋏, this approach preserves the important distinction between statements lacking proof and those proven false, thereby ensuring a more faithful reflection of intuitionistic principles. The resulting system, which employs two kinds of contradictions and negations within a single logical framework, resonates with recent developments in paraconsistent and relevant logics, while suggesting that natural language may inherently rely on this nuanced blend of notions.

학생 발표

김연홍 : 약-u-결합 유니놈 논리의 표준 완전성

이 발표에서는 Yang(2024)를 따라 약-u-결합 유니놈 논리의 표준 완전성을 탐구한다. 퍼지 논리의 표준 완전성 증명의 기본 발상은 특정 대수적 의미론을 단위구간 [0, 1]에 올바르게 매장하는 방법을 찾아내는 것이다. 이 작업에서 핵심은 대수적 의미론이 갖는 성질, 특히 병합 연산의 성질을 보존하는 데 있다.

퍼지 논리에서 가장 널리 알려진 병합 연산은 t-노름이다. 좌연속성, 준선형성 등 연산의 성질에 따라 t-노름을 분류할 수 있다. 나아가, t-노름의 기본 조건을 완화한 더 일반적인 연산에 대한 연구 또한 이루어져 왔다. 약-u-결합 유니놈에는 이 다양한 퍼지 병합 연산의 성질이 부분적으로 반영되어 있다. 따라서 이 발표에서는 주요 준구조 퍼지 논리의 표준 완전성 증명의 기본 발상을 정리하고, 이로부터 Yang(2024)의 표준 완전성 증명을 이해하는 한 방법을 제공하고자 한다.

백지선 : Graphs on Infinite Cardinals: The Erdős-Dushnik-Miller theorem

Exercise I.19 in Set Theory by Kunen states that any well-ordering on an infinite cardinal $\kappa$ agrees on $\kappa$-many elements with the usual ordering. A stronger result is described using the Erd\H{o}s-Rado arrow, $\kappa \rightarrow (\kappa, \omega)^2$, which demonstrates that any graph with a $\kappa$-sized vertex set contains either a $\kappa$-sized clique or $\omega$-sized independent set. In this talk, we explore the Erd\H{o}s-Dushnik-Miller theorem, $\kappa \rightarrow (\kappa, \omega+1) ^2$ for regular uncountable cardinals $\kappa$, as well as analogous results by Shelah for certain singular cardinals.

서민철 : Multi-Agent Simulative Belief Ascription

This paper presents the outline of the model of Multi-Agent Simulative Belief Ascription, (MASBA), a novel approach to model how an agent represents other agent’s belief state, incorporating belief revision to effectively address the dynamic nature of belief changes in multiagent contexts. In MASBA, each agent’s belief is represented as a distinct compartment, allowing for the sharing of beliefs through communication while maintaining their individual integrity. A key feature of MASBA is its handling of simulative beliefs, being casually characterised as ‘what would have believed if I were the case’, which may not always compatible with the ascribee’s actual belief state. When constructing the simulative belief state, the revision occurs with respect to the ascriber’s belief state but with a priority on the ascribee’s plausibility ordering. This structure enables MASBA to provide an intuitive perspective on cognitive faculty of ‘mindreading’, representing it as a mental simulation that merges our beliefs with the shared beliefs of others, thereby enriching our understanding of multi-agent belief dynamics and cognitive processes.

임기정 : 고전일차논리의 새로운 Coq 형식화와 건전성 및 완전성 정리의 증명

In classical first-order logic, the soundness theorem states that syntactic entailment implies semantic entailment, while the completeness theorem asserts the converse. In this study, assuming the law of excluded middle, proofs of the soundness theorem of a Hilbert calculus with respect to Tarski’s semantics and the completeness theorem for all countable first-order languages are presented. This formalisation, written in Coq, gives named quantifiers and Leibniz equality and enables one to assume an infinite number of axioms.