% Revised version of Part II, Chapter 9 of HOL DESCRIPTION
% Incorporates material from both of chapters 9 and 10 of the old
% version of DESCRIPTION
% Written by Andrew Pitts
% 8 March 1991
% revised August 1991
\chapter{Sintassi e Semantica}\label{logic}

\section{Introduzione}
\label{introduction}

Questo capitolo descrive la sintassi e la semantica a modelli della
logica supportata dal sistema \HOL{}, che è una variante della
teoria dei tipi semplici di Church\index{Church, A.}  \cite{Church} e
che sarà d'ora in poi chiamata la logica \HOL{}, o semplicemente \HOL. Il
meta-linguaggio per questa descrizione sarà l'Italiano, arricchito con
varie notazioni e convenzioni matematiche. Il liguaggio oggetto
di questa descrizione è la logica \HOL{}. Si noti che c'è un
`meta-linguaggio', in un senso differente, associato con la logica
\HOL\, cioè il linguaggio di programmazione \ML. Questo è il linguaggio usato
per manipolare la logica \HOL{} da parte degli utenti del sistema. Si spera
che in base al contesto, non risulti alcuna confusione da questi due usi della
parola `meta-linguaggio'. Quando l'oggetto dello studio è l'\ML\ (come in
\cite{sml}), l'\ML\ è il linguaggio oggetto considerato---e
l'Italiano è di nuovo il meta-linguaggio!

