nomeata
commented
5 months ago 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.
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?