# [FOM] Logiweb

Klaus Ebbe Grue grue at diku.dk
Fri Feb 9 18:56:23 EST 2007

```> Are you planning to jump-start the system by importing the contents of
> pre-existing formally-verified bodies of mathematics as such as the
> Mizar project?

Yes. I'm looking at Mizar right now. And I'm going to work on other
systems afterwards with focus on making the systems interoperable. (Help
will be very welcome, so don't hesitate to volunteer:-)

Logiweb and its predecessors have been used internally at the University
of Copenhagen since 1985 for teaching logic, so it may seem odd that it
does not already have a big library of results. But it has just been used
for individual student projects, and many students have simply proved the
same theorems.

> Will the system make it easy to keep track of which statements have
> been formally verified as following from particular well-known axiom
> systems such as PA and ZFC?

It depends on exactly what you mean.

First of all, Logiweb allows anybody to define their own proof checker.
And the answer to the question would be different for each proof checker.

But the proof checker that comes with Logiweb is pretty general. Using
that proof checker, a theorem could have form

(1)  PA |- x+y=y+x

or

(2)  ZFC |- x has no elements and y has no elements implies x = y

So it is obvious from the theorem which axiomatic system is used. Now one
could also define ZF (ZFC without C) and prove

(3)  ZF |- x has no elements and y has no elements implies x = y

It would be rather trivial to prove

(4)  ZFC |- ZF

And it would be trivial to combine (3) and (4) to get (2). Going the other
way would also be possible provided one has a proof of (2) which does not
use the axiom of choice: one could state (3) and then prove it by a term
which macroexpanded into a copy of the proof of (2).

The proof checker which comes with Logiweb also has the ability to handle
theorems like

(5)  ZFC + SI |- ZFC is consistent

Here SI is the axiom which states that there exists an inaccessible
ordinal. The point is that one can express theorems in theories which
are expressed as a sum of statements.

Until further, I plan to handle Mizar theorems by theorems that look
somewhat like this:

(6)  Mizar |- x has no elements and y has no elements implies x = y