% Revised version of Part II, Chapter 10 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{Teorie}\label{semantics}

\section{Introduzione}

Il risultato, se ce n'è uno, di una sessione con il sistema \HOL{} è un oggetto
chiamato una {\it teoria\/}. Questo oggetto è strettamente collegato con ciò che un
logico chiamerebbe una teoria\index{theories, nella logica HOL@teorie, nella logica \HOL{}!forma astratta di}, ma ci sono alcune differenze che sorgono
dalle necessità della dimostrazione meccanica. Una teoria \HOL{}, come la teoria di
un logico, contiene insiemi di tipi, costanti, definizioni e assiomi. In
aggiunta, tuttavia, una teoria \HOL{}, in qualsiasi punto del tempo, contiene una
esplicita lista di teoremi che sono già stati dimostrati dagli
assiomi e dalle definizioni. I logici non hanno alcuna necessità di distinguere i teoremi
attualmente dimostrati da quelli meramente dimostrabili; di conseguenza essi normalmente non
considerano insiemi di teoremi dimostrati come parte di una teoria; piuttosto, essi
considerano i teoremi di una teoria essere l'insieme (spesso infinito) di tutte
le conseguenze degli assiomi e le definizioni. Una differenza collegata
tra le teorie dei logici e le teorie \HOL{} è che per i logici,
le teorie sono oggetti statici, ma in \HOL{} esse possono essere pensate come
potenzialmente estensibili. Per esempio, il sistema \HOL{} fornisce strumenti
per aggiungere alle teorie e combinare teorie. Un'interazione tipica
con \HOL{} consiste nel combinare qualche teoria esistente, facendo qualche
definizione, dimostrando alcuni teoremi e poi salvare i nuovi risultati.

Lo scopo del sistema \HOL{} è di fornire strumenti per permettere
di costruire teorie ben-formate. La logica \HOL{} è tipizzata:
ogni teoria specifica una firma di constanti di tipo e individuali;
queste poi determinano gli insiemi dei tipi e dei termini come nel capitolo
precedente. Tutti i teoremi di tali teorie sono conseguenze logiche
delle definizioni e degli assiomi della teoria. Il sistema \HOL{} assicura
che solo teorie ben-formate possono essere costruite permettendo di creare
teoremi solo per {\it dimostrazione formale\/}. Esplicitare questo comporta
definire cosa significa essere un teorema, il che porta alla descrizione
del sistema di dimostrazione di \HOL{}, che sarà dato di seguito. Esso è dimostrato essere {\em
valido\/} per la semantica insiemistica di \HOL{} descritta nel
capitolo precedente. Questo significa che un teorema è soddisfatto da un modello
se ha una dimostrazione formale da assiomi che sono a loro volta soddisfatti dal
modello. Dal momento che una contraddizione logica non è soddisfatta da alcun
modello, questo garantisce in particolare che una teoria che possiede un modello
è necessariamente coerente, cioè non può essere dimostrata una contraddizione
logica dai suoi assiomi.

Questo capitolo descrive anche i vari meccanismi per i quali le teorie
\HOL\ possono essere estese a nuove teorie. Ogni meccanismo è mostrato
preservare la proprietà di possedere un modello. Così le teorie costruite
dalla teoria \HOL{} iniziale (che possiede un modello) usando
questi meccanismi sono garantite essere coerenti.


\section{Sequenti}
\label{sequents}

La logica \HOL{} è formulata in termini di asserzioni ipotetiche chiamate
{\em sequenti}\index{sequenti!nella deduzione naturale}. Fissando una
firma (standard) $\Sigma_\Omega$, un sequente è una coppia $(\Gamma,
t)$ dove $\Gamma$ è un insieme finito di formule su $\Sigma_\Omega$
e $t$ è una singola formula su $\Sigma_\Omega$\footnote{Si noti che
il sottoscritto di tipo è omesso dai termini quando è chiaro dal
contesto che essi sono formule, cioè hanno tipo \ty{bool}.}. L'insieme di
formule $\Gamma$ che formano il primo componente di un sequente è chiamato
il suo insieme di {\it assunzioni\/}\index{assunzioni!di sequenti} e il
termine $t$ che forma il secondo componente è chiamato la sua {\it
conclusione\/}\index{conclusioni!di sequenti}. Quando non dà origine ad
ambiguità, un sequente $(\{\},t)$ è scritto semplicemente $t$.


