Il principio di induzione

[solaàl]

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\).

[solaàl]

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}\).

[solaàl]

Vuoi un hint o preferisci pensarci?

Testo nascosto, fai click qui per vederlo

Quanti sottoggetti ha \(\mathbb N\) in \(\sf Dyn\)?

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

Codice:

data (N : Set) where
  Z : N
  Suc : N -> N


Z : N e Suc : N -> N sono proprio l'elemento distinto e l'endomorfismo in questione.

[solaàl]

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

[kaspar]

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?

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.

[Ancona]

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

[kaspar]

\(
\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\).

[solaàl]

Un sottoggetto di $X$ è un[a classe di isomorfismo di] monomorfismo verso $X$. Sì, il motivo è questo. Bello, no?

[Ancona]

In realtà l’ipotesi non doveva essere che $\mathbb{N}$ fosse oggetto iniziale in Dyn, ma solo che Dyn avesse un oggetto iniziale.

[solaàl]

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).