hi steve, i am afraid that the "falsehood" (all) x.P(x) => (exists) x.P(x) is a *tautology* of predicate logic, in any topos, for any predicate P:A-->Prop, with or without the free variables hanging around. if it helps, think of P:A-->Prop as an A-indexed set of elements of the lattice Prop. then (all) x.P(x) is the meet of P, whereas (exists) x.P(x) is the join of P, and the tautology says the meet is lower than the join. or constructively, (all) x.P(x) is the product of the A-indexed family P(x) (exists)x.P(x) is the coproduct so that (all) x.P(x) -->P(a) is a projection, and P(a) --> (exists) x.P(x) is an injection.

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).

to prove these last two formulas, observe that from true |-(b) ((all) a. P(a) --> (exists) x. P(x)) we can derive true |-() (all) b. ((all) a. P(a) --> (exists) x. P(x)) now use the equivalence true |-() ((all) b. ((all) a. P(a) --> (exists) x. P(x))) <-> (((all) a. P(a) --> (exists) x. P(x))) to conclude that the RHS is true. -- dusko [For admin and other information see: http://www.mta.ca/~cat-dist/ ]