I'm facing a (possibly simple) problem while proving a theorem.

I need to show that under several (true) assumptions, some element is not in a set. Such assumptions are all met and there is are lemmata that can be employed to reach the conclusion. The problem comes from the fact that the lemma for doing so must be applied an arbitrary number of times.

Lemma 1: $\forall x:\big(x\in X \iff P(x) \big)$

Lemma 2: $\forall x,y : (P(x) \land Q(y) \land x\neq y) \Rightarrow qq \neq x $

Lemma 3: $\forall x : P(x) \Rightarrow Q(x)$

Assumption: $\vert X\vert=k \land k\ge 2 %\big(\forall x\in X.P(x)\big)$

Desired result: $qq\not\in X$

What i tried so far:

Proof: Intuitively, it is easy to see that $qq\not\in X$ because I can choose two elements $a$ and $b$ of $X$ (they are distinct by definition), plug them in lemma 2, and get that $qq\neq a$. If we apply this idea $k$ times we get that $qq$ is not an element of $X$, hence it is not in $X$. $\Box$

When $k=2$ or bounded, this reasoning works.

The problem: $k$ is not known in advance and I can not mechanically apply Lemma 2 arbitrarily many times.

How can I prove this intuitive fact in a mechanical fashion? I've been (vaguely) suggested to employ a bijection but i still don't see how to do so.

  • $\begingroup$ Is the issue that $X$ might not be countable? Because induction will work for a finite or countably infinite $X$. (Whenever you notice "If we apply this idea $k$ times, it works", try induction.) $\endgroup$ Commented Aug 18, 2021 at 14:16
  • $\begingroup$ I will give it a try, perhaps it's simpler than i think. $\endgroup$
    – Chaos
    Commented Aug 18, 2021 at 19:21
  • $\begingroup$ In my domain of discourse $X$ is countable and finite. $\endgroup$
    – Chaos
    Commented Aug 18, 2021 at 20:28
  • $\begingroup$ @j_random_hacker Induction is not going to cut it. The inductive hyp. ceases to hold very quickly. $\endgroup$
    – Chaos
    Commented Aug 23, 2021 at 19:26
  • $\begingroup$ What is your inductive hypothesis, and what are your base case(s)? $\endgroup$ Commented Aug 24, 2021 at 2:27

1 Answer 1


I eventually proved the theorem in a mechanical fashion and I want to thank j_random_hacker for pointing out a proof sketch based on induction and correcting my wrong initial formal statement.

The actual (mechanical) solution did require the employment of an inductive predicate that allows the human prover to instantiate the inductive hypothesis to a set $X'$.

The employment of natural induction in a mechanized fashion seems to be insufficient for carrying out the proof. This specific problem is discussed further here: Induction examples in PVS, slide 23/61. A different solution suggested there is subtyping.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.