-
Notifications
You must be signed in to change notification settings - Fork 2
Logic of Elementary Topos
A topos T is a CCC with a subobject classifier Ω - such an object, with a monomorphism true: 1 ↣ Ω that any monomorphism f: A ↣ B is a pullback
for some χf. This arrow, χf, is called a classifying arrow for f (it's like a characteristic function for a set inclusion).
It was a definition. For a topos, we can define logical operations in Ω.
Provided by the definition.
false is an arrow that classifies 0 ↣ 1, where 0 is an initial object of T:
Ω does not have to have just two points, and it does not have to consist of just points. More, 0 and 1 don't have to be two distinct points; they can be the same point, in which case the topos T is degenerate (or is there a better word?)
We can define the three usual connectives, ∧, ∨, ⇒
It's a classifying arrow χ(true,true) for the monomorphism (true,true): 1 ↣ Ω×Ω:
(source: Johnstone, 1.49)
Implication is a classifying arrow χ(Ω1 ↣ Ω×Ω):
Where Ω1 is a "partial order" on Ω, that is, an equalizer of first projection π1 and conjunction ∧:
(source: Johnstone, 3.51)
This is the hardest part. Disjunction is build using union of subobjects. So, let's build a union first.
Given X1 ↣ X and X2 ↣ X, we build X1∩X1 ↣ X, and then a pushout
.
It's easy to show that we have a subobject, X1∪X2↣ X.
Now let's build a disjunction ∨.
Ω×Ω has two subobjects, and ; denote the union of these two subobjects as ΩU.
Disjunction ∨: Ω×Ω → Ω is the classifying arrow χΩU ↣ Ω×Ω:
(source: Johnstone 3.51, 1.55)
Negation is a composition of and implication ⇒.
Source: Johnstone, "Topos Theory"