How many disproofs are needed to complete an implication graph?

Let $X$ be the set of our mathematical objects. To show that $P_4$ is not implied by all of them, we would like to find an example $x$ such that $\alpha(x) \land \neg P_4(x)$ where $\alpha$ is $P_1, P_2, P_3$. However, due to the implications you have proved, it's enough to show $x$ such that $P_1(x) \land \neg P_4(x)$, that is $P_1 \not\to P_4$.

Yet, this is not all, to show that $P_4$ is independent we also need to find $x$ such that $P_4(x) \land \neg \alpha(x)$. Observe that you also have proved $\neg P_3(x) \to \neg P_2(x)$ and $\neg P_2(x) \to \neg P_1(x)$ for all $x \in X$, so it's enough to find $x$ with $P_4(x) \land \neg P_3(x)$, i.e. $P_4 \not\to P_3$.

That might seem like all, but it's not. We are forgetting $P_2 \not\to P_1$ and $P_3 \not\to P_2$ and $P_3 \not\to P_1$. For these we need an $x$ such that $P_2(x) \land \neg P_1(x)$ and some different $x$ such that $P_3(x) \land \neg P_2(x)$.

As for whether such an algorithm exists, definitely yes: for all subsets of possible implications you can check if that subset is enough to prove status of every implication. Nevertheless, that would be rather slow, so now the question is, can we make it faster? My guess is yes, but currently I have no proof.

I hope this helps $\ddot\smile$

Edit: Thanks to @bof for spoting a flaw in the algorithm I suggested.

Edit 2:

Here is a second attempt at an algorithm. I will start with a change in terminology, so that it is more concrete, and thus perhaps simpler.

Let $V = \{1,2,3,\ldots,n\}$ be the set of vertices and add a directed edge $i \to j$ if $P_i \to P_j$. Furthermore, for each vertex $v \in V$ create sets $A_v = \{i \in V \mid P_i \to P_v\}$, in particular $v \in A_v$. These sets have the property that $$P_i \to P_j \iff A_i \subseteq A_j,$$ that is $$P_i \not\to P_j \iff A_i \not\subseteq A_j \iff \exists v \in V.\ v \in A_i \land v \notin A_j.$$

Moreover, let us say that $A_i$ is a successor of $A_j$ iff $A_j \subsetneq A_i$ and for all $k$ such that $A_j \subseteq A_k \subseteq A_i$ we have $k = j$ or $k = i$ (intuitively, $A_i$ is one step ahead of $A_j$). Similarly, $A_i$ is a predecessor of $A_j$ iff $A_j$ is a successor of $A_i$ (intuitively $A_i$ is one step before $A_j$).

The algorithm:

1. Let $D$ be the set of all the pairs that were not settled yet, i.e. $$D \gets \{ (i,j) \in V \times V\mid A_i \not\subseteq A_j \land A_j \not\subseteq A_i\}$$
2. Pick any such pair $$(i,j) \gets \operatorname{any}(D)$$ Observe that $i \in A_i$, but $i \notin A_j$. We will not try to find an alternate pair with similar property.
3. Let $i'$ be any predecessor of $i$ such that $i' \notin A_j$ or $i$ if no such predecessor exists and assign $i'$ to $i$ \begin{align} &i' \gets \operatorname{any}\{k\in \operatorname{pred}(i) \mid k \notin A_j \}\\ &\mathtt{if}\ i' \neq \bot:\\ &\quad i\gets i' \end{align}
4. Do similarly with $j$, i.e. find an appropriate successor: \begin{align} &j' \gets \operatorname{any}\{k\in \operatorname{succ}(j) \mid i \notin A_k \}\\ &\mathtt{if}\ j' \neq \bot:\\ &\quad j\gets j' \end{align}
5. Repeat steps $4$ or $5$ until no further change is possible.
6. Prove $P_i \not\to P_j$ (i.e., output that pair as one of those that we need to prove).
7. Remove from $D$ any pair that is implied by $P_i \not\to P_j$.
8. Repeat from step $2$ until $D$ gets empty.

A few important points:

• Because the graph is a DAG, steps 3 and 4 cannot repeat infinitely.

