Change the language to 한국어
The contents of my talk are as follows.
0 . Introduction
I will raise some general questions like “What is logic?”, “What is a logical constant?” and “How the meanings of logical constants are to be explained?”, pointing out how they are related. After considering some criteria for logical constanthood, I’ll contrast two theories of meaning for logical constants and give reasons for favoring the verificationist account.
1 . A verificationist, proof-theoretic account of the meanings of logical constants
An explanation of the meanings of logical constants of the first-order logic (without identity) will be given broadly in line with Gentzen, Brouwer-Heyting-Kolmogorov, Dummett, Prawitz and Martin-Löf. In so doing, Prior’s objection to inferentialism and Dummett’s meaning theoretic principle of harmony will be considered. The significance of Prawitz’s inversion principle and normalization results for the meaning-theoretic account will be considered.
2 . The meaning of identity
There have been disagreements about the logical status of identity and about how the notion of identity is to be explained. I’ll brifely consider an attempt to define identity in terms of second-order quantifiers and examine the logical status of and the meanings of second-order quantifiers. The main aim of this part of my talk is to give a verificationist, proof-theoretic account of identity. This account is much in line with Martin-Löf’s works. I’ll argue that, contrary to some authors, there are proper introduction and elimination rules for identity which are in conformity with the verificationist account. In so doing, I’ll clarify what counts as the canonical verifications of identity propositions. I’ll also claim that a circularity implicit in a usual explanation of the meaning of identity can be avoided by distingushing definitional equality and identity proposition. The account will lead to the thesis of type-dependency of identity and object.
In this talk for general audiences, I will sketch basic notions of model theory and its applications to various subjects of mathematics such as number theory, geometry, combinatorics and more. If time permits I will talk about my recent works on model theory.
In this talk we discuss motivation, recent progress and perspectives of classifying partial differential equations according to their algorithmic complexity. The underlying framework of real complexity provides a bridge between classical fields: “discrete” computability and complexity theories, from one side; and “continuous” analysis (including functional spaces, linear algebra, manifolds, differential equations etc.) from the other, to mutual benefit of both.
In his paper, “On paradox without self-reference”, Neil Tennant proposed the conjecture for self-referential paradoxes that any derivation formalizing self-referential paradoxes only generates a looping reduction sequence. According to him, the derivation of the Liar paradox in natural deduction initiates a looping reduction sequence and the derivation of the Yablo’s paradox generates a spiral reduction. With the assumption that Yablo’s paradox lacks the self-reference, two derivations seem to support his conjecture.
The present paper proposes the counterexample to Tennant’s conjecture for self-referential paradoxes. We shall show that there is a derivation of the Liar paradox which generates a spiraling reduction procedure. Since the Liar paradox is a self-referential paradox, the result can be the counterexample to his conjecture.
Tennant has believed that classical reductio has no essential role to formalize paradoxes. As our counterexample applies the rule of classical reductio, he may reject the counterexample. So, it will be briefly argued that if classical reductio has no essential role for formulating paradoxes in natural deduction, neither does his rules for the liar sentence.
We show that antichain tree property (ATP) is witnessed by a formula in a single free variable. ATP was first introduced in the study of the differences between SOP1 and SOP2. When starting research on ATP, it is natural to ask whether ATP is witnessed in a single free variable, like other tree properties such as SOP1, SOP2, and TP2. To show this we introduce some combinatoric methods related to antichains and find the appropriate modifications of the Path-collapse lemma which is proved by Chernikov and Ramsey when they show the one-variable theorem for SOP2. This is joint work with JinHoo Ahn and Junguk Lee.
Throughout, we will fix a first order language \(\mathcal{L}\). A maximal consistent set of \(\mathcal{L}\)-formulas is called a complete type, and any tuples a and b have the same type iff for any \(\mathcal{L}\)-formula \(\varphi(x)\), \(a \models \varphi(x)\) iff \(b \models \varphi(x)\). There are more ‘strong’ concepts of types, called (Shelah-)strong type, Kim-Pillay type and Lascar (strong) type. In this talk, they will be introduced and their various characterizations will be explained. Especially, the Lascar group will also be introduced and the interpretations of strong types in terms of orbit equivalence relations (induced by subgroups of the Lascar group) are explained too.
Homotopy Type Theory (HoTT) has gathered the interest of logicians, mathematicians, computer scientists and philosophers ever since the introduction of the book of the same title by the Univalent Foundations Program (UFP). In Philosophy, HoTT is considered to be a new foundation for mathematics, distinct from or even rivalling ZFC set theory and category theory.
Path induction is the definition of identity in HoTT. Recently, Ladyman and Presell (2015) and Walsh (2017) have argued that path induction needs to be justified either (1) from pre-theoretic notions of identity or (2) from an inferentialist perspective by categorical harmony. In this talk, I examine whether path induction needs to be justified based on the foundational goals of HoTT proposed by the UFP. I argue that instead of path induction, the univalence axiom needs to be justified to show that the goals of UFP can be met.
This is a short introductory talk on the role of intuitionistic logic in computer science. In intuitionistic logic, when we need to prove an object’s existence, we must construct it. For disjunctions, we must specify whether the left or the right holds. In consequence, proofs using intuitionistic logic become much informative.
BHK interpretation and Kleene’s realizabiltiy interpretation yield a correspondence between proofs in intuitionistic logic and computation. Computable mathematics, the mathematics of computer science, is mathematics developed in the viewpoint of computability. And, intuitionistic mathematics is mathematics developed using intuitionistic logic. By building a (realizability) interpretation of an intuitionistic type theory, a foundation of intuitionistic mathematics, we formalize the correspondence between intuitionistic and computable mathematics.
Hopefully, this talk will attract people in computer science to pay more attention to logic (especially intuitionistic one since it is our language) and make people in logic to be interested in computer science. :)
The field of computational linguistics and the logics have been highly correlated from its beginning, since the formal logics have provided a concrete model for the semantic representation of the natural language. However, the recent advancement of the deep learning techniques have replaced formal logic’s role as a semantic representation tool to vector-based representations. Aforementioned two paradigms - logic based and deep learning based - have its own strengths and weaknesses. In the talk, brief history of the semantic representation of the natural language will be covered by comparing two major paradigms. Thereafter, a novel approach of merging two major paradigms will be discussed.