Estensione di una relazione d'ordine parziale ad una relazione d'ordine totale su un insieme finito

Lemma: sia $S$ un insieme qualsiasi, sia $\le$ una relazione d'ordine parziale sull'insieme $S$ e siano $a,b \in S$ due elementi non confrontabili tramite la relazione $\le$ (cioè tali che non valga nè $a \le b$ nè $b \le a$). Allora la relazione d'ordine parziale $\le$ si può estendere ad una relazione d'ordine parziale $\le'$ tale che $a \le' b$.

Teorema: sia $S$ un insieme finito e sia $\le$ una relazione d'ordine parziale sull'insieme $S$. Allora la relazione d'ordine parziale $\le$ si può estendere ad una relazione d'ordine totale $\bar \le$.

Supponiamo di aver già dimostrato il lemma e di volerlo utilizzare per dimostrare il teorema.
L'idea è abbastanza ovvia: partiamo dalla relazione d'ordine parziale $\le$, se questa relazione non è totale allora esistono due elementi $a,b \in S$ non confrontabili tramite la relazione $\le$, allora utilizziamo il lemma per estendere la relazione $\le$ ad una relazione $\le'$ tale che $a \le' b$, ripetiamo questo argomento finchè non otteniamo un ordine totale.
Ma come posso formalizzare questa semplice idea? In particolare, come posso mostrare che questo procedimento porta ad ottenere una relazione totale in un numero finito di passi?

Ancora il teorema di Szpjlrain? per un insieme generico, si tratta di usare sapientemente il lemma di Zorn. Per un insieme finito assai probabilmente non serve, perché l'induzione che estende \(\le\) (parziale) a \(\preceq\) (totale) è finita: \(\le\) è un insieme finito (è un sottoinsieme di \(S\times S\), che è finito), e la catena
\[(\_\le\_) \, := \, (\_\le^{(0)}\_) \kern.5em\subseteq\kern.5em (\_\le^{(1)}\_) \kern.5em\subseteq\kern.5em (\_\le^{(2)}\_) \kern.5em\subseteq\kern.5em \dots\] (notazione cursatissima!) che ti viene data dal lemma deve fermarsi in \(\preceq\).

A ogni passaggio aggiungi almeno (verosimilmente molti di più per conservare la relazione d'ordine) una coppia nella relazione e le coppie sono $|S|^2$, quindi hai anche una maggiorazione esplicita che ti dice che concludi in un numero finito di passaggi.

Il fatto che questo procedimento porta ad ottenere una relazione d'ordine totale in un numero finito di passi mi era chiaro, quello che chiedevo è come posso formalizzare questa dimostrazione, ovvero come la posso scrivere in maniera formale.

Ad esempio potrei scrivere:

Per il lemma una relazione d'ordine parziale $\le$ su $S$ in cui due elementi $a,b \in S$ non sono confrontabili tra loro può essere estesa ad una relazione d'ordine parziale $\le'$ su $S$ in cui $a \le' b$.
Se la relazione d'ordine parziale $\le'$ non è totale, essendo $S$ finito, si può ripetere l'argomento precedente fino ad ottenere una relazione d'ordine totale $\bar\le$ su $S$ che estende la relazione d'ordine parziale $\le$.

Avete qualche suggerimento per scriverla in maniera migliore?

@megas_archon: il teorema di Szpilrajn è la versione per insiemi qualsiasi, non richiede necessariamente il lemma di Zorn per essere dimostrato ma richiede comunque qualcosa in più di ZF. Ad ogni modo io non sono interessato a dimostrare il teorema di Szpilrajn ma solo la versione per insiemi finiti.

Ma te l'ho detto come formalizzare il fatto che finisci in un numero finito di passaggi.

Sia $S$ è l'insieme, \(R\subseteq S\times S\) una relazione d'ordine parziale su $S$, e \(H_0(R)\) l'insieme \(\{(x,y)\in S\times S\mid (x,y)\notin R, \, (y,x)\notin R\}\). Tutti gli insiemi in questione sono finiti, perché sono sottoinsiemi di \(S\times S\), che è finito.

Puoi quindi enumerare \(H = \{(x_1,y_1),\dots,(x_n,y_n)\}\). Ora considera \(R_1 = R\cup \{(x_1,y_1)\}\), fanne la chiusura transitiva \(R_1^+\). Se è un ordine totale, hai finito; altrimenti considera \(H_1(R):= H_0(R_1)\) definito come sopra, con la differenza che ora \(H_1(R)\) è strettamente più piccolo di $H$.

A ogni passo, se \(R_k^+\), definita in termini di \(R_k\), è totale, fermati, altrimenti vai avanti: al massimo ti serviranno tanti passi quant'era la cardinalità di $H_0(R)$.