발표 초록

김동우 (한국과학기술원), “On exact truthmaking for modalized statements”

The present paper attempts to provide an exact truthmaker semantical analysis of modalized propositions. According to the present proposal, an exact truthmaker for “Necessarily P” is a state that bans every exact truthmaker for “Not P”, and an exact truthmaker for “Possibly P” is a state that allows an exact truthmaker for P. Along the way, we shall also discuss some of the philosophical and technical issues in providing a formal analysis of exact truthmaking for modalized statements.

김동현 (한국교통대학교), “고등학교 및 대학 교양 논리학 교육 개편 방향”

교육부의 교육과정 개편에 따라 고등학교 교양 과목인 “논리학”의 교육과정 또한 새롭게 개편되었고 그에 따른 교과서가 제작 중에 있다. 본 발표에서는 기존 교육과정과 비교하여 새로운 교육과정이 어떤 특징이 있는지를 설명하고, 현재 진행중인 교과서 집필 현황에 대해 소개한다. 아울러 고등학교 논리학 교육이 대학의 교양 논리학 교육과 어떻게 연계되고 차별화되어야 하는가에 대한 발표자의 의견을 제시한다.

김준희 (고등과학원), “Pre-independence relations induced by Morley sequences in NSOP1 theories”

Given an arbitrary pre-independence relation, one can use its Morley sequences to derive a new pre-independence relation. We prove that in NSOP1 theories, if a pre-independence relation is stronger than Kim-independence and satisfies monotonicity, base monotonicity, right extension, and strong finite character, then its induced pre-independence relation satisfies existence. In particular, if a pre-independence relation is induced by non-forking independence relation, then it satisfies existence in NSOP1 theories. We will show via constructing a counterexample that this result is not true in general; thus, our example is not NSOP1.

배경민 (포스텍), “Formal specification and analysis of concurrent systems in rewriting logic”

Rewriting logic is a simple and flexible computational logic for specifying concurrent systems. Data types are algebraically specified in equational logic, while concurrent dynamic behavior is specified by rewrite rules. The execution of systems defined in rewriting logic is characterized by logical deduction, and can be analyzed using various formal analysis techniques, such as simulation, search, and theorem proving. Rewriting logic has been successfully applied to a wide range of applications, including cryptographic protocols, network protocols, cloud computing systems, real-time and cyber-physical systems, biological systems, and so on. In this talk, I will give an introduction to specification and analysis in rewriting logic, as well as a discussion on its recent advances and applications.

양은석 (전북대학교), “Fuzzy extensions of Implicational tonoid logics”

We address fuzzy extensions of implicational tonoid logics. To be more precise, we first define the class of implicational tonoid prelinear logics and show that tjose logics are complete with respect to linearly ordered matrices. We next introduce a relational semantics for finitary implicational tonoid prelinear logics and verify that those logics are complete on the semantics. Finally we generalize the term “semilinear” to a notion, which can be applied both in a algebraic context and in a set-theoretic context and show that those logics are semilinear in the set-theoretic context.

이정욱 (창원대학교), “An introduction to model companion : Infinite sets are NOT trivial!”

In this talk, I will introduce a notion of model companion from Model Theory, and I try to convince that infinite sets are NOT trivial in a model theoretic view through the lens of model companion.

장준영 (McGill University), “Adjoint Logic: Multiple Modalities into a Computational Framework”

Modal logics and modal types have taken important positions both in philosophical logic and computational type systems and changed our understanding of the structure of truth and computation: necessity logic/type (\(\square\)), temporal logic/type (\(\mathtt{next}\)), lax logic/type (\(\bigcirc\)), and so on. One natural question arises from the variety of important modalities: is there a unifying framework explaining many different modalities? Here I present the elegant and powerful framework, adjoint logic, which can describe all the previously mentioned modalities. The expressive power of this framework is well-demonstrated with its applications to analysis in the context of computer science: message-passing protocol, garbage collection, strictness, and dead-code elimination, amongst others.

전한울 (Cornell University), “Separating the Wholeness axioms”

Corazza introduced the Wholeness axiom, which asserts the existence of an elementary embedding \(j: V \to V\). Unlike the Reinhardt embedding, the Wholeness axiom is consistent with the axiom of choice. Hamkins formulated finer versions \(\mathsf{WA}_n\) of the Wholeness axioms and proved that \(\mathsf{WA}_0\) does not prove \(\mathsf{WA}_1\), but it is open whether \(\mathsf{WA}_{n+1}\) proves the consistency of \(\mathsf{WA}_n\). In this talk, I will briefly sketch the proof for \(\mathsf{Con}(\mathsf{ZFC}+\mathsf{WA}_0)\) from \(\mathsf{ZFC}+\mathsf{WA}_1\), which gives a partial answer to Hamkins’ question.

최승락 (서울시립대학교), “Which Reduction Procedures for Classical Reductio are Acceptable?”

The present talk represents the exploration of the dissimilar outcomes from Prawitz’s reduction procedure for classical reductio vis-á-vis Stålmarck-Andou’s for it. Furthermore, recent discussions on the criteria for acceptable reductions in proof theory have yet to resolve the question of which reduction procedures for classical reductio are deemed acceptable.

While Prawitz (1965, 1971)’s contributions, encompassing the normalization theorem, subformula property, and consistency for standard weak classical logic, are well-regarded, the normalization proof by Stålmarck(1991) and Andou(1995) for the standard full classical logic has not been widely investigated.

Subsequently to demonstrating the subformula property and consistency of the full classical logic, a comparative investigation of Prawitz’s and Stålmarck-Andou’s reduction procedures for classical reductio ensues. The assertion is made that Stålmarck-Andou’s reduction holds a more solid foundation than Prawitz’s, grounded in the history of natural deduction developed by Prawitz(1965, 1971, 2015), where the reduction process aims to eliminate the maximum formula occurrence, and a novel reduction process was devised to achieve normalization and the subformula property.

Yuyama, Takao (湯山 孝雄) (교토대학교), “Word problem for groups and G-automata”

The word problem for a group H is the set of words, over a fixed generating set of H, that represents the identity element in H. Muller and Schupp (1983) showed a remarkable theorem, which states that a group has context-free word problem if and only if it is a virtually free group. Context-free languages can also be defined as languages accepted by some F-automata where F is a free group of rank > 1. Elder, Kambites, and Ostheimer (2008) proved a “commutative analog” of Muller-Schupp theorem: the word problem of a group H is accepted by a G-automaton for an abelian group G if and only if H is a virtually free abelian group. However, their proof is somewhat complicated, in the sense that it depends on a deep theorem in geometric group theory due to Gromov. In this talk, I give a much simpler and direct proof of their theorem, which is based on Higman’s lemma and B. H. Neumann’s lemma.