講義科目名		応用数学A
科目ナンバリングコード
講義題目		Model Theory: mathematical foundations for specification languages The starting day is May 6!
授業科目区分		共通授業科目　(Common Subjects for All Departments)
開講年度		2021
開講学期		前期
曜日時限		前期 木曜日 ４時限
必修選択		選択 (Elective Subjects)
単位数		2.0
担当教員		GAINA DanielMircea
開講学部・学府		工学府
対象学部等
対象学年		1
開講地区		伊都地区
その他 （自由記述欄）		We will start our course on May 6.

履修条件		No special knowledge is required.
授業概要		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 M is the class of all models of a set F of formulas, we say that F is a ‘theory’ of M; 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 unit disk and interpret a line as a diameter or a circular arc orthogonal to the boundary. In this model (known as the Poincaré disk) the first four postulates hold but not 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. Another important feature is that we will consider first-order structures with empty carrier sets following Wilfrid Hodges’ approach in a A Shorter Model Theory, thus allowing for higher mathematical flexibility on the objects our logical languages describe. Many-sorted first-order structures can be regarded as models of concrete software systems. 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 ■　Discussion
授業形態 （内容）		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=36214 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> Note: The starting day is 6th of May! The first four lectures will be delivered from W1-D-710. Please feel free to attend and ask questions face-to-face. At the same time, everything will be made available online via Zoom.
使用する教材等		Textbook，PDF 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
授業計画		The course will be divided in 3 parts: (1) Introduction of many-sorted first-order logic (models, sentences and satisfaction relation), and basic logical concepts (substitutions, reachable models and proof rules). The main result delivered here is Gödel's completeness --- every semantic consequence has a proof. Lecturer: Daniel Gaina (2) A characterization of elementary equivalence by Ehrenfeucht-Fraïssé games, commonly known as Fraïssé-Hintikka Theorem. Since finite games are quite intuitive and easy to describe, Fraïssé-Hintikka Theorem gives a better handle on elementary equivalence than Keisler-Shelah Theorem characterizing elementary equivalence via ultrapowers. Lecturer: Tomasz Kowalski (3) The relationship between gaining expressive power in extending first-order logic and losing some of its important properties. A paramount result in this direction is Lindström’s theorem, which characterizes first-order logic among its extensions by two major properties: the Downward Löwenheim-Skolem Property and Compactness. In any proper extension of first-order logic at least one of the two fails. Lecturer: Guillermo Badia
キーワード		first-order logic, model theory, proof system, semantics
授業の進め方		There will be 12 lectures. Each lecture will last 2 hours. Daniel GAINA (Kyushu University) will be in charge of lectures 1 - 4. Tomasz KOWALSKI (La Trobe University, Australia) will be in charge of lectures 5 - 8. Guillermo Badia (The University of Queensland, Australia) will be in charge of lectures 9 - 12. 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.
その他
添付ファイル
更新日付		2021-05-12 09:17:30.269