Definizioni per ricorsione
\( \newcommand{\val}[1]{[\![{#1}]\!]} \)Uso le notazioni di H. B. Enderton, A Mathematical Introduction to Logic.
Sia \( U \) un insieme. Sia \( B\subset U \) un sottoinsieme di "elementi di base". Siano \( f\colon U\times U\to U \) e \( g\colon U\to U \) due funzioni. Sia \( C \) il più piccolo insieme \( B \)-induttivo rispetto alle funzioni \( f \) e \( g \); in altre parole, \( C \) è l'intersezione di tutti i sottoinsiemi \( S\subset U \) tali che \( B\subset S \) e tali che per ogni \( s_1,s_2\in S \) valga \( f(s_1,s_2)\in S \) e \( g(s_1)\in S \).
C'è un teorema di teoria degli insiemi (?) che afferma in soldoni che, se ho un modo \( h \) per assegnare un valore \( h(b) \) (in un qualche insieme \( V \)) a ogni \( b\in B \), un valore \( h(f(x,y)) \) ogni volta che conosco \( h(x) \) e \( h(y) \), e un valore \( h(g(x)) \) ogni volta che conosco \( h(x) \), allora ho un modo coerente per assegnare un valore \( h(x) \) a tutti gli \( x\in C \), a patto che \( C \) verifichi certe condizioni. Il claim preciso c'è sull'Enderton.
Le condizioni delle quali parlo sopra sono le seguenti: 1) le restrizioni \( f{\restriction_{C\times C}} \) e \( g{\restriction_C} \) devono essere iniettive; 2) l'immagine di \( f{\restriction_{C\times C}} \), l'immagine di \( g{\restriction_C} \) e l'insieme \( B \) devono essere insiemi a due a due disgiunti.
Non mi è molto chiaro che cosa affermano queste due richieste, e sto cercando un po' di esempi dove se ne fa cadere qualcuna e succede il disastro.
La lore di tutto ciò è ovviamente questa, comunque. Se prendo un insieme \( L = \{(,),\lnot,\land,\lor,\rightarrow,\leftrightarrow,p_1,p_2,\dots\} \) di simboli (il "linguaggio"), voglio estendere una funzione \( v\colon \{p_1,p_2,\dots\}\to \{0,1\} \) a una funzione \( \val{-}\colon \mathsf{Frm}_L\to \{0,1\} \) definita su tutto l'insieme \( \mathsf{Frm}_L \) delle "formule" su \( L \) definito induttivamente allo stesso modo di sopra, in maniera ad esempio che
\[
\begin{aligned}
\val{\phi\land\psi} &= \min\{\val\phi,\val\psi\}\\
\val{\phi\lor\psi} &= \max\{\val\phi,\val\psi\}
\end{aligned}
\] per ogni \( \phi,\psi\in \mathsf{Frm}_L \), eccetera.
Sia \( U \) un insieme. Sia \( B\subset U \) un sottoinsieme di "elementi di base". Siano \( f\colon U\times U\to U \) e \( g\colon U\to U \) due funzioni. Sia \( C \) il più piccolo insieme \( B \)-induttivo rispetto alle funzioni \( f \) e \( g \); in altre parole, \( C \) è l'intersezione di tutti i sottoinsiemi \( S\subset U \) tali che \( B\subset S \) e tali che per ogni \( s_1,s_2\in S \) valga \( f(s_1,s_2)\in S \) e \( g(s_1)\in S \).
C'è un teorema di teoria degli insiemi (?) che afferma in soldoni che, se ho un modo \( h \) per assegnare un valore \( h(b) \) (in un qualche insieme \( V \)) a ogni \( b\in B \), un valore \( h(f(x,y)) \) ogni volta che conosco \( h(x) \) e \( h(y) \), e un valore \( h(g(x)) \) ogni volta che conosco \( h(x) \), allora ho un modo coerente per assegnare un valore \( h(x) \) a tutti gli \( x\in C \), a patto che \( C \) verifichi certe condizioni. Il claim preciso c'è sull'Enderton.
Le condizioni delle quali parlo sopra sono le seguenti: 1) le restrizioni \( f{\restriction_{C\times C}} \) e \( g{\restriction_C} \) devono essere iniettive; 2) l'immagine di \( f{\restriction_{C\times C}} \), l'immagine di \( g{\restriction_C} \) e l'insieme \( B \) devono essere insiemi a due a due disgiunti.
Non mi è molto chiaro che cosa affermano queste due richieste, e sto cercando un po' di esempi dove se ne fa cadere qualcuna e succede il disastro.
La lore di tutto ciò è ovviamente questa, comunque. Se prendo un insieme \( L = \{(,),\lnot,\land,\lor,\rightarrow,\leftrightarrow,p_1,p_2,\dots\} \) di simboli (il "linguaggio"), voglio estendere una funzione \( v\colon \{p_1,p_2,\dots\}\to \{0,1\} \) a una funzione \( \val{-}\colon \mathsf{Frm}_L\to \{0,1\} \) definita su tutto l'insieme \( \mathsf{Frm}_L \) delle "formule" su \( L \) definito induttivamente allo stesso modo di sopra, in maniera ad esempio che
\[
\begin{aligned}
\val{\phi\land\psi} &= \min\{\val\phi,\val\psi\}\\
\val{\phi\lor\psi} &= \max\{\val\phi,\val\psi\}
\end{aligned}
\] per ogni \( \phi,\psi\in \mathsf{Frm}_L \), eccetera.
Risposte
Mi sembra che un caso particolare di questa costruzione quando $g$ è la funzione successore sugli ordinali alla von Neumann costruisca \(\mathbb N\). Però devi essere più preciso a proposito delle condizioni su $C$, del "modo coerente" di costruire \(h(f(x,y))\) a partire da \(hx, hy\), e su tutto il resto...
Ovviamente quello che stai facendo è restringere il monoide libero su $L$ a un sottoinsieme delle "parole che raggiungi ricorsivamente applicando $f,g$"; ma a questo punto perché solo $f,g$? Perché non includi le costanti? Perché non includi funzioni di arietà più alta?
Ovviamente quello che stai facendo è restringere il monoide libero su $L$ a un sottoinsieme delle "parole che raggiungi ricorsivamente applicando $f,g$"; ma a questo punto perché solo $f,g$? Perché non includi le costanti? Perché non includi funzioni di arietà più alta?
"megas_archon":Ti rispondo da qua; se i termini che uso non sono chiari in caso dimmelo. L'Enderton vuole usare questo fatto per mostrare che per definire una valutazione sull'insieme delle formule su un linguaggio è sufficiente definire una funzione sulle formule atomiche (cioè, sui simboli di proposizione). Il prof. in classe questo lo ha skippato e quindi volevo dimostrarlo io. In più stiamo studiando il sistema della logica proposizionale alla Hilbert \( \mathsf H_1 \), che ha solo i due connettivi \( \lnot \) e \( \rightarrow \).
Perché non includi funzioni di arietà più alta?
Quindi la risposta è "perché non mi servono".
"megas_archon":Il claim preciso è questo. Prendi un insieme \( U \) e un suo sottoinsieme \( B\subset U \). Prendi due funzioni \( f\colon U\times U\to U \) e \( g\colon U\to U \), tali che valgano le
devi essere più preciso a proposito delle condizioni su C
1) le restrizioni \( f{\restriction_{C\times C}} \) e \( g{\restriction_C} \) [sono] iniettive; 2) l'immagine di \( f{\restriction_{C\times C}} \), l'immagine di \( g{\restriction_C} \) e l'insieme \( B \) [sono] insiemi a due a due disgiunti.Allora, se \( V \) è un insieme e \( F\colon V\times V\to V \) e \( G\colon V\to V \) sono funzioni, data una funzione \( h\colon B\to V \) esiste un'unica funzione \( \bar h\colon C\to V \) tale che \( \bar h{\restriction_B} = h \) e tale che
\[
\begin{aligned}
\bar h(f(x,y)) &= F(\bar h(x),\bar h(y))\\
\bar h(g(x)) &= G(\bar h(x))
\end{aligned}
\], per ogni \( x,y\in C \) dove \( C \) è come prima l'intersezione di tutti i sottoinsiemi di \( U \) che contengono \( B \) e sono chiusi per \( f \) e \( g \).
La domanda mia era: perché mi servono per forza le condizioni 1) e 2) in quote? Sì, perché sennò il teorema non lo dimostro, però speravo di farmi un'idea migliore.
Sono andato a vedere che cosa dice Enderton, e mi sembra estremamente chiaro nel dare un'intuizione a proposito di "a cosa servono" quelle due condizioni:
Se vuoi una spiegazione un po' più ad alto livello, anche il paragone coi gruppi liberi è abbastanza illuminante: ogni omomorfismo di gruppi \(f : G\to H\) è determinato dall'immagine sui generatori di $G$ quando $G$ è liberamente generato; altrimenti, se ci sono delle relazioni sui generatori, $f$ deve essere "compatibile" con esse, ovvero contenere la congruenza che quelle relazioni determinano. (E questa è semplicemente una maniera, in algebra astratta, di asserire che la proprietà universale del quoziente per una congruenza, di solito chiamata "primo teorema di isomorfismo" e la proprietà universale di un gruppo libero convergono nel caso limite in cui $G$ è libero, e ogni funzione sui generatori estende a un unico omomorfismo di gruppi perché non ci sono relazioni non banali con cui $f$ deve essere compatibile per definire un omomorfismo.
Un eco di questo fenomeno si apprezza anche nel "primo teorema di isomorfismo per insiemi": data una funzione \(f : A\to B\) essa induce un'unica funzione \(A/R_f \to B\) sul quoziente di $A$ per la relazione di equivalenza generata da $f$ ($(a,a')\in R_f$ se e solo se $fa = fa'$), e questa funzione è sempre iniettiva.
Nel tuo caso quello che sta succedendo è che hai preso un insieme \(B\subseteq U\) e hai generato un insieme $C$ che è la "chiusura" di $B$ rispetto alle operazioni $f,g$: del resto, mi sembra una fatica di poco superiore definire, per una generica famiglia di funzioni \(\mathcal F = \{f_\lambda : U^{n_\lambda} \to U\}\) l'insieme \(\langle B \mid \mathcal F\rangle\) nella stessa maniera ricorsiva, definendo \(C_0 := B\), \(C_{n+1} := \bigcup_{f_\lambda} \{f_\lambda(x)\mid x\in C_n\}\) e \(C_\alpha = \bigcup_{\nu<\alpha} C_\alpha\) per un ordinale limite. (La mia impressione ora è che questa costruzione converga al primo ordinale limite dopo la cardinalità di \(\mathcal F\); se ha due elementi, \(C_\alpha = C_\omega\) per ogni \(\alpha > \omega\).
A questo punto sarebbe molto bello dire che una funzione definita su \(C=C_\omega\) è univocamente determinata dal dato di \(h, F,G\) (uso le notazioni del libro), o per meglio dire, che ogni terna \(h,F,G\) determina un'unica estensione \(h^\star : C\to V\) nel diagramma
\[\begin{CD}
B @>h>> V \\
@VjVV @| \\
C @>>h^\star> V
\end{CD}\] Ora però supponi che le condizioni di cui vuoi capire l'origine non siano verificate: ti trovi nell'imbarazzante situazione in cui siccome le immagini di $f,g$ ristrette a $C$ hanno intersezione non banale, esiste un \(x\in C\) tale che \(f(a,b)=x=g(t)\); a questo punto, non sai se usare la regola ricorsiva \(h^\star(x)=f(h^\star a,h^\star b)\) oppure la regola \(h^\star(x)= g(h^\star(t))\), perché questi due valori a priori sono diversi! Quindi, a queste ipotesi, \(h^\star\) non è una funzione (non è single-valued).
Ed è esattamente la stessa cosa che succede per i gruppi, solo che in quel caso la ricchezza della struttura permette di enunciare il primo teorema di isomorfismo in maniera più streamlined; incidentalmente questo è il motivo per cui la teoria dei gruppi si impara immediatamente e quella dei monoidi, che sono strutture piu semplici (meno operazioni, meno proprietà) no: per i monoidi il teorema di isomorfismo esiste ma enunciarlo "giusto" è più complicato (per farla breve, perché il nucleo di un omomorfismo di monoidi non dice tutto quello che vorresti a proposito dell'omomorfismo stesso).
Allora, alla fine, come eviti questo problema? Nei gruppi, dicendo che ogni funzione compatibile con la congruenza che presenta $G$ come quoziente di un libero si estende unicamente blabla. Qui, con le ipotesi di questo teorema. Se quindi vuoi una spiegazione analogica del motivo per cui le ipotesi sono là, a parte "perché altrimenti il teorema non lo dimostri", penso sia questa.
Ora, se vuoi una spiegazione ad ancora più alto livello, l'insieme dei numeri naturali è induttivo in quel senso, perché è eattamente \(\langle \{0\} \mid \text{s} \rangle\) quando \(\mathcal F\) contiene come unica funzione la funzione successore \(\text{s} : y\mapsto y + 1\) definita sull'"universo" $U$ dato dagli ordinali alla Von Neumann. Questo insieme ovviamente rispetta le ipotesi del tuo teorema, e infatti il teorema di ricorsione in questo caso diventa la proprietà universale dell'oggetto dei numeri naturali in \(\sf Set\): ogni endofunzione \(f : X \to X\) di un insieme $X$ in sé definisce un "sistema dinamico discreto" \(u : \mathbb N \to X\) a partire dalla condizione iniziale \(x_0\), "per ricorsione" dicendo che \(u_0 = x_0\) e \(u_{n+1} = u(\text{s}(n)) = f(x_n)\). Detta altrimenti, \(\mathbb N\) è l'oggetto iniziale di \(\sf Dyn\) click.
Ora, supponi di avere più funzioni \(f_\lambda\) (facciamo che sono sempre definite sulla gerarchia degli ordinali perché non ho fantasia); è assai probabile che anche qui tu stia cercando di costruire un oggetto iniziale in una categoria \({\sf Dyn}(\mathcal F)\), ma che questo non esista se le ipotesi del teorema di ricorsione non sono verificate. Chiaramente lascio a te definire questa roba, se proprio vuoi farlo, e controllare come è effettivamente fatto l'oggetto iniziale di \({\sf Dyn}(\mathcal F)\)...
If the content of the recursion theorem is not immediately apparent, try looking at it chromatically.
Se vuoi una spiegazione un po' più ad alto livello, anche il paragone coi gruppi liberi è abbastanza illuminante: ogni omomorfismo di gruppi \(f : G\to H\) è determinato dall'immagine sui generatori di $G$ quando $G$ è liberamente generato; altrimenti, se ci sono delle relazioni sui generatori, $f$ deve essere "compatibile" con esse, ovvero contenere la congruenza che quelle relazioni determinano. (E questa è semplicemente una maniera, in algebra astratta, di asserire che la proprietà universale del quoziente per una congruenza, di solito chiamata "primo teorema di isomorfismo" e la proprietà universale di un gruppo libero convergono nel caso limite in cui $G$ è libero, e ogni funzione sui generatori estende a un unico omomorfismo di gruppi perché non ci sono relazioni non banali con cui $f$ deve essere compatibile per definire un omomorfismo.
Un eco di questo fenomeno si apprezza anche nel "primo teorema di isomorfismo per insiemi": data una funzione \(f : A\to B\) essa induce un'unica funzione \(A/R_f \to B\) sul quoziente di $A$ per la relazione di equivalenza generata da $f$ ($(a,a')\in R_f$ se e solo se $fa = fa'$), e questa funzione è sempre iniettiva.
Nel tuo caso quello che sta succedendo è che hai preso un insieme \(B\subseteq U\) e hai generato un insieme $C$ che è la "chiusura" di $B$ rispetto alle operazioni $f,g$: del resto, mi sembra una fatica di poco superiore definire, per una generica famiglia di funzioni \(\mathcal F = \{f_\lambda : U^{n_\lambda} \to U\}\) l'insieme \(\langle B \mid \mathcal F\rangle\) nella stessa maniera ricorsiva, definendo \(C_0 := B\), \(C_{n+1} := \bigcup_{f_\lambda} \{f_\lambda(x)\mid x\in C_n\}\) e \(C_\alpha = \bigcup_{\nu<\alpha} C_\alpha\) per un ordinale limite. (La mia impressione ora è che questa costruzione converga al primo ordinale limite dopo la cardinalità di \(\mathcal F\); se ha due elementi, \(C_\alpha = C_\omega\) per ogni \(\alpha > \omega\).
A questo punto sarebbe molto bello dire che una funzione definita su \(C=C_\omega\) è univocamente determinata dal dato di \(h, F,G\) (uso le notazioni del libro), o per meglio dire, che ogni terna \(h,F,G\) determina un'unica estensione \(h^\star : C\to V\) nel diagramma
\[\begin{CD}
B @>h>> V \\
@VjVV @| \\
C @>>h^\star> V
\end{CD}\] Ora però supponi che le condizioni di cui vuoi capire l'origine non siano verificate: ti trovi nell'imbarazzante situazione in cui siccome le immagini di $f,g$ ristrette a $C$ hanno intersezione non banale, esiste un \(x\in C\) tale che \(f(a,b)=x=g(t)\); a questo punto, non sai se usare la regola ricorsiva \(h^\star(x)=f(h^\star a,h^\star b)\) oppure la regola \(h^\star(x)= g(h^\star(t))\), perché questi due valori a priori sono diversi! Quindi, a queste ipotesi, \(h^\star\) non è una funzione (non è single-valued).
Ed è esattamente la stessa cosa che succede per i gruppi, solo che in quel caso la ricchezza della struttura permette di enunciare il primo teorema di isomorfismo in maniera più streamlined; incidentalmente questo è il motivo per cui la teoria dei gruppi si impara immediatamente e quella dei monoidi, che sono strutture piu semplici (meno operazioni, meno proprietà) no: per i monoidi il teorema di isomorfismo esiste ma enunciarlo "giusto" è più complicato (per farla breve, perché il nucleo di un omomorfismo di monoidi non dice tutto quello che vorresti a proposito dell'omomorfismo stesso).
Allora, alla fine, come eviti questo problema? Nei gruppi, dicendo che ogni funzione compatibile con la congruenza che presenta $G$ come quoziente di un libero si estende unicamente blabla. Qui, con le ipotesi di questo teorema. Se quindi vuoi una spiegazione analogica del motivo per cui le ipotesi sono là, a parte "perché altrimenti il teorema non lo dimostri", penso sia questa.
Ora, se vuoi una spiegazione ad ancora più alto livello, l'insieme dei numeri naturali è induttivo in quel senso, perché è eattamente \(\langle \{0\} \mid \text{s} \rangle\) quando \(\mathcal F\) contiene come unica funzione la funzione successore \(\text{s} : y\mapsto y + 1\) definita sull'"universo" $U$ dato dagli ordinali alla Von Neumann. Questo insieme ovviamente rispetta le ipotesi del tuo teorema, e infatti il teorema di ricorsione in questo caso diventa la proprietà universale dell'oggetto dei numeri naturali in \(\sf Set\): ogni endofunzione \(f : X \to X\) di un insieme $X$ in sé definisce un "sistema dinamico discreto" \(u : \mathbb N \to X\) a partire dalla condizione iniziale \(x_0\), "per ricorsione" dicendo che \(u_0 = x_0\) e \(u_{n+1} = u(\text{s}(n)) = f(x_n)\). Detta altrimenti, \(\mathbb N\) è l'oggetto iniziale di \(\sf Dyn\) click.
Ora, supponi di avere più funzioni \(f_\lambda\) (facciamo che sono sempre definite sulla gerarchia degli ordinali perché non ho fantasia); è assai probabile che anche qui tu stia cercando di costruire un oggetto iniziale in una categoria \({\sf Dyn}(\mathcal F)\), ma che questo non esista se le ipotesi del teorema di ricorsione non sono verificate. Chiaramente lascio a te definire questa roba, se proprio vuoi farlo, e controllare come è effettivamente fatto l'oggetto iniziale di \({\sf Dyn}(\mathcal F)\)...
Ok, ci ho pensato un po' su stanotte e mi sembra che uno possa giustificare le condizioni di esistenza dell'estensione \[\begin{CD}
B @>h>> V \\
@VjVV @| \\
C @>>h^\star> V
\end{CD}\] guardandole come una condizione di fascio; mi sembra che sia vero un teorema di ricorsione più generale, dove le varie operazioni in \(\mathcal F\) formano una matching family; quando hanno immagini a due a due disgiunte questa condizione è banalmente verificata.
Partiamo dall'inizio: prendi un insieme \(U\) e una famiglia \(\mathcal F=\{f_\lambda : U^{n_\lambda}\to U\}\) di funzioni di varia arietà; adesso considera quello che nel messaggio precedente chiamavo \(\langle B\mid\{f_\lambda\}\rangle\) come la chiusura \(\mathcal F\)-induttiva di \(B\), cioè come il colimite rispetto a questa costruzione: \[\begin{cases}C_0 := B \\ C_{n+1} := \bigcup_{f_\lambda} \{f_\lambda(x)\mid x\in C_n\} \cup C_n \\ C_\alpha = \bigcup_{\mu < \alpha} C_\mu\end{cases}\] (l'ultimo è il caso di un ordinale limite). Chiaramente \(\{C_i\mid i\in {\sf Ord}\}\) è una catena, cioè \(C_0\subseteq C_1\subseteq C_2\subseteq\cdots\). Poi, ti viene data una famiglia \(F_\lambda : V^{n_\lambda} \to V\) da usare per la definizione ricorsiva di una estensione di \(h : B\to V\) a \(h^* : C \to V\).
Quel che vuoi è una condizione affinché questo problema di estensione transfinito abbia soluzione: \[\begin{CD}
C_0 = B @>h>> V \\
@VVV @| \\
C_1 @>>h^*_1> V\\
@VVV @| \\
C_2 @>>h^*_2> V\\
@VVV @| \\
C_3 @>>h^*_3> V\\
@VVV @| \\
\end{CD}\] in maniera tale da estendere via via \(h\) a un sovrainsieme di \(B\) sempre più largo avendo poi modo di beccare tutto \(C\). Del resto questo è il classico problema di estensione della sezione di un fascio a un insieme massimale di definizione, che si basa su una puntina di lemma di Zorn per trovare \(h^* : C \to V\) (hai certamente visto il teorema che costruisce la soluzione massimale di una ODE cazzimazzi; quello è un risultato di teoria dei fasci).
In questo caso per te il (pre)fascio è \({\sf Set}(j(-), V)\), dove \(j : \mathcal{P}_{\supseteq B}(U)\to {\sf Set}\) è la restrizione all'insieme delle parti di \(U\) che contengono \(B\), ma di questo ti importa relativamente, quello che vuoi ora è sfruttare la condizione che dice che questo prefascio (che è sempre separato, per il principio di estensionalità delle funzioni...) è un fascio, ossia che ogni matching family di sue sezioni ammette un'estensione (necessariamente unica).
Ricorda che se \(L : (Q,\le) \to {\sf Set}\) è un prefascio, la condizione di cui parlo afferma che per ogni elemento \(q\) di \(Q\) e ogni suo ricoprimento \(p_i\), data una famiglia \(s_i \in L(p_i)\) con la proprietà che \(s|_{p_i\land p_j} = s_j|_{p_i\land p_j}\), si riesce sempre a trovare una sezione \(s\in L(q)\) con la proprietà che \(s|_{p_i}=s_i\) per ogni \(i\in I\).
Le condizioni di Enderton sono una versione semplificata della condizione di fascio per \({\sf Set}(j(-), V)\), dove la condizione di essere una matching family è stata resa vacuamente vera dall'ipotesi che le immagini delle varie \(f_\lambda\) ristrette a \(C\) siano tutte disgiunte: se lo sono, non esiste precondizione di matching ed esiste sempre una estensione. Nel tuo caso, e nelle notazioni di sopra, \({\sf Set}(j(-), V)=L\), l'elemento che vuoi ricoprire è \(C\), e il ricoprimento su cui usi la condizione di fascio è la catena dei \(C_i\).
All in all questo ti dice non solo che il teorema di ricorsione di Enderton è vero, ma che è vero in condizioni un po' più generali, perché l'estensione esiste non solo quando lo vuole Enderton ma anche quando "dove sono definite, le \(f_\lambda\) coincidono". Questo evita l'imbarazzo che hai quando \(x = f_\lambda(u) = f_\mu(v)\) non sai se usare \(F_\lambda(h^*u)\) o \(F_\mu(h^*v)\) per calcolare \(h^*(x)\), perché questi sono gli stessi valori.
B @>h>> V \\
@VjVV @| \\
C @>>h^\star> V
\end{CD}\] guardandole come una condizione di fascio; mi sembra che sia vero un teorema di ricorsione più generale, dove le varie operazioni in \(\mathcal F\) formano una matching family; quando hanno immagini a due a due disgiunte questa condizione è banalmente verificata.
Partiamo dall'inizio: prendi un insieme \(U\) e una famiglia \(\mathcal F=\{f_\lambda : U^{n_\lambda}\to U\}\) di funzioni di varia arietà; adesso considera quello che nel messaggio precedente chiamavo \(\langle B\mid\{f_\lambda\}\rangle\) come la chiusura \(\mathcal F\)-induttiva di \(B\), cioè come il colimite rispetto a questa costruzione: \[\begin{cases}C_0 := B \\ C_{n+1} := \bigcup_{f_\lambda} \{f_\lambda(x)\mid x\in C_n\} \cup C_n \\ C_\alpha = \bigcup_{\mu < \alpha} C_\mu\end{cases}\] (l'ultimo è il caso di un ordinale limite). Chiaramente \(\{C_i\mid i\in {\sf Ord}\}\) è una catena, cioè \(C_0\subseteq C_1\subseteq C_2\subseteq\cdots\). Poi, ti viene data una famiglia \(F_\lambda : V^{n_\lambda} \to V\) da usare per la definizione ricorsiva di una estensione di \(h : B\to V\) a \(h^* : C \to V\).
Quel che vuoi è una condizione affinché questo problema di estensione transfinito abbia soluzione: \[\begin{CD}
C_0 = B @>h>> V \\
@VVV @| \\
C_1 @>>h^*_1> V\\
@VVV @| \\
C_2 @>>h^*_2> V\\
@VVV @| \\
C_3 @>>h^*_3> V\\
@VVV @| \\
\end{CD}\] in maniera tale da estendere via via \(h\) a un sovrainsieme di \(B\) sempre più largo avendo poi modo di beccare tutto \(C\). Del resto questo è il classico problema di estensione della sezione di un fascio a un insieme massimale di definizione, che si basa su una puntina di lemma di Zorn per trovare \(h^* : C \to V\) (hai certamente visto il teorema che costruisce la soluzione massimale di una ODE cazzimazzi; quello è un risultato di teoria dei fasci).
In questo caso per te il (pre)fascio è \({\sf Set}(j(-), V)\), dove \(j : \mathcal{P}_{\supseteq B}(U)\to {\sf Set}\) è la restrizione all'insieme delle parti di \(U\) che contengono \(B\), ma di questo ti importa relativamente, quello che vuoi ora è sfruttare la condizione che dice che questo prefascio (che è sempre separato, per il principio di estensionalità delle funzioni...) è un fascio, ossia che ogni matching family di sue sezioni ammette un'estensione (necessariamente unica).
Ricorda che se \(L : (Q,\le) \to {\sf Set}\) è un prefascio, la condizione di cui parlo afferma che per ogni elemento \(q\) di \(Q\) e ogni suo ricoprimento \(p_i\), data una famiglia \(s_i \in L(p_i)\) con la proprietà che \(s|_{p_i\land p_j} = s_j|_{p_i\land p_j}\), si riesce sempre a trovare una sezione \(s\in L(q)\) con la proprietà che \(s|_{p_i}=s_i\) per ogni \(i\in I\).
Le condizioni di Enderton sono una versione semplificata della condizione di fascio per \({\sf Set}(j(-), V)\), dove la condizione di essere una matching family è stata resa vacuamente vera dall'ipotesi che le immagini delle varie \(f_\lambda\) ristrette a \(C\) siano tutte disgiunte: se lo sono, non esiste precondizione di matching ed esiste sempre una estensione. Nel tuo caso, e nelle notazioni di sopra, \({\sf Set}(j(-), V)=L\), l'elemento che vuoi ricoprire è \(C\), e il ricoprimento su cui usi la condizione di fascio è la catena dei \(C_i\).
All in all questo ti dice non solo che il teorema di ricorsione di Enderton è vero, ma che è vero in condizioni un po' più generali, perché l'estensione esiste non solo quando lo vuole Enderton ma anche quando "dove sono definite, le \(f_\lambda\) coincidono". Questo evita l'imbarazzo che hai quando \(x = f_\lambda(u) = f_\mu(v)\) non sai se usare \(F_\lambda(h^*u)\) o \(F_\mu(h^*v)\) per calcolare \(h^*(x)\), perché questi sono gli stessi valori.
Allora. Intanto anch'io mi sono costruito degli esempi e adesso mi è abbastanza chiaro (tranne l'esempio coi colori... ??).
A quello che hai fatto ieri sera e a tutto il resto rispondo domani perché ora son cotto, però ti avviso che non ci capisco un **** ihih. (In realtà l'argomento riesco a seguirlo ma non riesco a fillare i dettagli. il punto è che adesso non ho tempo per leggere MacLaneMoerdijk).
P.S. il teorema sulle ODE lo conosco. La dimostrazione l'ho presente a spanne ma tanto la devo rivedere tra poco. C'è tanta roba di sheaf theory sotto o bastano le prime definizioni?
A quello che hai fatto ieri sera e a tutto il resto rispondo domani perché ora son cotto, però ti avviso che non ci capisco un **** ihih. (In realtà l'argomento riesco a seguirlo ma non riesco a fillare i dettagli. il punto è che adesso non ho tempo per leggere MacLaneMoerdijk).
P.S. il teorema sulle ODE lo conosco. La dimostrazione l'ho presente a spanne ma tanto la devo rivedere tra poco. C'è tanta roba di sheaf theory sotto o bastano le prime definizioni?
