Black hole helper block needed

[mohrm]

I just wanted to export the rule "(P->False) -> (P->Q)". Here is the proof I came up with: failed-export.pdf There is one local hypothesis which is not used (in the outer proof by contradiction), unfortunately the export function considers this the input of the exported rule, whereas the real input (P->False) is not present.

Is this a bug or have I done something wrong? I suppose I could live with it if the exported block had the unused local assumption as additional input but

[nomeata]

Side remark: First note that annotations blocks don’t work well with rule export: When you annotate something, everything (“P” etc.) is a constant, so the generated block will have these as constants (and not free variables).

[nomeata]

Could you also paste the generated rule?

Also, screenshots are nicer than PDFs, as these display inline on GitHub. Just run "import /tmp/foo.png" for the quickest way to get a screenshot :-)

[mohrm]

Sorry, here you are:

[nomeata]

Isn’t that expected? All open ports are there, and correctly connected.

It seems to be rather a request for a “black hole block” with no output that consumes an input that you explicitly do not want to use. Unfortunately, I do not think you can build such a block already yourself, so it needs to go into the helper block section. And will look quite strange there... but I don’t see a better way.

[nomeata]

BTW, this block can be created more easily:

[mohrm]

ah fuck! Again, I did not get that local inputs can also be used globally :-) I hope, this is generally gettable...

You're right, it is expected.

[nomeata]

But there still is a need to be able to tell the system “when exporting a block, ignore this output”. E.g. when you want a “A∧B ==> A" block, isn’t there?

[nomeata]

Another instance where a black hole block might be useful:

[mohrm]

Ah okay, so you want to export this as custom block, but can't because the upper implication has an unused inner exit. Right?

[lohner]

I've implemented a black hole block on the JS side a while back. Just uploaded it here: lohner/incredible@c471575828c32cf4bba6c195c0dbded68fdad6d9 . Exporting a custom rule of the example above works on my machine. However I didn't analyse other implications of that for the logic/soundness etc.

[nomeata]

I am still hoping that there is a less intrusive way of implementing that.

What if custom blocks would only include outputs that are connected? (Either to some other block that is not selected, or with a dangling connection) This would also allow to define custom blocks that use a certain output internally and also provide it as an output to the outside?