Object support

[JoJoDeveloping]

Hi all,

I'm not sure this is an issue, more of a design question, but did you ever consider adding "object nodes" to your machine? While your machine supports quantifiers, scoping is managed in a non-local way. If one misplaces their quantifier introduction rules, the proof will seem to work, except for that certain objects don't unify. This can be hard to debug.

Instead, the quantifier rules could produce "object outputs" which are similarly to the currently existing blocks, except that they output an object instead of a proof. You could use some different color for them. And then, these are subject to the same well-formedness rules insofar as that e.g. the object produced by an exists-elimination must be used only in proofs where the proof that this object inhabits some property is used (we know how first-order logic works).

One would further, of course, need to add blocks for functions, and a block that produces an otherwise not further specified object to make usable the rule that the universe is not empty. As an upside, the proof structure would much more clearly show which objects are instantiated into which quantifiers.

It would certainly be a solution for #133

So, have you ever thought about doing this?

[nomeata]

Yes, I did consider this back then, I think. It should be possible, but having to construct all terms explicitly would become far too verbose in many cases.

I wonder if you can actually express that in the current code, which a custom logic (defined in a Yaml file), of you simply define the blocks with explicit input and outputs for the object level term.

I don't expect to actually work on this, but it's a nice thought to entertain here.

[mikeshulman]

I would really like a feature like this, and I might be willing to work on it (or have a student work on it) at some point. I'm using IPM for teaching an intro-to-proof course this semester and it was really helpful for the unit on propositional logic, but I felt that the version of predicate logic without "object wires" would be more confusing than helpful. So instead I introduced the rules with object-wires myself and am having the students draw graphical quantifier proofs on paper. Some specific thoughts:

1. Proofs of the sort that are currently in Session 6, with completely arbitrary predicate and domain, can't possibly have nontrivial "terms" or "functions" anyway: the only object inputs available are object outputs of some other quantifier rule. I'm scaling it up on paper to proofs about concrete domains like integers by allowing them to draw a single block labeled "algebra" and do the algebra below the diagram, but I think it would already be really helpful for the fully abstract term-less proofs to be doable in IPM.
2. There doesn't need to be any requirement that the object produced by an exists-elimination be used only in proofs where its property is also used. ($\exists x. P(X)$ implies $\exists x. \top$.)
3. In my humble opinion, requiring that the universe be nonempty is an archaism that can and should be dispensed with in modern logic. So $\forall x. P(x)$ should not imply $\exists x. P(x)$, and this is another reason that I didn't want to use the current IPM session on predicate logic with my students.

How pluggable is the backend? In principle, it would be neat if the graphical frontend could be plugged into, say, an already-extant full-featured dependently typed proof assistant, so that it would be essentially just a graphical syntax for writing terms that the proof assistant would typecheck.

[nomeata]

Great to see some activity around this!

The backend is a bit of Haskell code, and can likely be changed to implement different inference rules, or even fundamentally different logics. So if you can implement your logic with this interface:

incredible/logic/Entry.hs

Line 18 in aa18e04

incredibleLogic :: Context -> Proof -> Either String Analysis

Then yes, should be possible to replace.

The non-empty universe requirement is inherited from HOL. I assume you saw the paper http://dx.doi.org/10.1007/978-3-319-43144-4_8? But probably it isn't so deeply embedded in the idea of graphs… keep me posted!

[mikeshulman]

Yeah, I get that the version of HOL currently implemented does force the universe to be nonempty. I'm just saying that isn't an intrinsically desirable property, so if we have a different set of rules that doesn't force the universe to be nonempty, there's no reason to add nonemptiness as an extra rule as the OP suggested.