Week 8 Lab: Prove in iset.mm

The same theorem proved against set.mm and then iset.mm, to see where a classical proof needs excluded middle. Then the verifier project check-in: where your verifier should be by now.

28 April 2027

Before the lab#

Download iset.mm; the metamath-exe README points there or to the metamath/set.mm repository. Download peano.mm too. Bring your verifier as it stands, and read “How to intuitionize classical proofs” on the Intuitionistic Logic Explorer home page. The definition exercise is due this week; submit it before the lab if you have not.

In the lab#

The first hour is one theorem, twice. Choose a propositional theorem from your earlier lab proofs and prove it in mmj2 against set.mm. Then start mmj2 with the LoadFile RunParm naming iset.mm (the batch documentation takes a filename there) and prove the same statement again. For some theorems it goes through unchanged.

Then take one from the home page’s cross reference of set.mm theorems that iset.mm lacks. notnotr, double negation elimination, is a good first choice; the page’s note is that “Double negation introduction holds but not double negation elimination.” Try it, and when it does not go, use the page’s rules of thumb: case elimination with pm2.61 splits into two theorems unless the proposition is decidable, and “Some things just won’t have intuitionistic proofs.” Write down which step needed excluded middle and what the table offers instead.

The second hour is the verifier project check-in. The course names, that morning, the tests in its suite that a verifier on track should pass by week 8; run yours against them in front of Teodor and say which pass. A verifier behind that mark is not penalised, but you leave with a list of what to do first. Bring the code: the questions worth asking are about the rule you have not enforced yet, and they are quicker with the file open.

Afterwards#

Nothing from the check-in is marked. The proof that went through in either database counts as this week’s lab proof, with your note on where the classical one needed excluded middle attached.