Marcel: A Sequent Theorem Prover for New Foundations

This is the home page of Marcel, a system for computer-assisted reasoning in a sequent calculus equivalent to Jensen's set theory NFU (the version of Quine's New Foundations which allows urelements).

Don't be scared by the mention of set theory: the current applications of Marcel are mostly educational in the areas of propositional and first-order logic: some work has been done at the level of elementary real analysis which involves algebraic calculations and a little bit of set theory (at a level where which set theory is in use is not an issue).

We are grateful to Marcel Crabbé, who has graciously agreed to serve as godfather to the prover "as long as he doesn't have to give it any presents" (so I don't have to come up with a new name!). The details of the sequent calculus used here come from his paper on a semantic proof of cut-elimination for New Foundations without any axiom of extensionality.

Source and Documentation for Marcel

The source file for the ML version of Marcel is here. This has been updated Oct 15 2015 to the version of that date. The logic of this version is different from that which was used to run the Guild files, source for which is preserved in the Guild directory. Further, the Oct 15 upgrade reverses the grouping of conjunction and disjunction to left instead of right; the old precedence is preserved in a comment in the source if desired to run old save files, but it is clear pragmatically that left grouping is to be preferred.

Marcel is written in Moscow ML, an implementation of Standard ML which is free to download through the link given. Please note that this is version 2.01. I will eventually update to a newer version of Moscow ML.

There is also a version which runs under Poly/ML or Moscow ML 2.10.1, available on request.

Here is the manual, which does include a command reference. This is the version of Oct 15, 2015.

Here is the final draft of Joanna Guild’s thesis (included by permission, to be replaced by the final version when this comes out of the Graduate Office).

I am anticipating moving the focus of this work to the Python version described in the next subsection, but some advanced features are still only found in the ML version.

Python version

Here is a version of Marcel written in Python (version of Jan 25 2017, currently under constant development [writing Jan 26 2017]), and here is some documentation [the lab manual below is likely to be more current]. This version is somewhat different in philosophy and quite different in notation and behavior. I anticipate teaching using the Python version henceforth: here I provide a draft of my lab manual. This looks like a very long document, but it is not as long as it appears: sample Marcel output takes up a lot of space (enormously more space than the input which generates it). This document will eventually contain a full technical reference (including mathematical details).

I am planning to use the Python version as a vehicle for an implementation of Frege's Basic Laws of Arithmetic, expanding on an observation previously made by Nino Cocchiarella, that the logic of Frege can be completely salvaged by imposing stratification restrictions on the formation of concepts. I provide a link here to my latest notes on this subject (which recently had to be corrected as I discovered an error in the definition of ordered pair and projections by using my software; the mechanical implementation has already proved useful). The type mechanism of the Python version was in fact motivated by thinking about the problem of implementing Frege (it differs significantly from that of the ML version) and proves also to be significantly simpler to implement.

Try running Marcel on a web page This link opens the Python version of Marcel in a web page (via trinket.io; look it up!), using Marcel's internal shell, which now needs better documentation! Here are docs under construction for the web page/native interface version.