IT/Logic/syntax.tex

14 teoria dei tipi semplici di Church\index{Church, A.}  \cite{Church} e
18 di questa descrizione � la logica \HOL{}. Si noti che c'� un
20 \HOL\, cio� il linguaggio di programmazione \ML. Questo � il linguaggio usato
25 l'Italiano � di nuovo il meta-linguaggio!
27 La sintassi di \HOL{} contiene categorie sintattiche di tipi e termini i cui
29 di insiemi. Questa interpretazione insiemistica sar� sviluppata accanto alla
30 descrizione della sintassi di \HOL{}, e nel prossimo capitolo il sistema di dimostrazione
31 di \HOL\ sar� mostrato essere valido per il ragionamento circa propriet�
33 `non standard' di \HOL, che non ci riguarderanno qui.}. Questo modello � dato in
34 termini di un insieme di insiemi fisso $\cal U$, che sar� chiamato l'{\em
40 \item[Inhab] Ogni elemento di $\cal U$ � un insieme non vuoto.
47 consistente di coppie ordinate $(x,y)$ con $x\in X$ e $y\in Y$, con
52 $P(X)=\{Y:Y\subseteq X\}$ � un elemento di $\cal U$.
60 U}}X$ � definito come l'insieme di tutte le funzioni che mandano ciascun elemento $X\in{\cal U}$ in
61 un qualche elemento di $X$. Queste funzioni si possono, dunque, considerare come se scegliessero per ogni elemento
62 $X\in{\cal U}$ un elemento di $X$ rappresentativo di tutto l'insieme $X$ e per
63 questo si parla di funzioni di scelta. {\bf Choice} isola una di queste funzioni: $\ch$.}.
66 Ci sono alcune conseguenze di queste assunzioni che saranno necessarie.
68 certi insiemi di coppie ordinate. Cos� l'insieme $X\fun Y$ di tutte le funzioni
69 da un insieme $X$ a un insieme $Y$ � un sottoinsieme di $P(X\times Y)$; ed � un
77 Iterando {\bf Prod}, si ottiene che il prodotto cartesiano di qualsiasi
78 numero finito, diverso da zero, di insiemi in $\cal U$ � ancora in $\cal U$.
79 $\cal U$ contiene anche il prodotto cartesiano di nessun insieme, il che equivale a
80 dire che contiene un insieme di un unico elemento (in virt� di {\bf Sub} applicato
82 precisione, sar� isolato un particolare insieme di un solo elemento.
85 \item[Unit] $\cal U$ contiene un distinto insieme di un solo elemento $1=\{0\}$.
88 Analogamente, a causa di {\bf Sub} e {\bf Infty}, $\cal U$ contiene
89 insiemi di due elementi, uno dei quali sar� isolato.
92 \item[Bool] $\cal U$ contiene un distinto insieme di due elementi
97 Le assunzioni di sopra circa $\cal U$ sono pi� deboli di quelle imposte su un
98 universo di insiemi dagli assiomi della
99 teoria degli insiemi di Zermelo-Fraenkel\index{teoria degli insiemi Zermelo-Fraenkel} con
100 l'Assioma di Scelta (\theory{ZFC})\index{assioma di scelta}\index{ZFC@\ml{ZFC}},
102 richiesto di soddisfare alcuna forma dell'Assioma di
103 Rimpiazzamento\index{assioma di rimpiazzamento}.
104 Di fatto, � possibile dimostrare l'esistenza di un insieme
105 $\cal U$ con le propriet� di sopra dagli assiomi di \theory{ZFC}.
106 (Per esempio si potrebbe considerare $\cal U$ consistere di tutti gli insiemi non vuoti
107 nella gerarchia cumulativa di von~Neumann formata prima della fase
109 possibile in linea di principio dare una versione completamente formale all'interno
111 di sotto.
116 I tipi\index{vincolo di tipo!nella logica HOL@nella logica \HOL{}} della
122 Ci sono quattro specie di tipi nella logica \HOL{}. Questi possono essere descritti
125 su variabili di tipo, \textsl{c} varia su tipi atomici e \textsl{op} varia su
126 operatori di tipo.
131 \put(.5,0){\makebox(0,0)[b]{\footnotesize variabili di tipo}}
153 \noindent In maggiore dettaglio, le quattro specie di tipi sono come segue.
157 \item {\bf Variabili di tipo:}\index{variabili di tipo, nella logica HOL@variabili di tipo, nella logica \HOL{} logic!forma astratta di} queste stanno per insiemi
158 arbitrari nell'universo. Nella formulazione originale di Church della teoria dei tipi
159 semplici, le variabili di tipo sono parte del meta-linguaggio e sono usate per
160 variare su tipi del linguaggio oggetto. Le dimostrazioni contenenti variabili di tipo
161 erano concepite come schemi di dimostrazione (cio� famiglie di dimostrazioni). Per supportare
162 tali schemi di dimostrazione {\it all'interno} della logica \HOL{}, le variabili di tipo sono
163 state aggiunte al sistema di tipi del linguaggio oggetto\footnote{Questa tecnica
168 teoria determina una particolare collezione di tipi atomici. Per
170 rispettivamente, l'insieme distinto di due elementi $\two$ e
173 \item {\bf Tipi composti:}\index{tipi composti, nella logica HOL@tipi composti, nella logica \HOL{}!forma astratta di} questi hanno la
175 $\sigma_n$ sono i tipi argomento e $op$ � un {\it operatore di tipo\/}
176 di ariet� $n$. Gli operatori di tipo denotano operazioni per costruire insiemi.
180 \ty{list} � un operatore di tipo con ariet� 1. Esso denota l'operazione
181 di formare tutte le liste finite di elementi da un dato insieme. Un altro
182 esempio � l'operatore \ty{prod} di ariet� 2 che denota
183 l'operazione di prodotto cartesiano. Il tipo $(\sigma_1,\sigma_2)\ty{prod}$
186 \item {\bf Tipi funzione:}\index{tipi funzione, nella logica HOL@tipi funzione, nella logica \HOL{}!forma astratta di} Se $\sigma_1$
189 denota l'insieme di tutte le funzioni (totali) dall'insieme denotato dal suo
193 $\fun$ � semplicemente un distinto operatore di tipo di ariet� 2 scritto con
196 modello di una teoria \HOL{}---contrariamente agli altri operatori di tipo che
203 tipi composto costruiti con operatori di tipo $0$-ari. Per esempio,
204 il tipo atomico \ty{bool} dei valori di verit� pu� essere considerato come
210 \subsection{Strutture di tipo}
212 \index{struttura di tipo, nella logica HOL@struttura di tipo, nella logica \HOL{}}
214 Il termine `costante di tipo' � usato per comprendere sia i tipi atomici sia gli operatori
215 di tipo. Si assume che sia dato un insieme infinito {\sf
216 TyNames} dei {\em nomi delle costanti di tipo\/}. La lettera
217 greca $\nu$ � usata per variare su membri arbitrari di {\sf TyNames},
219 atomici (cio� costanti di tipo $0$-ari), e \textsl{op} � usato per variare
220 sui nomi degli operatori di tipo (cio� costanti di tipo $n$-arie, dove
223 Si assume che sia dato un insieme infinito {\sf TyVars} di {\em variabili
224 di tipo\/}\index{variabili di tipo, nella logica HOL@variabili di tipo, nella logica \HOL{}}.
229 Una {\it struttura di tipo\/} � un insieme $\Omega$ di costanti di tipo. Una {\it costante
230 di tipo\/}\index{costanti di tipo, nella logica HOL@costanti di tipo, nella logica \HOL{}} � una coppia $(\nu,n)$ dove $\nu\in{\sf TyNames}$ � il
233 naturali). Si assume che non esistano due distinte costanti di tipo che hanno lo
256 Si assume che l'operatore di tipo $\fun$ associ\index{operatori di tipo, nella logica HOL@operatori di tipo, nella logica \HOL{}!associativit� degli} a
266 di tipo che occorrono in $\sigma$.
272 Un {\em modello} $M$ di una struttura di tipo $\Omega$ � specificato dando
273 per ogni costante di tipo $(\nu,n)$ una funzione $n$-aria
282 I tipi che non contengono alcuna variabile di tipo sono chiamati {\it monomorfici},
283 mentre quelli che contengono variabili di tipo sono chiamati {\it
285 significato di un tipo polimorfico? Si pu�
287 le sue variabili di tipo su insiemi particolari. Cos� il suo significato complessivo non � un
290 assegnazione di insiemi alle variabili di tipo rilevanti. L'ariet� $n$
291 corrisponde al numero di variabili di tipo coinvolte. E' conveniente
292 in tale contesto essere in grado di considerare che una variabile di tipo sia
293 coinvolta nella semantica di un tipo $\sigma$ sia che occorra effettivamente
294 in $\sigma$ sia che non occorra in esso, portando alla nozione di un
297 Un {\em contesto di tipo}\index{contesto di tipo}, $\alpha\!s$, � semplicemente una
298 lista finita (possibilmente vuota) di variabili di tipo {\em distinte\/}
301 $\alpha\!s.\sigma$, dove $\alpha\!s$ � un contesto di tipo, $\sigma$ � un
302 tipo (su una data struttura di tipo) e tutte le variabili di tipo
304 lista $\alpha\!s$ pu� anche contenere variabili di tipo che non occorrono in
309 in cui le variabili di tipo di $\sigma$ sono elencate in $\alpha\!s$. Al
310 fine di selezionare uno di tali contesti, assumiamo che {\sf TyVars}
313 delle variabili di tipo che esso contiene, elencate in ordine\footnote{E'
315 piuttosto che liste, ma scegliamo di non fare questo dal momento che complica
316 moderatamente la definizione della semantica che sar� data di
319 Sia $M$ un modello di una struttura di tipo $\Omega$. Per ogni
326 di $\sigma$ come segue.
329 \item Se $\sigma$ � una variabile di tipo, essa deve essere $\alpha_{i}$ per qualche unico
331 funzione di proiezione, che manda $(X_{1},\ldots,X_{n})\in{\cal U}^{n}$
336 $X\!s\in{\cal U}^n$ all'insieme di tutte le funzioni
339 uso della propriet� {\bf Fun} di $\cal U$.)
347 Si pu� ora definire che il significato di un tipo $\sigma$ in un modello $M$ �
353 contesto canonico di $\sigma$. Se $\sigma$ � monomorfico, allora $n=0$
355 $\den{\sigma}_{M}()$ di $\cal U$. Quando il particolare modello $M$ �
358 Per riassumere, dato un modello in $\cal U$ di una struttura di tipo $\Omega$,
360 $\cal U$ e pi� in generale, interpreta i tipi polimorfici\index{tipi, nella logica HOL@tipi, nella logica \HOL{}!polimorfici}\index{tipi polimorfici, nella logica HOL@tipi polimorfici, nella logica \HOL{}!semantica formale dei} che coinvolgono $n$ variabili di tipo come funzioni $n$-arie ${\cal
362 interpretati da insiemi di funzioni complete.
367 Supponiamo che $\Omega$ contenga una costante di tipo $(\textsl{b},0)$ e che
386 dei significati ai tipi in presenza di `ambienti' che assegnano insiemi in
387 $\cal U$ a tutte le variabili di tipo. L'uso di tipi-in-contesti � quasi
388 la stessa cosa di usare ambienti parziali con domini finiti---�
390 insieme finito (ordinato) di variabili di tipo. Al livello dei tipi non c'�
392 e la semantica dei termini che sar� data di sotto, dove c'� una dipendenza
393 sia dalle variabili di tipo sia dalle variabili individuali, l'approccio usato
399 Se $\sigma$ e $\tau_1,\ldots,\tau_n$ sono tipi su una struttura di tipo
405 ogni $i=1,\ldots,p$ di
406 $\tau_i$ per la variabile di tipo $\beta_i$ in $\sigma$.
407 Il tipo risultante � chiamato una {\it istanza\/}\index{tipi, nella logica HOL@tipi, nella logica \HOL{}!istanziazione di} di $\sigma$. Il
409 induzione sulla struttura di $\sigma$.
414 Supponiamo che $\sigma$ sia un tipo che contiene le variabili di tipo distinte
417 un'istanza di $\sigma$. Allora i tipi $\tau_1,\ldots,\tau_p$ sono
423 Abbiamo anche bisogno di sapere come la semantica dei tipi si comporta rispetto
430 lunghezza di $\beta\!s$), sia $\sigma'$ l'istanza
432 tipo-in-contesto e il suo significato in qualsiasi modello $M$ � collegato a quello di
434 � la lunghezza di $\alpha\!s$)
441 Ancora una volta, il lemma pu� essere dimostrato per induzione sulla struttura di
452 Ci sono quattro specie di termini nella logica \HOL{}. Queste possono essere
455 \index{combinazioni, nella logica HOL@combinazioni, nella logica \HOL{}!forma astratta di}
467 \put(.5,1.5){\makebox(0,0)[b]{\footnotesize applicazioni di funzione}}
481 Informalmente, un $\lambda$-termine\index{lambda termini, nella logica HOL@lambda termini, nella logica \HOL{}}\index{astrazione di funzione, nella logica HOL@astrazione di funzione, nella logica \HOL{}!forma astratta di} $\lambda x.\ t$ denota
482 una funzione $v\mapsto t[v/x]$, dove $t[v/x]$ denota il risultato di
483 sostituire $v$ per $x$ in $t$. Un'applicazione\index{applicazione di funzione, nella logica HOL@applicazione di funzione, nella logica \HOL{}!forma astratta di} $t\ t'$ denota il
484 risultato di applicare la
486 reso pi� preciso di sotto.
488 La grammatica {\small BNF} appena data omette di menzionare i tipi. Di fatto, ogni
492 tradizionalmente usata per variare su termini di tipo $\sigma$. Una
501 _{\sigma_1\fun\sigma_2}$$\index{costanti, nella logica HOL@costanti, nella logica \HOL{}!forma astratta di}
504 struttura di tipo $\Omega$, la definizione formale dei termini � relativa a
505 una data collezione di costanti tipizzate su $\Omega$. Assumiamo che sia dato
506 un insieme infinito {\sf Names} di nomi. Una {\em costante\/} su
509 � semplicemente un insieme $\Sigma_\Omega$ di tali costanti.
511 L'insieme {\sf Terms}$_{\Sigma_{\Omega}}$ di termini su
513 seguenti regole di formazione:
518 � un'istanza di $\sigma$, allora $(\con{c},{\sigma'})\in{\sf
520 costanti\/}\index{costanti, nella logica HOL@costanti, nella logica \HOL{}!forma astratta di} e sono scritti $\con{c}_{\sigma'}$.
525 variabili}\index{variabili, nella logica HOL@variabili, nella logica \HOL{}!forma astratta di}.  Il marcatore {\tt var}\ � semplicemente un accorgimento per
527 ${\tt var}\ x_{\sigma}$ sar� di solito scritta come $x_{\sigma}$, se
531 \item {\bf Applicazioni di funzione:}  Se $t_{\sigma'{\fun}\sigma}\in{\sf
553 L'applicazione di funzione\index{applicazione di funzione, nella logica HOL@applicazione di funzione, nella logica \HOL{}!associativit� della} � assunta associare
561 di tipo. Altrimenti � chiamato monomorfico. Si noti che un termine
565 $tyvars(t_{\sigma})$ denota l'insieme di variabili di tipo che occorrono in
568 L'occorrenza di una variabile $x_{\sigma}$ � chiamata {\it
569 legata\/}\index{variabili legate, nella logica HOL@variabili legate, nella logica \HOL{}}\index{variabili, nella logica HOL@variabili, nella logica \HOL{}!forma astratta di}
570  se essa occorre all'interno dello scopo di una $\lambda x_{\sigma}$
571 che chiude dal punto di vista testuale, altrimenti l'occorrenza � chiamata {\it
572 libera\/}\index{variabili libere, nella logica HOL@variabili libere, nella logica \HOL{}!forma astratta di}. Si noti che $\lambda x_{\sigma}$ non lega
579 Un {\em contesto\/}\index{contesti, nella semantica della logica HOL@contesti, nella semantica della logica \HOL{}} $\alpha\!s,\!x\!s$ consiste di un contesto
580 di tipo $\alpha\!s$ insieme con una lista $x\!s=x_{1},\ldots,x_{m}$ di
581 variabili distinte i cui tipi contengono solo variabili di tipo dalla
585 di qualche commento. Dal momento che una variabile � specificata sia da un nome sia da un
590 cautela quando si definisce il significato dell'istanziazione delle variabili di tipo,
595 $\:\;\alpha\!s,\!x\!s.t\;\:$ consiste di un contesto insieme con un termine
599 \item $\alpha\!s$ contiene qualsiasi variabile di tipo che occorre in $x\!s$ e $t$.
607 Il contesto $\alpha\!s,\!x\!s$ pu� contenere variabili (di tipo) che
612 rinominando le variabili legate in caso di necessit�\footnote{Si ricordi che due
615 data di seguito restringeremo l'attenzione a tali termini. Quindi il significato di un
616 termine arbitrario � considerato essere il significato di qualche $\alpha$-variante di
621 $\alpha\!s,\!x\!s.t$ � un termine-in-contesto. Come per le variabili di tipo,
624 canonico}\index{contesti canonici, nella logica HOL@contesti canonici, nella logica \HOL{}!di termini} del termine $t$.
630 di tipo $\Omega$ (si veda la Sezione~\ref{terms}). Un {\em modello\/} $M$ di
631 $\Sigma_{\Omega}$ � specificato da un modello della struttura di tipo pi�
639 di tipo che occorrono in $\sigma$. In altre parole
641 che assegna ad ogni $X\!s\in{\cal U}^{n}$ un elemento di
645 identificato con un elemento di quell'insieme.
648 semantica interpreta termini chiusi che non coinvolgono variabili di tipo come
649 elementi di insiemi in $\cal U$ (il particolare insieme coinvolto essendo derivato
651 in generale, se il termine chiuso coinvolge $n$ variabili di tipo allora �
652 interpretato come un elemento di un prodotto $\prod_{X\!s\in{\cal
654 U}$ � derivata dal tipo del termine (in un contesto di tipo derivato
657 di tipo nel termine, d� un significato per il termine come un elemento di un
659 libere ma nessuna variabile di tipo, allora � interpretato come una funzione
665 d� un significato per il termine. Infine, il caso pi� generale � quello di un
666 termine che coinvolge $n$ variabili di tipo e $m$ variabili libere: esso �
667 interpretato come un elemento di un prodotto
674 libere e dal tipo del termine (in un conteso di tipo derivato dal
692 sezione~\ref{semantics of types}. Il significato di $\alpha\!s,\!x\!s.t$
705 si ottiene un elemento $\den{\alpha\!s,\!x\!s.t}_{M}(X\!s)(y\!s)$ di
706 $\den{\alpha\!s.\tau}_{M}(X\!s)$. La definizione di
720 $(\con{c},\sigma)\in\Sigma_{\Omega}$ e $\sigma'$ � un'istanza di
721 $\sigma$.  Allora per il Lemma~1 di \ref{instances-and-substitution},
724 $\beta_{1},\ldots,\beta_{p}$ sono le variabili di tipo che occorronoin
728 che � un elemento di $\den{\alpha\!s.\tau}(X\!s)$ per il Lemma~2 di
732 Supponiamo che $t$ sia un termine applicazione di funzione\index{combinazioni, nella logica HOL@combinazioni, nella logica \HOL{}!semantica formale delle} $(t_{1}\
733 t_{2})$\index{applicazione di funzione, nella logica HOL@applicazione di funzione, nella logica \HOL{}!semantica formale delle} dove $t_{1}$ � di tipo
734 $\tau'\fun\tau$ e $t_{2}$ � di tipo $\tau'$. Allora
735 $f=\den{\alpha\!s,\!x\!s.t_{1}}(X\!s)(y\!s)$, essendo un elemento di
742 \item Supponiamo che $t$ sia il termine astrazione\index{astrazione di funzione, nella logica HOL@astrazione di funzione, nella logica \HOL{}!semantica formale della}
743 $\lambda x.t_{2}$ dove $x$ � di tipo $\tau_{1}$ e $t_{2}$ di
745 $\den{\alpha\!s.\tau}(X\!s)$ � l'insieme di funzioni
747 Definiamo $\den{\alpha\!s,\!x\!s.t}(X\!s)(y\!s)$ essere l'elemento di
755 Ora definiamo il significato di un termine $t_{\tau}$ in un modello $M$ essere la
762 contesto canonico di $t_{\tau}$. Cos� $n$ � il numero di variabili di tipi in
763 $t_{\tau}$, $\alpha\!s$ � una lista di quelle variabili di tipo, $m$ � il
764 numero di variabili ordinarie che occorrono libere in $t_{\tau}$ (assunte essere
765 distinte dalle variabili legate di $t_{\tau}$) e i $\sigma_{j}$ sono
766 i tipi di quelle variabili. (E' importante notare che la lista
767 $\alpha\!s$, che � parte del contesto canonico di $t$, pu� essere strettamente
768 pi� grande dei contesti di tipo canonici di $\sigma_{j}$ o $\tau$. Cos�
770 definizione di sopra.)
779 dove $\alpha\!s$ � la lista delle variabili di tipo che occorrono in $t_{\tau}$ e
780 $n$ � la lunghezza di quella lista. Se inoltre, nessuna variabile di tipo occorre in
784 La semantica dei termini appare qualcosa di complicato a casua della
785 possibile dipendenza di un termine sia dalle variabili di tipo sia dalle variabili
786 ordinarie. Esempi di come la definizione della semantica
788 di alcuni termini che denotano costanti logiche.
793 Dal momento che i termini possono coinvolgere sia variabili di tipo sia
794 variabili ordinarie, ci sono due differenti operazioni di sostituzione
795 sui termini che bisogna considerare---sostituzione di tipi per variabili
796 di tipo e sostituzione di termini per variabili.
798 \subsubsection*{Sostituire tipi per variabili di tipo nei termini}
799 \index{regola di sostituzione, nella logica HOL@regola di sostituzione, nella logica \HOL{}!semantica formale della}
805 tipi-in-contesto, allora sostituendo\index{sostituzione di tipo, nella logica HOL@sostituzione di tipo, nella logica \HOL{}!semantica formale della} i tipi
806 $\tau_{i}$ per le variabili di tipo $\alpha_{i}$ nella lista $x\!s$, si
807 ottiene una nuova lista di variabili $x\!s'$. Cos� il $j$\/esimo elemento di
811 Nell'istanziare\index{tipi, nella logica HOL@tipi, nella logica \HOL{}!istanziazione di} le variabili di tipo $\alpha\!s$ con i tipi
812 $\tau\!s$, nessuna coppia di due variabili distinte nella lista $x\!s$ diventano uguali
813 nella lista $x\!s'$\footnote{Una tale identificazione di variabili potrebbe
820 di tipo $\alpha\!s$ in $t$ (con un'adatta rinomina delle occorrenze
831 Il significato di $\alpha\!s',\!x\!s'.t'$ in un modello � collegato a quello
832 di $t$ come segue. Per tutti $X\!s'\in{\cal U}^{n'}$ (dove $n'$ � la
833 lunghezza di $\alpha\!s'$)
844 i lati dell'equazione di sopra sono elementi dello stesso insieme di funzioni.
849 \index{regola di sostituzione, nella logica HOL@regola di sostituzione, nella logica \HOL{}!semantica formale della}
855 $j=1,\ldots,m$ con $t_{j}$ dello stesso tipo di $x_{j}$, diciamo
870 Il significato di $\alpha\!s,\!x\!s'.t''$ in un modello � collegato con quello di
873 \den{\alpha\!s.\sigma'_{m'}}$ (dove $\sigma'_{j}$ � il tipo di
891 imporre qualche struttura specifica. In particolare, ogni struttura di tipo
893 l'insieme distinto di due elementi $\two\in{\cal U}$, considerato come un insieme
894 di valori di verit�. Le formule logiche sono allora identificate con
895 i termini\index{variabili di tipo, nella logica HOL@variabili di tipo, nella logica \HOL{}!forma astratta di}\index{termini, nella logica HOL@termini, nella logica \HOL{}!as logical formulas} di
898 requisiti sono formalizzati definendo la nozione di una
901 \subsection{Strutture di tipo standard}
904 Una struttura di tipo $\Omega$ � {\em standard\/} se contiene i
905 tipi atomici \ty{bool} (dei booleani o valori di verit�) e \ty{ind} (degli
907 al posto di \ty{bool} e $\iota$ al posto di \ty{ind}.)
909 Un modello $M$ di $\Omega$ � {\em standard\/} se $M(\bool)$ e $M(\ind)$ sono
913 Si assumer� d'ora in avanti che le strutture di tipo e i loro modelli
921 seguenti tre costanti primitive\index{costanti primitive, della logica HOL@costanti primitive, della logica \HOL{}}\index{costanti, nella logica HOL@costanti, nella logica \HOL{}!primitive, forma astratta di}:
931 L'interpretazione intesa di queste costanti � che $\imp$ denota
934 $\hilbert_{(\sigma\fun\ty{bool})\fun\sigma}$ denota una funzione di scelta
935 sull'insieme denotato da $\sigma$. Pi� precisamente, un modello $M$ di
953 la funzione di test dell'uguaglianza\index{uguaglianza, nella logica HOL@uguaglianza, nella logica \HOL{}!semantica formale della}, che manda $x,x'\in X$ a
965 U}$ la funzione di scelta\index{operatore di scelta, nella logica HOL@operatore di scelta, nella logica \HOL{}!semantica formale del} che manda $f\in(X\fun\two)$ a
989 (`falso')\index{valori di verit�, nella logica HOL@valori di verit�, nella logica \HOL{}!forma astratta di}, $\imp$ (`implica'), $\wedge$ (`e'), $\vee$
997 di Andrews~\cite{Andrews} e i riferimenti che esso contiene.
1001 I termini di tipo \ty{bool} sono chiamati {\it formule\/}\index{formule come termini, nella logica HOL@formule come termini, nella logica \HOL{}}.
1006 \index{uguaglianza, nella logica HOL@uguaglianza, nella logica \HOL{}!forma astratta di}
1007 \index{implicazione, nella logica HOL@implicazione, nella logica \HOL{}!forma astratta di}
1008 \index{operatore di scelta, nella logica HOL@operatore di scelta, nella logica \HOL{}!forma astratta di}
1009 \index{quantificatore esistenziale, nella logica HOL@quantificatore esistenziale, nella logica \HOL{}!forma astratta di}
1010 \index{quantificatore universale, nella logica HOL@quantificatore universale, nella logica \HOL{}!forma astratta di}
1024 Queste notazioni sono casi speciali di convenzioni generali di abbreviazione
1026 terza � un binder (si vedano le sezioni di \DESCRIPTION\/ sul parsing e