Smallest relation in complement of partial order that prohibits its extension Let $P$ be a partial order on a finite set $S$ (assume that every element is related to at least one other element besides itself…this raises a few quick questions: is this implied by the definition of partial order and if not, what are the "isolated" points called and what is a partial order with no such points called?) and $R$ be the smallest subset of $(S\times S)\setminus P$ such that for all partial orders $Q\supseteq P$, $$R\cap Q=\varnothing\implies P=Q.$$
Is the relation $R$ unique?  Does it have a name?  Is it equivalent to something else that does?
I asked a similar (perhaps the same) question in an unwieldy way on MSE at Minimal generating sub-relation of complement of partial order and got no response.
======= edit added by mathematrucker 16 Mar 2022 =======
While searching the literature unsuccessfully for @JosephVanName's nice "one pair extension property of finite partially ordered sets" below it occurred to me that it follows immediately from the fact that the poset under set containment of all unlabeled posets on $n$ points is graded by cardinality. This appears as Lemma 2.1 in New results from an algorithm for counting posets by Culberson and Rawlins (1990), which cites note (3.1) in Aigner, Producing posets (1981). Neither reference supplies a proof, so if anyone knows of one that does, please add it in the comments.
======= edit added by mathematrucker 23 Jul 2022 =======
The following 1988 precursor to Culberson and Rawlins's 1990 paper gives a proof of Lemma 2.1: On counting posets and the structure of the poset of posets. The authors call "isolated" points singletons and posets that have none are said to be in reduced form.
 A: I claim that the relation $R$ is in fact unique. The uniqueness follows from the one pair extension property of finite partially ordered sets.
Proposition: Suppose that $X$ is a finite set with partial ordering $P$. Then whenever $Q$ is a partial ordering on $X$ with $P\subseteq Q,P\neq Q$, there exists an ordered pair $(x,y)\in Q\setminus P$ such that $P\cup\{(x,y)\}$ is a partial ordering.
Proof: Suppose that $(x,y)\in Q\setminus P$. Then $x\not\leq_{P}y$ and
$y\not\leq_{P}x$. Let $x',y'$ be a pair such that
$x'\leq_{P}x,y\leq_{P}y'$, $x'\not\leq_{P}y'$, and
$$(x''\leq_{P}x',y'\leq_{P}y'')\implies(x''\leq_{P}y''\mbox{ or }x''=x',y''=y').$$
Let $T=P\cup\{(x',y')\}$. Note that since $y\leq y'$, $x'\leq x$, and $y\not\leq_{P}x$ we have $y'\not\leq_{P}x'$ and thus $(y',x')\not\in T$.
I claim that $T$ is a partial ordering. The ordering $T$ is clearly reflexive.
Suppose that $r\leq_{T}s,s\leq_{T}t$. If $(r,s),(s,t)\in P$, then $r\leq_{P}t$ by the transitivity of $P$. In the case that $(r,s)=(x',y')=(s,t)$, we have $r=s=t$, so $(r,t)\in T$ by reflexivity. Now, assume that $(r,s)=(x',y')$ and $s\leq_{P}t$.
Then either $r\leq_{P}t$ or $s=t$. In either case, $r\leq_{T}t$. If we assume $(s,t)=(x',y'),r\leq_{P}s$, then either $r=s$ which would imply that $r\leq_{T}t$ or we would have $r\leq_{P}t$ which would imply that $r\leq_{T}t$ as well. Therefore, $T$ is transitive.
Now, assume that $r\leq_{T}s\leq_{T}r$. If $(r,s)\neq(x',y')$ and $(s,r)\neq(x',y')$, then we know that $r\leq_{P}s\leq_{P}r$ which implies that $r=s$. On the other hand, we can assume without loss of generality that $(r,s)=(x',y')$. Since it was shown above that $y'\not\leq_{T}x'$ we conclude that $T$ is antisymmetric.
Hence $T$ is a partial ordering. Observe that $x'\leq_{Q}x\leq_{Q}y\leq_{Q}y'$, so $(x',y')\in Q$. Q.E.D.
Therefore, if we let $R$ be the collection of all ordered pairs $(x,y)\in X^{2}\setminus P$ where $P\cup\{(x,y)\}$ is a partial ordering, then if $Q$ is a partial ordering on $X$ with $P\subseteq Q$ and $Q\cap R=\varnothing$, then $Q=P$ (otherwise a new pair could be added to $R$, contradicting its definition).
