Existentials and propagation of associated variables

[thaumasiotes]

I've been working on session 6, problem 13 (given ∃x.∃y.P(x,y), show that ∃y.∃x.P(x,y). I feel like there's something about the ∃-related blocks that I don't understand, so this report will basically show a bunch of pictures and complain.

Here are two strategies, "top" and "bottom", that I've tried to make work. I believe they are logically equivalent:

On the bottom, I've derived P(c_7, c_8). I should be able to run that through the two instantiator blocks (8 and 7), and then through two existentializer blocks (e.g. 4 and 3), and have a complete proof. However, directly connecting the local output of block 8 to the local input of block 8 produces a skull-and-crossbones error:

This looks like a bug; it seems to me that Q_7 should unify with P(c_7, c_8), so that the ultimate output of this construction is P(c_7, c_8). I don't see how it can ever be incorrect to wire local output straight to local input.

On the top, I've tried a non-nested approach based on this pencil-and-paper proof:

1. ∃x.∃y.P(x,y) (given)
2. ∃y.P(m,y) (instantiate ∃x)
3. P(m,n) (instantiate ∃y)
4. ∃x.P(x,n) (existentialize m)
5. ∃y.∃x.P(x,y) (existentialize n)

The back-propagated input requirement shown above says that I need to provide input proving ∃x.∃x_1.P(y_4,y_3). #71 suggests that y_4 and y_3 are variables (not constants) which should unify as needed. So the provided input ∃x.∃y.P(x,y) should satisfy this requirement... but it doesn't:

What's happening in the propagation here? I agree that the local output of block 6, ∃y.P(c_6,y), is correct. But the rest looks wrong. The local input of block 6 should be ∃y.P(c_6,y) or equivalently ∃x.P(c_6,x). The non-local output of block 6 should be ∃x.P(c_6, x). The local output, local input, and non-local output of block 5 should be P(c_6, c_5). P(c_6,c_5) should satisfy the input requirement of block 4. Block 4's output should be ∃x.P(x,c_5).

Instead, the local input and output of block 6 are incorrectly stated to be mismatched, and the non-local output of block 6 is ∃x.P(y_4,y_3), which fails to bind y_3 to ∃x. This must be because the output is being propagated backward from later blocks. But if we disconnect the later blocks, we run into the same error we found in the bottom strategy:

And I can't even try to fix this with an annotation block specifying what I think Q_6 should be, because all symbols used in annotation blocks are constants and I can't input c_6.

[thaumasiotes]

Actually, on further thought, I don't see why the instantiator block has a local output and a local input at all. All it's supposed to do is conclude from ∃x.P(x) that P(c) for some c. Why isn't P(c) just non-local output from the block?

[rogpeppe]

I came here wondering about the same problem, and also raised #106 from my confusion.
Another issue that led me astray was the fact that you get a red line when making a perfectly valid connection:

Here's an actual solution that uses that line. I think that it would be nice if the hovering over a red line displays a tooltip saying what the issue is.

[nomeata]

Why isn't P(c) just non-local output from the block?

That would be unsound; the c must not “escape” the existential block, else you can prove false. I forgot the precise argument though…

[thaumasiotes]

That can't be true in general, because P(c) is a sound conclusion from ∃x.P(x). All it does is give a name, c, to the value that we know exists, and naming things will not prove a contradiction.

What's happening internally when a block puts out P(c)?

[thaumasiotes]

Here's a proof that (∀x.P(x))→⊥ proves ∃x.P(x)→⊥:

This proof uses a universalizing block to conclude from P(c_10) that ∀x.P(x). If you could do that with the output of an existential instantiator block, it would be an error.

But as far as I understand things, the conclusion shown in the proof is valid because c_10 originates from TND block 5, and was therefore chosen "without loss of generality". The preserved generality is what lets us generalize P(c_10) back to ∀x.P(x). A constant instantiated from an existential statement is not chosen without loss of generality.

Of course, in my model, it would make more sense for the value to be called c_5, after the block it comes from, rather than c_10 after the block that consumes it. So I suspect that the proof machine is thinking about things somewhat differently. And the proof-by-cases block connected to TND 5 really does need scoping; within the cases, c_10 has lost its generality.

[thaumasiotes]

(As a digression, I don't believe that proof is correct even though it's turned green. In order for that proof to work, I've just assumed that something exists. But ((∀x.P(x))→⊥) → (∃x.P(x)→⊥) is true regardless of whether anything exists, and the pictured proof doesn't show that. There should be a way to show that, if nothing exists, then ∀x.P(x) is true, which contradicts the premise that (∀x.P(x))→⊥.)

[nomeata]

Yes, the way the axioms are set up here only works for non-empty universes.

Did you have a look at the corresponding paper, in particular section 2.4?

In this formulation of predicate logic, the universe is unspecified, but not empty. In particular, it is valid to derive ∃x.P (x) from ∀x.P (x) (Fig. 12).

and

The asymmetry in Fig. 11 is striking, and the question arises why the elim-
ination block for the existential quantifier would not just produce P (c) as its
output, forming a proper dual to the universal quantifier introduction block. This
could work, but it would require the Incredible Proof Machine to intelligently
determine a scope for c; in particular it had to ensure that scopes nest properly.
With some scopes extending backwards (universal quantifier introduction) and
some forwards (existential quantifier elimination), automatically inferring sensible
and predictable scoping becomes tricky, so we chose to use a block shape that
makes the scope explicit. More on scopes in Section 3.2.