Eris

Interactive Proof Environment

Explorations in creating an direct manipulation logic tool

@prabros

Beginnings of creating a graphical logic environment where you can directly manipulate your proofs.

Semantic Zoom

17 August 2026

What if you could zoom through salient parts of your logical argumentation?

Zooming Logical Terms

Visualizes three levels of zoom on the logical terms. The first one shows the expression (P∧Q)∧(P∧R). In the second one, the middle ∧ is lifted as a common operation on containers with two terms (P∧Q) and (P∧R). In the third one, all the ∧s are lifted to visualize a container for (P∧Q), another for (P∧R), and both of them nested inside a big one with the operator ∧.

We will see this mechanism is in the context of a proof derivation shortly. For now, here are the various levels of detail of the logical terms.