Information Technology Reference
In-Depth Information
2
1
R
0
cov
S
base
U
1
).
The dependent type
cov
:
Definition 1 (Universal Cover of
S
S
is
given by circle-recursion, with
cov
(
base
):=
Z
cov
(
loop
):=
ua
(
succ
)
.
As in classical homotopy theory, we use the universal cover to define the
“winding number” of any path
p
:
base base
by
wind
(
p
)=
p
∗
(0). This gives a
map
Z
wind
:
ʩ
(
S
)
,
ʩ
(
which is inverse to the map
Z
S
)givenby
→
loop
z
.
z
Formalization of Mathematics
-
The idea of logical foundations of math has great conceptual and philosoph-
ical interest, but in the past this was too lengthy and cumbersome to be of
any use.
-
Explicit formalization of math is finally
feasible
, because computers can now
take over what was once too tedious or complicated to be done by hand.
-
Future historians of mathematics will wonder how Frege and Russell could
have invented formal logical foundations
before
there were any computers to
run them on!
-
Formalization can provide a
practical tool
for working mathematicians and
scientists: increased certainty and precision, supports collaborative work, cu-
mulativity of results, searchable library of code, ... I think that mathematics
will eventually be fully formalized.
-
UF uses a “synthetic” method involving high-level axiomatics and structural
descriptions; allows shorter, more abstract proofs; closer to mathematical
practice than the “analytic” method of ZFC. Use of UA is very powerful.
