皆様
６月１３日（木）に北陸先端科学技術大学院大学で行われます Baaz 教授、Gamsakhurdia 氏（ウィーン工科大学）の講演のお知らせです。 皆様、どうぞ奮ってご参加ください。
廣川 直 (JAIST)
----------------------------------------------------------------------- * JAIST Logic Seminar Series *
Date: June 13 (Thu), 2024, 15:30 - 17:10
Place: I-57g (seminar room on 5F of IS Building III) at JAIST (Access: https://www.jaist.ac.jp/english/top/access/index.html)
--------------------------------------------------------- Quantifier shifts M. Baaz, Vienna University of Technology (joint work with J. Aguilera, M. Gamsakhurdia, R. Jalali) ---------------------------------------------------------
Abstract: In this lecture we analyze the operation of quantifier shifts, one of the oldest deduction formalism in logic. Quantifier shifts are orthogonal to usual deduction rules and have a considerable impact on the complexity of proofs. To understand them better a variant of sequent calculus with relaxed Eigenvariable conditions is developed, which is able to represent quantifier shifts in a cut-free format. There is a non-elementary speed-up of cut-free proofs in the new format vs cut free proofs in the usual format, a manifestation of the proof-theoretic power of quantifier shifts. The intuitionistic version of this calculus is applied to prove, that an intermediary logic admits Standard Skolemization iff it admits all classical quantifier shifts.
-------------------------------------------------------- The Limits of Prenexation in First-order Gödel Logics Mariami Gamsakhurdia, Vienna University of Technology (joint work with Matthias Baaz) --------------------------------------------------------
Abstract: One of the first recognised characteristics of classical logic is the existence of a prenex form for each formula. The quantifier-shifting rules are used non-uniquely to construct these prenex forms. The expressive power of prenex fragments is easy to see in classical logic because it coincides with the whole logic, and in Intuitionistic logic since the prenex formulas are very weak (the validity of the prenex formula is decidable). However, because Gödel logics are intermediary logics, the expressibility of its prenex is relatively important.
It is clear that prenex normal forms cannot be constructed in the usual sense in Gödel logics because some of the quantifier-shift rules may fail, but this does not imply that no prenex normal form exists. However, demonstrating that such prenex forms do not exist is more difficult. Prenexation does not work for (G_{[0,1]}) when $0$ is not isolated, since the formula ((\neg \forall x A(x)\wedge \forall x \neg \neg A(x))) does not allow a prenex normal form. To prove this fact, we use a glueing argument. This result can be extended to all Gödel logics where there is one accumulation point from above, even if it is not $0$.
In this talk we provide the complete classification for the first-order Gödel logics with respect to the property that the formulas admit logically equivalent prenex normal forms. We show that the only first-order Gödel logics that admit such prenex forms are those with finite truth value sets since they allow all quantifier-shift rules and the logic (G_\uparrow) with only one accumulation point at $1$. In all the other cases, there are, in general, no logically equivalent prenex normal forms. We will also see that (G_\uparrow) is the intersection of all finite first-order Gödel logics.
The second stage of our research investigates the existence of the validity equivalent prenex normal form. Gödel logics with a finite truth value set admit such prenex forms. Gödel logics with an uncountable truth value set have the prenex normal form if and only if every surrounding of (0) is uncountable or (0) is an isolated point. Otherwise, uncountable Gödel logics are incomplete, and the prenex fragment is always complete with respect to the uncountable truth value set. Therefore, there is no effective translation to the valid formula and the valid prenex form. The countable case, however, is still up for debate.
References Matthias Baaz, Norbert Preining Gödel-Dummett logics, in: Petr Cintula, Petr Hájek, Carles Noguera (Eds.), Handbook of Mathematical Fuzzy Logic vol. 2, College Publications, (2011), pp. 585–626, chapter VII.
Matthias Baaz, Norbert Preining, Richard Zach First-order Gödel logics, Annals of Pure and Applied Logic vol. 147. (2007) pp. 23–47.