qed

Theory of Notation

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.

Example

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.

Demonstration

Proof assistant

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.

Programming Language

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.

`qed`