Proving certain obvious tautologies in the calculus of constructions

Question

I'm trying to prove that $\lnot (\exists y : S.Py) \rightarrow \exists y : S. \lnot Py$ (let me know if the encoding of $\exists$ matters!). I don't have any good ideas about how to do that, but I've tried various subgoals that look promising, but they bring more questions than answers.

1. My first attempt is first proving $\lnot (\exists y : S.Py) \rightarrow \Pi y:S.\lnot Py$ (this is easy) and then proving $\Pi y:S.Py \rightarrow \exists y:S.Py$ (I probably don't care about negation for this lemma and it's useful in its full generality, so I dropped the $\lnot$). The second part turns out to be surprisingly hard, and I failed at that, since I need to present a real witness of the existence, which I cannot do without any prior knowledge about $S$. Is it possible to prove it?

2. Then, a different subgoal that would have helped me is to get $\bot$ from $\Pi x : S.P x$ and $\Pi x : S.\lnot P x$, but I failed here too. The best I could get is $\Pi x:S. \bot$, but I cannot reduce this to $\bot$ without some inhabitant of $S$ that I don't know a priori (and this also has a striking resemblance to the blocker on the first point!). Is this one provable too?

3. And, disregarding those two points, what's the best way to prove the original implication?

I'm working in the calculus of constructions, but I have "axiomatic" terms in my context that represent double-negation elimination or the law of excluded third, shall it only be provable in classical predicate logic.

Answer 1

1. No, it is not possible to prove this because if $S$ is the null set, then the hypothesis that $(\forall y \in S)(Py)$ will be true while the conclusion $(\exists y\in S)(Py)$ will be false since $S$ is not the null set.

However, let's say $S$ is not the null set. That is, we know of some $y_0$ such that $y_0\in S$. Then, how do we go about proving this conditional?

Well, first we use Universal Elimination to go from $(\forall y \in S)(Py)$ to $Py_0$. Then, we use Existential Introduction to go from $Py_0$ to $(\exists y\in S)(Py)$

2. No, this contradiction is also not provable because $(\forall y \in S)(Py)$ and $(\forall y\in S)(\neg Py)$ are not inherently contradictory statements: If $S$ is the null set, both of these statements are vacuously true.

However, again, let's say $S$ is not the null set. Given $y_0 \in S$, how do we derive a contradiction from these statements?

Well, use Universal Elimination on both universal statements to get $Py_0$ and $\neg Py_0$. Then, use Contradiction Introduction to derive $\bot$.

The original conditional is only true if $S$ is not the null set. Therefore, I think I answered 3 in my sidenote to 1.