La sintassi di \HOL{} contiene categorie sintattiche di tipi e termini i cui
elementi sono intesi denotare rispettivamente certi insiemi e elementi
di insiemi. Questa interpretazione insiemistica sarà sviluppata accanto alla
descrizione della sintassi di \HOL{}, e nel prossimo capitolo il sistema di dimostrazione
di \HOL\ sarà mostrato essere valido per il ragionamento circa proprietà
del modello insiemistico\footnote{Ci sono altri, modelli
`non standard' di \HOL, che non ci riguarderanno qui.}. Questo modello è dato in
termini di un insieme di insiemi fisso $\cal U$, che sarà chiamato l'{\em
universo\/}\index{universo, nella semantica della logica HOL@universo, nella
semantica della logica \HOL{}\/} e che si assume avere le seguenti
proprietà.
\begin{description}

\item[Inhab] Ogni elemento di $\cal U$ è un insieme non vuoto.

\item[Sub] Se $X\in{\cal U}$ e $\emptyset\not=Y\subseteq X$, allora
$Y\in{\cal U}$.

\item[Prod] Se $X\in{\cal U}$ e $Y\in{\cal U}$, allora $X\times
Y\in{\cal U}$. L'insieme $X\times Y$ è il prodotto cartesiano,
consistente di coppie ordinate $(x,y)$ con $x\in X$ e $y\in Y$, con
l'usuale notazione insiemistica delle coppie ordinate, cioé
$(x,y)=\{\{x\},\{x,y\}\}$.

\item[Pow] Se $X\in{\cal U}$, allora anche l'insieme potenza
$P(X)=\{Y:Y\subseteq X\}$ è un elemento di $\cal U$.

\item[Infty] $\cal U$ contiene un distinto insieme infinito $\inds$.

\item[Choice] C'è un elemento distinto $\ch\in\prod_{X\in{\cal
U}}X$. Gli elementi del prodotto $\prod_{X\in{\cal U}}X$ sono
funzioni (dipendentemente tipizzate): così per tutti gli $X\in{\cal U}$, $X$ è
non vuoto per {\bf Inhab} e $\ch(X)\in X$ testimonia questo\footnote{[ndt] Il prodotto cartesiano generalizzato $\prod_{X\in{\cal
U}}X$ è definito come l'insieme di tutte le funzioni che mandano ciascun elemento $X\in{\cal U}$ in
un qualche elemento di $X$. Queste funzioni si possono, dunque, considerare come se scegliessero per ogni elemento
$X\in{\cal U}$ un elemento di $X$ rappresentativo di tutto l'insieme $X$ e per
questo si parla di funzioni di scelta. {\bf Choice} isola una di queste funzioni: $\ch$.}.

\end{description}
Ci sono alcune conseguenze di queste assunzioni che saranno necessarie.
Nella teoria degli insiemi le funzioni sono identificate dai loro grafi, che sono
certi insiemi di coppie ordinate. Così l'insieme $X\fun Y$ di tutte le funzioni
da un insieme $X$ a un insieme $Y$ è un sottoinsieme di $P(X\times Y)$; ed è un
insieme non vuoto quando $Y$ non è vuoto. Così {\bf Sub}, {\bf Prod} e {\bf
Pow} insieme implicano che $\cal U$ soddisfa anche
\begin{description}

\item[Fun] Se $X\in{\cal U}$ e $Y\in{\cal U}$, allora $X\fun Y\in{\cal U}$.

\end{description}
Iterando {\bf Prod}, si ottiene che il prodotto cartesiano di qualsiasi
numero finito, diverso da zero, di insiemi in $\cal U$ è ancora in $\cal U$.
$\cal U$ contiene anche il prodotto cartesiano di nessun insieme, il che equivale a
dire che contiene un insieme di un unico elemento (in virtù di {\bf Sub} applicato
a qualsiasi insieme in ${\cal U}$---{\bf Infty} garantisce che ce n'è uno); per
precisione, sarà isolato un particolare insieme di un solo elemento.
\begin{description}

\item[Unit] $\cal U$ contiene un distinto insieme di un solo elemento $1=\{0\}$.

\end{description}
Analogamente, a causa di {\bf Sub} e {\bf Infty}, $\cal U$ contiene
insiemi di due elementi, uno dei quali sarà isolato.
\begin{description}

\item[Bool] $\cal U$ contiene un distinto insieme di due elementi
$\two=\{0,1\}$.

\end{description}

Le assunzioni di sopra circa $\cal U$ sono più deboli di quelle imposte su un
universo di insiemi dagli assiomi della
teoria degli insiemi di Zermelo-Fraenkel\index{teoria degli insiemi Zermelo-Fraenkel} con
l'Assioma di Scelta (\theory{ZFC})\index{assioma di scelta}\index{ZFC@\ml{ZFC}},
principalmente perché a $\cal U$ non è
richiesto di soddisfare alcuna forma dell'Assioma di
Rimpiazzamento\index{assioma di rimpiazzamento}.
Di fatto, è possibile dimostrare l'esistenza di un insieme
$\cal U$ con le proprietà di sopra dagli assiomi di \theory{ZFC}.
(Per esempio si potrebbe considerare $\cal U$ consistere di tutti gli insiemi non vuoti
nella gerarchia cumulativa di von~Neumann formata prima della fase
$\omega+\omega$.) Così, come per altri pezzi della matematica, è
possibile in linea di principio dare una versione completamente formale all'interno
della teoria degli insiemi \theory{ZFC} della semantica della logica \HOL{} che sarà fornita
di sotto.

\section{Tipi}
\label{types}

I tipi\index{vincolo di tipo!nella logica HOL@nella logica \HOL{}} della
logica \HOL{} sono espressioni che denotano insiemi (nell'universo  $\cal U$).
Seguendo la tradizione,
$\sigma$, possibilmente decorato con sottoscritti o primi, è usato per
variare su tipi arbitrari.

Ci sono quattro specie di tipi nella logica \HOL{}. Questi possono essere descritti
informalmente dalla seguente grammatica {\small BNF},
in cui $\alpha$ varia
su variabili di tipo, \textsl{c} varia su tipi atomici e \textsl{op} varia su
operatori di tipo.

\newlength{\ttX}
\settowidth{\ttX}{\tt X}
\newcommand{\tyvar}{\setlength{\unitlength}{\ttX}\begin{picture}(1,6)
\put(.5,0){\makebox(0,0)[b]{\footnotesize variabili di tipo}}
\put(0,1.5){\vector(0,1){4.5}}
\end{picture}}
\newcommand{\tyatom}{\setlength{\unitlength}{\ttX}\begin{picture}(1,6)
\put(.5,2.3){\makebox(0,0)[b]{\footnotesize tipi atomici}}
\put(.5,3.3){\vector(0,1){2.6}}
\end{picture}}
\newcommand{\funty}{\setlength{\unitlength}{\ttX}\begin{picture}(1,6)
\put(.5,1.5){\makebox(0,0)[b]{\footnotesize tipi funzione}}
\put(.5,0){\makebox(0,0)[b]{\footnotesize (dominio $\sigma_1$, rango $\sigma_2$)}}
\put(1,2.5){\vector(0,1){3.5}}
\end{picture}}
\newcommand{\cmpty}{\setlength{\unitlength}{\ttX}\begin{picture}(1,6)
\put(2,3.3){\makebox(0,0)[b]{\footnotesize tipi composti}}
\put(1.9,4.5){\vector(0,1){1.5}}
\end{picture}}
%
$$\sigma\quad ::=\quad {\mathord{\mathop{\alpha}\limits_{\tyvar}}}
        \quad\mid\quad{\mathord{\mathop{c}\limits_{\tyatom}}}
        \quad\mid\quad\underbrace{(\sigma_1, \ldots , \sigma_n){op}}_{\cmpty}
        \quad\mid\quad\underbrace{\sigma_1\fun\sigma_2}_{\funty}$$

\noindent In maggiore dettaglio, le quattro specie di tipi sono come segue.

\begin{enumerate}

\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
arbitrari nell'universo. Nella formulazione originale di Church della teoria dei tipi
semplici, le variabili di tipo sono parte del meta-linguaggio e sono usate per
variare su tipi del linguaggio oggetto. Le dimostrazioni contenenti variabili di tipo
erano concepite come schemi di dimostrazione (cioè famiglie di dimostrazioni). Per supportare
tali schemi di dimostrazione {\it all'interno} della logica \HOL{}, le variabili di tipo sono
state aggiunte al sistema di tipi del linguaggio oggetto\footnote{Questa tecnica
fu inventata da Robin Milner per la logica oggetto \PPL\ del suo sistema
\LCF.}.

\item {\bf Tipi atomici:}\index{tipi atomici} questi denotano insiemi fissati nell'universo. Ogni
teoria determina una particolare collezione di tipi atomici. Per
esempio, i tipi atomici standard \ty{bool} e \ty{ind} denotano,
rispettivamente, l'insieme distinto di due elementi $\two$ e
l'insieme distinto infinito $\inds$.

\item {\bf Tipi composti:}\index{tipi composti, nella logica HOL@tipi composti, nella logica \HOL{}!forma astratta di} questi hanno la
forma $(\sigma_1,\ldots,\sigma_n)\ty{op}$, dove $\sigma_1$, $\dots$,
$\sigma_n$ sono i tipi argomento e $op$ è un {\it operatore di tipo\/}
di arietà $n$. Gli operatori di tipo denotano operazioni per costruire insiemi.
Il tipo $(\sigma_1,\ldots,\sigma_n)\ty{op}$ denota l'insieme che risulta
dall'applicare l'operazione denotata da $op$ agli insiemi denotati da
$\sigma_1$, $\dots$, $\sigma_n$. Per esempio,
\ty{list} è un operatore di tipo con arietà 1. Esso denota l'operazione
di formare tutte le liste finite di elementi da un dato insieme. Un altro
esempio è l'operatore \ty{prod} di arietà 2 che denota
l'operazione di prodotto cartesiano. Il tipo $(\sigma_1,\sigma_2)\ty{prod}$
è scritto come $\sigma_1\times\sigma_2$.

\item {\bf Tipi funzione:}\index{tipi funzione, nella logica HOL@tipi funzione, nella logica \HOL{}!forma astratta di} Se $\sigma_1$
e $\sigma_2$ sono tipi, allora $\sigma_1\fun\sigma_2$ è il tipo
funzione con {\it dominio\/} $\sigma_1$ e {\it rango} $\sigma_2$. Esso
denota l'insieme di tutte le funzioni (totali) dall'insieme denotato dal suo
dominio all'insieme denotato dal suo rango. (Nella letteratura
$\sigma_1\fun\sigma_2$ è scritto senza la freccia e
alla rovescia--cioè come $\sigma_2\sigma_1$.) Si noti che sintatticamente
$\fun$ è semplicemente un distinto operatore di tipo di arietà 2 scritto con
notazione infissa. E' isolato nella definizione dei tipi \HOL{}
perché denoterà sempre la stessa operazione in qualsiasi
modello di una teoria \HOL{}---contrariamente agli altri operatori di tipo che
possono essere interpretati in modo differente in modelli differenti. (Si veda
la Sezione~\ref{semantics of types}.)

\end{enumerate}

Risulta conveniente identificare i tipi atomici con
tipi composto costruiti con operatori di tipo $0$-ari. Per esempio,
il tipo atomico \ty{bool} dei valori di verità può essere considerato come
un'abbreviazione per $()\ty{bool}$. Questa identificazione sarà fatta nei
dettagli tecnici che seguono, ma nella presentazione informale
i tipi atomici continueranno ad essere distinti dai tipi composti,
e $()c$ sarà scritto come $c$.

\subsection{Strutture di tipo}
\label{type structures}
\index{struttura di tipo, nella logica HOL@struttura di tipo, nella logica \HOL{}}

Il termine `costante di tipo' è usato per comprendere sia i tipi atomici sia gli operatori
di tipo. Si assume che sia dato un insieme infinito {\sf
TyNames} dei {\em nomi delle costanti di tipo\/}. La lettera
greca $\nu$ è usata per variare su membri arbitrari di {\sf TyNames},
si continuerà ad usare \textsl{c} per variare sui nomi dei tipi
atomici (cioè costanti di tipo $0$-ari), e \textsl{op} è usato per variare
sui nomi degli operatori di tipo (cioè costanti di tipo $n$-arie, dove
$n>0$).

Si assume che sia dato un insieme infinito {\sf TyVars} di {\em variabili
di tipo\/}\index{variabili di tipo, nella logica HOL@variabili di tipo, nella logica \HOL{}}.
Le lettere greche $\alpha,\beta,\ldots$, possibilmente con indici
sottoscritti o apici, sono usate per variare su {\sf Tyvars}. Gli insiemi
{\sf TyNames} e {\sf TyVars} sono assunti disgiunti.

Una {\it struttura di tipo\/} è un insieme $\Omega$ di costanti di tipo. Una {\it costante
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
nome della costante e $n$ è la sua arietà. Così $\Omega\subseteq{\sf
TyNames}\times\natnums$ (dove $\natnums$ è l'insieme dei numeri
naturali). Si assume che non esistano due distinte costanti di tipo che hanno lo
stesso nome
cioé ogni volta che $(\nu, n_1)\in\Omega$ e
$(\nu, n_2)\in\Omega$, allora $n_1 = n_2$.

L'insieme {\sf Types}$_{\Omega}$ dei tipi su una struttura ${\Omega}$
può ora essere definito come il più piccolo insieme tale che:

\begin{itemize}

\item {\sf TyVars}$\ \subseteq\ ${\sf Types}$_{\Omega}$.

\item Se $(\nu,0)\in\Omega$ allora $()\nu\in{\sf Types}_{\Omega}$.

\item Se $(\nu,n)\in\Omega$ e $\sigma_i\in{\sf Types}_{\Omega}$ per
$1\leq i\leq n$, allora $(\sigma_1,\ \ldots\ ,\sigma_n)\nu\in{\sf
Types}_{\Omega}$.

\item Se $\sigma_1\in{\sf Types}_{\Omega}$ e $\sigma_2\in{\sf
Types}_{\Omega}$ allora $\sigma_1\fun\sigma_2\in{\sf Types}_{\Omega}$.


\end{itemize}
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
destra, così che
\[
\sigma_1\fun\sigma_2\fun\ldots\fun \sigma_n\fun\sigma
\]
abbrevia
\[
\sigma_1\fun(\sigma_2\fun\ldots\fun (\sigma_n\fun\sigma)\ldots)
\]
La notazione $tyvars(\sigma)$ è usata per denotare l'insieme delle variabili
di tipo che occorrono in $\sigma$.

\subsection{Semantica dei tipi}
\label{semantics of types}


Un {\em modello} $M$ di una struttura di tipo $\Omega$ è specificato dando
per ogni costante di tipo $(\nu,n)$ una funzione $n$-aria
\[
M(\nu):{\cal U}^{n}\longrightarrow{\cal U}
\]
Così dati gli insiemi $X_1,\ldots,X_n$ nell'universo $\cal U$,
$M(\nu)(X_1,\ldots,X_n)$ è anche un insieme nell'universo. Nel caso $n=0$,
questo equivale a specificare un elemento $M(\nu)\in{\cal U}$ per il
tipo atomico $\nu$.

I tipi che non contengono alcuna variabile di tipo sono chiamati {\it monomorfici},
mentre quelli che contengono variabili di tipo sono chiamati {\it
polimorfici}\index{tipi polimorfici, nella logica HOL@tipi polimorfici, nella logica \HOL{}}\index{tipo, nella logica HOL@tipo, nella logica \HOL{}!polimorfico}. Qual è il
significato di un tipo polimorfico? Si può
dire quale insieme denota un tipo polimorfico solo una volta che si sono istanziate
le sue variabili di tipo su insiemi particolari. Così il suo significato complessivo non è un
singolo insieme, ma è piuttosto una funzione con valori su insiemi ${\cal
U}^{n}\longrightarrow{\cal U}$, che assegna un insieme per ogni particolare
assegnazione di insiemi alle variabili di tipo rilevanti. L'arietà $n$
corrisponde al numero di variabili di tipo coinvolte. E' conveniente
in tale contesto essere in grado di considerare che una variabile di tipo sia
coinvolta nella semantica di un tipo $\sigma$ sia che occorra effettivamente
in $\sigma$ sia che non occorra in esso, portando alla nozione di un
tipo-in-contesto.

Un {\em contesto di tipo}\index{contesto di tipo}, $\alpha\!s$, è semplicemente una
lista finita (possibilmente vuota) di variabili di tipo {\em distinte\/}
$\alpha_{1},\ldots,\alpha_{n}$. Un {\em
tipo-in-contesto\/}\index{tipo-in-contesto} è una coppia, scritta
$\alpha\!s.\sigma$, dove $\alpha\!s$ è un contesto di tipo, $\sigma$ è un
tipo (su una data struttura di tipo) e tutte le variabili di tipo
che occorrono in $\sigma$ appaiono da qualche parte nella lista $\alpha\!s$. La
lista $\alpha\!s$ può anche contenere variabili di tipo che non occorrono in
$\sigma$.

Per ogni $\sigma$ ci sono dei contesti minimi $\alpha\!s$ per cui
$\alpha\!s.\sigma$ è un tipo-in-contesto, che differiscono solo per l'ordine
in cui le variabili di tipo di $\sigma$ sono elencate in $\alpha\!s$. Al
fine di selezionare uno di tali contesti, assumiamo che {\sf TyVars}
venga con un fissato ordine totale e definiamo il contesto {\em
canonico}\index{contesti canonici, nella logica HOL@contesti canonici, nella logica \HOL{}!dei tipi} del tipo $\sigma$ in modo che esso consista esattamente
delle variabili di tipo che esso contiene, elencate in ordine\footnote{E'
possibile lavorare con contesti non ordinati, specificati da insiemi finiti
piuttosto che liste, ma scegliamo di non fare questo dal momento che complica
moderatamente la definizione della semantica che sarà data di
sotto}.

Sia $M$ un modello di una struttura di tipo $\Omega$. Per ogni
tipo-in-contesto
$\alpha\!s.\sigma$ su $\Omega$, definiamo una funzione
\[
\den{\alpha\!s.\sigma}_{M}:{\cal U}^{n}\longrightarrow{\cal U}
\]
(dove $n$ è la lunghezza del contesto) per induzione sulla struttura
di $\sigma$ come segue.
\begin{itemize}

\item Se $\sigma$ è una variabile di tipo, essa deve essere $\alpha_{i}$ per qualche unico
$i=1,\ldots,n$ e allora $\den{\alpha\!s.\sigma}_{M}$ è la $i$\/esima
funzione di proiezione, che manda $(X_{1},\ldots,X_{n})\in{\cal U}^{n}$
a $X_{i}\in{\cal U}$.

\item Se $\sigma$ è un tipo funzione\index{tipi funzione, nella logica HOL@tipi funzione, nella logica \HOL{}!semantica formale dei}
$\sigma_{1}\fun\sigma_{2}$, allora $\den{\alpha\!s.\sigma}_M$ manda
$X\!s\in{\cal U}^n$ all'insieme di tutte le funzioni
da $\den{\alpha\!s.\sigma_1}_M(X\!s)$ a
$\den{\alpha\!s.\sigma_2}_M(X\!s)$. (Questo fa
uso della proprietà {\bf Fun} di $\cal U$.)

\item Se $\sigma$ è un
tipo composto $(\sigma_{1},\ldots,\sigma_{m})\nu$, allora
$\den{\alpha\!s.\sigma}_{M}$ manda $X\!s$ a
$M(\nu)(S_{1},\ldots,S_{m})$ dove ogni $S_{j}$ è
$\den{\alpha\!s.\sigma_{j}}_{M}(X\!s)$.
\end{itemize}
Si può ora definire che il significato di un tipo $\sigma$ in un modello $M$ è
la funzione
\[
\den{\sigma}_{M}:{\cal U}^{n}\longrightarrow{\cal U}
\]
data da $\den{\alpha\!s.\sigma}_{M}$, dove $\alpha\!s$ è il
contesto canonico di $\sigma$. Se $\sigma$ è monomorfico, allora $n=0$
e $\den{\sigma}_{M}$ può essere identificato con l'elemento
$\den{\sigma}_{M}()$ di $\cal U$. Quando il particolare modello $M$ è
chiaro dal contesto, $\den{\_}_{M}$ sarà scritto $\den{\_}$.

Per riassumere, dato un modello in $\cal U$ di una struttura di tipo $\Omega$,
la semantica interpreta i tipi monomorfici su $\Omega$ come gli insiemi in
$\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
U}^{n}\longrightarrow{\cal U}$ sull'universo. I tipi funzione sono
interpretati da insiemi di funzioni complete.

\medskip

\noindent{\bf Esempi\ }
Supponiamo che $\Omega$ contenga una costante di tipo $(\textsl{b},0)$ e che
il modello $M$ assegni l'insieme $\two$ a $\textsl{b}$. Allora:
\begin{enumerate}

\item $\den{\textsl{b}\fun\textsl{b}\fun\textsl{b}}=\two\fun\two\fun\two\in{\cal U}$.

\item $\den{(\alpha\fun\textsl{b})\fun\alpha}:{\cal U}\longrightarrow{\cal U}$
è la funzione che manda $X\in{\cal U}$ a $(X\fun\two)\fun X\in{\cal U}$.

\item $\den{\alpha,\beta . (\alpha\fun\textsl{b})\fun\alpha}:{\cal
U}^{2}\longrightarrow{\cal U}$ è la funzione che manda $(X,Y)\in{\cal
U}^{2}$ a $(X\fun\two)\fun X\in{\cal U}$.

\end{enumerate}

\medskip

\noindent{\bf Nota\ }
Un approccio più tradizionale alla semantica implicherebbe dare
dei significati ai tipi in presenza di `ambienti' che assegnano insiemi in
$\cal U$ a tutte le variabili di tipo. L'uso di tipi-in-contesti è quasi
la stessa cosa di usare ambienti parziali con domini finiti---è
solo che il contesto vincola il dominio ammissibile a un particolare
insieme finito (ordinato) di variabili di tipo. Al livello dei tipi non c'è
molto da scegliere tra i due approcci. Tuttavia per la sintassi
e la semantica dei termini che sarà data di sotto, dove c'è una dipendenza
sia dalle variabili di tipo sia dalle variabili individuali, l'approccio usato
qui sembra migliore.

\subsection{Istanze e sostituzione}
\label{instances-and-substitution}

Se $\sigma$ e $\tau_1,\ldots,\tau_n$ sono tipi su una struttura di tipo
$\Omega$,
\[
\sigma[\tau_{1},\ldots,\tau_{p}/\beta_{1},\ldots,\beta_{p}]
\]
denoterà il tipo risultante dalle sostituzioni simultanee per
ogni $i=1,\ldots,p$ di
$\tau_i$ per la variabile di tipo $\beta_i$ in $\sigma$.
Il tipo risultante è chiamato una {\it istanza\/}\index{tipi, nella logica HOL@tipi, nella logica \HOL{}!istanziazione di} di $\sigma$. Il
seguente lemma circa le istanze sarà utile più avanti; esso è dimostrato per
induzione sulla struttura di $\sigma$.

\medskip

\noindent{\bf Lemma 1\ }{\it
Supponiamo che $\sigma$ sia un tipo che contiene le variabili di tipo distinte
$\beta_1,\ldots,\beta_p$ e che
$\sigma'=\sigma[\tau_{1},\ldots,\tau_{n}/\beta_1,\ldots,\beta_p]$ sia
un'istanza di $\sigma$. Allora i tipi $\tau_1,\ldots,\tau_p$ sono
determinati univocamente da $\sigma$ e $\sigma'$.
}

\medskip

Abbiamo anche bisogno di sapere come la semantica dei tipi si comporta rispetto
alla sostituzione:

\medskip

\noindent{\bf Lemma 2\ }{\it Dati i tipi-in-contesto $\beta\!s.\sigma$ e
$\alpha\!s.\tau_i$ ($i=1,\ldots,p$, dove $p$ è la
lunghezza di $\beta\!s$), sia $\sigma'$ l'istanza
$\sigma[\tau\!s/\beta\!s]$. Allora anche $\alpha\!s.\sigma'$ è un
tipo-in-contesto e il suo significato in qualsiasi modello $M$ è collegato a quello di
$\beta\!s.\sigma$ come segue. Per tutti gli $X\!s\in{\cal U}^n$ (dove $n$
è la lunghezza di $\alpha\!s$)
\[
\den{\alpha\!s.\sigma'}(X\!s) =
\den{\beta\!s.\sigma}(\den{\alpha\!s.\tau_{1}}(X\!s),
    \ldots ,\den{\alpha\!s.\tau_{p}}(X\!s))
\]
}
Ancora una volta, il lemma può essere dimostrato per induzione sulla struttura di
$\sigma$.

\section{Termini}
\label{terms}

I termini della logica \HOL{} sono espressioni che denotano elementi degli insiemi
denotati dai tipi. La meta-variabile $t$
è usata per variare su termini arbitrari, possibilmente decorata
con indici sottoscritti o apici.

Ci sono quattro specie di termini nella logica \HOL{}. Queste possono essere
descritte approssimativamente nella seguente grammatica {\small BNF}, in
cui $x$ varia su variabili e $c$ varia su costanti.
\index{combinazioni, nella logica HOL@combinazioni, nella logica \HOL{}!forma astratta di}

\settowidth{\ttX}{\tt X}
\newcommand{\var}{\setlength{\unitlength}{\ttX}\begin{picture}(1,6)
\put(.5,0){\makebox(0,0)[b]{\footnotesize variabili}}
\put(0,1.5){\vector(0,1){4.5}}
\end{picture}}
\newcommand{\const}{\setlength{\unitlength}{\ttX}\begin{picture}(1,6)
\put(.5,2.3){\makebox(0,0)[b]{\footnotesize costanti}}
\put(.5,3.5){\vector(0,1){2.4}}
\end{picture}}
\newcommand{\app}{\setlength{\unitlength}{\ttX}\begin{picture}(1,6)
\put(.5,1.5){\makebox(0,0)[b]{\footnotesize applicazioni di funzione}}
\put(.5,0){\makebox(0,0)[b]{\footnotesize (funzione $t$, argomento $t'$)}}
\put(0.5,2.5){\vector(0,1){3.5}}
\end{picture}}
\newcommand{\abs}{\setlength{\unitlength}{\ttX}\begin{picture}(1,6)
\put(1,3.3){\makebox(0,0)[b]{\footnotesize $\lambda$-astrazioni}}
\put(0.7,4.5){\vector(0,1){1.5}}
\end{picture}}
%
$$ t \quad ::=\quad {\mathord{\mathop{x}\limits_{\var}}}
        \quad\mid\quad{\mathord{\mathop{\con{c}}\limits_{\const}}}
        \quad\mid\quad\underbrace{t\ t'}_{\app}
        \quad\mid\quad\underbrace{\lambda x .\ t}_{\abs}$$

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
una funzione $v\mapsto t[v/x]$, dove $t[v/x]$ denota il risultato di
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
risultato di applicare la
funzione denotata da $t$ al valore denotato da $t'$. Questo sarà
reso più preciso di sotto.

La grammatica {\small BNF} appena data omette di menzionare i tipi. Di fatto, ogni
termine nella
logica \HOL{} è associato con un unico tipo.
La notazione $t_{\sigma}$ è
tradizionalmente usata per variare su termini di tipo $\sigma$. Una
grammatica più accurata dei
termini è:

$$ t_{\sigma} \quad ::=\quad {\mathord{\mathop{x_{\sigma}}\limits_{}}}
\quad\mid\quad
{\mathord{\mathop{\con{c}_{\sigma}}\limits_{}}}
\quad\mid\quad (t_{\sigma'\fun\sigma}\ t'_{\sigma'})_{\sigma}
\quad\mid\quad(\lambda x_{\sigma_1} .\ t_{\sigma_2})
_{\sigma_1\fun\sigma_2}$$\index{costanti, nella logica HOL@costanti, nella logica \HOL{}!forma astratta di}

Di fatto, esattamente come la definizione dei tipi era relativa a una particolare
struttura di tipo $\Omega$, la definizione formale dei termini è relativa a
una data collezione di costanti tipizzate su $\Omega$. Assumiamo che sia dato
un insieme infinito {\sf Names} di nomi. Una {\em costante\/} su
$\Omega$ è una coppia $(\con{c}, \sigma)$, dove $\con{c}\in{\sf Names}$
e $\sigma\in{\sf Types}_{\Omega}$. Una {\em firma} su $\Omega$
è semplicemente un insieme $\Sigma_\Omega$ di tali costanti.

L'insieme {\sf Terms}$_{\Sigma_{\Omega}}$ di termini su
$\Sigma_{\Omega}$ è definito essere il più piccolo insieme chiuso sotto le
seguenti regole di formazione:
\begin{enumerate}

\item {\bf Costanti:} Se $(\con{c},\sigma)\in{\Sigma_{\Omega}}$ e
$\sigma'\in{\sf Types}_{\Omega}$
è un'istanza di $\sigma$, allora $(\con{c},{\sigma'})\in{\sf
Terms}_{\Sigma_{\Omega}}$. I termini formati in questo modo sono chiamati {\it
costanti\/}\index{costanti, nella logica HOL@costanti, nella logica \HOL{}!forma astratta di} e sono scritti $\con{c}_{\sigma'}$.

\item {\bf Variabili:}  Se  $x\in{\sf  Names}$  e  $\sigma\in{\sf
Types}_{\Omega}$, allora ${\tt var}\ x_{\sigma}\in{\sf
Terms}_{\Sigma_{\Omega}}$. I termini formati in questo modo sono chiamati {\it
variabili}\index{variabili, nella logica HOL@variabili, nella logica \HOL{}!forma astratta di}.  Il marcatore {\tt var}\ è semplicemente un accorgimento per
distinguere le variabili da costanti con lo stesso nome.  Una variabile
${\tt var}\ x_{\sigma}$ sarà di solito scritta come $x_{\sigma}$, se
è chiaro dal contesto che $x$ è una variabile piuttosto che una
costante

\item {\bf Applicazioni di funzione:}  Se $t_{\sigma'{\fun}\sigma}\in{\sf
Terms}_{\Sigma_{\Omega}}$ e $t'_{\sigma'}\in{\sf
Terms}_{\Sigma_{\Omega}}$, allora $(t_{\sigma'\fun\sigma}\
t'_{\sigma'})_{\sigma}\in {\sf Terms}_{\Sigma_{\Omega}}$.
(I termini formati in questo modo sono chiamati {\it combinazioni}.)

\item {\bf $\lambda$-Astrazioni:} Se ${\tt var}\ x_{\sigma_1}
\in{\sf Terms}_{\Sigma_{\Omega}}$  e $t_{\sigma_2}\in{\sf
Terms}_{\Sigma_{\Omega}}$, allora $(\lambda x_{\sigma_1}.\
t_{\sigma_2})_{\sigma_1\fun\sigma_2}
\in{\sf Terms}_{\Sigma_{\Omega}}$.

\end{enumerate}

Si noti che è possibile avere costanti e variabili\index{variabili, nella logica HOL@variabili, nella logica \HOL{}!con gli stessi nomi}
con lo stesso nome. E' anche possibile avere variabili differenti con
lo stesso nome, se esse hanno tipi differenti.

Il tipo sottoscritto a un termine può essere omesso se è chiaro dalla
struttura del termine o dal contesto in cui occorre quale deve essere il
suo tipo.

L'applicazione di funzione\index{applicazione di funzione, nella logica HOL@applicazione di funzione, nella logica \HOL{}!associatività della} è assunta associare
a sinistra, così che $t\ t_1\ t_2\ \ldots\ t_n$ abbrevia $(\
\ldots\ ((t\ t_1)\ t_2)\ \ldots\ t_n)$.

La notazione $\lambda x_1\ x_2\ \cdots\ x_n.\ t$ abbrevia $\lambda
x_1.\ (\lambda x_2.\ \cdots\ (\lambda x_n.\ t)\ \cdots\ )$.

Un termine è chiamato polimorfico\index{termini polimorfici, nella logica HOL@termini polimorfici, nella logica \HOL{}} se contiene una variabile
di tipo. Altrimenti è chiamato monomorfico. Si noti che un termine
$t_{\sigma}$ può essere polimorfico anche se $\sigma$ è
monomorfico -- per esempio,
$(f_{\alpha\fun\textsl{b}}\ x_{\alpha})_{\textsl{b}}$, dove $\textsl{b}$ è un tipo atomico. L'espressione
$tyvars(t_{\sigma})$ denota l'insieme di variabili di tipo che occorrono in
$t_{\sigma}$.

L'occorrenza di una variabile $x_{\sigma}$ è chiamata {\it
legata\/}\index{variabili legate, nella logica HOL@variabili legate, nella logica \HOL{}}\index{variabili, nella logica HOL@variabili, nella logica \HOL{}!forma astratta di}
 se essa occorre all'interno dello scopo di una $\lambda x_{\sigma}$
che chiude dal punto di vista testuale, altrimenti l'occorrenza è chiamata {\it
libera\/}\index{variabili libere, nella logica HOL@variabili libere, nella logica \HOL{}!forma astratta di}. Si noti che $\lambda x_{\sigma}$ non lega
$x_{\sigma'}$ se $\sigma\neq \sigma'$. Un termine in cui tutte le occorrenze
delle variabili sono legate è chiamato {\it chiuso\/}.

\subsection{Termini-in-contesto}
\label{terms-in-context}

Un {\em contesto\/}\index{contesti, nella semantica della logica HOL@contesti, nella semantica della logica \HOL{}} $\alpha\!s,\!x\!s$ consiste di un contesto
di tipo $\alpha\!s$ insieme con una lista $x\!s=x_{1},\ldots,x_{m}$ di
variabili distinte i cui tipi contengono solo variabili di tipo dalla
lista $\alpha\!s$.

La condizione che $x\!s$ contenga variabili {\em distinte\/} necessita
di qualche commento. Dal momento che una variabile è specificata sia da un nome sia da un
tipo, è permesso che $x\!s$ contenga
nomi\index{variabili, nella logica HOL@variabili, nella logica \HOL{}!con gli stessi nomi} ripetuti,
 purché ai nomi siano attaccati tipi
differenti. Questo aspetto della sintassi  significa che si deve procedere con
cautela quando si definisce il significato dell'istanziazione delle variabili di tipo,
dal momento che l'istanziazione può far sì che delle variabili diventino uguali
`accidentalmente'. Si veda la Sezione~\ref{term-substitution}.

Un {\em termine-in-contesto\/}\index{term-in-context}
$\:\;\alpha\!s,\!x\!s.t\;\:$ consiste di un contesto insieme con un termine
$t$ che soddisfa le seguenti condizioni:
\begin{itemize}

\item $\alpha\!s$ contiene qualsiasi variabile di tipo che occorre in $x\!s$ e $t$.

\item $x\!s$ contiene qualsiasi variabile che occorre libera in $t$.

\item $x\!s$ non contiene alcuna variabile che occorre
legata in $t$.

\end{itemize}
Il contesto $\alpha\!s,\!x\!s$ può contenere variabili (di tipo) che
non appaiono in $t$. Si noti che la combinazione della seconda e della terza
condizione implica che una variabile non può avere occorrenze sia libere sia
legate in $t$. Per un termine arbitrario, c'è sempre un
termine $\alpha$-equivalente che soddisfa questa condizione, ottenuto
rinominando le variabili legate in caso di necessità\footnote{Si ricordi che due
termini sono detti essere $\alpha$-equivalenti se differiscono soltanto nei
nomi delle loro variabili legate.}. Nella semantica dei termini che sarà
data di seguito restringeremo l'attenzione a tali termini. Quindi il significato di un
termine arbitrario è considerato essere il significato di qualche $\alpha$-variante di
esso non avente variabili sia libere sia legate. (La semantica uguaglierà
le $\alpha$-varianti, così che non importa quale è scelta.) Evidentemente
per un tale termine c'è un contesto minimale $\alpha\!s,\!x\!s$, unico
a meno dell'ordine in cui le variabili sono elencate, per il quale
$\alpha\!s,\!x\!s.t$ è un termine-in-contesto. Come per le variabili di tipo,
assumeremo dato un fissato ordine totale sulle variabili. Quindi l'unico
contesto minimo con le variabili elencate in ordine sarà chiamato il contesto {\em
canonico}\index{contesti canonici, nella logica HOL@contesti canonici, nella logica \HOL{}!di termini} del termine $t$.

\subsection{Semantica dei termini}
\label{semantics of terms}

Sia $\Sigma_{\Omega}$ una firma\index{firme, della logica HOL@firme, della logica \HOL{}!semantica formale delle} su una struttura
di tipo $\Omega$ (si veda la Sezione~\ref{terms}). Un {\em modello\/} $M$ di
$\Sigma_{\Omega}$ è specificato da un modello della struttura di tipo più
per ogni costante\index{costanti primitive, della logica HOL@costanti primitive, della logica \HOL{}} $(\con{c},\sigma)\in\Sigma_{\Omega}$ un
elemento
\[
M(\con{c},\sigma) \in
\prod_{X\!s\in{\cal U}^{n}}\den{\sigma}_{M}(X\!s)
\]
del prodotto cartesiano indicato, dove $n$ è il numero delle variabili
di tipo che occorrono in $\sigma$. In altre parole
$M(\con{c},\sigma)$ è una funzione (dipendentemente tipizzata)
che assegna ad ogni $X\!s\in{\cal U}^{n}$ un elemento di
$\den{\sigma}_{M}(X\!s)$. Nel caso che $n=0$ (così che
$\sigma$ è monomorfico), $\den{\sigma}_{M}$ era identificato
con un insieme in $\cal U$ e quindi $M(c,\sigma)$ può essere
identificato con un elemento di quell'insieme.

Il significato dei termini \HOL{} in un tale modello sarà ora descritto. La
semantica interpreta termini chiusi che non coinvolgono variabili di tipo come
elementi di insiemi in $\cal U$ (il particolare insieme coinvolto essendo derivato
dal tipo del termine come nella Sezione~\ref{semantics of types}). Più
in generale, se il termine chiuso coinvolge $n$ variabili di tipo allora è
interpretato come un elemento di un prodotto $\prod_{X\!s\in{\cal
U}^{n}}Y(X\!s)$, dove la funzione $Y:{\cal U}^{n}\longrightarrow{\cal
U}$ è derivata dal tipo del termine (in un contesto di tipo derivato
dal termine). Così il significato del termine è una funzione (dipendentemente tipizzata)
che, quando applicata a qualsiasi significato scelto per le variabili
di tipo nel termine, dà un significato per il termine come un elemento di un
insieme in $\cal U$. Dall'altro lato, se il termine coinvolge $m$ variabili
libere ma nessuna variabile di tipo, allora è interpretato come una funzione
$Y_1\times\cdots\times Y_m\fun Y$ dove gli insiemi $Y_1,\ldots,Y_m$ in
$\cal U$ sono interpretazioni dei tipi delle variabili libere nel
termine e l'insieme $Y\in{\cal U}$ è l'interpretazione del tipo del
termine; così il significato del termine è una funzione che, quando
applicata a qualsiasi significato scelto per le variabili libere nel termine,
dà un significato per il termine. Infine, il caso più generale è quello di un
termine che coinvolge $n$ variabili di tipo e $m$ variabili libere: esso è
interpretato come un elemento di un prodotto
\[
\prod_{X\!s\in{\cal
U}^{n}}Y_{1}(X\!s)\times\cdots\times Y_{m}(X\!s) \;\fun\; Y(X\!s)
\]
dove le funzioni $Y_{1},\ldots,Y_{m},Y:{\cal
U}^{n}\longrightarrow{\cal U}$ sono determinati dai tipi delle variabili
libere e dal tipo del termine (in un conteso di tipo derivato dal
termine).

Più precisamente, dato un termine-in-contesto $\alpha\!s,\!x\!s.t$
su $\Sigma_{\Omega}$ supponiamo che
\begin{itemize}

\item $t$ abbia il tipo $\tau$

\item $x\!s=x_{1},\ldots,x_{m}$ ed ogni $x_{j}$ abbia il tipo $\sigma_{j}$

\item $\alpha\!s=\alpha_{1},\ldots,\alpha_{n}$.

\end{itemize}
Allora dal momento che $\alpha\!s,\!x\!s.t$ è un termine-in-contesto, $\alpha\!s.\tau$
e $\alpha\!s.\sigma_{j}$ sono tipi-in-contesto, e quindi danno origine
a funzioni $\den{\alpha\!s.\tau}_{M}$ e
$\den{\alpha\!s.\sigma_{j}}_{M}$ da ${\cal U}^{n}$ a $\cal U$ come nella
sezione~\ref{semantics of types}. Il significato di $\alpha\!s,\!x\!s.t$
nel modello $M$ sarà dato da un elemento
\[
\den{\alpha\!s,\!x\!s.t}_{M} \in \prod_{X\!s\in{\cal U}^{n}}
\left(\prod_{j=1}^{m}\den{\alpha\!s.\sigma_{j}}_{M}(X\!s)\right)
\fun \den{\alpha\!s.\tau}_{M}(X\!s) .
\]
In altre parole, dato
\begin{eqnarray*}
X\!s & = & (X_{1},\ldots,X_{n})\in{\cal U}^{n} \\
y\!s & = & (y_{1},\ldots,y_{m})\in\den{\alpha\!s.\sigma_{1}}_{M}(X\!s)
           \times\cdots\times \den{\alpha\!s.\sigma_{m}}_{M}(X\!s)
\end{eqnarray*}
si ottiene un elemento $\den{\alpha\!s,\!x\!s.t}_{M}(X\!s)(y\!s)$ di
$\den{\alpha\!s.\tau}_{M}(X\!s)$. La definizione di
$\den{\alpha\!s,\!x\!s.t}_{M}$ procede per induzione sulla struttura del
termine $t$ come segue. (Come prima, il sottoscritto $M$ sarà omesso dalle
parentesi semantiche $\den{ \_ }$ quando il particolare modello coinvolto è
chiaro dal contesto.)
\begin{itemize}

\item
Se $t$ è una variabile\index{variabili, nella logica HOL@variabili, nella logica \HOL{}!semantica formale delle}, deve essere $x_{j}$ per qualche unico
$j=1,\ldots,m$, so $\tau=\sigma_{j}$ e allora
$\den{\alpha\!s,\!x\!s.t}(X\!s)(y\!s)$ è definito essere $y_{j}$.

\item
Supponiamo che $t$ sia una costante\index{costanti, nella logica HOL@costanti, nella logica \HOL{}!semantica formale delle} $\con{c}_{\sigma'}$, dove
$(\con{c},\sigma)\in\Sigma_{\Omega}$ e $\sigma'$ è un'istanza di
$\sigma$.  Allora per il Lemma~1 di \ref{instances-and-substitution},
$\sigma'=\sigma[\tau_{1},\ldots,\tau_{p}/\beta_{1},\ldots,\beta_{p}]$
per tipi univocamente determinati $\tau_{1},\ldots,\tau_{p}$ (dove
$\beta_{1},\ldots,\beta_{p}$ sono le variabili di tipo che occorronoin
$\sigma$). Allora definiamo $\den{\alpha\!s,\!x\!s.t}(X\!s)(y\!s)$ essere
$M(\con{c},\sigma)(\den{\alpha\!s.\tau_{1}}(X\!s),
\ldots,\den{\alpha\!s.\tau_{p}}(X\!s))$,
che è un elemento di $\den{\alpha\!s.\tau}(X\!s)$ per il Lemma~2 di
\ref{instances-and-substitution} (dal momento che $\tau$ è $\sigma'$).

\item
Supponiamo che $t$ sia un termine applicazione di funzione\index{combinazioni, nella logica HOL@combinazioni, nella logica \HOL{}!semantica formale delle} $(t_{1}\
t_{2})$\index{applicazione di funzione, nella logica HOL@applicazione di funzione, nella logica \HOL{}!semantica formale delle} dove $t_{1}$ è di tipo
$\tau'\fun\tau$ e $t_{2}$ è di tipo $\tau'$. Allora
$f=\den{\alpha\!s,\!x\!s.t_{1}}(X\!s)(y\!s)$, essendo un elemento di
$\den{\alpha\!s.\tau'\fun\tau}(X\!s)$, è una funzione dall'insieme
$\den{\alpha\!s.\tau'}(X\!s)$ all'insieme $\den{\alpha\!s.\tau}(X\!s)$
che si può applicare all'elemento
$y=\den{\alpha\!s,\!x\!s.t_{2}}(X\!s)(y\!s)$. Definiamo
$\den{\alpha\!s,\!x\!s.t}(X\!s)(y\!s)$ essere $f(y)$.

\item Supponiamo che $t$ sia il termine astrazione\index{astrazione di funzione, nella logica HOL@astrazione di funzione, nella logica \HOL{}!semantica formale della}
$\lambda x.t_{2}$ dove $x$ è di tipo $\tau_{1}$ e $t_{2}$ di
tipo $\tau_{2}$. Così $\tau=\tau_{1}\fun\tau_{2}$ e
$\den{\alpha\!s.\tau}(X\!s)$ è l'insieme di funzioni
$\den{\alpha\!s.\tau_{1}}(X\!s)\fun\den{\alpha\!s.\tau_{2}}(X\!s)$.
Definiamo $\den{\alpha\!s,\!x\!s.t}(X\!s)(y\!s)$ essere l'elemento di
questo insieme che è la funzione che manda
$y\in\den{\alpha\!s.\tau_{1}}(X\!s)$ a
$\den{\alpha\!s,\!x\!s,\!x.t_{2}}(X\!s)(y\!s,y)$. (Si noti che dal momento che
$\alpha\!s,\!x\!s.t$ è un termine in contesto, per convenzione la variabile
legata $x$ non occorre in $x\!s$ e così anche
$\alpha\!s,\!x\!s,\!x.t_{2}$ è un termine in contesto.)
\end{itemize}
Ora definiamo il significato di un termine $t_{\tau}$ in un modello $M$ essere la
funzione dipendentemente tipizzata
\[ \den{t_{\tau}} \in \prod_{X\!s\in{\cal U}^{n}}
   \left(\prod_{j=1}^{m}\den{\alpha\!s.\sigma_{j}}(X\!s)\right)
   \fun \den{\alpha\!s.\tau}(X\!s)
\]
data da $\den{\alpha\!s,\!x\!s.t_{\tau}}$, dove $\alpha\!s,\!x\!s$ è il
contesto canonico di $t_{\tau}$. Così $n$ è il numero di variabili di tipi in
$t_{\tau}$, $\alpha\!s$ è una lista di quelle variabili di tipo, $m$ è il
numero di variabili ordinarie che occorrono libere in $t_{\tau}$ (assunte essere
distinte dalle variabili legate di $t_{\tau}$) e i $\sigma_{j}$ sono
i tipi di quelle variabili. (E' importante notare che la lista
$\alpha\!s$, che è parte del contesto canonico di $t$, può essere strettamente
più grande dei contesti di tipo canonici di $\sigma_{j}$ o $\tau$. Così
non avrebbe senso scrivere semplicemente $\den{\sigma_{j}}$ o $\den{\tau}$ nella
definizione di sopra.)

Se $t_{\tau}$ è un termine chiuso, allora $m=0$ e per ogni $X\!s\in{\cal
U}^{n}$ si può identificare $\den{t_{\tau}}$ con l'elemento
$\den{t_{\tau}}(X\!s)()\in\den{\alpha\!s.\tau}(X\!s)$. Così per termini chiusi
si ottiene
\[ \den{t_{\tau}} \in \prod_{X\!s\in{\cal U}^{n}}
\den{\alpha\!s.\tau}(X\!s)
\]
dove $\alpha\!s$ è la lista delle variabili di tipo che occorrono in $t_{\tau}$ e
$n$ è la lunghezza di quella lista. Se inoltre, nessuna variabile di tipo occorre in
$t_{\tau}$, allora $n=0$ e $\den{t_{\tau}}$ può essere identificato con
l'elemento $\den{t_{\tau}}()$ dell'insieme $\den{\tau}\in{\cal U}$.

La semantica dei termini appare qualcosa di complicato a casua della
possibile dipendenza di un termine sia dalle variabili di tipo sia dalle variabili
ordinarie. Esempi di come la definizione della semantica
funziona in pratica si può trovare nella Sezione~\ref{LOG}, dove è dato il significato
di alcuni termini che denotano costanti logiche.

\subsection{Sostituzione}
\label{term-substitution}

Dal momento che i termini possono coinvolgere sia variabili di tipo sia
variabili ordinarie, ci sono due differenti operazioni di sostituzione
sui termini che bisogna considerare---sostituzione di tipi per variabili
di tipo e sostituzione di termini per variabili.

\subsubsection*{Sostituire tipi per variabili di tipo nei termini}
\index{regola di sostituzione, nella logica HOL@regola di sostituzione, nella logica \HOL{}!semantica formale della}

Supponiamo che $t$ sia un termine, con contesto canonico $\alpha\!s,\!x\!s$ diciamo,
dove $\alpha\!s = \alpha_1,\ldots,\alpha_n$, $x\!s = x_1,\ldots,x_m$
e dove per $j=1,\ldots,m$ il tipo della variabile $x_j$ è
$\sigma_j$. Se $\alpha\!s'.\tau_{i}$ ($i=1,\ldots,n$) sono
tipi-in-contesto, allora sostituendo\index{sostituzione di tipo, nella logica HOL@sostituzione di tipo, nella logica \HOL{}!semantica formale della} i tipi
$\tau_{i}$ per le variabili di tipo $\alpha_{i}$ nella lista $x\!s$, si
ottiene una nuova lista di variabili $x\!s'$. Così il $j$\/esimo elemento di
$x\!s'$ ha il tipo $\sigma'_{j} = \sigma_{j}[\tau\!s/\alpha\!s]$. Saranno considerate solo
sostituzioni con la seguente proprietà.
\begin{quote}
Nell'istanziare\index{tipi, nella logica HOL@tipi, nella logica \HOL{}!istanziazione di} le variabili di tipo $\alpha\!s$ con i tipi
$\tau\!s$, nessuna coppia di due variabili distinte nella lista $x\!s$ diventano uguali
nella lista $x\!s'$\footnote{Una tale identificazione di variabili potrebbe
accadere se le variabili avessero lo stesso nome componente e i loro tipi
diventassero uguali in seguito all'istanziazione.}.
\end{quote}
Questa condizione assicura che $\alpha\!s',x\!s'$ sia davvero un contesto. Allora
si ottiene un nuovo termine-in-contesto $\alpha\!s',\!x\!s'.t'$
sostituendo i tipi $\tau\!s=\tau_{1},\ldots,\tau_{n}$ per le variabili
di tipo $\alpha\!s$ in $t$ (con un'adatta rinomina delle occorrenze
legate delle variabili per renderle distinte dalle variabili in
$x\!s'$). La notazione
\[
t[\tau\!s/\alpha\!s]
\]
è usata per il termine $t'$.

\medskip

\noindent{\bf Lemma 3\ }{\it
Il significato di $\alpha\!s',\!x\!s'.t'$ in un modello è collegato a quello
di $t$ come segue. Per tutti $X\!s'\in{\cal U}^{n'}$ (dove $n'$ è la
lunghezza di $\alpha\!s'$)
}
\[
\den{\alpha\!s',\!x\!s'.t'}(X\!s') =
   \den{t}(\den{\alpha\!s'.\tau_{1}}(X\!s'),\ldots,
   \den{\alpha\!s'.\tau_{n}}(X\!s')).
\]

\medskip

Il lemma~2 in \ref{instances-and-substitution} è necessario per vedere che entrambi
i lati dell'equazione di sopra sono elementi dello stesso insieme di funzioni.
La validità dell'equazione è dimostrata per induzione sulla struttura
del termine $t$.

\subsubsection*{Sostituire termini per variabili nei termini}
\index{regola di sostituzione, nella logica HOL@regola di sostituzione, nella logica \HOL{}!semantica formale della}

Supponiamo che $t$ sia un termine, con contesto canonico $\alpha\!s,\!x\!s$ diciamo,
dove $\alpha\!s = \alpha_1,\ldots,\alpha_n$, $x\!s = x_1,\ldots,x_m$
e dove per $j=1,\ldots,m$ il tipo della variabile $x_j$ è
$\sigma_j$. Se si hanno termini-in-contesto $\alpha\!s,\!x\!s'.t_{j}$ per
$j=1,\ldots,m$ con $t_{j}$ dello stesso tipo di $x_{j}$, diciamo
$\sigma_{j}$, allora si ottiene un nuovo termine-in-contesto
$\alpha\!s,\!x\!s'.t''$ sostituendo i termini
$t\!s=t_1,\ldots,t_m$ per le variabili $x\!s$ in $t$ (con la rinomina
adatta delle occorrenze legate delle variabili per prevenire che le variabili
libere delle $t_{j}$ diventino legate dopo la sostituzione). La
notazione
\[
t[t\!s/x\!s]
\]
è usata per il termine $t''$.

\medskip

\noindent{\bf Lemma 4\ }{\it
Il significato di $\alpha\!s,\!x\!s'.t''$ in un modello è collegato con quello di
$t$ come segue. Per tutti $X\!s\in{\cal U}^{n}$ e tutti
$y\!s'\in\den{\alpha\!s.\sigma'_{1}} \times\cdots\times
\den{\alpha\!s.\sigma'_{m'}}$ (dove $\sigma'_{j}$ è il tipo di
$x'_{j}$)}
\[
\den{\alpha\!s,\!x\!s'.t''}(X\!s)(y\!s') = \den{t}(X\!s)(
\den{\alpha\!s,\!x\!s'.t_{1}}(X\!s)(y\!s'),\ldots,
\den{\alpha\!s,\!x\!s'.t_{m}}(X\!s)(y\!s'))
\]

\medskip

Di nuovo, questo risultato è dimostrato per induzione sulla struttura del
termine $t$.


\section{Nozioni standard}

Fino ad ora la sintassi dei tipi e dei termini è stata molto generale. Per
rappresentare le formule standard della logica è necessario
imporre qualche struttura specifica. In particolare, ogni struttura di tipo
deve contenere un tipo atomico \ty{bool} che è inteso denotare
l'insieme distinto di due elementi $\two\in{\cal U}$, considerato come un insieme
di valori di verità. Le formule logiche sono allora identificate con
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
tipo \ty{bool}. In aggiunta, varie
costanti logiche sono assunte essere in tutte le firme. Questi
requisiti sono formalizzati definendo la nozione di una
firma standard.

\subsection{Strutture di tipo standard}
\label{standard-type-structures}

Una struttura di tipo $\Omega$ è {\em standard\/} se contiene i
tipi atomici \ty{bool} (dei booleani o valori di verità) e \ty{ind} (degli
individui). (Nella letteratura, è spesso utilizzato il simbolo $o$
al posto di \ty{bool} e $\iota$ al posto di \ty{ind}.)

Un modello $M$ di $\Omega$ è {\em standard\/} se $M(\bool)$ e $M(\ind)$ sono
rispettivamente gli insiemi distinti $\two$ e $\ind$ nell'universo
$\cal U$.

Si assumerà d'ora in avanti che le strutture di tipo e i loro modelli
sono standard.

\subsection{Firme standard}
\label{standard-signatures}
\index{firme, della logica HOL@firme, della logica \HOL{}!standard}\index{firme standard, della logica HOL@firme standard, della logica \HOL{}}

Una firma $\Sigma_{\Omega}$ è {\em standard\/} se contiene le
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}:
\[
{\imp}_{\ty{bool}\fun\ty{bool}\fun\ty{bool}}
\]
\[
{=}_{\alpha\fun\alpha\fun\ty{bool}}
\]
\[
\hilbert_{(\alpha\fun\ty{bool})\fun\alpha}
\]
L'interpretazione intesa di queste costanti è che $\imp$ denota
l'implicazione, $=_{\sigma\fun\sigma\fun\ty{bool}}$ denota l'uguaglianza
sull'insieme denotato da $\sigma$, e
$\hilbert_{(\sigma\fun\ty{bool})\fun\sigma}$ denota una funzione di scelta
sull'insieme denotato da $\sigma$. Più precisamente, un modello $M$ di
$\Sigma_{\Omega}$ sarà chiamato {\em standard\/}\index{modelli standard, della logica HOL@modelli standard, della logica \HOL{}} se
\begin{itemize}

\item
$M({\imp},\bool\fun\bool\fun\bool)\in(\two\fun\two\fun\two)$ è
la funzione d'implicazione standard\index{implicazione, nella logica HOL@implicazione, nella logica \HOL{}!semantica formale della}, che manda $b,b'\in\two$ su
\[
(b\imp b') = \left\{ \begin{array}{ll}
                           0 & \mbox{se $b=1$ e $b'=0$} \\
                           1 & \mbox{altrimenti}
                          \end{array}
             \right.%}
\]

\item
$M({=},\alpha\fun\alpha\fun\bool)\in\prod_{X\in{\cal U}}.X\fun
X\fun\two$ è la funzione che assegna ad ogni $X\in{\cal U}$
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
\[
(x=_{X}x') = \left\{ \begin{array}{ll}
                           1 & \mbox{se $x=x'$} \\
                           0 & \mbox{altrimenti}
                          \end{array}
             \right.%}
\]

\item
\index{operatore epsilon}$M(\hilbert,(\alpha\fun\bool)\fun\alpha)\in\prod_{X\in{\cal
U}}.(X\fun\two)\fun X$ è la funzione cha assegna ad ogni $X\in{\cal
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
\[
\ch_{X}(f) = \left\{ \begin{array}{ll}
                           \ch(f^{-1}\{1\})
                             & \mbox{se $f^{-1}\{1\}\not=\emptyset$}\\
                           \ch(X) & \mbox{altrimenti}
                          \end{array}
             \right.%}
\]
dove $f^{-1}\{1\}=\{x\in X : f(x)=1\}$. (Si noti che $f^{-1}\{1\}$ è in
$\cal U$ quando non è vuota, per la proprietà {\bf Sub}
dell'universo $\cal U$ data nella Sezione~\ref{introduction}. La funzione
$\ch$ è data dalla proprietà {\bf Choice}.)

\end{itemize}

Si assumerà da qui in avanti che le firme e i loro modelli sono
standard.

\medskip

\noindent{\bf Nota\ }
Questa particolare scelta delle costanti primitive è arbitraria. La
collezione standard delle costanti logiche include $\T$ (`vero'), $\F$
(`falso')\index{valori di verità, nella logica HOL@valori di verità, nella logica \HOL{}!forma astratta di}, $\imp$ (`implica'), $\wedge$ (`e'), $\vee$
(`o'), $\neg$ (`non'), $\forall$ (`per tutti'), $\exists$ (`esiste'),
$=$ (`è uguale'), $\iota$ (`il'), e $\hilbert$ (`un'). Questo
insieme è ridondante, dal momento che può essere definito (in un senso spiegato nella
Sezione~\ref{defs}) da vari sottoinsiemi. In pratica, è
necessario lavorare con l'insieme completo delle costanti logiche, e il
particolare sottoinsieme preso come primitivo non è importante. il lettore
interessato può esplorare ulteriormente questo argomento leggendo il libro
di Andrews~\cite{Andrews} e i riferimenti che esso contiene.

\medskip

I termini di tipo \ty{bool} sono chiamati {\it formule\/}\index{formule come termini, nella logica HOL@formule come termini, nella logica \HOL{}}.

Sono usate le seguenti abbreviazioni notazionali:

\begin{center}
\index{uguaglianza, nella logica HOL@uguaglianza, nella logica \HOL{}!forma astratta di}
\index{implicazione, nella logica HOL@implicazione, nella logica \HOL{}!forma astratta di}
\index{operatore di scelta, nella logica HOL@operatore di scelta, nella logica \HOL{}!forma astratta di}
\index{quantificatore esistenziale, nella logica HOL@quantificatore esistenziale, nella logica \HOL{}!forma astratta di}
\index{quantificatore universale, nella logica HOL@quantificatore universale, nella logica \HOL{}!forma astratta di}
\index{operatore epsilon}
\begin{tabular}{|l|l|}\hline
{\rm Notazione} & {\rm Significato}\\ \hline
$t_{\sigma}=t'_{\sigma}$ &
  $=_{\sigma\fun\sigma\fun\ty{bool}}\ t_{\sigma}\ t'_{\sigma}$\\ \hline
$t\imp t'$ &
  $\imp_{\ty{bool}\fun\ty{bool}\fun\ty{bool}}\ t_\ty{bool}\
t'_\ty{bool}$\\ \hline
$\hilbert x_{\sigma}.\ t$ &
  $ \hilbert_{(\sigma\fun\ty{bool})\fun\sigma}
(\lambda x_{\sigma}.\ t)$\\ \hline
\end{tabular}
\end{center}
Queste notazioni sono casi speciali di convenzioni generali di abbreviazione
supportate dal sistema \HOL{}. Le prime due sono infissi e la
terza è un binder (si vedano le sezioni di \DESCRIPTION\/ sul parsing e
il pretty-printing).



%%% Local Variables:
%%% mode: latex
%%% TeX-master: "logic"
%%% End:
