Serve la doppia induzione? Direi di no...

[fields]

Lemma 1. Su $n$.
Lemma 2. Su $n$.
Lemma 3. Su $m$.
?

Esatto. Oppure anche tutto su $n$, data la simmetria del 3.

[G.D.]

Provo quindi a riassumere gli insegnamenti che mi hai fornito.

La doppia induzione propriamente intesa è una particolare induzione transfinita nella quale procedo due volte con una induzione semplice su due variabili $m$ e $n$ con due diverse ipotesi induttive, una per $m$ e una per $n$.

Quando ho due variabili $m$ e $n$ e voglio dimostrare con l'induzione una certa proprietà $P(m,n)$, se posso ricondurmi ad una induzione semplice sulla quantità $z=f(m,n)$ allora posso lasciare arbitraria una delle due variabili e indurre una sola volta sull'altra. Altrimenti, usando le strategy 1 e 2 di MathLinks posso indurre prima su una variabile e poi sull'altra eseguendo, con un certo abuso di linguaggio, una doppia induzione, nel senso di induzione ripetuta due volte.

Ancora grazie per la cortesia.

[fields]

La doppia induzione propriamente intesa è una particolare induzione transfinita nella quale procedo due volte con una induzione semplice su due variabili $m$ e $n$ con due diverse ipotesi induttive, una per $m$ e una per $n$.

Si', e ottieni questo effetto annidando le due induzioni, come nell'esempio che hai riportato sulla commutativita' dell'addizione.

Quando ho due variabili $m$ e $n$ e voglio dimostrare con l'induzione una certa proprietà $P(m,n)$, se posso ricondurmi ad una induzione semplice sulla quantità $z=f(m,n)$ allora posso lasciare arbitraria una delle due variabili e indurre una sola volta sull'altra.

Tecnicamente e' un'induzione su $z$, cioe' sulla quantita' $f(m,n)$. Non fai alcuna induzione su $m,n$.

La formula che dimostri per induzione, rispetto alla variabile $z$, formalmente e'

$\forall m \forall n z=f(m,n)-> P(m,n)$

quindi sostanzialmente sia $m$ che $n$ saranno entrambe arbitrarie. Questo perche' nel passo induttivo dimostri

$\forall m \forall n z+1=f(m,n)-> P(m,n)$

e lo farai dicendo: siano m,n arbitrari, dimostriamo

$z+1=f(m,n)-> P(m,n)$

etc.

[G.D.]

OK. Grazie mille per il prezioso contributo.