[Logiweb] Referencing faulty pages

[Klaus Ebbe Grue]

Hi Frederik

> Suppose you're working on a page called B, which references a page called A. 
> Page A is faulty; that is, it wasn't deemed correct by the proof checker. In 
> contrast, page B in itself is not faulty. Now you let the proof checker 
> verify page B. What happens? Will the checker take the correctness of page A 
> for granted, or will it deem page B faulty because it references faulty 
> lemmas from page A?

If a proof on page B references a lemma proved on page A, and page A was 
deemed faulty, then page B is deemed faulty. Apart from that, errors on 
page A does not affect the correctness of page B. For that reason, one can 
freely use definitions available on faulty pages as long as one does not 
use lemmas from A.

As an additional remark, if page A was deemed correct, but was checked by 
a different proof checker, then the present proof checker does not allow 
references to lemmas on page A. In other words, the proof checker trusts 
itself, but does not trust any other proof checker.

Klaus