Il principio di induzione
Partendo dal fatto che \(\mathbb N\) è un oggetto iniziale di \(\sf Dyn\) mostrate il "principio di induzione": se \(P : \mathbb N \to \{0,1\}\) è una proposizione che soddisfa le seguenti due proprietà
i1. \(P0\) è vera
i2. se \(Pn\) è vera, allora \(P(n+1)\) è vera.
Allora \(Pn\) è vera per ogni \(n : \mathbb N\).
i1. \(P0\) è vera
i2. se \(Pn\) è vera, allora \(P(n+1)\) è vera.
Allora \(Pn\) è vera per ogni \(n : \mathbb N\).
Risposte
"arnett":
1. Credo che questo si faccia usando che ${0,1}$ sta in Dyn,
Acqua! Il punto è proprio: come si lega l'iterazione (ossia la proprietà universale di \(\mathbb N\)) al principio di induzione e alla ricorsione?
2. Ma questo non crea un problema di circolarità? L'affermazione che $(\NN, s, 0)$ sta in Dyn segue dal teorema di ricorsività, che però è provato usando anche l'induzione.\(\mathbb N\) è l'algebra iniziale dell'endofuntore \(\_\sqcup 1 : \sf Set \to Set\).
3. "Dyn" per cosa sta?Sistemi \(\sf Dyn\)amici. Un insieme \(f : X \to X\) con un endomorfismo fissa l'orbita di un monoide, quello degli endomorfismi di \(X\) che agisce su \(X\) con le iterate di \(f\); se vuoi, esiste un unico omomorfismo di monoidi \(\Phi_f : \mathbb N \to \text{End}(X)\) tale che \(\Phi_f(n)=f^{\circ n}\).
Vuoi un hint o preferisci pensarci?
Mi spiace, non so cosa sia l'algebra di un endofuntore, argh, e di conseguenza non capisco come questo si leghi alla domanda che ho fatto.Non è importante saperlo; hai chiesto se si crea una circolarità nella definizione, la risposta era per dirti: no, non mi pare. Del resto, cosa intendi per "dimostrare" che \(\mathbb N\) è un oggetto di \(\sf Dyn\)? Un oggetto di \(\sf Dyn\) è un insieme puntato con un endomorfismo. \(\mathbb N\) è definito da
data (N : Set) where Z : N Suc : N -> N[inline]Z : N[/inline] e [inline]Suc : N -> N[/inline] sono proprio l'elemento distinto e l'endomorfismo in questione.
Il punto di questo esercizio è proprio che è esattamente il contrario, è il principio di induzione, solitamente considerato primitivo, a potersi dimostrare mediante la proprietà universale di N
"arnett":Sì e c'hai ragione. Solo che la richiesta è un'altra, essenzialmente: fai tabula rasa di ciò che già sai e per te ora \(\mathbb N\) è l'oggetto iniziale di \(\mathbf{Dyn}\). Sono impostazioni diverse: in una il principio di induzione è assioma e questa dimostra la proprietà di ricorsione, mentre qui è assioma la proprietà di ricorsione e con questa dimostri il principio di induzione.
Che $\NN$ stia in Dyn non presuppone altro che il dato dell'insieme con la mappa di successivo e lo zero; ma il fatto che $\NN$, così strutturato, sia iniziale in Dyn non dipende dall'induzione? Cioè il fatto che in Dyn ci sia una sola freccia che esce da $\NN$ non si dimostra per induzione?
impostazioni diverse: in una il principio di induzione è assioma e questa dimostra la proprietà di ricorsione, mentre qui è assioma la proprietà di ricorsione e con questa dimostri il principio di induzione.
No. L'esercizio è: Dyn ha oggetto iniziale $iff$ Induzione
\(
\newcommand\setn{\mathbb N}
\newcommand\calp{\mathcal P}
\newcommand\dyn{\mathbf{Dyn}}
\)Non so cosa siano i sottoggetti e non so nemmeno come lavorarci ancora. Provo a proporre un qualcosa che mi è venuto in mente facendo altro.
L'ipotesi è quindi che \((\setn, 0, \_+1)\) sia l'oggetto insiziale di \(\dyn\). Sia inoltre un oggetto \((A, 0, \sigma)\) di \(\dyn\) con \(A \subseteq \setn\) tale che per ogni \(n\) se \(n \in A\) allora \(n+1 \in A\) e \[
\sigma : A \to A, \quad \sigma(n) = \begin{cases} n+1 & \text{se } n+1 \in A \\ n & \text{altrimenti} \end{cases}.
\] Per la proprietà universale che gode \((\setn, 0, \_+1)\) all'interno di \(\dyn\), si ha che esiste un'unica funzione \(f : \setn \to A\) tale che \(f(0) = 0\) e \[
f(n+1) = \sigma(f(n)) = \begin{cases} f(n)+1 & \text{se } f(n)+1 \in A \\ f(n) & \text{altrimenti} \end{cases}.
\] Tuttavia la funzione \(f \circ (\_+1)\) è costretta a comportarsi nel primo modo, visto che se \(f(n)+1 \notin A\), allora pure \(f(n) \notin A\), e quindi \(A \owns f(n+1) = f(n) \notin A\). In particolare la funzione \(i : \setn \to A\) con \(i(x) = x\) è la nostra \(f\), sempre per l'unicità nella proprietà universale. In altri termini \(\setn \subseteq A\) e, quindi a chiusura di tutto, \(A = \setn\).
\newcommand\setn{\mathbb N}
\newcommand\calp{\mathcal P}
\newcommand\dyn{\mathbf{Dyn}}
\)Non so cosa siano i sottoggetti e non so nemmeno come lavorarci ancora. Provo a proporre un qualcosa che mi è venuto in mente facendo altro.
L'ipotesi è quindi che \((\setn, 0, \_+1)\) sia l'oggetto insiziale di \(\dyn\). Sia inoltre un oggetto \((A, 0, \sigma)\) di \(\dyn\) con \(A \subseteq \setn\) tale che per ogni \(n\) se \(n \in A\) allora \(n+1 \in A\) e \[
\sigma : A \to A, \quad \sigma(n) = \begin{cases} n+1 & \text{se } n+1 \in A \\ n & \text{altrimenti} \end{cases}.
\] Per la proprietà universale che gode \((\setn, 0, \_+1)\) all'interno di \(\dyn\), si ha che esiste un'unica funzione \(f : \setn \to A\) tale che \(f(0) = 0\) e \[
f(n+1) = \sigma(f(n)) = \begin{cases} f(n)+1 & \text{se } f(n)+1 \in A \\ f(n) & \text{altrimenti} \end{cases}.
\] Tuttavia la funzione \(f \circ (\_+1)\) è costretta a comportarsi nel primo modo, visto che se \(f(n)+1 \notin A\), allora pure \(f(n) \notin A\), e quindi \(A \owns f(n+1) = f(n) \notin A\). In particolare la funzione \(i : \setn \to A\) con \(i(x) = x\) è la nostra \(f\), sempre per l'unicità nella proprietà universale. In altri termini \(\setn \subseteq A\) e, quindi a chiusura di tutto, \(A = \setn\).
Un sottoggetto di $X$ è un[a classe di isomorfismo di] monomorfismo verso $X$. Sì, il motivo è questo. Bello, no?
In realtà l’ipotesi non doveva essere che $\mathbb{N}$ fosse oggetto iniziale in Dyn, ma solo che Dyn avesse un oggetto iniziale.
Beh, in realtà l'ho frasata proprio colà invece (costà?)
Il fatto è che i sottoggetti di un oggetto iniziale sono "pochi". Cioè che gli oggetti iniziali tendono a essere strutture semplici. Cioè che tendono a essere strutture semplici (eventualmente in senso degenere).
Il fatto è che i sottoggetti di un oggetto iniziale sono "pochi". Cioè che gli oggetti iniziali tendono a essere strutture semplici. Cioè che tendono a essere strutture semplici (eventualmente in senso degenere).
Sì, ho visto dopo che nell’esercizio iniziale la richiesta era proprio quella.. ma così mi pare troppo facile.
Beh, mi sembra di non aver usato qualche cosa di peculiare a \((\mathbb N, 0, \_+1)\). Con qualche leggera modifica a quanto ho mostrato si potrebbe tranquillamente fare penso come dici tu, Ancona.
Non ho letto quello che hai fatto te. Comunque hai ragione a dire che l’esercizio che propongo io non è molto più difficile
Se vi dà fastidio che questo esercizio sia così semplice, posso proporne di estremamente più difficili.
Non credo stia «dando fastidio».
Se c'è qualcuno che ti può rispondere, sì. Altrimenti potresti dosare (anche se non è sano, alla lunga, continuare ad avere cose premasticate...).
"solaàl":
posso proporne di estremamente più difficili
Se c'è qualcuno che ti può rispondere, sì. Altrimenti potresti dosare (anche se non è sano, alla lunga, continuare ad avere cose premasticate...).
A me “dava fastidio” solo il fatto di dare già per ipotesi che $\mathbb{N}$ fosse l’oggetto iniziale. Non ho antipatia per gli esercizi facili. Gli esercizi estremi sono curioso di vederli ma chi vuoi che te li risolva...
Se c'è qualcuno che li sa risolvere, mi piacerebbe vedere come si riesce a muovere... ^-^ Per quel che vale, io almeno potrei provare, questo esercizio per esempio mi è riuscito, altri no... Bhé, se sono troppo estremi, non mi basta la comprensione di un testo scritto in italiano per capire...
Accedi a tutti gli appunti
Tutor AI: studia meglio e in meno tempo