Dear Dusko, You've missed the point about the adjunctions: that the adjunction is between two different contexts. Constructively we have two Heyting algebras here: H() has formulae (modulo equivalence) with no free variables, H(b) has formulae with at most one free variable, namely b. The inclusion homomorphism H() -

H(b) has right and left adjoints given by universal and existential quantification.

The adjunction, or your proof, show that (all) a. P(a) --> (exists) x. P(x) is equivalent to true, or that (all) a. P(a) <= (exists) x. P (x), _in H(b)_. That's because it works by cutting P(b), which is present only in H(b). We should not conclude that it is equivalent to true in H(). The notation "(all) a. P(a) --> (exists) x. P(x)" conceals the difference, but it comes out clearly with a sequent calculus that keeps track of the possible free variables - see e.g. part C of the Elephant. With this notation you distinguish between, on the one hand, true |-(b) ((all) a. P(a) --> (exists) x. P(x)) or (all) a. P(a) |-(b) (exists) x. P(x) (both valid) and, on the other, true |-() ((all) a. P(a) --> (exists) x. P(x)) or (all) a. P(a) |-() (exists) x. P(x) (both not valid). All the best, Steve. On 23 Oct 2011, at 22:11, Dusko Pavlovic wrote:

...

variable a. To avoid the vacuity and get a falsehood you have to quantify out the free variable, as

((all) a. P(a)) --> ((exists) x. P(x))

here is a proof of this apparent falsehood:

(all) a. P(a) --> (all) b. P(b) (exists) b. P(b) --> (exists) x. P(x) -------------------------------- ------------------------------------- (all) a. P(a) --> P(b) P(b) --> (exists) x. P(x) ---------------------------------------------------------------------- ----------------- (all) a. P(a) --> (exists) x. P(x)

(it's is just adjunctions in foundations again: we compose the counit of the adjunction of one quantifier with the unit of the other one. note that it is valid constructively. i am not sure, but i think gentzen gave a different proof in an example.)

-- dusko

[For admin and other information see: http://www.mta.ca/~cat-dist/ ]