Even simpler: P(a) --> (exists) x. P(x) is a theorem of the pure predicate calculus, which is "clearly" false in the empty universe when P is taken to be the identically true predicate.
i assume that even this pure predicate calculus defines its predicates over a set A as the maps A --> Prop, where Prop is the set truth values. is that right? then there is just one predicate P:A-->Prop if A=0 (empty). you may call this predicate identically true, or identically false if you like. do we also agree (with Gentzen) that a sequent (exists x). Q(x,y)=>R(y) gives a sequent Q(x,y)=>R(y)? (tacitly, R gets a dummy variable x in this second sequent.) if we agree with this, then for the predicate P:0-->Prop the identity sequent (exists) a. P(a) => (exists) x. P(x) gives the sequent P(a)=> (exists) x. P(x) this is not so unintuitive if you realize that (exists) x. P(x) in this sequent must be a predicate over 0, in order to be compared with the truth value of the predicate P(a) over 0. but there is just one predicate over 0, so these two predicates must be equal. maybe it's time that we all recall lawvere's "Adjunctions in foundations", that appeared some 35 years ago. in its best times, categorical logic offered powerful tools to expand our logical intuitions. -- dusko [For admin and other information see: http://www.mta.ca/~cat-dist/ ]