Nuprl Definition : less_than'
At one time, ⌜a < b⌝ was a primitive type, and the equality rule for it
said that ⌜a < b⌝ was a type if ⌜a ∈ ℤ⌝ and ⌜b ∈ ℤ⌝.
An elimination rule said that if ⌜t ∈ a < b⌝ then ⌜t ~ Ax⌝.
All of these properties are easily derivable if we simply define
⌜a < b⌝ using the primitive `less` comparison operator
⌜if (a) < (b) then True else False⌝
However, from the fact that ⌜if (a) < (b) then True else False⌝
is a proposition (even when we know that it is a true proposition)
it does not follow that ⌜a ∈ ℤ⌝ and ⌜b ∈ ℤ⌝ because, for example
from a:⇃({...3}), b:⇃({4...}) we can prove that
⌜if (a) < (b) then True else False ∈ ℙ⌝.
Therefore, we call ⌜if (a) < (b) then True else False⌝ ⌜less_than'(a;b)⌝
and reserve ⌜a < b⌝ for the proposition that includes ⌜(a ∈ ℤ) ∧ (b ∈ ℤ)⌝⋅
less_than'(a;b) == if (a) < (b) then True else False
Definitions occuring in Statement :
false: False,
true: True,
less: if (a) < (b) then c else d
Definitions occuring in definition :
less: if (a) < (b) then c else d,
true: True,
false: False
FDL editor aliases :
less_than'
Latex:
less\_than'(a;b) == if (a) < (b) then True else False
Date html generated:
2016_07_08-PM-04_46_37
Last ObjectModification:
2016_01_04-AM-10_27_00
Theory : core_2
Home
Index