## シラバス参照

 Model Theory: mathematical foundations for specification languages

GAINA DanielMircea

その他
（自由記述欄）
 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=21801https://imi.kyushu-u.ac.jp/~daniel/model-theory/model-theory.htmlPlease contact the organizers for details concerning the connection via Zoom. Daniel GAINA Yoshihiro MIZOGUCHI

 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-ShelahTheorem (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.

  D. Marker, Model Theory: An Introduction, Springer 2002  W. Hodges, A shorter model theory, Cambridge University Press, 1997 H.-D. Ebbinghaus, J. Flum, W. Thomas, Mathematical Logic: Second Edition, 1994 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 (for consultation in English) or at Yoshihiro MIZOGUCHI (for consultation in Japanese).

 By report. There is no final examination.
その他