qed
One of the primary attractions of Morse set theory is that it is formalised in an elegant notation devised by Morse. It is entirely formal to the extent that it is directly implementable on a computer while also allowing the 'user' serious notational freedom. So-called 'syntactic sugar' is easily definable in the language itself.
In Morse's book, he gives the following:
(If p then q ≡ (p → q))
((p implies q) ≡ (p → q))
((p ↔ q) ≡ ((p → q) ∧ (q → p)))
((p if and only if q) ≡ (p ↔ q))
These four definitions are all formal definitions in Morse's
language. (If p then (q implies r) if and only if (q implies (p
implies r)))
is as much a formal theorem as ((p → (q → r)) ↔
(q → (p → r)))
.
As a result, the syntactic structure of a formula is fundamentally
very simple: linear arrays of symbols, where symbols can be anything like
x
, If
or →
.
qed
has support for entering and displaying formulas in
Morse's notation using a modal interface that will be familiar to Vim
users.
In part, qed
is a proof assistant—a programme that
helps in writing and checking proofs. Unlike most proof assistants,
qed
is based on set theory rather than type theory.
Specifically, it implements a constructive version of the theory defined
by Morse's book 'A Theory of Sets', as described in the book 'Morse Set
Theory as a Foundation for Constructive Mathematics' by Alps and
Bridges.
As I have just recently started working on qed
, the proof
assistant is still a work in progress.
Constructive Morse set theory lends itself to programming in two different ways. Firstly, programs can be automatically extracted from constructive proofs. Secondly, there is a facility in the language itself to talk about the lambda calculus. I hope to explore both of these possibilities in the future.
As I have just recently started working on qed
, the work
on the programming facilities has not yet been started.
You can contact me about this project at miles.rout@pg.canterbury.ac.nz.
milesrout:qed
—The repository for this project