custom block fails unexpectedly

[rogpeppe]

I am almost certainly getting something wrong here, but ISTM that if one abstracts out a custom block from a correct proof, then builds the same proof with that custom block, that it should work. But that doesn't appear to be the case for me.

Here's an example. We start with a correct proof for (!x.P(x)->Q(x))->False => ?x.P(x)->False, with the blocks selected that we want to abstract out into a custom block (I am trying to see if it's possible to make a custom block encapsulating a particular instance of proof by contradiction). The "crown" block is a double-negative custom block.

Then with all the highlighted blocks removed and the custom block used instead (I've included an unwired-up instance of the custom block to show its generic connection types):

I'd expect this to work. What's wrong here?

[nomeata]

Custom blocks have certain restrictions, in particular in an higher-order context, that are sometimes hard to understand. It might also be a bug, of course…

I am a bit confused by the P₇ predicate of the custom block. It seems to come out of nowhere, and I wonder how that should be quantified (I built the Proof Machine a while ago, so I don’t remember all the details…)

Can you use the annotation block to create a custom block that has ⊥ instead of P₇? Does that fix the problem?