移民后不久，小柯尔斯坦的父母为了让他改掉吮手指的坏习惯，骗他说吮手指的小孩子在英国会被警察叔叔剪掉大拇指。没过多久，他们就发现小彼得竟然站在一大堆警察面前吮手指，还一边 (用德语) 问警察：“你们的剪刀呢？” 由此可见，柯尔斯坦在很小的时候就是一个实验主义者了。
# Week 1
# HoTT in type theory context
ITT(Intensional type theory) is a intuitionistic type theory that serves as the core theory for other type theories. Other type theories are merely extensions of
ETT(Extensional type theory) extends
ER(equality of reflection) and
UIP(uniqueness of identity proofs):
Since types are perceived as sets in
ETTgives rise to a intuitionistic theory of sets.
HIT(higher inductive types) and
Since types are perceived as abstract spaces in
HoTTgives rise to a intuitionistic theory of .
# Intuitionistic propositional logic
Intuitionistic logic means it is a proof-relevant logic.
As advanced by Per Matin-Lof, a modern presentation of
IPL(intuitionistic propositional logic) distinguishes the notions of judgment and proposition.
A judgment is something that may be known, whereas a proposition is something that sensibly may be the subject of a judgment.
IPL, the two most basic judgements are A prop and A true:
- A prop A is a well-formed proposition
- A true Proposition A is intuitionistically true, i.e., has a proof.
The inference rules for the prop judgment are called formation rules.
The inference rules for the true judgment are divided into classes: introduction rules and elimination rules.
# Negative fragment of IPL
Another familiar and simple proposition is truth, which is denoted by .
The last form of proposition in the negative fragment of
IPL is implication.
However, to define implication, a different form of judgment is required: entailment, which is written as:
we can understand the left part as the “context”, denoted by , or the assumptions for . So we can rewrite the conjunction as:
transitivity are undeniable properties of entailment
because they give meaning to assumptions—assumptions are strong enough to prove
conclusions (reflexivity), but are only as strong as the proofs they stand for (transitivity).
But there are also structural properties that can be denied:
contraction , and
permutation . Logics that deny any of these properties are called
Denying contraction (along with weakening) leads to linear logic, in which we
wish to reason about the number of copies of an assumption. This is a powerful way
to express consumable resources. In this course, we will always have the principle of
where is a permutation of .
Denying permutation (along with weakening and contraction) leads to ordered,
or noncommutative, logic. It is a powerful way to express ordered structures, like
lists or even formal grammars. In this course, we will always have the principle of
The introduction rule for implication is:
We use implication to internalize the entailment as a proposition: is not a proposition while is a proposition.
We may write the elimination rule as . However, we can consider “” as some stuff like function. We would prefer the uncurried form of elimination rule, which is:
it’s somehow “(A, B) -> C” instread of “A -> (B -> C)”.
# Positive fragment of IPL
The introduction rule for disjunction is:
The elimination rule for disjunction is:
The unit of disjunction is falsehood, the proposition that is trivially never true, which we write as . Its formation rule is immdeidate evidence that is a well-formed proposition:
Because is never true, it has no introduction rule. However, it does have an elimination rule, which captures “ex falso quolibet”:
# Order-theoretic formulation of IPL
# Conjunction as meet
The elimination rules for conjunction (along with reflexivity of entailment) ensure
that and .
To ensure completeness of the order-theoretic formulation, we include the rules:
which say that is a lower bound of A and B.
The introduction rule for conjunction ensures that if both
and . Order-theoretically, this is expressed as the rule:
which says that is larger than or equal to any lower bound of A and B.
Taken together these rules show that is the greatest lower bound, or meet, of A and B.
# Truth as greatest element
The introduction rule for truth ensures that . Order-theoretically, we have
which says that is the greatest, or final element.
# Disjunction as join
The introduction rules for disjunction ensure that and , we include the rules:
which say that is an upper bound of A and B.
The elimination rule for disjunction (along with reflexivity of entailment) ensures that
if both and .
Order-theorectically, we have the rule:
which says that is as small as any upper bound of A and B.
Taken together these rules show that is the least upper bound, or join, of A and B.
# Falsehood as least element
The elimination rule for falsehood (along with reflexivity of entailment) ensures that
. The order-theoretic counterpart is:
which says that is the least, or initial element.
# Implication as exponential
The elimination rule for implication (along with reflexivity of entailment) ensures that
. For the order-theoretic formulation to be complete, we include the rule:
The introduction rule for implication ensures that if
. We have:
Taken together, is the exact upper bound of the set .
What’s more, we can consider as the exponential: .
Why? We use a more familiar denotation “” for implication, you may realize that the set of functions from set A to set B is also denoted as .
The process of currying and uncurrying is just the arithmetic law:
# Week 2
# Lindenbaum algebra
IPL has the structure of a preorder, where we declare if and only if .
Let be some theory in
IPL and define a relation on the propositions in by:
Obviously, is an equivalence relation.
Definition. The Lindenbaum algebra of is defined to be the collection of -equivalence classes of propositions in . Write . The ordering on the Lindenbaum algebra is inherited from .
# Decidability and stability
Definition. A prop is decidable if and only if .
Decidability is what separates constructive logic from classic logic: in classic logic, every proposition is decidable while in constructive logic, it’s not.
- are decidable.
- We would expect is decidable, where denotes the quality of natural numbers.
- we would not expect is decidable, where denotes the quality of real numbers, because they are infinite.
Definition. A prop is stable if and only if .
Again, in classic logic, every proposition is stable, while in constructive logic let’s consider the following lemma:
We must show .
- We first prove :
- So in fact,.
Then we have
The lemma says the exclude middle proposition is not stable since can be proved but cannot.
# Disjunctive property
A theory T has the
DP(disjunctive property) if implies or .
IPL , if then or .
Naive attempt at a proof: The idea is to perform induction on all
possible derivations of .
Since can only be obtained by and .
Here we already obtained a proof for , is just similar.
then we can find that since , there must be a proof for .
The we can use to substitute all the occurence in for . Then we get a smaller derivation for . Thus we can repeat the process and in finite repeatation we can fall back on or other deduction rules.
# Admissible properties
Definition. A deduction rule is admissible in
IPL if nothing changes when it is added to the existing rules of
Theorem. The structural properties of are admissible.
Firstly we can prove that Reflexivity, Contraction and Exchange are admissible. Take Reflexivity as an example:
it is admissible in that it can be substituted by:
And for contraction, for any derivation we can substitute any in by .
So the rule does not change anything.
For weakening rule, we need to use the induction:
Suppose that and are admissible, then there will be derivation without weakening for them:
then we can prove that is also admissible:
Then by induction we can shrink the derivation, until the proposition don’t have “”. The last proposition is proved by some rules other than weakening, so the weakening is admissible.
Other rules are proved in the same way. In a word, structural properties (Reflexivity, Contraction, Exchange, Weakening, Transitivity) are admissible, while negative and positive fragments (conjunction,disjunction)
# Proof terms
# Proof terms as variables
We use the notation to denote that is a proof of proposition .
To track the proofs, we will write:
where each is a proof term.
We can think as the hypothesis for the proof,
but what we really want is for them to behave like varaibles, the proof
will use the variables to prove.
# Structural Properties of Entailment with Proof Terms
- Reflexivity/Variable rule:
which means, if the previous proof can prove the proposition , then is no longer needed. We can substitute with in the proof of .
If we have two different proofs for the same proposition ,then we can pick one of them or and substitute the other one with :
# Negative fraggment of IPL with proof terms
- Truth: truth is trivially always true, so it doesn’t need any proof:
- Conjunction Introduction:We combine the proof as :
- Conjunction Elimination:
- Implication Introduction: we may view the proof as a variable:
- Implication Elimination:
# Identity of proofs
# Definitional equality
We need the definitional equality to define the equality of two proofs: are the same. We denote it as and want it to be the least congruence containing(closed under) the rules.
A congruence is an equivalence relation that respects our operations, for the equivalence relation that respects our operations, it basically means that if , then that their images under any operator should be equivalent. In
other words, we should be able to replace with everywhere. For example, it shoule be true that:
There might be many congruences that contains the rules. Given two congruences and , we say
is finer that if implies .
# Gentzen’s Inversion Principle
Gentzen’s Inversion Principle captures the intuition that “the elimination rules should cancel the introduction rules modulo definitional equility”.
The following are the rules for the negative fragment of
# Gentzen’s Unicity Principle
Gentzen’s Unicity Principle captures the intuition that “there should be one way to prove something under definitional equivalence”.
# Proposition as types
There is a correspondence between propositions and types:
Later we will see the objects of the types introduced in the right column.
# Categorical Theoretic Approach
In a Heyting Algebra, we have a preorder when
However, we now wish to keep track of proofs, so if
is a proof from to , we want to think it as a map
We should be able to compose maps:
Now we can think about objects in the category that corresponds to propositions given in the correspondence.
1 is the terminal object, also called the final object,
which corresponds to . For any object there is a unique map . This corresponds to being the greatest object in a Heyting Algebra, meaning that for all , .
For any objects and there is an object that is the product of and , which corresponds to the join . The product has the following universal property:
where the diagram commutes.
First, the existence condition means that there are maps:
The universal property says that for every object such that and , there exists a unique map such that:
and the diagram commutes meaning
Furthermore, the map is unique in the sense that
so in other words, .
Another way to say above is:
Given objects and , an exponential (which corresponds to ) is an object with the following universal property:
such that the diagram commutes.
This means that there exists a map (application map) that corresponds to implication elimination.
The universal property is that for all objects that have a map , there exists a unique map such that:
This means that the diagram commutes. Another way to express the induced map is .\
The map is unique, meaning that
# The and rules
# Gentzen’s Inversion Principles ( rules)
Recall the rules:
where means if x then y else z. means that in
the proof , we use the left proof and to prove .
# Gentzen’s Unicity Principles ( rules)
Recall the rules we have given so far: