Nuprl Definition : less_than'

At one time, ⌜a < b⌝ was primitive type, and the equality rule for it
said that ⌜a < b⌝ was type if ⌜a ∈ ℤ⌝ and ⌜b ∈ ℤ⌝.
An elimination rule said that if ⌜t ∈ a < b⌝ then ⌜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 proposition (even when we know that it is 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'

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