講義科目名		応用数学Ⅱ
科目ナンバリングコード		MAT-MAT6782W
講義題目		Model Theory: mathematical foundations for specification languages
授業科目区分		専攻教育科目（数理学コース・学際科目） / Specialized Courses
開講年度		2020
開講学期		前期
曜日時限		前期 木曜日 ４時限
必修選択		選択 / Elective
単位数		2
担当教員		GAINA DanielMircea 溝口　佳寛
開講学部・学府		数理学府
対象学部等		数理学府 / Graduate School of Mathematics
対象学年		修士課程 / Master's course
開講地区		伊都地区
その他 （自由記述欄）		The start of 2020 Spring Semester was moved to 7th of May. In order to comply with the university rules, we will start our course on 7th of May, too.

履修条件		No special knowledge is required
授業概要		The course is an introduction to model theory:  The course is an introduction to model theory: a branch of mathematics that deals with the classification of structures by means of logical formulas. Mathematical structures (groups, rings, fields, ordered sets, lattices, and others) can be classified according to the logical formulas that are true in them. Conversely, given some logical formulas, one wants to find classes of structures in which the formulas are true. We call those structures `models' of the formulas; moreover, when S is the class of all models of a set F of formulas, we say that F is a `theory' of S; hence, the name of model theory. Historically, mathematicians have used models all the time, they just did not build a theory around it. For example, to demonstrate that Euclid's fifth postulate does not follow from the rest, one can take a sphere: a (non-standard) model of all the postulates except the fifth. Model theory however is relatively young, it did not exist before the second half of the 20th Century. In addition, this course provides the foundations of software specification and formal verification of systems from the perspective of the work on algebraic specification. It also introduces some basic concepts necessary for the design of an algebraic-specification language. One important characteristic of the present course is the use of many-sorted first-order structures (instead of single-sorted structures), which consist of collections of sets (of data values) together with functions and relations over those sets. Each such structure can be regarded as a model of a concrete software system. Therefore, we can learn a lot about software systems by analyzing their model theory. This abstraction corresponds to the view that the correctness of the input/output behaviour of a software system takes precedence over other properties such as efficiency.
授業形態 （項目）		■　Lecture・Seminar □　Experiment □　Group Work・Pair Work □　Activities inside/outside campus □　Presentation ■　Discussion □　PBL/TBL
授業形態 （内容）		The lecture will be given online via Zoom using slides and other electronic files. The slides and the recorded lectures will be distributed on Moodle and Daniel GAINA's homepage: https://moodle.s.kyushu-u.ac.jp/course/view.php?id=21801 https://imi.kyushu-u.ac.jp/~daniel/model-theory/model-theory.html Please contact the organizers for details concerning the connection via Zoom. Daniel GAINA <daniel@imi.kyushu-u.ac.jp> Yoshihiro MIZOGUCHI <ym@imi.kyushu-u.ac.jp>
使用する教材等		Textbook，PPT Documents，Audiovisual materials
全体の教育目標		Setting the foundation for the development of logical reasoning and the ability to understand both concrete and abstract problems
個別の教育目標		basic notions and results of first-order logic and model theory and their applications in mathematics and computer science
授業計画		(1) First-order languages and logic. • Introducing many-sorted first order logic, and basic logic concepts: proof systems, models, completeness, compactness. (2) Beginning model theory. • Fundamental model theoretic constructions and notions: homomorphisms, substructures, elementary substructures, elementary equivalence, direct products. (3) Naming the elements by adding constants. • Various diagrams: atomic, positive, elementary. Their basic properties. (4) Preservation theorems. • Using diagrams to prove preservation theorems for: substructures (universal formulas), homomorphic images (positive existential), direct products (Horn formulas), unions of chains (Π 2 formulas), HSP (equations). (5) Ultraproducts. • Fundamental theorem of ultraproducts ( Loś Theorem), compactness (again), embedding into ultraproducts of finitely generated substructures, elementary classes, Keisler-Shelah Theorem (without proof), non-finite axiomatisability, non-standard models. (6) Quantifier elimination and model completeness. • Introducing quantifier elimination as a method of proving decidability. Industrial applications of the method mentioned. (7) Eherenfeucht-Fraıssé games. • Games for elementary equivalence and back-and-forth equivalence. Isomorphism, elementary equivalence and similar equivalences “in between”. Application to regular languages (a regular language is first-order definable if and only if it is star-free).
キーワード		many-sorted first-order logic, model theory, proof system, semantics, substructure
授業の進め方		Assistant Prof. Daniel GAINA (Kyushu University) will be in charge of lectures 1 - 4, 9 and 10. Assoc. Prof Tomasz Kowalski will be in charge of lectures 5 - 9, 11, and 12. First lecture will be given on 7th of May. The lecture will be held between 16:00 ~18:00 (JST). Questions are accepted in English but also in Japanese (to Prof. Yoshihiro MIZOGUCHI).
テキスト		Lecture notes will be available online.
参考書		[1] D. Marker, Model Theory: An Introduction, Springer 2002 [2] W. Hodges, A shorter model theory, Cambridge University Press, 1997 [3] H.-D. Ebbinghaus, J. Flum, W. Thomas, Mathematical Logic: Second Edition, 1994 [4] C.C. Chang, H. Jerome Keisler, Model Theory: Third Edition, Elsevier, 1990
学習相談		Flexible, upon appointment or walk-in. Appointments can be made by email at Daniel GAINA <daniel@imi.kyushu-u.ac.jp> (for consultation in English) or at Yoshihiro MIZOGUCHI <ym@imi.kyushu-u.ac.jp> (for consultation in Japanese).
試験／成績評価の方法等		By report. There is no final examination.
その他		https://moodle.s.kyushu-u.ac.jp/course/view.php?id=21801
添付ファイル
更新日付		2020-05-13 08:50:34.429