Logic of Elementary Topos - vpatryshev/wowiki GitHub Wiki

Logic of Elementary Topos

Definition

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 Ω.

Logical Values

true: 1 ↣ Ω

Provided by the definition.

false: 1 ↣ Ω

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?)

Logical Connectives

We can define the three usual connectives, ∧, ∨, ⇒

Conjunction ∧: Ω×Ω → Ω

It's a classifying arrow χ(true,true) for the monomorphism (true,true): 1 ↣ Ω×Ω:

(source: Johnstone, 1.49)

Implication ⇒: Ω×Ω → Ω

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)

Disjunction ∨: Ω×Ω → Ω

This is the hardest part. Disjunction is build using union of subobjects. So, let's build a union first.

Union of Subobjects

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 ¬: Ω → Ω

Negation is a composition of and implication ⇒.

Source: Johnstone, "Topos Theory"

⚠️ **GitHub.com Fallback** ⚠️