Post #2103980
2026-02-12 13:51 UTC
@constantine @edwinb
The sort # ∈ Γ is interpreted as a map Γ → ϕ
Should this be Γ → Ω?
Replies (1)
-
@constantine@types.pl 2026-02-12 13:59
@ncf @edwinb No, what is Ω? If you mean the subobject classifier then no, # ∈ Γ is not the sort of propositions over Γ. Rather it is itself a particular proposition over Γ. # is interpreted as φ in the second order model, and the first order model “relativises” everything by Γ so it becomes Γ -> φ.