Logiweb(TM)

14.274 Lemma P occurs on a page which has not been checked

Prev Up Next Page 745 of 800 Search internet


Origin: check. Landing-place: diagnose.

Lemma P occurs on a page which has not been checked by the present proof checker. Avoid referencing that lemma.

When a proof references a lemma on another page, the verifier checks two things: First, that that other page has been proof checked. Second, that the outcome of verification was positive.

The verifier checks that the other page has been proof checked by looking up the rack of the other page, then looking up the codex in the rack, then looking up the claim aspect of the page symbol in the codex. Then the verifier checks that the claim is identical to the verifier itself. If the claim is a conjunction built up using x &c y then the verifier checks that the verifier itself belongs to the conjunction.

Note that the verifier of the check page has no reservations about pages checked by other proof checkers. But the verifier protests the moment one uses a lemma from a page it has not checked itself.

Also note that the verifier of the check page accepts to work in conjunction with other checkers.

Prev Up Next Page 745 of 800 Search logiweb.eu

Copyright © 2010 Klaus Grue, GRD-2010-01-05