Post #2103981
2026-02-12 13:59 UTC
@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 Γ -> φ.
Replies (1)
-
@constantine@types.pl 2026-02-12 14:06
@ncf @edwinb Maybe the wording is a bit weird though, it should maybe say “interpreted as (Γ → φ)” because otherwise it sounds like there is a particular unspecified map of type Γ → φ..