A Universe of Sorts

§ CS and type theory: Talks by vovodesky

Talk 1: Computer Science and Homotopy Theory
Think of ZFC sets as rooted trees. Have two axioms:
(1) all branches of all vertices are non-isomorphic (otherwise a set would have two copies of the same element)
(2) Each leaf must be at finite depth from the root.
This is horrible to work with, so type theory!
Talk 2: What if foundations of math is inconsistent?
We "know" that first order math is consistent. We can prove that it is impossible to prove that first order math is consistent!
Choice 1: If we "know" FOL is consistent, then we should be able to transform this knowledge into a proof, then 2nd incompleteness is false.
Choice 2: Admit "transcendental" part of math, write dubious philosophy.
Choice 3: Admit that our sensation that FOL +arithmetic is consistent is an illusion and admit that FOL arithmetic is inconsistent.
Time to consider Choice 3 seriously?

§ First order arithmetic

Mathematical object which belongs to class of objects called formal theories. Has four pieces of data:

Special symbols, names of variables.
Syntactic rules.
Deduction rules: Construct new closed formulas from old closed formula.
Axioms: collection of closed formulas.

Anything that is obtainable from these deduction rules is called a theorem. First order logic have symbols: ∀, ∃, ⇒, !(not) and so on. First order theory is inconsistent if there a closed formula

A

such that both

A

and

!A

is a theorem.

Free variables describe subsets. Eg: ∃ n: n^2 = m describes the set { m : ∃ n: n^2 = m }.
It's possible to construct subsets (formulae with one free variable) whose membership is undedicable. So you can prove that it is impossible to say anything whatsoever about these subsets.

§ Gentzen's proof and problems with it

Tries to reason about trees of deduction. Show that proofs correspond to combinatorial objects. Show that inconsistency corresponds to an infinite decreasing sequence that never terminates. Then he says that it is "self evident" that this cannot happen. But it is not self evident!

§ What would inconsistency of FOL mean for mathematicians?

Inconsistency of FOL implies inconsistency of many other systems (eg. set theory).
Inconsistency of FOL implies inconsistency of constructive (intuitionistic) mathematics! (WTF?) shown by Godel in 1933. Takes a proof of contradiction in classical and strips off LEM.
We need foundations that can create reliable proofs despite being inconsistent!
Have systems that react to inconsistency in less drastic ways. One possible candidate is constructive type theories. A proof of a formula in such a system is itself a formula in the system. There are no deduction rules, only syntactic rules. So a proof is an object that can be studied in the system. If one has a proof of contradiction, then such a proof can be detected --- they have certain properties that can be detected by an algorithm (what properties?)

§ New workflow

Formalize a problem.
Construct creative solution.
Submit proof to a "reliable" verifier. If the verifier terminates, we are done. If the verifier does not terminate, we need to look for other proofs that can terminate.
our abstract thinking cancels out by normalisation :P

§ Summary

Correct interpretation of 2nd incompleteness is a step of proof of inconsistency of FOL (Conjecture).
In math, we need to learn how to use inconsistent theories to obtain reliable proofs. Can lead to more freedom in mathematical workflow.

§ Univalent Foundations: New Foundations of Mathematics

Talk 3: Univalent foundations --- New Foundations of Mathematics

Was uncertain about future when working on 2-categories and higher math. No way to ground oneself by doing "computations" (numerical experiments). To make it worse, the existing foundations of set theory is bad for these types of objects.
Selected papers on Automath.
Overcoming category theory as new foundations was very difficult for vovodesky.
Categories are "higher dimensional sets"? NO! Categories are "posets in the next dimension". Correct version of "sets in the next dimension" are groupoids (WHY?) MathOverflow question
Grothendeick went from isomorphisms to all morphisms, this prevented him from gravitating towards groupoids.
Univalent foundations is a complete foundational system.
Sets are groupoids on the next dimension

§ Vovodesky's univalence principle --- Joyal

Talk 5: Vovodesky's univalence principle --- Joyal

Univanent type theory is arrived at by adding univalence to MLTT.
Goal of univalent foundations is to apply UTT to foundations.
Univalence is to type theory what induction principle is to peano arithmetic
Univalence implies descent. Descent implies Blakers Massey-theorem, which implies Goodwille calculus.

The syntactic system of type theory is a tribe .
A clan is a category equipped with a class of carrable maps called fibrations. A map is carrable if we can pull it back along any other map.
A clan is a category along with maps called "fibrations", such that (1) every isomorphism is a fibration, (1) closed under composition, (3) fibrations are carrable, (4) base change of fibration is a fibration, (4) Category has a terminal object, and map into the terminal object is a fibration.
A map $u: A \rightarrow B$ is anodyne if it does something good with respect to fibrations.
A tribe is a clan such that (1) base chnge of anodyne along fibration is anodyne, (2) every map factorizes as anodyne followed by fibration.
Kan complexes form a tribe. A fibration is a Kan fibration. A map is anodyne here if it is a monomorphism and a homotopy equivalence.
Given a tribe $E$ , can build a new tribe by slicing $E/A$ (this is apparently very similar to things people do in Quillen Model categories).
A tribe is like a commutative ring. We can extend by adding new variables to get polynomial rings. An elementary extension is extending the tribe by adding a new element.
If $E$ is a tribe, an object of $E$ is a type. We write E |- A : Type.
If we have a map $a: 1 -> A$ , we regard this as an element of A: E |- a : A.
A fibration is a family of objects. This is a dependent type x : A |- E(x): Type. E(x) is the fiber of p: E -> A at a variable element x : A.
A section of a fibration gives an element of the fibration. We write this as x : A |- s(x) : E(x). s(x) denotes the value of s: A -> E of a variable element x : A. (Inhabitance is being able to take the section of a fiber bundle?!)
change of parameters / homomorphism is substitution.

y : B |- E(y) : Type
--------------------
x : A |- E(f(x)) : Type

This is pulling back along fibrations.

Elementary extension E -> E(A) are called as context extensions.

|- B : Type
-----------
x : A |- B : Type

A map between types is a variable element f(x) : B indexed by x : A

x : A |- f(x) : B

Sigma formation rule: The total space of the union is the sum of all fibers(?)

x: A |- E(x): Type
------------------
|- \sum{x : A}E(x): Type

x: A |- E(x): Type
------------------
y : B |- \sum{x : f^{-1}(y)}E(x): Type

Path object for $A$ is obtained by factorial diagonal map diag: a -> (a, a) as an anodyne map r: A -> PA followed by a fibration (s, t) : PA -> A x A.

A homotopy h: f ~ g between two maps f, g : A -> B is a map h: A -> PBsuch that sh = f and th = g. homotopy is a congruence.
x: A, y : A |- Id_A(x, y) : Type called the identity type of A.
An element p: Id_A(x, y) is a proof that x =A y.
Reflexivity term x : A |- r(x) : Id_A(x, x) which proves x =A x.
The identity type is a path object
$\gamma(x, y): Id_A(x, y) -> Eq(E(x), E(y))$ . $\gamma$ is some kind of connection: given a path from $x$ to $y$ , it lets us transport $E(x)$ to $E(y)$ , where the $Eq$ is the distortion from the curvature?