Intuitivamente un modello $M$ di $\Sigma_\Omega$ {\em
soddisfa}\index{soddisfazione di sequenti, da parte di un modello} un sequente
$(\Gamma, t)$ se qualsiasi interpretazione delle variabili libere rilevanti come
elementi di $M$ che rendono le formule in $\Gamma$ vere, rendono vera
anche la formula $t$. Per rendere questo più preciso, supponiamo che
$\Gamma=\{t_1,\ldots,t_p\}$ e sia $\alpha\!s,\!x\!s$  un
contesto contenente tutte le variabili di tipo e tutte le variabili libere
che occorrono nelle formule $t,t_{1},\ldots,t_{p}$. Supponiamo che
$\alpha\!s$ abbia lunghezza $n$, che $x\!s=x_{1},\ldots,x_{m}$ e che il
tipo di $x_{j}$ sia $\sigma_{j}$. Dal momento che le formule sono termini di tipo
$\bool$, la semantica dei termini definita nel capitolo precedente da
origine a elementi $\den{\alpha\!s,\!x\!s.t}_M$ e
$\den{\alpha\!s,\!x\!s.t_{k}}_M$ ($k=1,\ldots,p$) in
\[
\prod_{X\!s\in{\cal U}^{n}} \left(
\prod_{j=1}^{m}\den{\alpha\!s.\sigma_{j}}_M(X\!s)\right) \fun \:\two  \]
Diciamo che il modello $M$ {\em soddisfa\/} il sequente $(\Gamma,t)$ e
scriviamo
\[
\Gamma \models_{M} t
\]
se per tutti gli $X\!s\in{\cal U}^{n}$ e
tutti gli $y\!s\in\den{\alpha\!s.\sigma_{1}}_M(X\!s)\times\cdots\times
\den{\alpha\!s.\sigma_{m}}_M(X\!s)$ con
\[
\den{\alpha\!s,\!x\!s.t_{k}}_M(X\!s)(y\!s)=1
\]
per tutti i $k=1,\ldots,p$, è anche il caso che
\[
\den{\alpha\!s,\!x\!s.t}_M(X\!s)(y\!s)=1.
\]
(Si ricordi che $\two$ è l'insieme $\{0,1\}$.)

Nel caso $p=0$, la soddisfazione di $(\{\},t)$ da parte di $M$ sarà scritta
$\models_{M} t$. Così $\models_{M} t$ significa che la funzione dipendentemente tipizzata
\[
\den{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 \:\two
\]
è costante con valore $1\in\two$.

\section{Logica}

Un sistema deduttivo\index{sistemi deduttivi}
${\cal D}$ è un insieme di coppie $(L,(\Gamma,t))$ dove $L$ è una
lista (possibilmente vuota) di sequenti e $(\Gamma,t)$ è un sequente.

Un sequente $(\Gamma,t)$ segue da\index{segue da, nella deduzione naturale}
un insieme di sequenti
$\Delta$ per un sistema deduttivo
${\cal D}$ se
e solo se esistono sequenti
$(\Gamma_1,t_1)$, $\ldots$ , $(\Gamma_n,t_n)$ tali che:
\begin{enumerate}
\item $(\Gamma,t) = (\Gamma_n,t_n)$, e
\item per tutti gli $i$ tali che $1\leq i\leq n$
\begin{enumerate}
\item o
$(\Gamma_i,t_i)\in \Delta$ o
\item $(L_i,(\Gamma_i,t_i))\in{\cal D}$ per qualche lista $L_i$ di membri di
$\Delta\cup\{(\Gamma_1,t_1),\ldots,(\Gamma_{i-1},t_{i-1})\}$ .
\end{enumerate}
\end{enumerate}
La sequenza $(\Gamma_1,t_1),\cdots,(\Gamma_n,t_n)$
è chiamata una {\it dimostrazione\/}\index{dimostrazione!nella deduzione naturale} di
$(\Gamma,t)$ da $\Delta$ rispetto a ${\cal D}$.

Si noti che se $(\Gamma,t)$ segue da $\Delta$, allora anche $(\Gamma,t)$
segue da qualsiasi $\Delta'$ tale che $\Delta\subseteq\Delta'$.
Questa proprietà è chiamata {\it monotonicità\/}\index{monotonicità, nei sistemi deduttivi}.

La notazione\index{turnstile} $t_1,\ldots,t_n\vdash_{{\cal
D},\Delta} t$ significa che il sequente $(\{t_1,\ldots,t_n\},\ t)$
segue da $\Delta$ per ${\cal D}$.  Se o ${\cal D}$ o $\Delta$
è chiaro dal contesto allora può essere omesso.  Nel caso in cui
non ci siano ipotesi\index{ipotesi!di sequenti} (cioè $n=0$),
si scrive semplicemente $\vdash t$.

In pratica, un particolare sistema deduttivo è di solito specificato da un
numero di \emph{regole d'inferenza} (schematiche),
\index{regole d'inferenza, della logica HOL@regole d'inferenza, della logica \HOL{}!forma astratta di primitive}
che prendono la forma
\[
\frac{\Gamma_1\turn t_1 \qquad\cdots\qquad\Gamma_n\turn t_n}
{\Gamma \turn t}
\]
I sequenti sopra la linea sono chiamate le {\it
ipotesi\/}\index{ipotesi!di regole d'inferenza} della regola e il
sequente sotto la linea è chiamato la sua {\it
conclusione}\index{conclusioni!di regole d'inferenza}. Una tale regola è
schematica perché può contenere meta-variabili
che stanno per termini arbitrari dei tipi appropriati. Istanziando
queste meta-variabili con termini reali, si ottiene una lista di sequenti
sopra la linea e un singolo sequente sotto la linea che insieme
costituiscono un elemento particolare del sistema deduttivo. Le
istanziazioni permesse per una particolare regola possono essere ristrette
imponendo una {\em condizione a lato\/} della regola.


\subsection{Il sistema deduttivo \HOL{}}
\label{HOLrules}

Il sistema deduttivo della logica \HOL{} è specificato da otto regole
d'inferenza, date di seguito. Le prime tre regole non hanno ipotesi;
le loro conclusioni possono essere dedotte sempre. Gli identificatori nelle parentesi
quadre sono i nomi delle funzioni \ML\ nel sistema \HOL{} che
implementano le corrispondenti regole d'inferenza (si veda \DESCRIPTION). Qualsiasi
condizioni a lato che restringano lo scopo di una regola sono date immediatamente
al di sotto di essa.

\bigskip

\subsubsection*{Introduzione di assunzione [{\small\tt
ASSUME}]}\index{introduzione di assunzione, nella logica HOL@Introduzione di assunzione, nella logica \HOL{}!forma astratta di}
\[
\overline{t \turn t}
\]

\subsubsection*{Riflessività [{\small\tt
REFL}]}\index{REFL@\ml{REFL}}\index{riflessività, nella logica HOL@riflessività, nella logica \HOL{}!forma astratta di}
\[
\overline{\turn t = t}
\]

\subsubsection*{Beta-conversione [{\small\tt BETA\_CONV}]}
\index{beta-conversione, nella logica HOL@beta-conversione, nella logica \HOL{}!forma astratta di}\index{BETA_CONV@\ml{BETA\_CONV}}
\[
\overline{\turn (\lquant{x}t_1)t_2 = t_1[t_2/x]}
\]
\begin{itemize}
\item Dove $t_1[t_2/x]$ è
il risultato di sostituire $t_2$ per $x$
in $t_1$, con un'adatta rinomina delle variabili per impedire che le variabili libere
in $t_2$ diventino legate dopo la sostituzione.
\end{itemize}

\subsubsection*{Sostituzione [{\small\tt
SUBST}]}\index{SUBST@\ml{SUBST}} \index{sostituzione regola, nella logica HOL@sostituzione, regola di, nella logica \HOL{}!forma astratta di}
\[
\frac{\Gamma_1\turn t_1 = t_1'\qquad\cdots\qquad\Gamma_n\turn t_n =
t_n'\qquad\qquad \Gamma\turn t[t_1,\ldots,t_n]}
{\Gamma_1\cup\cdots\cup\Gamma_n\cup\Gamma\turn t[t_1',\ldots,t_n']}
\]
\begin{itemize}
\item Dove $t[t_1,\ldots,t_n]$ denota un termine $t$ con alcune occorrenze
libere di sottotermini $t_1$, $\ldots$ , $t_n$ isolati e
$t[t_1',\ldots,t_n']$ denota il risultato di sostituire ciascuna occorrenza
selezionata di $t_i$ per $t_i'$ (per $1{\leq}i{\leq}n$), con una rinomina
adatta delle variabili per impedire che variabili libere in $t_1'$ diventino
legate dopo la sostituzione.
\end{itemize}

\subsubsection*{Astrazione [{\small\tt ABS}]}
\index{ABS@\ml{ABS}}\index{regola di astrazione}
\[
\frac{\Gamma\turn t_1 = t_2}
{\Gamma\turn (\lquant{x}t_1) = (\lquant{x}t_2)}
\]
\begin{itemize}
\item Purché $x$ non sia libera in $\Gamma$.
\end{itemize}

\subsubsection*{Istanziazione di tipo [{\small\tt INST\_TYPE}]}
\index{type instantiation, nella logica HOL@type instantiation, nella logica \HOL{}!forma astratta di}
\newcommand{\insttysub}{[\sigma_1,\ldots,\sigma_n/\alpha_1,\ldots,\alpha_n]}
\[
\frac{\Gamma\turn t}
{\Gamma\insttysub\turn t\insttysub}
\]
\begin{itemize}
\item Dove $t\insttysub$ è il risultato di sostituire, in parallelo,
	i tipi $\sigma_1$, $\dots$, $\sigma_n$ per le variabili di tipo
	$\alpha_1$, $\dots$, $\alpha_n$ in $t$, e dove $\Gamma\insttysub$
	è il risultato di eseguire la stessa sostituzione in tutte le
	ipotesi del teorema.
\item Dopo l'istanziazione, le variabili libere nell'input non possono
	diventare legate, ma variabili libere distinte nell'input possono diventare
	identiche.
\end{itemize}

\subsubsection*{Scaricamento di assunzione [{\small\tt
DISCH}]}\index{discharging assumptions, nella logica HOL@discharging assumptions, nella logica \HOL{}!forma astratta di}\index{DISCH@\ml{DISCH}}
\[
\frac{\Gamma\turn t_2}
{\Gamma -\{t_1\} \turn t_1 \imp t_2}
\]
\begin{itemize}
\item Dove $\Gamma -\{t_1\}$ è la sottrazione insiemistica di $\{t_1\}$
da $\Gamma$.
\end{itemize}

\subsubsection*{Modus Ponens [{\small\tt
MP}]}\index{MP@\ml{MP}}\index{Modus Ponens, nella logica HOL@Modus Ponens, nella logica \HOL{}!forma astratta di}
\[
\frac{\Gamma_1 \turn t_1 \imp t_2  \qquad\qquad   \Gamma_2\turn t_1}
{\Gamma_1 \cup \Gamma_2 \turn t_2}
\]

In aggiunta a queste otto regole, ci sono anche quattro {\it
assiomi\/}\index{assiomi!come regole d'inferenza} che avrebbero potuto essere
considerate come regole d'inferenza senza le ipotesi. Questo non è fatto,
tuttavia, dal momento che è più naturale formulare gli assiomi usando qualche
costante logica definita e il principio di definizione di costante non è
stato ancora descritto. Gli assiomi sono dati nella Sezione~\ref{INIT} e
le definizioni delle costanti logiche extra che essi coinvolgono sono date nella
Sezione~\ref{LOG}.

Il particolare insieme di regole e assiomi scelti per assiomatizzare la logica
\HOL\ è piuttosto arbitrario. In parte è basato sulle regole che erano state
utilizzate nella logica
\LCF\index{LCF@\LCF}\
\PPL\index{PPlambda (same as PPLAMBDA), of LCF system@\ml{PP}$\lambda$ (same as \ml{PPLAMBDA}), of \ml{LCF} system}, dal momento che \HOL{} è stato
implementato modificando il sistema \LCF. In particolare, la
regola di sostituzione\index{substitution rule, nella logica HOL@substitution rule, nella logica \HOL{}!implementation of} {\small\tt SUBST} è esattamente
la stessa della corrispondente regola in \LCF; il codice che implementa questa regola
fu scritto da Robin Milner ed è altamente ottimizzato. Poiché
la sostituzione è un'attività così pervasiva nella dimostrazione, si è ritenuto
importante che la primitiva di sistema fosse il più veloce possibile. Da un
punto di vista logico sarebbe stato meglio avere una primitiva
di sostituzione più semplice, come la `Regola R' della logica di Andrews ${\cal
Q}_0$, e poi derivare regole più complicate da essa.

\subsection{Teorema di validità}
\index{soundness!of HOL deductive system@of \HOL{} deductive system}
\label{soundness}

\index{inference rules, della logica HOL@inference rules, della logica \HOL{}!formal semantics of}
\emph{Le regole del sistema deduttivo \HOL{} sono {\em valide} per
	la nozione di soddisfacimento definita nella Sezione~\ref{sequents}: per
	qualsiasi istanza di regole d'inferenza, se un modello (standard)
	soddisfa le ipotesi della regola soddisfa anche la
	conclusione.}

\medskip

\noindent{\bf Dimostrazione\ }
La verifica della validità delle regole è semplice.
Le proprietà della semantica rispetto alla sostituzione date dai
Lemmi 3 e 4 nella Sezione~\ref{term-substitution} sono necessari per le regole
\ml{BETA\_CONV}, \ml{SUBST} and
\ml{INST\_TYPE}\index{INST_TYPE@\ml{INST\_TYPE}}\footnote{Si noti in
	particolare che la seconda restrizione su \ml{INST\_TYPE} permette
	il risultato sulla semantica della sostituzione di tipi per variabili di tipo
	nei termini da applicare}. Il fatto che $=$ e $\imp$ siano
interpretate in modo standard (come nella Sezione~\ref{standard-signatures}) è
necessario per le regole \ml{REFL}\index{REFL@\ml{REFL}},
\ml{BETA\_CONV}\index{BETA_CONV@\ml{BETA\_CONV}},
\ml{SUBST}\index{SUBST@\ml{SUBST}}, \ml{ABS}\index{ABS@\ml{ABS}},
\ml{DISCH}\index{DISCH@\ml{DISCH}} e \ml{MP}\index{MP@\ml{MP}}.

\section{Teorie \HOL{}}
\label{theories}

Una {\it teoria\/}\index{theories, nella logica HOL@theories, nella logica \HOL{}!forma astratta di} \HOL{} ${\cal T}$ è una $4$-tupla:
\begin{eqnarray*}
{\cal T} & = & \langle{\sf Struc}_{\cal T},{\sf Sig}_{\cal T},
               {\sf Axioms}_{\cal T},{\sf Theorems}_{\cal T}\rangle
\end{eqnarray*}
dove
\begin{myenumerate}

\item ${\sf Struc}_{\cal T}$ è una struttura di tipo\index{type structures, of HOL theories@type structures, of \HOL{} theories}  chiamata la
struttura di tipo di ${\cal T}$;

\item ${\sf Sig}_{\cal T}$ è una firma\index{signatures, della logica HOL@signatures, della logica \HOL{}!of HOL theories@of \HOL{} theories}
su ${\sf Struc}_{\cal T}$ chiamata la firma di ${\cal T}$;

\item ${\sf Axioms}_{\cal T}$ è un insieme di sequenti su ${\sf Sig}_{\cal T}$
chiamati gli assiomi\index{assiomi, in una teoria HOL@assiomi, in una teoria \HOL{}}
 di  ${\cal T}$;

\item ${\sf Theorems}_{\cal T}$ è un insieme di sequenti su
${\sf Sig}_{\cal T}$ chiamati i teoremi
%
\index{theorems, nella logica HOL@theorems, nella logica \HOL{}!forma astratta di}
%
di ${\cal T}$, con
la proprietà che ogni membro segue da ${\sf Axioms}_{\cal T}$ per
il sistema deduttivo \HOL{}.

\end{myenumerate}

Gli insiemi ${\sf Types}_{\cal T}$ e ${\sf Terms}_{\cal T}$ dei tipi e
dei termini di una teoria ${\cal T}$ sono, rispettivamente, gli insiemi dei tipi e
dei termini costruibili dalla struttura di tipo e dalla firma di ${\cal
T}$, cioè:
\begin{eqnarray*}
{\sf Types}_{\cal T} & = & {\sf Types}_{{\sf Struc}_{\cal T}}\\
{\sf Terms}_{\cal T} & = & {\sf Terms}_{{\sf Sig}_{\cal T}}
\end{eqnarray*}
Un modello di una teoria $\cal T$ è specificato dando un modello (standard)
$M$ della sottostante firma della teoria con la proprietà che
$M$ soddisfa tutti i sequenti che sono assiomi di $\cal T$.  A causa
del Teorema di Validità~\ref{soundness}, segue che $M$ soddisfa
anche qualunque sequente nell'insieme dei teoremi dati, ${\sf
Theorems}_{\cal T}$.

\subsection{La teoria {\tt MIN}}
\label{sec:min-thy}

La {\it teoria minimale\/}\index{MIN@\ml{MIN}}\index{minimal theory, della logica HOL@minimal theory, della logica \HOL{}} \theory{MIN} è definita da:
\[
\theory{MIN} =
\langle\{(\bool,0),\ (\ind,0)\},\
 \{\imp_{\bool\fun\bool\fun\bool},
=_{\alpha\fun\alpha\fun\bool},
\hilbert_{(\alpha\fun\bool)\fun\alpha}\},\
\{\},\ \{\}\rangle
\]
Dal momento che la teoria \theory{MIN} ha una firma che consiste solo di
elementi standard e non ha assiomi, essa possiede un unico modello standard,
che sarà indicato con {\em Min}.

Benché la teoria \theory{MIN} contiene solo la sintassi standard
minimale, sfruttando i costrutti di ordine superiore di \HOL{} si può
costruire su di essa una collezione di termini piuttosto ricca. La seguente
teoria introduce nomi per alcuni di questi termini che denotano utili
operazioni logiche nel modello {\em Min}.

Nell'implementazione, alla teoria \theory{MIN} è dato il nome
\theoryimp{min}, e contiene anche il distinto operatore di tipo
binario $\fun$, per costruire spazi di funzione.

\subsection{La teoria {\tt LOG}}
\index{LOG@\ml{LOG}}
\label{LOG}

La teoria \theory{LOG} ha la stessa struttura
di tipo di \theory{MIN}. La sua firma contiene le costanti in
\theory{MIN}. e le seguenti costanti:
\[
\T_\ty{bool}
\index{T@\holtxt{T}!forma astratta di}
\index{truth values, nella logica HOL@truth values, nella logica \HOL{}!forma astratta di}
\]
\[
\forall_{(\alpha\fun\ty{bool})\fun\ty{bool}}
\index{universal quantifier, nella logica HOL@universal quantifier, nella logica \HOL{}!forma astratta di}
\]
\[
\exists_{(\alpha\fun\ty{bool})\fun\ty{bool}}
\index{existential quantifier, nella logica HOL@existential quantifier, nella logica \HOL{}!forma astratta di}
\]
\[
\F_\ty{bool}
\index{F@\holtxt{F}!forma astratta di}
\]
\[
\neg_{\ty{bool}\fun\ty{bool}}
\index{negation, nella logica HOL@negation, nella logica \HOL{}!forma astratta di}
\]
\[
\wedge_{\ty{bool}\fun\ty{bool}\fun\ty{bool}}
\index{conjunction, nella logica HOL@conjunction, nella logica \HOL{}!forma astratta di}
\]
\[
\vee_{\ty{bool}\fun\ty{bool}\fun\ty{bool}}
\index{disjunction, nella logica HOL@disjunction, nella logica \HOL{}!forma astratta di}
\]
\[
\OneOne_{(\alpha\fun\beta)\fun\ty\bool}
\index{one-to-one predicate, nella logica HOL@one-to-one predicate, nella logica \HOL{}!forma astratta di}
\]
\[
\Onto_{(\alpha\fun\beta)\fun\ty\bool}
\index{onto predicate, nella logica HOL@onto predicate, nella logica \HOL{}!forma astratta di}
\]
\[
\TyDef_{(\alpha\fun\ty{bool})\fun(\beta\fun\alpha)\fun\ty{bool}}
\]
In connessione con queste costanti è usata la seguente notazione speciale:
\begin{center}
\index{existential quantifier, nella logica HOL@existential quantifier, nella logica \HOL{}!abbreviation for multiple}
\index{universal quantifier, nella logica HOL@universal quantifier, nella logica \HOL{}!abbreviation for multiple}
\begin{tabular}{|l|l|}\hline
{\rm Notation} & {\rm Meaning}\\ \hline $\uquant{x_{\sigma}}t$ &
$\forall(\lambda x_{\sigma}.\ t)$\\ \hline $\uquant{x_1\ x_2\ \cdots\
x_n}t$ & $\uquant{x_1}(\uquant{x_2} \cdots\ (\uquant{x_n}t)
\ \cdots\ )$\\ \hline
$\equant{x_{\sigma}}t$
  & $\exists(\lambda x_{\sigma}.\ t)$\\ \hline
$\equant{x_1\ x_2\ \cdots\ x_n}t$
  & $\equant{x_1}(\equant{x_2} \cdots\ (\equant{x_n}t)
\ \cdots\ )$\\ \hline
$t_1\ \wedge\ t_2$  & $\wedge\ t_1\ t_2$\\ \hline
$t_1\ \vee\ t_2$  & $\vee\ t_1\ t_2$\\ \hline
\end{tabular}\end{center}

Gli assiomi della teoria \theory{LOG} consistono dei seguenti
sequenti:
\[
\begin{array}{l}

\turn \T       =  ((\lquant{x_{\ty{bool}}}x) =
               (\lquant{x_{\ty{bool}}}x))    \\
\turn \forall  =  \lquant{P_{\alpha\fun\ty{bool}}}\ P =
                    (\lquant{x}\T ) \\
\turn \exists  =  \lquant{P_{\alpha\fun\ty{bool}}}\
                    P({\hilbert}\ P) \\
\turn \F       =  \uquant{b_{\ty{bool}}}\ b  \\
\turn \neg    =  \lquant{b}\ b \imp \F \\
\turn {\wedge}  =  \lquant{b_1\ b_2}\uquant{b}
                     (b_1\imp (b_2 \imp b)) \imp b \\
\turn {\vee}  =  \lquant{b_1\ b_2}\uquant{b}
                   (b_1 \imp b)\imp ((b_2 \imp b) \imp b) \\
\turn \OneOne  =  \lquant{f_{\alpha \fun\beta}}\uquant{x_1\ x_2}
                    (f\ x_1 = f\ x_2)  \imp (x_1 = x_2) \\
\turn \Onto  =  \lquant{f_{\alpha\fun\beta}}
                  \uquant{y}\equant{x} y = f\ x \\
\turn \TyDef  =   \begin{array}[t]{l}
                  \lambda P_{\alpha\fun\ty{bool}}\
                  rep_{\beta\fun\alpha}.
                  \OneOne\ rep\ \ \wedge{}\\
                  \quad(\uquant{x}P\ x \ =\ (\equant{y} x = rep\ y))
                  \end{array}
\end{array}
\]
Ininfe, come per la teoria \theory{MIN}, l'insieme ${\sf
Theorems}_{\theory{LOG}}$ è considerato essere vuoto.

Si noti che gli assiomi della teoria \theory{LOG} sono essenzialmente {\em
definizioni\/} delle nuove costanti di \theory{LOG} come termini nella
teoria originaria \theory{MIN}. (Il meccanismo per fare tali
estensioni alle teorie attraverso definizioni di nuove costanti sarà riportato
in generale nella Sezione~\ref{defs}.) I primi sette assiomi definiscono le
costanti logiche per la verità, la quantificazione universale, la quantificazione
esistenziale, la falsità, la negazione, la congiunzione e la disgiunzione.
Benché queste definizioni possano essere oscure a qualche lettore, esse sono di
fatto definizioni standard di queste costanti logiche in termini di
implicazione, uguaglianza e scelta all'interno della logica di ordine superiore. I
due assiomi successivi definiscono le proprietà di una funzione di essere iniettiva e suriettiva;
esse saranno usate per esprimere l'assioma dell'infinito (si veda
la Sezione~\ref{INIT}), tra le altre cose. L'ultimo assioma definisce una
costante usata per le definizioni di tipo (si veda la Sezione~\ref{tydefs}).

L'unico modello standard {\em Min\/} di \theory{MIN} dà origine a un
unico modello standard di
\theory{LOG}\index{LOG@\ml{LOG}!formal semantics of}. Questo
perché, data la semantica dei termini formulata nella
Sezione~\ref{semantics of terms}, per soddisfare le equazioni di sopra si è
costretti ad interpretare le nuove costanti nel modo seguente:
\index{assiomi!semantica formale degli assiomi della logic HOL@semantica formale degli assiomi della logic \HOL{}|(}
\begin{itemize}

\item $\den{\T_{\bool}}\index{T@\holtxt{T}!formal semantics of} = 1 \in \two$

\item \index{universal quantifier, nella logica HOL@universal quantifier, nella logica \HOL{}!formal semantics of}
$\den{\forall_{(\alpha\fun\bool)\fun\bool}}\in\prod_{X\in{\cal
 U}}(X\fun\two)\fun\two$ manda $X\in{\cal U}$ e $f\in X\fun\two$ a
\[
\den{\forall}(X)(f) = \left\{ \begin{array}{ll} 1 & \mbox{se
$f^{-1}\{1\}=X$} \\ 0 & \mbox{altrimenti} \end{array} \right.
\]
\index{universal quantifier, nella logica HOL@universal quantifier, nella logica \HOL{}!formal semantics of}

\item \index{existential quantifier, nella logica HOL@existential quantifier, nella logica \HOL{}!formal semantics of}
$\den{\exists_{(\alpha\fun\bool)\fun\bool}}\in\prod_{X\in{\cal
 U}}(X\fun\two)\fun\two$ manda $X\in{\cal U}$ e $f\in X\fun\two$ a
\[
\den{\exists}(X)(f) = \left\{ \begin{array}{ll}
                                   1 & \mbox{se $f^{-1}\{1\}\not=\emptyset$} \\
                                   0 & \mbox{altrimenti}
                                  \end{array}
                          \right. \]

\item $\den{\F_{\bool}} = 0 \in \two$\index{F@\holtxt{F}!formal semantics of}

\item $\den{\neg_{\bool\fun\bool}}\in\two\fun\two$ manda $b\in\two$ a
 \[ \den{\neg}(b) = \left\{ \begin{array}{ll}
                             1 & \mbox{se $b=0$} \\
                             0 & \mbox{altrimenti}
                            \end{array}
                    \right. \]\index{negation, nella logica HOL@negation, nella logica \HOL{}!formal semantics of}

\item $\den{\wedge_{\bool\fun\bool\fun\bool}}\in\two\fun\two\fun\two$ manda
$b,b'\in\two$ a
 \[ \den{\wedge}(b)(b') = \left\{ \begin{array}{ll}
                                   1 & \mbox{se $b=1=b'$} \\
                                    0 & \mbox{altrimenti}
                                  \end{array}
                           \right. \]\index{conjunction, nella logica HOL@conjunction, nella logica \HOL{}!formal semantics of}

\item $\den{\vee_{\bool\fun\bool\fun\bool}}\in\two\fun\two\fun\two$ manda
$b,b'\in\two$ a
 \[ \den{\vee}(b)(b') = \left\{ \begin{array}{ll}
                                 0 & \mbox{se $b=0=b'$} \\
                                 1 & \mbox{altrimenti}
                                \end{array}
                        \right. \]\index{disjunction, nella logica HOL@disjunction, nella logica \HOL{}!formal semantics of}

\item $\den{\OneOne_{(\alpha\fun\beta)\fun\bool}}\in\prod_{(X,Y)\in{\cal
 U}^{2}} (X\fun Y)\fun \two$ manda $(X,Y)\in{\cal U}^{2}$ e
 $f\in(X\fun Y)$   a
 \[ \den{\OneOne}(X,Y)(f) = \left\{ \begin{array}{ll}
                                     0 & \mbox{se $f(x)=f(x')$
                                               per qualche $x\not=x'$ in $X$} \\
                                     1 & \mbox{altrimenti}
                                    \end{array}
                            \right. \]\index{one-to-one predicate, nella logica HOL@one-to-one predicate, nella logica \HOL{}!formal semantics of}

\item $\den{\Onto_{(\alpha\fun\beta)\fun\bool}}\in\prod_{(X,Y)\in{\cal
 U}^{2}} (X\fun Y)\fun \two$ manda $(X,Y)\in{\cal U}^{2}$ e
 $f\in(X\fun Y)$   a
 \[ \den{\Onto}(X,Y)(f) = \left\{ \begin{array}{ll}
                                   1 & \mbox{se $\{f(x):x\in X\}=Y$} \\
                                   0 & \mbox{altrimenti}
                                  \end{array}
                           \right. \]\index{onto predicate, nella logica HOL@onto predicate, nella logica \HOL{}!formal semantics of}

\item $\den{\TyDef_{(\alpha\fun\bool)\fun(\beta\fun\alpha)\fun\bool}}\in
 \prod_{(X,Y)\in{\cal U}^{2}} (X\fun\two)\fun(Y\fun X)\fun\two$ \\
 manda $(X,Y)\in{\cal U}^{2}$, $f\in(X\fun\two)$ and $g\in(Y\fun X)$  a
 \[ \den{\TyDef}(X,Y)(f)(g) = \left\{ \begin{array}{ll}
                                        1 & \mbox{se
                                            $\den{\OneOne}(Y,X)(g)=1$}\\
                                          & \mbox{e $f^{-1}\{1\}=
                                            \{g(y) : y\in Y\}$} \\
                                        0 & \mbox{altrimenti.}
                                       \end{array}
                               \right.
\]
\end{itemize}
\index{assiomi!semantica formale degli assiomi della logic HOL@semantica formale degli assiomi della logic \HOL{}|)}
Dal momento che queste definizioni sono state ottenute applicando la semantica dei
termini ai lati sinistri dell'equazioni che formano gli assiomi di
\theory{LOG}, questi assiomi sono soddisfatti e si ottiene un modello della
teoria \theory{LOG}.


\subsection{La teoria {\tt INIT}}
\label{INIT}

La teoria \theory{INIT}\index{INIT@\ml{INIT}!forma astratta di} si
ottiene aggiungendo i seguenti quattro assiomi\index{assiomi!della logica HOL@della logica \HOL{}} alla teoria
\theory{LOG}.
\[
\index{BOOL_CASES_AX@\ml{BOOL\_CASES\_AX}!forma astratta di}
\index{ETA_AX@\ml{ETA\_AX}!forma astratta di}
\index{SELECT_AX@\ml{SELECT\_AX}!forma astratta di}
\index{INFINITY_AX@\ml{INFINITY\_AX}!forma astratta di}
\index{assioma di scelta}
\index{assioma dell'infinito}
\begin{array}{@{}l@{\qquad}l}
\mbox{\small\tt BOOL\_CASES\_AX}&\vdash \uquant{b} (b = \T ) \vee (b = \F )\\
 \\
\mbox{\small\tt ETA\_AX}&
\vdash \uquant{f_{\alpha\fun\beta}}(\lquant{x}f\ x) = f\\
 \\
\mbox{\small\tt SELECT\_AX}&
\vdash \uquant{P_{\alpha\fun\ty{bool}}\ x} P\ x \imp
P({\hilbert}\ P)\\
  \\
\mbox{\small\tt INFINITY\_AX}&
\vdash \equant{f_{\ind\fun \ind}} \OneOne \ f \conj \neg(\Onto \ f)\\
\end{array}
\]

L'unico modello standard di \theory{LOG} soddisfa questi quattro assiomi
e di conseguenza è l'unico modello standard della teoria
\theory{INIT}.\index{INIT@\ml{INIT}!formal semantics of} (Per l'assioma
{\small\tt SELECT\_AX} è necessario usare la definizione di
$\den{\hilbert}$ data nella Sezione~\ref{standard-signatures}; per l'assioma
{\small\tt INFINITY\_AX} è ncessario il fatto che $\den{\ind}=\inds$ è
un insieme infinito.)

La teoria \theory{INIT} è la teoria iniziale\index{initial theory,
  della logica HOL@initial theory, della logica \HOL{}!forma astratta di} della
logica \HOL{}. Una teoria che estende \theory{INIT} sarà chiamata una
{\em teoria standard}\index{teoria standard}.

\subsection{Implementare le teorie \texttt{LOG} e \texttt{INIT}}
\label{sec:implementing-log-init}

L'implementazione combina le teorie \theory{LOG} e
\theory{INIT} in una teoria \theoryimp{bool}. Essa include tutte le
costanti e gli assiomi da queste teorie, e include un numero di
risultati derivati circa queste costanti. Per maggiori informazioni sulla
teoria \theoryimp{bool} d'implementazione, si veda \DESCRIPTION.

\subsection{Coerenza}
\label{consistency}

Una teoria (standard) è {\em coerente\/}\index{teoria coerente} se
non è il caso che ogni sequente nella sua firma possa essere
derivato dagli assiomi della teoria usando la logica \HOL{}, o
in modo equivalente, se non può essere derivato in questo modo il particolare sequente $\turn\F$.

L'esistenza di un modello (standard) di una teoria è sufficiente per
stabilire la sua coerenza. Perché per il Teorema
di Validità~\ref{soundness}, qualsiasi sequente che possa essere derivato dagli
assiomi della teoria sarà soddisfatto dal modello, mentre il sequente
$\turn\F$ non è mai soddisfatto in alcun modello. Così in particolare,
la teoria iniziale \theory{INIT} è coerente.

Tuttavia, è possibile che una teoria sia coerente ma non
possieda un modello standard. Questo avviene perché la nozione di un
modello {\em standard\/} è piuttosto restrittiva---in particolare non c'è alcuna
scelta su come interpretare gli interi e la loro aritmetica in un tale
modello. Il famoso teorema di incompletezza di G\"odel assicura che ci
sono sequenti che sono soddisfatti in tutti i modelli standard (cioè che sono
`veri'), ma che non sono dimostrabili nella logica \HOL{}.





\section{Estensioni di teorie}
\index{extension, della logica HOL@extension, della logica \HOL{}!forma astratta di}
\label{extensions}

Una teoria ${\cal T}'$ è detta essere un'{\em
estensione\/}\index{extension, of theory} di una teoria ${\cal T}$ se:
\begin{myenumerate}
\item ${\sf Struc}_{{\cal T}}\subseteq{\sf Struc}_{{\cal T}'}$.
\item ${\sf Sig}_{{\cal T}}\subseteq{\sf Sig}_{{\cal T}'}$.
\item ${\sf Axioms}_{{\cal T}}\subseteq{\sf Axioms}_{{\cal T}'}$.
\item ${\sf Theorems}_{{\cal T}}\subseteq{\sf Theorems}_{{\cal T}'}$.
\end{myenumerate}
In questo caso, qualsiasi modello $M'$ della teoria più grande ${\cal T}'$ può essere
ristretto a un modello della teoria più piccola $\cal T$ nel modo
seguente. Primo, $M'$ dà origine a un modello della struttura e della firma
di $\cal T$ semplicemente dimenticando i valori di $M'$ alle costanti che non sono
in ${\sf Struc}_{\cal T}$ or ${\sf Sig}_{\cal T}$. Indicando questo modello
con $M$, si ha che per ogni $\sigma\in{\sf Types}_{\cal T}$, $t\in{\sf
Terms}_{\cal T}$ e per tutti i contesti adatti che
\begin{eqnarray*}
\den{\alpha\!s.\sigma}_{M}   & = & \den{\alpha\!s.\sigma}_{M'} \\
\den{\alpha\!s,\!x\!s.t}_{M} & = & \den{\alpha\!s,\!x\!s.t}_{M'}.
\end{eqnarray*}
Di conseguenza se $(\Gamma,t)$ è un sequente su ${\sf Sig}_{\cal T}$
(e di conseguenza anche su ${\sf Sig}_{{\cal T}'}$), allora $\Gamma
\models_{M} t$ se e solo se $\Gamma \models_{M'} t$. Dal momento che ${\sf
Axioms}_{\cal T}\subseteq{\sf Axioms}_{{\cal T}'}$ e $M'$ è un modello
di ${\cal T}'$, segue che $M$ è un modello di $\cal T$. $M$ sarà
chiamata la {\em restrizione}\index{restrictions, of models} del
modello $M'$ della teoria ${\cal T}'$ alla sotto-teoria $\cal T$.

\bigskip

Ci sono due meccanismi principali per fare estensioni alle teorie in \HOL:
\begin{itemize}

\item Estensione attraverso la specifica di una costante   (si veda la Sezione~\ref{specs}).

\item Estensione attraverso la specifica di un tipo (si veda la
Sezione~\ref{tyspecs}).\footnote{Questo meccanismo di estensione di teorie non è
implementato nel sistema \HOL{}4.}

\end{itemize}
Il primo meccanismo permette la `specifica libera' di costanti (come nella
notazione {\bf Z}~\cite{Z}, per esempio); la seconda permette di
introdurre nuovi tipi e operatori di tipo. Come casi speciali (quando la
cosa che si sta definendo è univocamente determinata) si hanno anche:
\begin{itemize}

\item Estensione attraverso la definizione di una costante (si veda la Sezione~\ref{defs}).

\item Estensione attraverso la definizione di un tipo (si veda la Sezione~\ref{tydefs}).

\end{itemize}
Questi meccanismi sono descritti nelle seguenti sezioni. Essi producono
tutti delle {\it estensioni definizionali\/} nel senso che essi estendono
una teoria aggiungendo delle nuove costanti e dei nuovi tipi che sono definiti in termini
di proprietà di quelli esistenti. La loro proprietà chiave è che la
teoria estesa possiede un modello (standard) se la teoria originale
lo ha. Così è garantito che una serie di queste estensioni che iniziano dalla teoria
\theory{INIT} risulterà in una teoria con un modello
standard, e di conseguenza in una teoria coerente. E' anche possibile estendere
teorie semplicemente aggiungendo nuove costanti e tipi non interpretati. Questo
preserva la coerenza, ma difficilmente sarà utile senza assiomi
addizionali. Tuttavia, quando si aggiungono arbitrariamente nuovi
assiomi\index{assiomi!non necessità di aggiungere}, non c'è alcuna garanzia
che la coerenza sia preservata. I vantaggi della postulazione rispetto
alla definizione sono stati paragonati da Bertrand Russell ai vantaggi del
furto rispetto al lavoro onesto\footnote{Si veda la pagina 71 del libro di Russel {\sl
Introduction to Mathematical Philosophy\/}}. Dal momento che è sin troppo facile
introdurre assiomatizzazioni incoerenti, gli utenti del sistema \HOL{} sono
caldamente invitati a resistere alla tentazione di aggiungere assiomi, ma di lavorare
onestamente attraverso teorie definizionali.




\subsection{Estensione per definizione di costanti}
\index{extension, della logica HOL@extension, della logica \HOL{}!by constant definition|(}
\label{defs}

Una {\it definizione di costante\/}\index{definizione di costante} su una
firma $\Sigma_{\Omega}$ è una formula della forma
$\con{c}_{\sigma} = t_{\sigma}$, tale che:
\begin{myenumerate}

\item
$\con{c}$ non è il nome di alcuna costante in $\Sigma_{\Omega}$;

\item
$t_{\sigma}$ è un termine chiuso in ${\sf Terms}_{\Sigma_{\Omega}}$.

\item
tutte le variabili di tipo che occorrono in $t_\sigma$ occorrono anche in $\sigma$

\end{myenumerate}

Data una teoria $\cal T$ e una tale definizione di costante su ${\sf
Sig}_{\cal T}$, allora l'{\em estensione definizionale\/}\index{constant definition extension, della logica HOL@constant definition extension, della logica \HOL{}!forma astratta di} di ${\cal T}$
per $\con{c}_{\sigma}=t_{\sigma}$ è la teoria ${\cal T}{+_{\it
def}}\langle
\con{c}_{\sigma}=t_{\sigma}\rangle$ definita da:
\[
{\cal T}{+_{\it def}}\langle
\con{c}_{\sigma}=t_{\sigma}\rangle\  =\ \langle
\begin{array}[t]{l}
{\sf Struc}_{\cal T},\
{\sf Sig}_{\cal T}\cup\{(\con{c},\sigma)\},\\
{\sf Axioms}_{\cal T}\cup\{
\con{c}_{\sigma}=t_{\sigma} \},\
{\sf Theorems}_{\cal T}\rangle
\end{array}
\]

Si noti che il meccanismo di estensione per definizione di costante è già
stato usato implicitamente nel formare la teoria \theory{LOG} dalla
teoria \theory{MIN} nella Sezione~\ref{LOG}. Così con la notazione
di questa sezione si ha
\[
\theory{LOG}\; =\; \theory{MIN}\;\begin{array}[t]{@{}l}
   {+_{\it def}} \langle \T\index{T@\holtxt{T}!forma astratta di}\index{truth values, nella logica HOL@truth values, nella logica \HOL{}!forma astratta di} \ =\
     ((\lquant{x_{\ty{bool}}}x) = (\lquant{x_{\ty{bool}}}x))\rangle\\
   {+_{\it def}}\langle {\forall}\index{universal quantifier, nella logica HOL@universal quantifier, nella logica \HOL{}!forma astratta di}\ =\ \lquant{P_{\alpha\fun\ty{bool}}}\ P =
     (\lquant{x}\T )\rangle\\
   {+_{\it def}}\langle {\exists}\index{existential quantifier, nella logica HOL@existential quantifier, nella logica \HOL{}!forma astratta di}\ =\
     \lquant{P_{\alpha\fun\ty{bool}}}\ P({\hilbert}\ P)\rangle\\
   {+_{\it def}}\langle \F\index{F@\holtxt{F}!forma astratta di}
 \ =\ \uquant{b_{\ty{bool}}}\ b\rangle\\
   {+_{\it def}}\langle \neg\ =\ \lquant{b}\ b \imp \F \rangle\index{negation, nella logica HOL@negation, nella logica \HOL{}!forma astratta di}\\
   {+_{\it def}}\langle {\wedge}\index{conjunction, nella logica HOL@conjunction, nella logica \HOL{}!forma astratta di}\ =\ \lquant{b_1\ b_2}\uquant{b}
     (b_1\imp (b_2 \imp b)) \imp b\rangle\\
   {+_{\it def}}\langle {\vee}\index{disjunction, nella logica HOL@disjunction, nella logica \HOL{}!forma astratta di}\ =\ \lquant{b_1\ b_2}\uquant{b}
     (b_1 \imp b)\imp ((b_2 \imp b) \imp b)\rangle\\
   {+_{\it def}}\langle\OneOne \ =\ \lquant{f_{\alpha \fun\beta}}
     \uquant{x_1\ x_2} (f\ x_1 = f\ x_2)  \imp (x_1 = x_2)\rangle\index{one-to-one predicate, nella logica HOL@one-to-one predicate, nella logica \HOL{}!forma astratta di}\\
   {+_{\it def}}\langle\Onto \  =\ \lquant{f_{\alpha\fun\beta}}\index{onto predicate, nella logica HOL@onto predicate, nella logica \HOL{}!forma astratta di}
     \uquant{y}\equant{x} y = f\ x\rangle\\
   {+_{\it def}}\langle\TyDef \  =\
        \begin{array}[t]{@{}l}
          \lambda P_{\alpha\fun\ty{bool}}\ rep_{\beta\fun\alpha}.\\
          \OneOne\ rep\ \ \wedge\\
          (\uquant{x}P\ x \ =\ (\equant{y} x = rep\ y)) \rangle\\
\end{array}\end{array}
\]

Se $\cal T$ possiede un modello standard allora lo ha anche l'estensione
${\cal T}{+_{\it def}}\langle\con{c}_{\sigma}=t_{\sigma}\rangle$. Questo
sarà dimostrato come un corollario del corrispondente risultato nella\linebreak
Sezione~\ref{specs} mostrando che l'estensione per definizione di costante
è di fatto un caso speciale di estensione per specifica di costante.
(Questa riduzione richiede che si stia trattando con teorie
{\em standard\/} nel senso della sezione~\ref{INIT}, dal momento che benché
la quantificazione esistenziale non sia necessaria per le definizioni di costanti, è
necessaria per formulare il meccanismo di specifica di costante.)

\medskip

\noindent{\bf Nota\ } La condizione (iii) nella definizione di
ciò che costituisce una definizione di costante corretta è una restrizione
importante senza la quale la coerenza non potrebbe essere garantita. Per vedere
questo, consideriamo il termine $\equant{f_{\alpha\fun\alpha}} \OneOne \ f
\conj \neg(\Onto \ f)$, che esprime la proposizione che il (l'insieme
di elementi denotati dal) tipo $\alpha$ è infinito. Il termine contiene
la variabile di tipo $\alpha$, mentre il tipo del termine, $\ty{bool}$,
no. Così per (iii)
\[
\con{c}_\ty{bool} =
\equant{f_{\alpha\fun\alpha}} \OneOne \ f \conj \neg(\Onto \ f)
\]
non è permessa come definizione di una costante. Il problema è che il
significato del lato destro della definizione varia con $\alpha$,
mentre il significato della costante sul lato sinistro è fissato,
dal momento che non contiene $\alpha$. Di fatto, se ci fosse permesso di
estendere la teoria coerente $\theory{INIT}$ con questa definizione, il
risultato darebbe una teoria incoerente. Perché istanziare $\alpha$ a
$\ty{ind}$ nel lato destro risulta in un termine che è dimostrabile
dagli assiomi di $\theory{INIT}$, e di conseguenza $\con{c}_\ty{bool}=\T$ è
dimostrabile nella teoria estesa. Ma ugualmente, istanziare $\alpha$
a $\ty{bool}$ rende la negazione del lato destro dimostrabile
dagli assiomi di $\theory{INIT}$, e di conseguenza anche $\con{c}_\ty{bool}=\F$ è
dimostrabile nella teoria estesa. Combinando questi teoremi, si
ha che $\T=\F$, cioè $\F$ è dimostrabile nella teoria estesa.
\index{extension, della logica HOL@extension, della logica \HOL{}!by constant definition|)}

\subsection{Estensione per specifica di costante}
\index{extension, della logica HOL@extension, della logica \HOL{}!by constant specification|(}
\label{specs}

Le specifiche di costanti\index{constant specification extension, della logica HOL@constant specification extension, della logica \HOL{}!abstract form
of} introducono costanti (o insiemi di costanti)
che soddisfano proprietà (coerenti) arbitrariamente date. Per esempio, una
teoria potrebbe essere estesa da una specifica di costante in modo da avere due nuove
costanti $\con{b}_1$ e $\con{b}_2$ di tipo \ty{bool} tali che
$\neg(\con{b}_1=\con{b}_2)$. Questa specifica non definisce
in modo univoco $\con{b}_1$ e $\con{b}_2$, dal momento che è soddisfatta sia da
$\con{b}_1=\T$ e $\con{b}_2=\F$, sia da $\con{b}_1=\F$ e
$\con{b}_2=\T$. Per assicurare che tali specifiche sono
coerenti\index{consistency, della logica HOL@consistency, della logica \HOL{}!under constant specification}, esse possono essere fatte solo se è
già stato dimostrato che le proprietà che le nuove costanti devono
avere sono coerenti. Questo impedisce, per esempio, di introdurre tre
costanti booleane $\con{b}_1$, $\con{b}_2$ e $\con{b}_3$ tali che
$\con{b}_1\neq \con{b}_2$, $\con{b}_1\neq \con{b}_3$ e
$\con{b}_2\neq \con{b}_3$.

Supponiamo che $\equant{x_1\cdots x_n}t$ sia una formula, con $x_1,\ldots, x_n$
variabili distinte. Se $\turn \equant{x_1 \cdots x_n}t$, allora una
specifica di costante permette di introdurre le nuove costanti $\con{c}_1$, $\ldots$ ,
$\con{c}_n$ che soddisfano:
\[
\turn t[\con{c}_1,\cdots,\con{c}_n/x_1,\cdots,x_n]
\]
dove $t[\con{c}_1,\cdots,\con{c}_n/x_1,\cdots,x_n]$ denota il
risultato di sostituire simultaneamente $\con{c}_1, \ldots, \con{c}_n$
per $x_1, \ldots, x_n$ rispettivamente. Naturalmente il tipo di ciascuna
costante $\con{c}_i$ deve essere lo stesso del tipo della corrispondente
variabile $x_i$. Per assicurare che questo meccanismo di estensione preserva la
proprietà di possedere un modello, è imposto su questi tipi un ulteriore
requisito più tecnico: essi devono contenere ciascuno tutte le variabili
di tipo che occorrono in $t$. Questa condizione è discussa ulteriormente nella
Sezione~\ref{constants} di sotto.

Formalmente, una {\em specifica di costante\/}\index{constant specification}
per una teoria ${\cal T}$ è data da

\medskip
\noindent{\bf Dati}
\[
\langle(\con{c}_1,\ldots,\con{c}_n),
\lquant{{x_1}_{\sigma_1},\ldots,{x_n}_{\sigma_n}}t_{\ty{bool}}\rangle
\]

\noindent{\bf Condizioni}
\begin{myenumerate}

\item
$\con{c}_1,\ldots,\con{c}_n$ sono nomi distinti che
non sono i nomi di alcuna costante in ${\sf Sig}_{\cal T}$.

\item
$\lquant{{x_1}_{\sigma_1}
\cdots {x_n}_{\sigma_n}}t_{\ty{bool}}\ \in\ {\sf Terms}_{\cal T}$.

\item
$tyvars(t_{\ty{bool}})\ =\ tyvars(\sigma_i)$ per $1\leq i\leq n$.

\item
$\equant{{x_1}_{\sigma_1}\ \cdots\ {x_n}_{\sigma_n}}t
\ \in\ {\sf Theorems}_{\cal T}$.

\end{myenumerate}
L'estensione di una teoria standard ${\cal T}$ per mezzo di una tale specifica
di costante è denotata da
\[
{\cal T}{+_{\it spec}}\langle(\con{c}_1,\ldots,\con{c}_n),
\lquant{{x_1}_{\sigma_1},\ldots,{x_n}_{\sigma_n}}t_{\ty{bool}} \rangle
\]
ed è definita essere la teoria:
\[
\langle
\begin{array}[t]{@{}l}
{\sf Struc}_{\cal T},\\
{\sf Sig}_{\cal T} \cup
\{{\con{c}_1}_{\sigma_1}, \ldots,
{\con{c}_n}_{\sigma_n}\},\\
{\sf Axioms}_{\cal T}\cup
\{ t[\con{c}_1,\ldots,\con{c}_n/x_1,\ldots,x_n] \},\\
{\sf Theorems}_{\cal T}
\rangle
\end{array}
\]

\noindent{\bf Proposizione\ }{\em
La teoria ${\cal
T}{+_{\it spec}}\langle(\con{c}_1,\ldots,\con{c}_n),
\lquant{{x_1}_{\sigma_1},\ldots,{x_n}_{\sigma_n}}t_{\ty{bool}}
\rangle$ ha un modello standard se la teoria ${\cal T}$ lo ha.}

\medskip

\noindent{\bf Dimostrazione\ }
Supponiamo che $M$ sia un modello standard di ${\cal T}$. Sia
$\alpha\!s=\alpha_{1},\ldots,\alpha_{m}$ la lista di variabili di tipo
distinte che occorrono nella formula $t$. Allora $\alpha\!s,\!x\!s.t$ è un
termine-in-contesto, dove $x\!s=x_{1},\ldots,x_{n}$. (Cambiando ogni variabile
legata in $t$ in modo da renderle distinte da $x\!s$ se necessario.)
Interpretando questo termine-in-contesto nel modello $M$ si ottiene
\[
\den{\alpha\!s,\!x\!s.t}_{M} \in \prod_{X\!s\in{\cal U}^{m}}
\left(\prod_{i=1}^{n}\den{\alpha\!s.\sigma_{i}}_{M}(X\!s)\right)
\fun \two
\]
Ora $\equant{x\!s}t$ è in ${\sf Theorems}_{\cal T}$ e di conseguenza per il
Teorema di Validità \ref{soundness}\index{consistency, della logica HOL@consistency, della logica \HOL{}!under constant specification} questo
sequente è soddisfatto da $M$. Usando la semantica di $\exists$ data nella
Sezione~\ref{LOG}, questo significa che per ogni $X\!s\in{\cal
U}^{m}$ l'insieme
\[
S(X\!s) = \{y\!s\in\den{\alpha\!s.\sigma_{1}}_{M}(X\!s) \times\cdots\times
          \den{\alpha\!s.\sigma_{n}}_{M}(X\!s)\; : \;
          \den{\alpha\!s,\!x\!s.t}_{M}(X\!s)(y\!s)=1 \}
\]
non è vuoto. Dal momento che è anche un sottoinsieme di un prodotto finito di insiemi in
$\cal U$, ne segue che è un elemento di $\cal U$ (usando le proprietà
{\bf Sub} e {\bf Prod} dell'universo). Così si può applicare la funzione
di scelta globale $\ch\in\prod_{X\in{\cal U}}X$ per selezionare un elemento specifico.
\[
(s_{1}(X\!s),\ldots,s_{n}(X\!s)) =
\ch(S(X\!s)) \in \prod_{i=1}^{n}\den{\alpha\!s.\sigma_{i}}_{M}(X\!s)
\]
per il quale  $\den{\alpha\!s,\!x\!s.t}_{M}(X\!s)$ prende il valore $1$. Estendiamo
$M$ a un modello $M'$ della firma di ${\cal
T}{+_{\it spec}}\langle(\con{c}_1,\ldots,\con{c}_n),
\lquant{{x_1}_{\sigma_1},\ldots,{x_n}_{\sigma_n}}t_{\ty{bool}}
\rangle$ definendo che il suo valore per
ogni nuova costante $(\con{c}_{i},\sigma_{i})$ sia
\[
M'(\con{c}_{i},\sigma_{i}) =
s_{i} \in \prod_{X\!s\in{\cal U}^{m}}\den{\sigma_{i}}_{M}(X\!s) .
\]
Si noti che la Condizione (iii) nella definizione di una specifica
di costante assicura che $\alpha\!s$ è il contesto canonico di ogni
tipo $\sigma_{i}$, così che
$\den{\sigma_{i}}=\den{\alpha\!s.\sigma_{i}}$ e quindi $s_{i}$ è
di fatto un elemento del prodotto di sopra.

Dal momento che $t$ è un termine della sotto-teoria $\cal T$ di \linebreak${\cal
T}{+_{\it spec}}\langle(\con{c}_1,\ldots,\con{c}_n),
\lquant{{x_1}_{\sigma_1},\ldots,{x_n}_{\sigma_n}}t_{\ty{bool}}
\rangle$,
come notato all'inizio della Sezione~\ref{extensions}, si ha che
$\den{\alpha\!s,\!x\!s.t}_{M'} = \den{\alpha\!s,\!x\!s.t}_{M}$. Di conseguenza per
la definizione degli $s_{i}$, per tutti gli $X\!s\in{\cal U}^{m}$
\[
\den{\alpha\!s,\!x\!s.t}_{M'}(X\!s)(s_{1}(X\!s),\ldots,s_{n}(X\!s)) = 1
\]
Quindi usando il Lemma~4 nella
Sezione~\ref{term-substitution} sulla semantica della sostituzione insieme con
la definizione di $\den{\con{c}_{i}}_{M'}$, si ottiene infine che
per tutti gli $X\!s\in{\cal U}^{m}$
\[
\den{t[\con{c}_{1},\ldots,\con{c}_{n}/x_{1},\ldots,x_{n}]}_{M'}(X\!s)=1
\]
o in altre parole che $M'$ soddisfa
$t[\con{c}_{1},\ldots,\con{c}_{n}/x_{1},\ldots,x_{n}]$.
Quindi $M'$ è un modello di ${\cal T}{+_{\it
spec}}\langle(\con{c}_1,\ldots,\con{c}_n),
\lquant{{x_1}_{\sigma_1},\ldots,{x_n}_{\sigma_n}}t_{\ty{bool}}
\rangle$, come richiesto.

\medskip

Le costanti che sono affermate esistere in una specifica di costante
non sono necessariamente determinate in modo univoco. In modo corrispondente, ci possono
essere più modelli differenti di ${\cal T}{+_{\it
spec}}\langle(\con{c}_1,\ldots,\con{c}_n),
\lquant{{x_1}_{\sigma_1},\ldots,{x_n}_{\sigma_n}}t_{\ty{bool}}
\rangle$ la cui restrizione a $\cal T$ è $M$; la costruzione di sopra
produce un tale modello in una maniera uniforme facendo uso della funzione
di scelta globale sull'universo.

L'estensione per mezzo di una definizione di costante, $\con{c}_\sigma=t_\sigma$, è un
caso speciale di estensione per specifica di costante. Perché sia $t'$
la formula $x_\sigma=t_\sigma$, dove $x_\sigma$ è una variabile che non
occorre in $t_\sigma$. Allora chiaramente $\turn
\equant{x_\sigma}t'$ e si può applicare il metodo della specifica
di costante per ottenere la teoria
\[
{\cal T}{+_{\it spec}}\langle \con{c},\lquant{x_\sigma}t'\rangle
\]
Ma dal momento che $t'[\con{c}_\sigma/x_\sigma]$ è semplicemente
$\con{c}_\sigma=t_\sigma$,
questa estensione porta esattamente a ${\cal T}{+_{\it def}}\langle
\con{c}_{\sigma}=t_{\sigma}\rangle$.
Così come corollario della Proposizione, si ha che per ogni modello
standard $M$ di $\cal T$, c'è un modello standard $M'$ di ${\cal
T}{+_{\it def}}\langle\con{c}_{\sigma}=t_{\sigma}\rangle$ la cui
restrizione a $\cal T$ è $M$. In contrasto con il caso delle specifiche
di costante, $M'$ è determinato in modo univoco da $M$ e dalla definizione di
costante
\index{extension, della logica HOL@extension, della logica \HOL{}!by constant specification|)}

\subsection{Note circa le costanti in \HOL{}}
\label{constants}

Si noti come la Condizione (iii) nella definizione di una specifica di costante
sia stata necessaria nella dimostrazione che il meccanismo di estensione preserva la
proprietà di possedere un modello standard. Il suo ruolo è di assicurare che
le costanti introdotte abbiano, attraverso i loro tipi, la stessa dipendenza dalle
variabili di tipo che ha la formula che le specifica. La
situazione è la stessa di quella discussa nella Nota nella
Sezione~\ref{defs}. In un senso, ciò che causava il problema
nell'esempio dato in quella Nota non è tanto il metodo di estensione per mezzo
dell'introduzione di costanti, ma piuttosto la sintassi di \HOL{} che non
permette alle costanti di dipendere esplicitamente dalle variabili di tipo (nel modo
in cui lo fanno gli operatori di tipo). Così nell'esempio si vorrebbe
introdurre una costante `polimorfica' $\con{c}_\ty{bool}(\alpha)$
che dipende esplicitamente da $\alpha$, e definirla essere
$\equant{f_{\alpha\fun\alpha}} \OneOne \ f \conj
\neg(\Onto \ f)$. Allora nella teoria estesa si potrebbe derivare
$\con{c}_\ty{bool}(\ty{ind})=\T$ e
$\con{c}_\ty{bool}(\ty{bool})=\F$, ma ora non risulta alcuna contraddizione dal momento che
$\con{c}_\ty{bool}(\ty{ind})$ e $\con{c}_\ty{bool}(\ty{bool})$
sono differenti.

Nella versione attuale di \HOL, le costanti sono coppie-(nome,tipo).
Si potrebbe immaginare una leggera estensione della sintassi di \HOL{} con
costanti `polimorfiche', specificate da coppie
$(\con{c},\alpha\!s.\sigma)$ dove ora $\alpha\!s.\sigma$ è un
tipo-in-contesto e la lista $\alpha\!s$ può ben contenere variabili di tipo
extra che non occorrono in $\sigma$. Una tale coppia darebbe origine
al particolare termine costante
$\con{c}_\sigma(\alpha\!s)$, e più in generale ai
termini costanti $\con{c}_{\sigma'}(\tau\!s)$ ottenuti da
questo istanziando le variabili di tipo $\alpha_i$ con i tipi
$\tau_i$ (così $\sigma'$ è l'istanza di $\sigma$ ottenuta
sostituendo  $\tau\!s$ per $\alpha\!s$). Questa nuova sintassi di costanti
polimorfiche è paragonabile alla sintassi esistente dei tipi composti (si veda
la sezione~\ref{types}): un operatore di tipo $n$-ario $\textsl{op}$ da origine a un
tipo composto $(\alpha_1,\ldots,\alpha_n){\textsl{op}}$ che dipende da $n$
variabili di tipo. Analogamente, la sintassi di sopra delle costanti polimorfiche
registra come esse dipendono dalle variabili di tipo (as well as which generic
type the constant has).

Tuttavia, registrare esplicitamente la dipendenza delle costanti dalle variabili di tipo
da origine a una sintassi ingombrante che in pratica si preferirebbe
evitare laddove possibile. E' possibile evitarlo se il contesto
di tipo $\alpha\!s$ in $(\con{c},\alpha\!s.\sigma)$ è di fatto il
contesto {\em canonico\/} di $\sigma$, cioè contiene esattamente le variabili
di tipo di $\sigma$. Perché allora si può applicare il Lemma~1 della
Sezione~\ref{instances-and-substitution} per dedurre che la
costante polimorfica $\con{c}_{\sigma'}(\tau\!s)$ può essere abbreviata
alla costante ordinaria $\con{c}_{\sigma'}$ senza ambiguità---l'informazione
mancante $\tau\!s$ può essere ricostruita da $\sigma'$ e
dall'informazione circa la costante $\con{c}$ data nella firma.
Da questo prospettiva, il lato piuttosto tecnico delle Condizioni (iii) nelle
Sezioni~\ref{defs} e \ref{specs} diventano molto meno misteriose:
esse precisamente assicurano che nell'introdurre nuove costanti si stia sempre
trattando solo con i contesti canonici, e così si possano usare costanti ordinarie
piuttosto che quelle polimorfiche senza ambiguità. In questo modo si evita
di complicare la sintassi esistente al costo di restringere
in qualche modo l'applicabilità di questi meccanismi di estensioni delle teorie.


\subsection{Estensione per definizione di tipo}
\index{extension, della logica HOL@extension, della logica \HOL{}!by type definition|(}
\index{representing types, nella logica HOL@representing types, nella logica \HOL{}!forma astratta di|(}
\label{tydefs}

Ogni tipo (monomorfico) $\sigma$ nella teoria iniziale \theory{INIT}
determina un insieme\linebreak $\den{\sigma}$ nell'universo $\cal U$. Tuttavia,
ci sono molti più insiemi in $\cal U$ dei tipi che sono in
\theory{INIT}. In particolare, mentre $\cal U$ è chiuso rispetto
all'operazione di prendere un sottoinsieme non-vuoto di $\den{\sigma}$, non c'è
alcun meccanismo corrispondente per formare un `sottotipo' di $\sigma$. Piuttosto,
i sottoinsiemi sono denotati indirettamente attraverso funzioni caratteristiche, per mezzo delle quali un
termine chiuso $p$ di tipo $\sigma\fun\ty{bool}$ determina il sottoinsieme
$\{x\in\den{\sigma} : \den{p}(x)=1\}$ (che è un insieme nell'universo
purché non sia vuoto). Tuttavia, è utile avere un
meccanismo per introdurre nuovi tipi che sono sottotipi di quelli
esistenti. Tali tipi sono definiti\index{extension, della logica HOL@extension, della logica \HOL{}!by type definition} in \HOL{} introducendo una nuova costante
di tipo e asserendo un assioma che la caratterizza denotare un
insieme in biezione (cioè in corrispondenza uno-a-uno) con un sottoinsieme
non-vuoto di un tipo esistente (chiamato il {\em tipo rappresentante\/}).
Per esempio, il tipo \ml{num} è definito essere uguale a un sottoinsieme
numerabile del tipo \ml{ind}, che è garantito esistere dall'assioma
{\small\tt INFINITY\_AX} (si veda la Sezione~\ref{INIT}).

Così come definire tipi, è anche conveniente essere in grado di definire
operatori di tipo. Un esempio sarebbe un operatore di tipo \ty{inj} che
mappasse un insieme all'insieme di funzioni uno-a-uno (cioè iniettive) su
di esso. Il sottoinsieme di $\sigma\fun\sigma$ che rappresenta $(\sigma)\ty{inj}$
sarebbe definito dal predicato \OneOne. Un altro esempio sarebbe un
operatore di tipo per il prodotto cartesiano binario \ty{prod}. Questo è definito
scegliendo un tipo rappresentante che contiene due variabili di tipo, diciamo
$\sigma[\alpha_1;\alpha_2]$, tale che per ogni tipo $\sigma_1$ e
$\sigma_2$, un sottoinsieme di $\sigma[\sigma_1;\sigma_2]$ rappresenta il
prodotto cartesiano di $\sigma_1$ e $\sigma_2$. I dettagli di una tale
definizione sono dati nella sezione di \DESCRIPTION\/ sulla teoria dei
prodotti cartesiani.

I tipi in \HOL{} devono denotare insiemi non-vuoti. Così è
coerente\index{consistency, della logica HOL@consistency, della logica \HOL{}!under type definition} definire un nuovo tipo isomorfo a un
sottoinsieme specificato da un predicato $p$, solo se c'è almeno una cosa
per cui $p$ vale, cioè $\turn\equant{x}p\ x$. Per esempio,
sarebbe incoerente definire un operatore di tipo binario \ty{iso} tale
che $(\sigma_1,\sigma_2)\ty{iso}$ denotasse l'insieme di funzioni
uno-a-uno da $\sigma_1$ {\em onto\/} $\sigma_2$ perché per qualche
valore di $\sigma_1$ e $\sigma_2$ l'insieme sarebbe vuoto; per
esempio $(\ty{ind},\ty{bool})\ty{iso}$ denoterebbe l'insieme vuoto. Per
evitare questo, una precondizione di definire un nuovo tipo è che il
sottoinsieme rappresentante non sia vuoto.

Riassumendo, un nuovo tipo è definito:
\begin{enumerate}
\item Specificando un tipo esistente.
\item Specificando un sottoinsieme di questo tipo.
\item Dimostrando che questo sottoinsieme non è vuoto.
\item Specificando che il nuovo tipo è isomorfo a questo sottoinsieme.
\end{enumerate}

\noindent In maggiore dettaglio,
definire un nuovo tipo $(\alpha_1,\ldots,\alpha_n)\ty{op}$ consiste nel:
\begin{enumerate}
\item
Specificare un tipo-in-contesto, $\alpha_1,\ldots,\alpha_n.\sigma$ diciamo.
Il tipo
$\sigma$ è chiamato il {\it tipo rappresentante\/}, e il tipo
$(\alpha_1,\ldots,\alpha_n)\ty{op}$ è inteso essere isomorfo a un
sottoinsieme di $\sigma$.

\item
Specificare un termine-in-contesto chiuso, $\alpha_1,\ldots,\alpha_n,.p$
diciamo, di tipo $\sigma\fun\bool$. Il termine $p$ è chiamato la {\it
funzione caratteristica\/}\index{characteristic function, of type definitions}. Questo definisce il sottoinsieme di $\sigma$ al quale
$(\alpha_1,\ldots,\alpha_n)\ty{op}$ deve essere isomorfo\footnote{La
ragione per richiedere che $p$ sia chiuso, cioè non abbia variabili
libere, è che altrimenti per coerenza l'operatore di tipo definito
dovrebbe {\em dipendere\/} da (cioè essere una funzione di) queste
variabili. Tali tipi dipendenti non fanno (ancora!) parte del sistema \HOL{}}.

\item
Dimostrare $\turn \equant{x_{\sigma}} p\ x$.

\item
Asserire un assioma che dice che $(\alpha_1,\ldots,\alpha_n)\ty{op}$ è
isomorfo al sottoinsieme di $\sigma$ selezionato da $p$.

\end{enumerate}

Per rendere questo formale, la teoria \theory{LOG} fornisce
la costante polimorfica \TyDef\ definita nella Sezione~\ref{LOG}.
La formula
$\equant{f_{(\alpha_1,\ldots,\alpha_n)\ty{op}\fun\sigma}}\TyDef\ p\ f$
asserisce che
esiste una funzione uno-a uno $f$ da $(\alpha_1,\ldots,\alpha_n)\ty{op}$
al sottoinsieme di elementi di $\sigma$ per cui $p$ è vero.
Di conseguenza, l'assioma che caratterizza $(\alpha_1,\ldots,\alpha_n)\ty{op}$ è:
\[
\turn \equant{f_{(\alpha_1,\ldots,\alpha_n)\ty{op}\fun\sigma}}\TyDef\
p\ f
\]

Definire un nuovo tipo $(\alpha_1,\ldots,\alpha_n)\ty{op}$ in una teoria
${\cal T}$ così consiste nell'introdurre $\ty{op}$ come un nuovo
operatore di tipo $n$-ario e l'assioma di sopra come un nuovo assioma. Formalmente, una {\em
definizione di tipo\/}\index{type definitions, nella logica HOL@type definitions, nella logica \HOL{}!abstract structure of} per una teoria ${\cal
T}$ è data da

\medskip

\noindent{\bf Dati}
\[
\langle (\alpha_1,\ldots,\alpha_n)\ty{op},\ \sigma,\
p_{\sigma\fun\ty{bool}}\rangle
\]

\noindent{\bf Condizioni}

\begin{myenumerate}
\item
$(\ty{op},n)$ non è il nome di una costante di tipo in ${\sf Struc}_{\cal T}$.

\item
$\alpha_1,\ldots,\alpha_n.\sigma$ è un tipo-in-contesto con $\sigma
\in{\sf Types}_{\cal T}$.

\item $p_{\sigma\fun\bool}$ è un termine chiuso in ${\sf Terms}_{\cal T}$
le cui variabili di tipo occorrono in $\alpha_1,\ldots,\alpha_n$.

\item
$\equant{x_{\sigma}}p\ x \ \in\ {\sf Theorems}_{\cal T}$.
\end{myenumerate}

L'estensione di una teoria standard ${\cal T}$ per mezzo di una tale definizione di tipo
è denotata da
\[
{\cal
T}{+_{tydef}}\langle(\alpha_1,\ldots,\alpha_n)\ty{op},\sigma,p\rangle
\]
e definita essere la teoria
\[
\langle
\begin{array}[t]{@{}l}
{\sf Struc}_{\cal T}\cup\{(\ty{op},n)\},\\
  {\sf Sig}_{\cal T},\\
  {\sf Axioms}_{\cal T}\cup\{
\equant{f_{(\alpha_1,\ldots,\alpha_n)\ty{op}
\fun\sigma}}\TyDef\ p\ f\},\\
  {\sf Theorems}_{\cal T}\rangle\\
\end{array}
\]

\medskip

\noindent{\bf Proposizione\ }{\em
La teoria ${\cal T}{+_{\it
tydef}}\langle(\alpha_1,\ldots,\alpha_n)\ty{op},\sigma,p\rangle$ ha un
modello standard se la teoria ${\cal T}$ lo ha.}

\medskip

Al posto di dare una dimostrazione diretta di questo risultato, esso sarà dedotto come
corollario della proposizione corrispondente nella prossima sezione.
\index{extension, della logica HOL@extension, della logica \HOL{}!by type definition|)}
\index{representing types, nella logica HOL@representing types, nella logica \HOL{}!forma astratta di|)}


\subsection{Estensione per specifica di tipo}
\index{extension, della logica HOL@extension, della logica \HOL{}!by type specification|(}
\label{tyspecs}
\noindent
(\textbf{Nota:} Questo meccanismo di estensione \emph{non} è
implementato nel sistema HOL4. Fu proposto da T.~Melham e
raffina una proposta di R.~Jones e R.~Arthan.)

\smallskip
\noindent Il meccanismo di definizione di
tipo permette d'introdurre nuovi tipi dando una concreta
rappresentazione del tipo come un `sottotipo' di un tipo esistente. Si
potrebbe invece desiderare d'introdurre un nuovo tipo che soddisfa qualche proprietà
senza dare un'esplicita rappresentazione per il tipo. Per
esempio, si potrebbe volere estendere \theory{INIT} con un tipo atomico
$\ty{one}$ che soddisfa $\turn\uquant{f_{\alpha\fun\ty{one}}\
  g_{\alpha\fun\ty{one}}}f=g$ senza scegliere un tipo specifico in
$\theory{INIT}$ e dicendo che $\ty{one}$ è in biezione con un
suo sottoinsieme di un elemento. (L'idea è quella che la scelta del
tipo rappresentante è irrilevante per le proprietà di $\ty{one}$ che
possono essere espresse in \HOL.) Il meccanismo descritto in questa sezione
fornisce un modo di ottenere questo preservando allo stesso tempo
la proprietà fondamentale di possedere un modello standard e quindi
di mantenere la coerenza.

Ogni formula chiusa $q$ che coinvolge una singola variabile di tipo $\alpha$ può
essere pensata come se specificasse una proprietà $q[\tau/\alpha]$ dei tipi
$\tau$. La sua interpretazione in un modello è della forma
\[
\den{\alpha,.q}\in \prod_{X\in{\cal U}}\den{\alpha.\bool}(X)
\;= \prod_{X\in{\cal U}}\two \;=\; {\cal U}\fun\two
\]
che è una funzione caratteristica sull'universo, che determina un
sottoinsieme $\{X\in{\cal U}:\den{\alpha,.q}(X)=1\}$ che consiste di quegli
insiemi nell'universo per cui vale la proprietà $q$. Il modo
più generale per assicurare la coerenza nell'introduzione di un nuovo tipo
atomico $\nu$ che soddisfa $q[\nu/\alpha]$ sarebbe dimostrare
`$\equant{\alpha}q$'. Tuttavia, una tale
formula con la quantificazione sui tipi non è\footnote{ancora!} parte della
logica \HOL{} e si potrebbe procedere in modo indiretto---sostituendo la
formula con una (logicamente più debole) che può essere espressa formalmente con
la sintassi \HOL{}. La formula usata è
\[
(\equant{f_{\alpha\fun\sigma}}{\sf Type\_Definition}\ p\ f)\ \imp\ q
\]
dove $\sigma$ è un tipo, $p_{\sigma\fun\ty{bool}}$ è un termine chiuso
e non coinvolge la variabile di tipo $\alpha$. Questa formula dice `$q$
vale di qualsiasi tipo che è in biezione con il sottotipo di $\sigma$
determinato da $p$'. Se questa formula è dimostrabile e il sottotipo non è
vuoto, cioè se
\[
\equant{x_\sigma}p\ x
\]
è dimostrabile, allora è coerente introdurre un'estensione con un nuovo
tipo atomico $\nu$ che soddisfa $q[\nu/\alpha]$.

Nel dare la definizione formale di questo meccanismo di estensione, saranno
fatti due raffinamenti. Per prima cosa, a $\sigma$ è permesso essere
polimorfico e di conseguenza è introdotta una nuova costante di ripo di arietà
appropriata, piuttosto che semplicemente un tipo atomico. In secondo luogo, alle formule
esistenziali di sopra è permesso di essere dimostrate (nella teoria che deve essere
estesa) da qualche ipotesi\footnote{Questo raffinamento accresce
l'applicabilità del meccanismo di estensione senza accrescere il suo
potere espressivo. Avremmo potuto fare un raffinamento simile per l'altro
meccanismo di estensione di teoria.}. Così una {\em specifica
di tipo\/}\index{specifica di tipo} per una teoria $\cal T$ è
data da

\medskip

\noindent{\bf Dati}
\[
\langle (\alpha_1,\ldots,\alpha_n)\ty{op},\sigma,p,\alpha,\Gamma,q\rangle
\]

\noindent{\bf Condizioni}

\begin{myenumerate}
\item
$(\ty{op},n)$ è una costante di tipo che non è in
${\sf Struc}_{\cal T}$.

\item
$\alpha_1,\ldots,\alpha_n.\sigma$ è un tipo-in-contesto con
$\sigma\in{\sf Types}_{\cal T}$.

\item $p_{\sigma\fun\bool}$ è un termine chiuso in ${\sf Terms}_{\cal T}$
le cui variabili di tipo occorrono in $\alpha\!s=\alpha_1,\ldots,\alpha_n$.

\item $\alpha$ è una variabile di tipo distinta da quelle in
$\alpha\!s$.

\item $\Gamma$ è una lista di formule chiuse in ${\sf Terms}_{\cal T}$
che non coinvolgono la variabile di tipo $\alpha$.

\item $q$ è una formula chiusa in ${\sf Terms}_{\cal T}$.

\item I sequenti
\begin{eqnarray*}
(\Gamma & , & \equant{x_\sigma}p\ x )\\
(\Gamma & , & (\equant{f_{\alpha\fun\sigma}}{\sf Type\_Definition}\
                 p\ f)\ \imp\ q )
\end{eqnarray*}
sono in ${\sf Theorems}_{\cal T}$.

\end{myenumerate}
L'estensione di una teoria standard $\cal T$ per mezzo di una tale specifica
di tipo è denotata
\[
{\cal T}{+_{\it tyspec}} \langle
(\alpha_1,\ldots,\alpha_n)\ty{op},\sigma,p,\alpha,\Gamma,q\rangle
\]
ed è definita essere la teoria
\[
\langle
\begin{array}[t]{@{}l}
{\sf Struc}_{\cal T}\cup\{(\ty{op},n)\},\\
  {\sf Sig}_{\cal T},\\
  {\sf Axioms}_{\cal
  T}\cup\{(\Gamma , q[(\alpha_1,\ldots,\alpha_n)\ty{op}/\alpha])\},\\
  {\sf Theorems}_{\cal T}\rangle
\end{array}
\]

\noindent{\bf Esempio\ } Per eseguire l'estensione di \theory{INIT}
mensionata all'inizio di questa sezione, si forma
\[
\theory{INIT}{+_{\it tyspec}} \langle
()\ty{one},\ty{bool},p,\alpha,\emptyset,q\rangle
\]
dove $p$ è il termine $\lquant{b_\bool}b$ e $q$ è la formula
$\uquant{f_{\beta\fun\alpha}\ g_{\beta\fun\alpha}}f=g$. Così il
risultato è una teoria che estende \theory{INIT} con una
nuova costante di tipo $\ty{one}$ che soddisfa l'assioma
$\uquant{f_{\beta\fun\ty{one}}\ g_{\beta\fun\ty{one}}}f=g$.

Per verificare che questa è un'applicazione corretta del meccanismo
di estensione, si devono controllare le Condizioni da (i) a (vii) di sopra. Solo l'ultima
non è banale: essa impone l'obbligo di dimostrare
due sequenti dagli assiomi di \theory{INIT}. Il primo sequente dice
che $p$ definisce un sottoinsieme abitato di $\bool$, il che è certamente
vero dal momento che $\T$ testimonia questo fatto. Il secondo sequente dice
in effetti che qualsiasi tipo $\alpha$ che sia in biezione con il sottoinsieme di
$\bool$ definito da $p$ ha la proprietà che c'è al massimo una
funzione ad esso da qualsiasi tipo dato $\beta$; la dimostrazione di questo dagli
assiomi di \theory{INIT} è lasciata come esercizio.

\medskip

\noindent{\bf Proposizione\ }{\em
The theory ${\cal T}{+_{\it tyspec}}\langle
(\alpha_1,\ldots,\alpha_n)\ty{op},\sigma,p,\alpha,\Gamma,q
\rangle$ ha un modello standard se la teoria ${\cal T}$ lo ha.}

\medskip

\noindent{\bf Dimostrazione\ }
Scriviamo $\alpha\!s$ per $\alpha_1,\ldots,\alpha_n$, e supponiamo che
$\alpha\!s'={\alpha'}_1,\ldots,{\alpha'}_m$  sia la lista delle variabili
di tipo che occorrono in $\Gamma$ e $q$, ma che non sono ancora nella lista
$\alpha\!s,\alpha$.

Supponiamo che $M$ sia un modello standard di ${\cal T}$. Dal momento che $\alpha\!s,.p$ è
un termine-in-contesto di tipo $\sigma\fun\ty{bool}$, interpretarlo in
$M$ porta a
\[
\den{\alpha\!s,.p}_{M}
\in \prod_{X\!s\in{\cal U}^{n}}\den{\alpha\!s.\sigma\fun\ty{bool}}_M(X\!s)
= \prod_{X\!s\in{\cal U}^{n}}
   \den{\alpha\!s.\sigma}_M(X\!s)\fun\two .
\]

Non c'è alcuna perdita di generalità nell'assumere che $\Gamma$ consista di
una singola formula $\gamma$. (Semplicemente rimpiazziamo $\Gamma$ con la congiunzione delle
formula che esso contiene, con la convenzione che questa congiunzione sia
$\T$ se $\Gamma$ è vuoto.) Per l'assunzione su $\alpha\!s'$ e per la
Condizione~(iv), $\alpha\!s,\alpha\!s',.\gamma$ è un termine-in-contesto.
Interpretarlo in $M$ porta a
\[
\den{\alpha\!s,\alpha\!s'.\gamma}_{M}
\in \prod_{(X\!s,X\!s')\in
{\cal U}^{n+m}}\den{\alpha\!s,\alpha\!s'.\ty{bool}}_M(X\!s,X\!s')
={\cal U}^{n+m}\fun\two
\]

Ora $(\gamma,\equant{x_{\sigma}}p\ x)$ è in ${\sf Theorems}_{\cal T}$
e di conseguenza per il Teorema di Validità~\ref{soundness} questo sequente è
soddisfatto da $M$. Usando la semantica di $\exists$ data nella
Sezione~\ref{LOG} e la definizione di soddisfacimento di un sequente dalla
Sezione~\ref{sequents}, questo significa che per tutti gli $(X\!s,X\!s')\in{\cal U}^{n+m}$
se $\den{\alpha\!s,\alpha\!s'.\gamma}_M(X\!s,X\!s')=1$, allora
l'insieme
\[
\{y\in\den{\alpha\!s.\sigma}_{M}\: :\: \den{\alpha\!s,.p}(X\!s)(y)=1\}
\]
non è vuoto. (Questo usa il fatto che $p$ non coinvolge
le variabili di tipo $\alpha\!s'$, così per il Lemma~4 nella
Sezione~\ref{term-substitution}
$\den{\alpha\!s,\alpha\!s'.p}_M(X\!s,X\!s')=\den{\alpha\!s,.p}_M(X\!s)$.)
Dal momento che è anche un sottoinsieme di un insieme in $\cal U$, esso
segue per la proprietà {\bf Sub} dell'universo che questo insieme è un elemento di
$\cal U$. Così definendo
\[
S(X\!s) = \left\{\hspace{-1mm}
\begin{array}{ll}
\{y\in\den{\alpha\!s.\sigma}_{M} : \den{\alpha\!s,.p}(X\!s)(y)=1\}
  & \mbox{\rm se $\den{\alpha\!s,.\gamma}_M(X\!s,X\!s')=1$, qualche $X\!s'$}\\
1 & \mbox{\rm altrimenti}
\end{array}
\right.%\}
\]
si ha che $S$ è una funzione ${\cal U}^n\fun{\cal U}$. Estendiamo $M$
a un modello della firma di ${\cal T}'$ definendo che il suo valore alla
nuova costante di tipo $n$-aria $\ty{op}$ sia questa funzione $S$. Si noti
che i valori di $\sigma$, $p$, $\gamma$ e
$q$ in $M'$ sono gli stessi di quelli in $M$, dal momento che queste espressioni non
coinvolgono la nuova costante di tipo $\ty{op}$.

Per ogni $X\!s\in{\cal U}^{n}$ definiamo $i_{X\!s}$ essere la funzione
d'inclusione per il sottoinsiem $S(X\!s)\subseteq\den{\alpha\!s.\sigma}_{M}$
se $\den{\alpha\!s,\alpha\!s'.\gamma}_M(X\!s,X\!s')=1$ per qualche
$X\!s'$, e altrimenti essere la funzione
$1\fun\den{\alpha\!s.\sigma}_{M}$ che manda $0\in 1$ in
$\ch(\den{\alpha\!s.\sigma}_{M})$. Allora
$i_{X\!s}\in(S(X\!s)\fun\den{\alpha\!s.\sigma}_{M'}(X\!s))$ poiché
$\den{\alpha\!s.\sigma}_{M'}=\den{\alpha\!s.\sigma}_M$. Usando la
semantica di $\TyDef$ data nella Sezione~\ref{LOG}, si ha che per qualsiasi
$(X\!s,X\!s')\in{\cal U}^{n+m}$, se
$\den{\alpha\!s,\alpha\!s'.\gamma}_{M'}(X\!s,X\!s')=1$ allora
\[
\den{\TyDef}_{M'}(\den{\alpha\!s.\sigma}_{M'} ,
   S(X\!s))(\den{\alpha\!s,.p}_{M'})(i_{X\!s}) = 1.
\]
Così $M'$ soddisfa il sequente
\[
(\gamma\ ,\ \equant{f_{(\alpha\!s)\ty{op}\fun\sigma}}\TyDef\ p\ f).
\]
Ma dal momento che il sequente $(\gamma,(\equant{f_{\alpha\fun\sigma}}{\sf
Type\_Definition}\ p\ f)\ \imp\ q )$ è in ${\sf Theorems}_{\cal T}$,
è soddisfatto dal modello $M$ e di conseguenza anche dal modello $M'$
(dal momento che il sequente non coinvolge la nuova costante di tipo $\ty{op}$).
Istanziando $\alpha$ a $(\alpha\!s)\ty{op}$ in questo sequente (cosa che
è ammissibile dal momento che per la Condizione~(iv) $\alpha$ non occorre in
$\gamma$), si ha che $M'$ soddisfa il sequente
\[
(\gamma\ ,\
(\equant{f_{(\alpha\!s)\ty{op}\fun\sigma}}\TyDef\ p\ f)\imp
q[(\alpha\!s)\ty{op}/\alpha]).
\]
Applicando il Modus Ponens, si conclude che $M'$ soddisfa
$(\gamma\ ,\ q[(\alpha\!s)\ty{op}/\alpha])$ e
quindi $M'$ è un modello di ${\cal T}'$, come richiesto.

\medskip

Un'estensione per definizione di tipo è di fatto un caso speciale di estensione
per specifica di tipo. Per vedere questo, supponiamo che
$\langle (\alpha_1,\ldots,\alpha_n)\ty{op},\ \sigma,\
p_{\sigma\fun\ty{bool}}\rangle$ sia una definizione di tipo per una teoria
$\cal T$. Scegliendo una variabile di tipo $\alpha$ differente da
$\alpha_1,\ldots,\alpha_n$, $q$ denoti la formula
\[
\equant{f_{\alpha\fun\sigma}}{\sf Type\_Definition}\ p\ f
\]
Allora $\langle
(\alpha_1,\ldots,\alpha_n)\ty{op},\sigma,p,\alpha,\emptyset,q\rangle$
soddisfa tutte le condizioni necessarie per essere una specifica di tipo per
$\cal T$. Dal momento che $q[(\alpha_1,\ldots,\alpha_n)\ty{op}/\alpha]$ è solo
$\equant{f_{(\alpha_1,\ldots,\alpha_n)\ty{op}\fun\sigma}}{\sf
Type\_Definition}\ p\ f$, si ha che
\[
{\cal T}{+_{tydef}}
\langle(\alpha_1,\ldots,\alpha_n)\ty{op},\sigma,p\rangle
={\cal T}{+_{\it tyspec}}
\langle(\alpha_1,\ldots,\alpha_n)\ty{op},\sigma,p,\alpha,\emptyset,q\rangle
\]
Così la Proposizione nella Sezione~\ref{tydefs} è un caso speciale della
Proposizione di sopra.

In un'estensione per specifica di tipo, la proprietà $q$ che è
affermata della nuova costante di tipo introdotta non ha bisogno di determinare la
costante di tipo in modo univoco (persino fino alla biezione). In modo corrispondente ci
possono essere molti modelli standard differenti della nuova teoria estesa la
cui restrizione a $\cal T$ è un dato modello $M$. Per contro, una definizione
di tipo determina la nuova costante di tipo in modo univoco fino alla biezione,
e due modelli qualsiasi della teoria estesa che si restringono allo stesso
modello della teoria originaria saranno isomorfi.
\index{extension, della logica HOL@extension, della logica \HOL{}!by type specification|)}



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