Thm* A B
(
C:Prop. (A
C)
(B
C)
C)
Thm* a,b:A. a = b
(
P:(A
Prop). P(a)
P(b))
we cannot adopt these as definitions, although it is not unusual to do so in some other accounts of higher-order logic. The reason is that we have adopted a "predicative" semantics (a term of Bertrand Russell's of uncertain etymology) which avoids defining a proposition by quantifying over a domain that includes the proposition to be defined. Basically, in a predicative logic, to assign meaning to a quantificational expression one must "already" have given meaning to all the expressions that might be used as witnesses. So, assigning a meaning to C:Prop. (A
C)
(B
C)
C"
C:Prop. (A
C)
(B
C)
C"
The solution adopted here is to stratify the propositions into a hierarchy
Thm* A,B:Prop{i}. (
C:Prop{i}. (A
C)
(B
C)
C)
Prop{i'}
Thm* A:Type{i}, a,b:A. (
P:(A
Prop{i}). P(a)
P(b))
Prop{i'}
where
Thm* A,B:Prop{i}. (A
B)
Prop{i}
Thm* T:Type{i}, a,b:T. (a = b
T)
Prop{i}
As with
Quantification over types raises the propositional level, just as does quantification over propositions, indeed,
Thm* Prop{i} Type{i'}
Thm* Prop{i} Prop{i'}
Because the universes and propositional types are cumulative, one can often state theorems with a single level variable. For example,
Thm* A:Type{k}, P:(A
Prop{j}). (
x:A. P(x))
Prop{[k | j]}
which says that the existential is a proposition at the maximum of the two levels of its domain and predicate, follows simply from the at-first-sight less general
Thm* A:Type{i}, P:(A
Prop{i}). (
x:A. P(x))
Prop{i}
since if Type{k}
A
Prop{j}
Type{[k | j]}
A
Prop{[k | j]}
x:A. P(x))
Prop{[k | j]}
Thm* A:Type, P:(A
Prop). (
x:A. P(x))
Prop
See also
About:
![]() | ![]() | ![]() | ![]() | ![]() | ![]() | ![]() | ![]() | ![]() | ![]() |