mathematical ontology

Freek Wiedijk University of Nijmegen

MoWGLI & Authomath meeting DFKI, Saarbrücken 2004 03 23, 10:00 different things that can be investigated two aspects of encoded mathematics inside a computer

meta level = ‘form’ ⇒ computer science ← focus of MoWGLI
object level = ‘meaning’ ⇒ mathematics

formal versus informal mathematics

‘informal terms’ ⇒ not well-understood mathematics

many formulas in computer algebra many formulas in physics

‘formal terms’ ⇒ mathematics with a clear semantics

formal mathematics a common formal library? systems for formal mathematics … … with a significant formal library, in which everything is proved

• Coq

• C-CoRN

• Mizar

• HOL

• IMPS

• NuPRL

• Isabelle

• PVS relating formal libraries six libraries about finite sets Coq standard library, Jean-Christophe’s fsets library for Coq, Dan Synek’s contrib to C-CoRN, & the libraries of Mizar, HOL, IMPS

find the common statements • database with for each system the lemmas about finite sets

• pointers relating ‘the same’ statements in different systems relating formal libraries (continued)

the empty set has zero elements

Coq: standard library

cardinal_Empty : forall m:nat, cardinal U (Empty_set U) m -> 0 = m

Coq: fsets library

cardinal_1 : (s:t)(Empty s) -> (cardinal s)=O

Mizar

CARD_2:19 : 0 = Card {}
CARD_4:17 : X = {} iff Card X = 0

HOL

CARD_CLAUSES : CARD ({}:A->bool) = 0

IMPS

EMPTY-INDIC-HAS-F-CARD-ZERO-REWRITE : f_card{empty_indic{ind_1}}=0

term language for common statements of the systems what features should this term language have?

• higher order = first class binders (excludes Mizar)

• subtypes (excludes Coq, HOL, IMPS)

• coercions (excludes Mizar, HOL, IMPS)

• dependent types (excludes HOL, IMPS)

• overloading (excludes Coq, HOL, IMPS)

• a global ‘set’ type (excludes HOL, IMPS)

• partial operations (excludes Mizar, HOL) having none of these features is too poor but it is not nice to exclude a system to be able to have a feature ! division in the real numbers is already non-trivial

\frac{1}{0} = 0 ?

Coq standard library independent (= not provable & negation not provable)
C-CoRN not well-formed
Mizar before: independent; now: provably true
HOL provably true
IMPS provably false
PVS not well-formed

a nice plan

1. term language define a term signature define when a term over this signature is ‘well-formed’

2. map this term language to the n systems define a mapping of the well-formed terms to Coq define a mapping of the well-formed terms to C-CoRN define a mapping of the well-formed terms to Mizar …

coherence: a well-formed statement should be provable in system X iff it is provable in system Y a nice plan (continued)

3. create a small database of sample statements in this term language statements from a trivial domain (finite sets) statements from an algebraic domain (basic theory of vector spaces) statements from an analytic domain (theory of natural logarithm)

4. prove the mapped version of each sample statement in each system prove statement A in system X prove statement B in system X … prove statement A in system Y prove statement B in system Y … between systems: not only statements but also proofs

proofs in the style of the Mizar system block structured proof language

statements connected by tactics

leave out the tactics, just keep the statements proofs that are meaningful across systems !

‘formal proof sketches’

closely related to Laurent Théry’s Color Your Proof system section 4.1 of Abramowitz & Stegun 57 formulas can be rendered with a signature of 45 symbols (this signature is similar to that of Content MathML)

but: what does it mean?

     eq(ln(0),minus(infinity))
     eq(e,approx(27182818284,10))
     eq(integral([z]div(1,z),z),ln(z))

… summary what I want is formal mathematics that is not bound to just one system the three things I’ve talked about:

• relate libraries about the same subject in different systems (the example of the finite sets libraries)

• define a term language for a common core of formal statements (the nice plan with four parts)

• make a version of section 4.1 of Abramowitz & Stegun where all terms have a well-defined formal semantics