Proprietà semplici di $NN$

[compa90]

Buonasera, ho il seguente dubbio, che per molti di voi sarà sicuramente banale, ed è il seguente:

Considero l’insieme dei numeri naturali $NN$ senza lo zero, inoltre considero $a,b,c$ naturali per cui $a+b=c$, allora $a=c-b$.

Mi è chiara la tesi, ma se volessi dimostrarla in modo formale non so come fare, tuttavia la dimostrerei così
$a+b=c->a+b-b=c-b->a+(b-b)=c-b->a+0=c-b->a=c-b$
Supponendo che fosse corretto il ragionamento, mi chiedo $a+0$ lo posso valutare dal momento che $0$ non è un elemento di $NN$ ?

[axpgn]

Se è per quello neanche $-b$ lo è ...

[compa90]

Si hai ragione, allora come posso dimostrarla ?

[Studente Anonimo]

Dipende tutto dalle definizioni.

Come ti è stato definito $NN$?
Come ti è stata definita la sottrazione?

Inoltre vorrei ricordare che per alcuni $0$ appartiene a $NN$, per altri no, quindi a maggior ragione dipende tutto dalle definizioni che ti hanno dato.

[compa90]

@martino
$NN$, senza lo zero, invece per la sottrazione, considero $a,b \in NN$ dove $a$ rappresenta il minuendo, $b$ il sottraendo, ed è definita quando $a>b$, e il risultato $c:=b-a$ si dice differenza. Queste sono "le mie" definizioni.

@ martino ve ne sono altre, oltre a quella di includere $0$ in $NN$ ?

[axpgn]

Forse meglio $c:=a-b$ dato che hai per definizione $a>b$ ...
Inoltre con quella definizione lo zero "non esiste" ovvero non ne hai bisogno ...
A dir la verità non capisco cosa vorresti dimostrare perché quanto cerchi di dimostrare ti viene dato per definizione quindi non c'è nulla da dimostrare ... IMHO

[megas_archon]

Prima di tutto, \(0\in\mathbb N\) perché lo dice Dio e chiunque ti ha detto di toglierlo non deve rompere i coglioni.

Secondo, le definizioni sui numeri naturali si danno tutte per induzione.

A queste premesse, non vedo altro modo di definire la sottrazione se non questo:
\[
\begin{align*}
\_-\_ : \mathbb N \times \mathbb N &\to \mathbb N\\
n - 0 &= n\\
0 - (1+m) &= 0\\
(1+n) - (1+m) &= n - m\\
\end{align*}
\] (questa definizione di solito è quella che si chiama "monus" ed è equivalente ad iterare la funzione "predecessore", cioè l'inversa della funzione successore -l'unico costruttore di \(\mathbb N\) insieme a $0$).

Ora, la dimostrazione che vuoi fare si fa anche lei per induzione: la proposizione è "se \(a+b=c\), allora \(a=c-b\)", ossia \(\forall abc.(a+b=c \Rightarrow a = c-b)\), si fa per esempio tenendo fissati \(a,c\) e facendo induzione su $b$: se $b=0$, allora
\[a=a+0=a+b=c = c-0\] e se \(b=1+k\), \(c-(1+k) =...\) (si fa anche lei per casi: se $c=0$, allora \(0-(1+k)=0\), e questo è possibile solo se \(a=b=0\), quindi è vero; e se \(c=1+r\) allora \(c-(1+k)=r-k\) che usando il passo induttivo...).

Chiaramente la tua dimostrazione è una banalità, quando la fai a mano: se \(a+b=c\) allora \(c-b = (a+b)-b = a + (b-b) = a+0 = a\), ma qui ti serve un lemma che dice che \((x+y)-z= x+(y-z)\), e un lemma che ti dice che \(x-x=0\) -ciascuno dei quali si dimostra, che sorpresa, per induzione!- e quindi la fatica di raggruppare tra loro tre tautologie è circa la stessa.

[Studente Anonimo]

"compa90":$NN$, senza lo zero

Ripeto, qual è la tua definizione di $NN$?

invece per la sottrazione, considero $a,b \in NN$ dove $a$ rappresenta il minuendo, $b$ il sottraendo, ed è definita quando $a>b$, e il risultato $c:=b-a$ si dice differenza. Queste sono "le mie" definizioni.

Non sono definizioni. Sono notazioni.

È come se io dicessi "la potenza di base $a$ e esponente $b$ è per definizione $a^b$". Non ho definito niente. Ti ho solo detto che quando vedo il simbolo $a^b$ lo chiamo potenza.

Un altro esempio: "la derivata di una funzione $f(x)$ è per definizione $f'(x)$". Non è una definizione.

Un altro esempio: "la somma tra $a$ e $b$ è la loro addizione". Non significa niente, non ho definito niente.

Forse questo rende meglio l'idea: se io per esempio dicessi "il poresco tra $a$ e $b$ è la loro stoppola, il risultato è $c:=a€b$. $a$ si dice primendo, $b$ si dice secondendo". Cosa ho detto? Niente.

Spero di aver reso l'idea.