• If $(i,j) \in D$, then after steps $3$ and $4$ the new pair $(i,j)$ is still in $D$.

  • Suppose otherwise and let $(i',j')$ be the new pair. Please remember that $i' \in A_{i'} \subseteq A_i$ and $i' \notin A_{j'} \supseteq A_j$ because that is how that new pair was constructed. If $(i',j')\notin D$, then it had to be removed from $D$ at some point and there had to be a pair $(i'',j'')$ such that $i'' \in A_{i''} \subseteq A_{i'} \subseteq A_i$ and $i'' \notin A_{j''} \supseteq A_{j'} \supseteq A_j$, but that implies $(i,j) \notin D$.

• Thus, every time we get to step 7 at least one pair gets removed, so the algorithm finishes in finite time.

• When we finish step $5$, the pair $(i,j)$ has property that no statement $P_{i'} \not\to P_{j'}$ for some other pair $(i',j')$ could imply $P_i \not\to P_j$.
  • Suppose otherwise that there is such a pair $(i', j')$. That means $i' \in A_{i'} \subseteq A_i$ and $i' \notin A_{j'} \supseteq A_j$, but that implies step $5$ could not finish because $(i',j)$ or $(i,j')$ is a valid change.
• Therefore, every pair that the algorithm outputs has to be proven.
• As the algorithm finishes only when $D$ is empty, all necessary pairs will get printed.

I hope I didn't miss anything this time.

We may assume that equivalent statements have been identified, so that the relation of implication is antisymmetric as well as being reflexive and transitive, i.e., it's a partial order. Thus the problem may be stated as follows:

Let $V$ be a finite set partially ordered by a relation $R.$ What is the smallest set $D\subseteq(V\times V)\setminus R$ such that every transitive relation $T\subseteq V\times V,$ which contains $R$ and is disjoint from $D,$ is equal to $R?$

Clearly, any such set $D$ must contain any pair $(a,b)\in(V\times V)\setminus R$ such that $R\cup\{(a,b)\}$ is a transitive relation; otherwise $T=R\cup\{(a,b)\}$ would be a transitive relation containing $R$ and disjoint from $D$ and unequal to $R.$ Let $D_0$ be the set of all such pairs:

$$D_0=\{(a,b)\in(V\times V)\setminus R:R\cup\{(a,b)\}\text{ is transitive}\}.$$

I claim that $D_0$ is the desired set. Let $T\subseteq V\times V$ be a transitive relation such that $R\subseteq T$ and $T\cap D_0=\emptyset;$ I have to show that $T=R.$ Assume for a contradiction that $T\setminus R\ne\emptyset.$ Choose a minimal (with respect to the partial order $R$) element $a\in V$ such that $(a,y)\in T\setminus R$ for some $y,$ and then choose a maximul element $b\in V$ such that $(a,b)\in T\setminus R.$ It is easy to see that $R\cup\{(a,b)\}$ is transitive, whence $(a,b)\in D_0,$ contradiction our assumption that $T\cap D_0=\emptyset.$

In other words, writing $x\le y$ for $(x,y)\in R,$ we can describe $D_0$ as the set of ordered pairs $(a,b)\in(V\times V)$ satisfying the conditions:

$$a\not\le b$$ $$\forall x\in V\ (x\lt a\implies x\le b);$$ $$\forall x\in V\ (b\lt x\implies a\le x.$$

For $a\in V$ let $F(a)$ be the set of all maximal elements of $\{x:x\lt a\},$ and let $G(a)$ be the set of all minimal elements of $\{x:b\lt x\}.$ If we wish to compute $D_0,$ we might start by computing the sets $F(a)$ and $G(a)$ for each $a\in V;$ then, for each ordered pair $a\not\le b,$ we just have to check the inequalities $x\le b$ for $x\in F(a),$ and $a\le x$ for $x\in G(b).$

Example. If $V=\{v_0,v_1,v_2,v_3\}$ and $R=\{(v_0,v_0),(v_0,v_1),(v_1,v_1),(v_2,v_2),(v_2,v_3),(v_3,v_3)\},$ then $D_0=\{(v_0,v_3),(v_1,v_0),(v_2,v_1),(v_3,v_2)\}.$