\documentclass{eptcs}

\usepackage{amsmath, amssymb}

\newcommand{\Nat}{\mathbb{N}}
\begin{document}

\noindent
La dimostrazione del Teorema di Deduzione di Herbrand del testo di Martini e' un esempio
di uso dell'induzione completa.
Prima di studiare tale dimostrazione, la presente nota potrebbe risultare utile.\\
\subsection*{Uso dell'induzione sulla lunghezza della deduzioni.}

L'induzione completa (cosi' come l'induzione matematica) puo' essere usata per dimostrare
affermazioni della forma
$$
\forall n\in\Nat. \varphi(n)
$$
dove $\varphi$ e' appunto una affermazione che riguarda i numeri naturali.
Il Teorema di Deduzione di Herbrand pero' riguarda le deduzioni nel sistema formale ${\cal P}_0$.
Come e' possibile allora utilizzare il principio di induzione per dimostrare proprieta' 
 relative alle deduzioni in  ${\cal P}_0$ (o in altri sistemi formali)?\\
Per capirlo, utilizziamo l'induzione per il seguente semplice risultato:
$$
\text{\em Se}\quad \vdash_{{\cal P}_0} \alpha  \quad\text{\em allora } \quad \models \alpha
$$
Questa e' una versione semplificata del teorema di correttezza per ${\cal P}_0$
(Teorema 3.5 del testo di Martini) per il quale consideriamo solo il caso in cui $\Gamma=\emptyset$.
Quanto affermato prima si puo' leggere come
$$
\text{\em Se $\alpha$ e' derivabile (senza usare ipotesi) in ${\cal P}_0$ allora $\alpha$ e' una tautologia.}
$$ 
Poiche' qualsiasi derivazione ha un numero naturale maggiore di uno come lunghezza, quello che abbiamo appena scritto
si puo' dire, in modo equivalente, come segue:
\begin{quote}
{\em Per ogni numero naturale $n\geq 1$, se $\alpha$ e' derivabile  (senza usare ipotesi) in ${\cal P}_0$ utilizzando una derivazione lunga $n$  allora $\alpha$ e' una tautologia.}
\end{quote}
A questo punto e' facile accorgersi che, se definiamo
\begin{quote}
$\varphi(n)$ = {\em Se $\alpha$ e' derivabile  (senza usare ipotesi)  in ${\cal P}_0$ utilizzando una derivazione lunga $n$\\
\phantom{$\varphi(n)$ =} allora $\alpha$ e' una tautologia.}
\end{quote}
quello che dobbiamo dimostrare e' 
$$
\forall n\geq 1. \varphi(n)
$$
Possiamo utilizzare il principio di induzione. \\

Per la dimostrazione e' piu' comodo
utilizzare l'induzione completa. Per convincersene, provate a rifare quanto segue utilizzando
l'induzione matematica. Non vi risultera' tanto facile.

Per utilizzare l'induzione completa per dimostrare  $\forall n\geq 1. \varphi(n)$ procediamo 
quindi a dimostrare le premesse dell'induzione completa.
\begin{description}
\item[$\varphi(1)$]
Dobbiamo cioe' far vedere che 
e $\alpha$ e' derivabile  (senza usare ipotesi) utilizzando una derivazione lunga $1$ in ${\cal P}_0$ allora $\alpha$ e' una tautologia.
Una derivazione di  $\alpha$ lunga $1$ e' necessariamente della forma
$$1. \alpha\quad\qquad (Ax)$$
Dove $Ax$ e' uno degli assiomi di ${\cal P}_0$. Inoltre siamo sicuri che $\alpha$ non puo' essere
una ipotesi (poiche' $\alpha$ e' derivata senza usare ipotesi) e che non e' la conclusione di una
regola di inferenza (poiche' l'unica regola di inferenza e' $MP$, per cui nella derivazione
dovremmo avere, prima di $\alpha$, due premesse della forma $\delta$ e $\delta\rightarrow\alpha$,
e questo e' impossibile, poiche' la nostra derivazione e' lunga $1$).
A questo punto possiamo utilizzare quanto dimostrato nell'esercizio 6 della parte ``Logica'' degli Esercizi ed affermare che $\alpha$ e' una tautologia. Questo completa la dimostrazione di  $\varphi(1)$.
\item[$(\forall 1\leq y<n. \varphi(y)) \Rightarrow \varphi(n)$]\quad
Dobbiamo far vedere  che vale $\varphi(n)$ per un generico $n$ se assumiamo che valga $\varphi$ per tutti i numeri compresi tra 1 ed $n$.
Facciamo quindi tale assunzione (chiamata ``ipotesi induttiva'') e proviamo a far vedere che vale $\varphi(n)$. Ricordiamo che 
var vedere che vale $\varphi(n)$ corrisponde a far vedere che
\begin{quote}
{\em Se $\alpha$ e' derivabile  (senza usare ipotesi) in ${\cal P}_0$ utilizzando una derivazione lunga $n$ allora $\alpha$ e' una tautologia.}
\end{quote}
Se $\alpha$ e' derivabile utilizzando una derivazione lunga $n$ vuol dire che esiste una derivazione
della forma\\
$$\begin{array}{cl}
1. & \ldots\\
\vdots &\vdots \\
n. & \alpha\qquad   (X) 
\end{array}
$$
Se  $(X) = (Ax)$ dove $Ax$ e'  uno degli assiomi di ${\cal P}_0$, abbiamo finito, poiche'
sappiamo (come detto prima) che gli assiomi di ${\cal P}_0$ sono tautologie.
Inoltre $(X)$ non puo' essere {\em (ipotesi)} perche' stiamo considerando teoremi di ${\cal P}_0$,
e quindi non utilizziamo ipotesi. 
L'unica altra possibilita' e' che $(X) = (MP(i,j))$ per qualche $i$ e $j$.
In questo caso la derivazione ha quindi la forma
$$\begin{array}{cl}
1. & \ldots\\
\vdots &\vdots \\
i. & \delta\\
\vdots &\vdots \\
j. & \delta\rightarrow\alpha\\
\vdots &\vdots \\
n. & \alpha\qquad   (MP(i,j)) 
\end{array}
$$
Dove, ovviamente, $i<n$ e $j<n$.
Prendiamo ora la parte di derivazione fino a $i$.
$$\begin{array}{cl}
1. & \ldots\\
\vdots &\vdots \\
i. & \delta\\
\end{array}
$$
Questa derivazione ci mostra che $\delta$ e' derivabile (senza usare ipotesi) in ${\cal P}_0$
utilizzando una derivazione lunga $i<n$.
Siccome la nostra ipotesi induttiva ci dice che $\varphi$ vale per tutti i numeri piu' piccoli di $n$,
vuol dire possiamo assumere che valga $\varphi(i)$. Per cui, visto che abbiamo appena visto che
$\delta$ e' derivabile utilizzando una derivazione lunga $i$, possiamo affermare che  $\delta$ e' una tautologia.

Continuiamo ora prendendo la parte lunga $j$ della derivazione lunga $n$, cioe'
$$\begin{array}{cl}
1. & \ldots\\
\vdots &\vdots \\
j. & \delta\rightarrow\alpha\\
\end{array}
$$
Visto che $j<n$, la nostra ipotesi induttiva ci permette di affermare $\varphi(j)$, e quindi che $\delta\rightarrow\alpha$ e' una tautologia.

A questo punto, possiamo far riferimento alla Proposizione 3.14 del testo di Martini (che va dimostrata come esercizio), che ci assicura che
se le premesse della regola MP sono tautologie, lo e' anche la sua conclusione.
Per cui, siccome abbiamo fatto vedere (utilizzando l'ipotesi induttiva) che 
$\delta$ e $\delta\rightarrow\alpha$ sono tautologie, possiamo affermare che anche $\alpha$ e' una tautologia.\\
Abbiamo cosi' fatto vedere che $(\forall 1\leq y<n. \varphi(y)) \Rightarrow \varphi(n)$.
\end{description}

\noindent
Avendo dimostrato $\varphi(1)$ e $(\forall 1\leq y<n. \varphi(y)) \Rightarrow \varphi(n)$, il principio
di induzione completa ci permette di affermare quello che volevamo, e cioe'
$$
\forall n\geq1\in\Nat. \varphi(n)
$$

\end{document}


