Introduction to categorical logic 1

Notes from this Youtube video.
The purpose of this course is to give an introduction to first order categorical logic with the aim of explaining the notion of classifying topos of a geometric theory, especially the way classifying toposes can be used for discovering connections between mathematical theories, much as in the spirit of Grothendieck, toposes are unifying spaces.
Toposes as a tool that could be used for connecting different mathematical theories with each other, and transfering results, notions and properties across them.
Why is logic important in connection with such a unifying project ? Because logic allows to formalize the notion of mathematical theory. So the comparison between mathematical theories becomes something that can be carried out in a most rigorous way.

Classifying toposes provide even more than just logic because the notion of classifying topos really formalizes the notion of content of a mathematical theory.
This is particularily important in connection with the goal of unifying different theories because if you discover that two theories have the same classifying topos, then this means that the two theories tell the same story in different languages. Every time you have multiple points of view on a given situation, you can switch from one to an other, according to the features of the problem you want to investigate.

Two theories tell the same story
in different languages

First-order languages

These are the most studied language in logic, they admit very nice model theory, and thanks to classifying toposes also a functorial model theory, in the sense that models can be thought as functors preserving a certain kind of structure.
These are a wide class of languages that can be used for describing mathematical structures.

Syntax and semantics

The basic point of logic is to make a separation between two different levels : the level of syntax and the level of semantics.
The semantics are just the mathematical structures that one wants to investigate ; for instance varieties, groups, whatever.

Usually the mathematicians work, from a logical point of view, with the semantics.
Syntax is the world of languages, of ways that we may use for describing the structures.
In general we can describe a same thing in many different ways. In logic, it's the same thing, we can have many different syntaxes for a given semantical content.

And logic is all about the relationship between this two levels. It is very important to bear in mind that logic is all about a duality between the structures and the way we can describe them.
Structures Way we describe structures
A given semantical content Many different syntaxes
Varieties, groups, ... Languages
First-order languages

Second-order languages

In the axioms of a first-order theory, you are only allowed to quantify over individuals of your structures, and not over collections of individuals
(or collections of collections of individuals).

For instance, the commutativity property in a ring can be formalized in a first-order way.
But describing the properties of real numbers is second-order, if you want to formalize the real numbers as a set of elements because you have to refer to collections of such elements.

First-order languages

These are the basic restrictions that one makes in order to have a well-behaved model theory.
If we want to investigate Grothendieck toposes in a logical point of view, we will always remain at the first-order level, even though we will use Sites also, which is a second-order notion.

Sites, Topos, Grothendieck topology, sieves

Between 05:50 and 11:08 : quick presentation