## From High School Algebra to University Algebra

School of Computer Science

University of Nottingham

Monday, 8 June 2009, 14:00 (note the unusual weekday!)

Cybernetica Bldg (Akadeemia tee 21), room B101

**Abstract**: Tarski coined the name "High School Algebra" for
the algebraic theory of a semiring with exponentiation. The intended
interpretation are the natural numbers and Tarski conjectured that
High School Algebra is complete - however this was refuted by
Wilkie. DiCosmo observed that High School Algebra can also be
interpreted as isomorphisms in a lambda calculus with coproducts
(biCCCs) and that Wilkie's counterexample corresponds to an isomorphism
which is valid in this calculus but which cannot be derived by
composing isomorphisms. Inspired by this interpretation we introduce
"University Algebra" moving to a dependently typed lambda calculus
with Pi, Sigma, and 1, 2. We observe that Wilkie's counterexample can
be derived from basic isomorphisms and discuss why we think that
University Algebra is actually complete, i.e. can derive all
isomorphisms between finite sets.

Tarmo Uustalu

Last update 4.6.2009