Go backward to 5.2 The Categoricity of the Reals
Go up to 5 More About the Specification BasicReal
Go forward to 5.4 A Short Remark on Related Work

## 5.3 The Specification of the Reals in Higher-Order CASL

We here rely on higher-order CASL as proposed in [HKBM98]. We give two specifications of the reals in higher-order CASL, one using sequences, as BasicReal, and the other one using bounded sets. Both specifications are equivalent.

spec
DefineHigherOrderReal1 =
Nat and OrderedField with Elem |-> Real
then
ops
 __ < __: pred(Real × pred(Real)); __ < __: pred(pred(Real) × Real); isBounded: pred(pred(Real)); __ < __: pred(Real × (Nat -> Real)); __ < __: pred((Nat -> Real × Real); isBounded: pred(Nat -> Real)
vars
r,s:Real; M:pred(Real); a:Nat -> Real
.
M < r <=> forall s:Real . M(s) => s < r
.
r < M <=> forall s:Real . M(s) => r < s
.
isBounded(M) <=> exists ub,lb:Real . lb < M /\ M < ub
.
a < r <=> forall n:Nat . a(n) < r
.
r < a <=> forall n:Nat . r < a(n)
.
isBounded(a) <=> exists ub,lb:Real . lb < a /\ a < ub
%%
weak choice:
.
¬ isBounded(M) => exists a:Nat -> Real. ¬ isBounded(a) /\ forall n:Nat. M(a(n))
then
ops
partialSums : (Nat -> Real) -> Nat -> Real
vars
n:Nat; r:Real; a:Nat -> Real
.
partialSums(a)(0) = a(0)
.
partialSums(a)(succ(n)) = partialSums(a)(n) + a(succ(n))
%%
Convergence, infinite sums, and Cauchy sequences:
ops
lim,sum : Nat -> Real ->? Real
preds
 __ -> __ : (Nat -> Real) × Real; converges,cauchy : Nat -> Real
vars
r:Real; a:Nat -> Real
%%
Convergence of a sequence:
.
 a->r <=> forall epsilon:Real . epsilon > 0 => ( exists n:Nat . forall m:Nat . m > n => abs(a(m) - r) < epsilon )
.
lim(a)=r <=> a->r
.
converges(a) <=> def lim(a)
%%
infinite sums:
.
sum(a) = lim(partialSums(a))
%%
Cauchy sequences:
.
 cauchy(a) <=> forall epsilon:Real . epsilon > 0 => (exists n:Nat . forall m,k:Nat . m > n /\ k > n => abs(a(m) - a(k)) < epsilon )
then
%%
completeness axiom:
var
a:Nat -> Real
.
cauchy(a) => converges(a)
end
spec
DefineHigherOrderReal2 =
OrderedField with Elem |-> Real
then
ops
 __ < __: pred(Real × pred(Real)); __ < __: pred(pred(Real) × Real); isBounded: pred(pred(Real)); inf,sup : pred(Real) ->? Real
vars
r,s:Real; M:pred(Real)
.
M < r <=> forall s:Real . M(s) => s < r
.
r < M <=> forall s:Real . M(s) => r < s
.
inf(M)=r <=> r < M /\ forall s:Real . s < M => s < r
.
sup(M)=r <=> M < r /\ forall s:Real . M < s => r < s
.
isBounded(M) <=> exists ub,lb:Real . lb < M /\ M < ub
%%
completeness:
.
isBounded(M) => def inf(M) /\ def sup(M)
end

CoFI Note: M-7 -- Version: 0.2 -- 13 April 1999.
Comments to till@informatik.uni-bremen.de