Talk Abstracts

Choi, Seungrak (University of Seoul), “Dialetheism on Arithmetic: Is there any inconsistent primitive recursive relation?”

In this talk, I will introduce dialetheism on arithmetic which is the view that there exists a true contradiction even in arithmetic. After we investigate inconsistent semantics on arithmetic and its application to Gödel’s incompleteness theorem, we will deal with the interesting philosophical claim from Graham Priest that even primitive recursive relations may be inconsistent. Although he carefully presented his claim using the expression ‘may be,’ Priest(2006) gave a definite claim that even numerical equations can be inconsistent.

With the summary of Priest’s argument for the inconsistent primitive recursive relation, I will argue that his identity relation cannot be both primitive recursive and inconsistent. Since he did not propose a new definition of ‘primitive recursive function’ that fits to his dialetheism, he should seriously consider my argument. Furthermore, for a general case, I will argue that there is no inconsistent primitive recursive relation with regard to the standard notion of ‘primitive recursive function.’

Jeon, Hanul (Cornell University), “Constructive Ackermann’s interpretation”

Ackermann proved that we could interpret \(\mathsf{ZFC}\) without the axiom of Infinity into Peano Arithmetic (\(\mathsf{PA}\)). 70 years later, Kaye and Wong improved Ackermann’s result that \(\mathsf{PA}\) is, in fact, bi-interpretable with a finite set theory, which is an extension of \(\mathsf{ZFC}\) without Infinity. In my talk, I will explore the results of Kaye and Wong in a constructive manner. While there is a unique constructive counterpart of \(\mathsf{PA}\), known as Heyting arithmetic (\(\mathsf{HA}\)), there are at least two constructive analogs of \(\mathsf{ZFC}\), namely, Intuinionistic \(\mathsf{ZF}\) (\(\mathsf{IZF}\)) and Constructive \(\mathsf{ZF}\) (\(\mathsf{CZF}\)). It turns out that \(\mathsf{HA}\) is bi-interpretable with \(\mathsf{CZF^{fin}}\), the theory obtained by removing Infinity from \(\mathsf{CZF}\) and adding the assertion “every set is finite.” Kaye and Wong also explored the bi-interpretability between subtheories of \(\mathsf{HA}\) and a finite set theory. In my talk, I will characterize subtheories of \(\mathsf{HA}\) and \(\mathsf{CZF^{fin}}\) that are bi-interpretable with each other.

Kim, Dongwoo (CUNY), “Exact Truthmaker Semantics: in relation to multi-valued semantics”

I present the basic ideas of exact truthmaker semantics, which has been developed by Kit Fine in a series of papers. I focus on its relation to some of the well-known multi-valued semantics, such as K3, LP, and Belnap’s four-valued semantics, and discuss how the standard exact truthmaker semantics provides a unifying formal framework.

Lee, Hyoyoon (Yonsei University), “Godel’s Incompleteness Theorem; sketch of the rigorous proof”

The statements and results of Godel’s Incompleteness Theorems are fairly well-known, but the rigorous mathematical proof of it is not so easy to understand for the people who don’t know well about mathematical logic. I aim to give a rough, but mathematically precise sketch of the proof that, hopefully, can be understood by anyone having some basic sophistication in mathematics. The proof in this talk will be based on Byunghan Kim’s lecture note, which can be found in his homepage. The sketch will contain crucial definitions and key technical lemmas in the proof, including: Definition of recursiveness, \(\beta\)-function Lemma that enables us to code the sequence of numbers into a single natural number, Representability Theorem, Godel numbering, Fixed Point Theorem, and so on.

Lee, Junguk (KAIST), “ACFs are simple as much as infinite sets : An introduction to quantifier elimination”

I will introduce the notion of quantifier elimination (QE) from model theory, which is a powerful tool to understand definable sets for various first order structures. We will see several mathematical structures having QE, for example, infinite sets, dense linear order without endpoints, algebraically closed fields, real closed fields, and so on. And as applications of QE, I will briefly explain model-theoretic proofs of Chevalley’s theorem on constructible sets and of Hilbert’s 17th problem.

Selivanova, Svetlana (KAIST), “Computational Properties of Differential Equations Solution Operators”

In this talk we discuss recent computability and complexity results for solution operators of differential equations, with the main focus on linear systems of partial differential equations. We show two different approaches: (i) real complexity and (ii) computation with coefficients in real closed fields; as well as summarize dependence of the results on smoothness of initial data.

Thies, Holger (Kyoto University), “An application of constructive dependent type theory to certified computation over the reals”

In exact real computation, real numbers are treated as basic entities that can be manipulated exactly without introducing rounding errors. This is often realized by adding a datatype for reals and arithmetic operations on them as primitives in programming languages. In this talk, we describe some recent progress on formally verifying exact real computation. We propose a constructive axiomatization of real numbers in a dependent type theory which formalizes real numbers in a conceptually similar way as some mature implementations of exact real computation. We implemented our theory in the Coq proof assistant and use Coq’s code extraction tools to extract Haskell programs from proofs. We extended the extraction to map primitive operations on constructive real numbers directly to the corresponding operation in the AERN framework, a Haskell implementation of exact real computation. In the talk, we particularly focus on aspects of the formalization dealing with multivaluedness and non-deterministic computation. We also present some examples of extracting non-deterministic programs from proofs.

(This talk is based on j.w.w. Sewon Park and Michal Konečný)

Yang, Eunsuk (Jeonbuk National University), “Implicational tonoids, embeddability, and representations”

We investigate implicational tonoids and their representations. More precisely, we first review implicational tonoid matrices. We then introduce their representations. We in particular consider embeddability property for implicational tonoid matrices. Finally, we generalize these to assertional implicational tonoid algebras and their embeddabilty and representations.