A formula like $\forall x \exists y(x+y=0)$ can be represented as a tree. Something like so:
--- 0
|
∀x -- ∃y -- =
| --- x
| |
--- +
|
--- y
What I'm looking for is software that can produce and edit such trees quickly and easily. Not something like LaTeX where you have to type first and see the compiled result later; rather, I'd like to be able to work "on the fly" with expression trees, editing the text that is displayed at different nodes, cut/copy/pasting subtrees, etc.
Is there any software around that can do this?
I am willing to pay for commercial software if that's what it takes.
Motivation.
The idea is to present a proof as a sequence of expression trees, displayed in the form of a slideshow. Let me explain.
Traditionally, proofs are written in the style of an essay, as a sequence of paragraphs involving imperatives like let, assume, suppose etc.
I'm interested in presenting such proofs in a more "algebraic" manner.
The idea is that just as we can prove a trigonometric identity (say) by repeatedly transforming it via a sequence of $\leftrightarrow$'s or $\leftarrow$'s until we end up at a statement that is already known to be true, similarly we can prove an entire theorem by repeatedly transforming it via a sequence of $\leftrightarrow$'s or $\leftarrow$'s until we end up with a trivially true statement.
There's two problems with this idea.
The first is that a single theorem may take up a lot of space to state, and the intermediate forms may be much larger than the original theorem. So you wouldn't want to be rewriting the same theorem again and again with tiny increments each step; this would be incredibly tedious. However this can be solved by presenting the proof on a computer as a slideshow; each slide could display a formal sentence that is a small perturbation of the sentence written on the previous slide, with annotations indicating what has changed.
The second problem is that the moment you formalize complicated theorems into (say) first-order logic (for ease of algebraic manipulation), you wind up with multiple-bracket nestings that are incredibly hard to follow. However, this can be solved by writing sentences not as strings, but rather as expression trees. Such a presentation allows arbitrary-complexity formulae with no need for brackets. This motivates my question.
Take a look at the Fōrmulæ project: http://www.formulae.org . If the edition of such these expressions is not currently supported, you can create it, because it is a collaborative, open source project.
Expressions can be edited on the fly, internally they are trees, and you can use cut/copy/paste subtrees, just as you want.
You can also write code for the transformation rules, if you want to create a theorem prover.
I am currently writing code for logical programming -in order to do something like what Prolog does-. If you are not a programmer I can help you with writing the code for your project.