[FOM] Logiweb

[Klaus Ebbe Grue]

> 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

I hope the examples above more or less answer your question. Else please 
ask again.

Cheers,
Klaus