Year 1 (January-December 1998)
The work this year would fall into two parts. In the first semester we will be testing, improving, and collecting data about the success of our lessons on function and logic, counting and induction in the Cornell discrete mathematics course and from outside users (via CoNote on the Web). We will have advertized these lessons on the Web and at meetings such as FIE. We will be writing a report and improving the lessons as well as teaching the material and supporting others who are using the material remotely.
In the summer and second semester we will be using NuprlW to create fully interactive lessons as extensions of the Web lessons. We will test these as we did the lessons for discrete mathematics. We will also finish material for a senior level logic course by adding lessons on proof formats, specifically Tableau and Natural Deduction proofs.
Use of NuprlW will represent another major contribution of the Nuprl research program (funded by DARPA, ONR and NSF) to education.
Year 2 (January-December 1999)
The work will again divide into two parts. We will deploy the fully interactive lessons, both in discrete mathematics and in logic. The logic material will include a module we are calling the Gödel Project which will include an account of the Gödel incompleteness theorem.
In the second semester, we will either build lessons to enhance the automata library or the semantics of programming library depending on what subjects get developed further as part of our research program. At this point we will have a Courseware Library of nearly two dozen lessons that can support at least four courses in Mathematics and Computer Science.
The final phase of this grant would be to organize an increased group of instructors using our material. The details of this will depend on the exact composition of the users and their feedback to us.
Appendix Here we give a summary of a theory that covers the existence and uniqueness of factorizations in abelian cancellation monoids. The final theorems of this theory can easily be instantiated to give the fundamental theorem of arithmetic.
Basic Definitions The basic definitions for divisibility theory over an abelian monoid g are:
Here, | is the divides relation, is the associated
relation and p| is the `properly divides' relation. The
=
relation is Nuprl's typed equality
relation: it states that
and
are equal members of type
.
The divides relation is a preorder:
The type AbMonoid is the class of abelian monoids. An element g of this class is a tuple <|g|,xg,1g> where xg is an
commutative associative binary operator over the carrier |g|, and
1g is the unit. The i index in the {i} suffix is
implicitly quantified over the natural numbers: it indicates the size of
the universe of types that the carrier comes from.
The predicates and functions in factorization theory respect
associates and predicates concerning equality lift to predicates
concerning associates. For example, xg respects and
cancellation with respect to equality implies cancellation with
respect to
:
where:
Other definitions are for reducibility, atomicity and primeness. For convenience, both types and predicates were defined for atomicity and primeness:
From these definitions various facts were proven such as that every prime is an atom in a cancellation monoid:
Existence Theorem The theorem characterizing when factorizations into atoms exist is:
The theorem says that in a cancellation monoid with a well-founded
`properly divides' relation, every non-unit can be factorized into atoms.
The predicate Dec(reducible(g;c))) states that reducibility
is a decidable property in g. This assumption is necessary because
the theorem was proven constructively. The function g
takes
the product using xg of the elements of list
. If
is the
empty list, it returns 1g.
An abbreviated proof listing for the theorem is shown in
. The proof is presented in a style
very similar to that in which Nuprl proofs are normally presented: The
goal proven is shown at the top, and after each BY one or more
inference steps are explained which refine the goal immediately above
the BY into zero or more subgoals below the BY. For
compactness, the proof only shows those parts of the sequent that have
been changed by the refinement.
Normally, proofs show the names of tactics after each BY. Here, to improve readability, we have paraphrased the tactics in English and have elided a few intermediate steps of the proof. The full proof when printed out is less than two times longer.
Here is a version of the theorem and proof, closer to how it might appear in a text-book.
For all Abelian Monoids ,
Proof: Let be an arbitrary Abelian Monoid with the given properties, and let
be an arbitrary non-unit of
. We must find the factorization
. Proceed by induction on the well-founded divisibility relation, written p|.
Summarizing and numbering the unused assumption (6 is the induction hypothesis).
QED
Uniqueness Theorem The theorem characterizing when factorizations are unique is:
The relation
upto
says that list
and
list
are a permutation of each other up to the equivalence relation
on the elements of the list. Here, with
being the relation
g, it captures the notion of factorizations being `essentially'
the same.
An abbreviated proof of the theorem is shown in
. The full proof printout is about 2.5
times longer. Additional notation is introduced in the proof
as follows:
role of computer science It is interesting that computer science and engineering have played three major roles in enabling the enterprise we describe. It has produced hardware platforms of sufficient power to do the work. It has created software systems that accelerate programming productivity to the point that ambitious systems can be built with small staffs. It has also re-centered the philosophical debate about the value of formal mathematics. By generating large software systems governed completely by formal rules, it has changed a philosophical question. At the beginning of the century, in response to Hilbert's program it was, ``Can formalism explain and justify mathematical practice?" Now at the end of the century it is, ``How can we use mathematics to explain and control the monumental amount of useful formal material (including the mathematical) that will be a large factor of the human condition in the 21st century?"
We are proposing to capitalize on the existence of this new artifiact by bringing it into the classroom. This will enable us to teach mathematics, computing, and their applications in science and engineering in new ways. But it will also teach a lesson unique to our times. We can demonstrate a new kind of knowledge in which explanation is completely precise and rests ultimately on only explicit assumptions in a way we can track.