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; 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.

Theory Files

All theory files here predate the Oct 15 upgrade which reverses grouping of conjunction and disjunction. This can be fixed by replacing the current precedence declarations for propositional connectives by those found in a comment in the source.

Here is my own current implementation project, a development of Edmund Landau's classic Foundations of Analysis (in progress). This has been updated June 22 (and needs June 22 prover version to run correctly). The Automath group also implemented this book.

Here are some theorems of set theory (details of New Foundations might be or become relevant in this file). This file was extensively affected by the June 22 prover update: this is a new version which works with that update.

Here is the file with the axioms for Joanna Guild's development of elementary real analysis (this is not her file, but an adaptation of that file to the current prover version; also, this file has errors in it, but if you page through it you will get the axioms). See the following link for the full development.

Here is the directory with the files for Joanna Guild's Master's thesis project. This contains a proof of the theorem that every positive real number has a square root from the axioms of an ordered field. Unfortunately, the initial portions of this work were done under an old version of the prover and the resulting proofs have to be ported forward to the new version in the complicated way described in the "read me" file in the directory.

Here find a directory with files under construction by Nathan Bailey, a student who did a presentation on Marcel for the Undergraduate Research Conference at BSU in spring 2007. He is currently proving theorems from Ross's real analysis book (the Math 314 text).