1% Revised version of Part II, Chapter 10 of HOL DESCRIPTION 2% Incorporates material from both of chapters 9 and 10 of the old 3% version of DESCRIPTION 4% Written by Andrew Pitts 5% 8 March 1991 6% revised August 1991 7\chapter{Teorie}\label{semantics} 8 9\section{Introduzione} 10 11Il risultato, se ce n'� uno, di una sessione con il sistema \HOL{} � un oggetto 12chiamato una {\it teoria\/}. Questo oggetto � strettamente collegato con ci� che un 13logico chiamerebbe una teoria\index{theories, nella logica HOL@teorie, nella logica \HOL{}!forma astratta di}, ma ci sono alcune differenze che sorgono 14dalle necessit� della dimostrazione meccanica. Una teoria \HOL{}, come la teoria di 15un logico, contiene insiemi di tipi, costanti, definizioni e assiomi. In 16aggiunta, tuttavia, una teoria \HOL{}, in qualsiasi punto del tempo, contiene una 17esplicita lista di teoremi che sono gi� stati dimostrati dagli 18assiomi e dalle definizioni. I logici non hanno alcuna necessit� di distinguere i teoremi 19attualmente dimostrati da quelli meramente dimostrabili; di conseguenza essi normalmente non 20considerano insiemi di teoremi dimostrati come parte di una teoria; piuttosto, essi 21considerano i teoremi di una teoria essere l'insieme (spesso infinito) di tutte 22le conseguenze degli assiomi e le definizioni. Una differenza collegata 23tra le teorie dei logici e le teorie \HOL{} � che per i logici, 24le teorie sono oggetti statici, ma in \HOL{} esse possono essere pensate come 25potenzialmente estensibili. Per esempio, il sistema \HOL{} fornisce strumenti 26per aggiungere alle teorie e combinare teorie. Un'interazione tipica 27con \HOL{} consiste nel combinare qualche teoria esistente, facendo qualche 28definizione, dimostrando alcuni teoremi e poi salvare i nuovi risultati. 29 30Lo scopo del sistema \HOL{} � di fornire strumenti per permettere 31di costruire teorie ben-formate. La logica \HOL{} � tipizzata: 32ogni teoria specifica una firma di constanti di tipo e individuali; 33queste poi determinano gli insiemi dei tipi e dei termini come nel capitolo 34precedente. Tutti i teoremi di tali teorie sono conseguenze logiche 35delle definizioni e degli assiomi della teoria. Il sistema \HOL{} assicura 36che solo teorie ben-formate possono essere costruite permettendo di creare 37teoremi solo per {\it dimostrazione formale\/}. Esplicitare questo comporta 38definire cosa significa essere un teorema, il che porta alla descrizione 39del sistema di dimostrazione di \HOL{}, che sar� dato di seguito. Esso � dimostrato essere {\em 40valido\/} per la semantica insiemistica di \HOL{} descritta nel 41capitolo precedente. Questo significa che un teorema � soddisfatto da un modello 42se ha una dimostrazione formale da assiomi che sono a loro volta soddisfatti dal 43modello. Dal momento che una contraddizione logica non � soddisfatta da alcun 44modello, questo garantisce in particolare che una teoria che possiede un modello 45� necessariamente coerente, cio� non pu� essere dimostrata una contraddizione 46logica dai suoi assiomi. 47 48Questo capitolo descrive anche i vari meccanismi per i quali le teorie 49\HOL\ possono essere estese a nuove teorie. Ogni meccanismo � mostrato 50preservare la propriet� di possedere un modello. Cos� le teorie costruite 51dalla teoria \HOL{} iniziale (che possiede un modello) usando 52questi meccanismi sono garantite essere coerenti. 53 54 55\section{Sequenti} 56\label{sequents} 57 58La logica \HOL{} � formulata in termini di asserzioni ipotetiche chiamate 59{\em sequenti}\index{sequenti!nella deduzione naturale}. Fissando una 60firma (standard) $\Sigma_\Omega$, un sequente � una coppia $(\Gamma, 61t)$ dove $\Gamma$ � un insieme finito di formule su $\Sigma_\Omega$ 62e $t$ � una singola formula su $\Sigma_\Omega$\footnote{Si noti che 63il sottoscritto di tipo � omesso dai termini quando � chiaro dal 64contesto che essi sono formule, cio� hanno tipo \ty{bool}.}. L'insieme di 65formule $\Gamma$ che formano il primo componente di un sequente � chiamato 66il suo insieme di {\it assunzioni\/}\index{assunzioni!di sequenti} e il 67termine $t$ che forma il secondo componente � chiamato la sua {\it 68conclusione\/}\index{conclusioni!di sequenti}. Quando non d� origine ad 69ambiguit�, un sequente $(\{\},t)$ � scritto semplicemente $t$. 70 71 72Intuitivamente un modello $M$ di $\Sigma_\Omega$ {\em 73soddisfa}\index{soddisfazione di sequenti, da parte di un modello} un sequente 74$(\Gamma, t)$ se qualsiasi interpretazione delle variabili libere rilevanti come 75elementi di $M$ che rendono le formule in $\Gamma$ vere, rendono vera 76anche la formula $t$. Per rendere questo pi� preciso, supponiamo che 77$\Gamma=\{t_1,\ldots,t_p\}$ e sia $\alpha\!s,\!x\!s$ un 78contesto contenente tutte le variabili di tipo e tutte le variabili libere 79che occorrono nelle formule $t,t_{1},\ldots,t_{p}$. Supponiamo che 80$\alpha\!s$ abbia lunghezza $n$, che $x\!s=x_{1},\ldots,x_{m}$ e che il 81tipo di $x_{j}$ sia $\sigma_{j}$. Dal momento che le formule sono termini di tipo 82$\bool$, la semantica dei termini definita nel capitolo precedente da 83origine a elementi $\den{\alpha\!s,\!x\!s.t}_M$ e 84$\den{\alpha\!s,\!x\!s.t_{k}}_M$ ($k=1,\ldots,p$) in 85\[ 86\prod_{X\!s\in{\cal U}^{n}} \left( 87\prod_{j=1}^{m}\den{\alpha\!s.\sigma_{j}}_M(X\!s)\right) \fun \:\two \] 88Diciamo che il modello $M$ {\em soddisfa\/} il sequente $(\Gamma,t)$ e 89scriviamo 90\[ 91\Gamma \models_{M} t 92\] 93se per tutti gli $X\!s\in{\cal U}^{n}$ e 94tutti gli $y\!s\in\den{\alpha\!s.\sigma_{1}}_M(X\!s)\times\cdots\times 95\den{\alpha\!s.\sigma_{m}}_M(X\!s)$ con 96\[ 97\den{\alpha\!s,\!x\!s.t_{k}}_M(X\!s)(y\!s)=1 98\] 99per tutti i $k=1,\ldots,p$, � anche il caso che 100\[ 101\den{\alpha\!s,\!x\!s.t}_M(X\!s)(y\!s)=1. 102\] 103(Si ricordi che $\two$ � l'insieme $\{0,1\}$.) 104 105Nel caso $p=0$, la soddisfazione di $(\{\},t)$ da parte di $M$ sar� scritta 106$\models_{M} t$. Cos� $\models_{M} t$ significa che la funzione dipendentemente tipizzata 107\[ 108\den{t}_M \in \prod_{X\!s\in{\cal U}^{n}} 109\left(\prod_{j=1}^{m}\den{\alpha\!s.\sigma_{j}}_M(X\!s)\right) \fun \:\two 110\] 111� costante con valore $1\in\two$. 112 113\section{Logica} 114 115Un sistema deduttivo\index{sistemi deduttivi} 116${\cal D}$ � un insieme di coppie $(L,(\Gamma,t))$ dove $L$ � una 117lista (possibilmente vuota) di sequenti e $(\Gamma,t)$ � un sequente. 118 119Un sequente $(\Gamma,t)$ segue da\index{segue da, nella deduzione naturale} 120un insieme di sequenti 121$\Delta$ per un sistema deduttivo 122${\cal D}$ se 123e solo se esistono sequenti 124$(\Gamma_1,t_1)$, $\ldots$ , $(\Gamma_n,t_n)$ tali che: 125\begin{enumerate} 126\item $(\Gamma,t) = (\Gamma_n,t_n)$, e 127\item per tutti gli $i$ tali che $1\leq i\leq n$ 128\begin{enumerate} 129\item o 130$(\Gamma_i,t_i)\in \Delta$ o 131\item $(L_i,(\Gamma_i,t_i))\in{\cal D}$ per qualche lista $L_i$ di membri di 132$\Delta\cup\{(\Gamma_1,t_1),\ldots,(\Gamma_{i-1},t_{i-1})\}$ . 133\end{enumerate} 134\end{enumerate} 135La sequenza $(\Gamma_1,t_1),\cdots,(\Gamma_n,t_n)$ 136� chiamata una {\it dimostrazione\/}\index{dimostrazione!nella deduzione naturale} di 137$(\Gamma,t)$ da $\Delta$ rispetto a ${\cal D}$. 138 139Si noti che se $(\Gamma,t)$ segue da $\Delta$, allora anche $(\Gamma,t)$ 140segue da qualsiasi $\Delta'$ tale che $\Delta\subseteq\Delta'$. 141Questa propriet� � chiamata {\it monotonicit�\/}\index{monotonicit�, nei sistemi deduttivi}. 142 143La notazione\index{turnstile} $t_1,\ldots,t_n\vdash_{{\cal 144D},\Delta} t$ significa che il sequente $(\{t_1,\ldots,t_n\},\ t)$ 145segue da $\Delta$ per ${\cal D}$. Se o ${\cal D}$ o $\Delta$ 146� chiaro dal contesto allora pu� essere omesso. Nel caso in cui 147non ci siano ipotesi\index{ipotesi!di sequenti} (cio� $n=0$), 148si scrive semplicemente $\vdash t$. 149 150In pratica, un particolare sistema deduttivo � di solito specificato da un 151numero di \emph{regole d'inferenza} (schematiche), 152\index{regole d'inferenza, della logica HOL@regole d'inferenza, della logica \HOL{}!forma astratta di primitive} 153che prendono la forma 154\[ 155\frac{\Gamma_1\turn t_1 \qquad\cdots\qquad\Gamma_n\turn t_n} 156{\Gamma \turn t} 157\] 158I sequenti sopra la linea sono chiamate le {\it 159ipotesi\/}\index{ipotesi!di regole d'inferenza} della regola e il 160sequente sotto la linea � chiamato la sua {\it 161conclusione}\index{conclusioni!di regole d'inferenza}. Una tale regola � 162schematica perch� pu� contenere meta-variabili 163che stanno per termini arbitrari dei tipi appropriati. Istanziando 164queste meta-variabili con termini reali, si ottiene una lista di sequenti 165sopra la linea e un singolo sequente sotto la linea che insieme 166costituiscono un elemento particolare del sistema deduttivo. Le 167istanziazioni permesse per una particolare regola possono essere ristrette 168imponendo una {\em condizione a lato\/} della regola. 169 170 171\subsection{Il sistema deduttivo \HOL{}} 172\label{HOLrules} 173 174Il sistema deduttivo della logica \HOL{} � specificato da otto regole 175d'inferenza, date di seguito. Le prime tre regole non hanno ipotesi; 176le loro conclusioni possono essere dedotte sempre. Gli identificatori nelle parentesi 177quadre sono i nomi delle funzioni \ML\ nel sistema \HOL{} che 178implementano le corrispondenti regole d'inferenza (si veda \DESCRIPTION). Qualsiasi 179condizioni a lato che restringano lo scopo di una regola sono date immediatamente 180al di sotto di essa. 181 182\bigskip 183 184\subsubsection*{Introduzione di assunzione [{\small\tt 185ASSUME}]}\index{introduzione di assunzione, nella logica HOL@Introduzione di assunzione, nella logica \HOL{}!forma astratta di} 186\[ 187\overline{t \turn t} 188\] 189 190\subsubsection*{Riflessivit� [{\small\tt 191REFL}]}\index{REFL@\ml{REFL}}\index{riflessivit�, nella logica HOL@riflessivit�, nella logica \HOL{}!forma astratta di} 192\[ 193\overline{\turn t = t} 194\] 195 196\subsubsection*{Beta-conversione [{\small\tt BETA\_CONV}]} 197\index{beta-conversione, nella logica HOL@beta-conversione, nella logica \HOL{}!forma astratta di}\index{BETA_CONV@\ml{BETA\_CONV}} 198\[ 199\overline{\turn (\lquant{x}t_1)t_2 = t_1[t_2/x]} 200\] 201\begin{itemize} 202\item Dove $t_1[t_2/x]$ � 203il risultato di sostituire $t_2$ per $x$ 204in $t_1$, con un'adatta rinomina delle variabili per impedire che le variabili libere 205in $t_2$ diventino legate dopo la sostituzione. 206\end{itemize} 207 208\subsubsection*{Sostituzione [{\small\tt 209SUBST}]}\index{SUBST@\ml{SUBST}} \index{sostituzione regola, nella logica HOL@sostituzione, regola di, nella logica \HOL{}!forma astratta di} 210\[ 211\frac{\Gamma_1\turn t_1 = t_1'\qquad\cdots\qquad\Gamma_n\turn t_n = 212t_n'\qquad\qquad \Gamma\turn t[t_1,\ldots,t_n]} 213{\Gamma_1\cup\cdots\cup\Gamma_n\cup\Gamma\turn t[t_1',\ldots,t_n']} 214\] 215\begin{itemize} 216\item Dove $t[t_1,\ldots,t_n]$ denota un termine $t$ con alcune occorrenze 217libere di sottotermini $t_1$, $\ldots$ , $t_n$ isolati e 218$t[t_1',\ldots,t_n']$ denota il risultato di sostituire ciascuna occorrenza 219selezionata di $t_i$ per $t_i'$ (per $1{\leq}i{\leq}n$), con una rinomina 220adatta delle variabili per impedire che variabili libere in $t_1'$ diventino 221legate dopo la sostituzione. 222\end{itemize} 223 224\subsubsection*{Astrazione [{\small\tt ABS}]} 225\index{ABS@\ml{ABS}}\index{regola di astrazione} 226\[ 227\frac{\Gamma\turn t_1 = t_2} 228{\Gamma\turn (\lquant{x}t_1) = (\lquant{x}t_2)} 229\] 230\begin{itemize} 231\item Purch� $x$ non sia libera in $\Gamma$. 232\end{itemize} 233 234\subsubsection*{Istanziazione di tipo [{\small\tt INST\_TYPE}]} 235\index{type instantiation, nella logica HOL@type instantiation, nella logica \HOL{}!forma astratta di} 236\newcommand{\insttysub}{[\sigma_1,\ldots,\sigma_n/\alpha_1,\ldots,\alpha_n]} 237\[ 238\frac{\Gamma\turn t} 239{\Gamma\insttysub\turn t\insttysub} 240\] 241\begin{itemize} 242\item Dove $t\insttysub$ � il risultato di sostituire, in parallelo, 243 i tipi $\sigma_1$, $\dots$, $\sigma_n$ per le variabili di tipo 244 $\alpha_1$, $\dots$, $\alpha_n$ in $t$, e dove $\Gamma\insttysub$ 245 � il risultato di eseguire la stessa sostituzione in tutte le 246 ipotesi del teorema. 247\item Dopo l'istanziazione, le variabili libere nell'input non possono 248 diventare legate, ma variabili libere distinte nell'input possono diventare 249 identiche. 250\end{itemize} 251 252\subsubsection*{Scaricamento di assunzione [{\small\tt 253DISCH}]}\index{discharging assumptions, nella logica HOL@discharging assumptions, nella logica \HOL{}!forma astratta di}\index{DISCH@\ml{DISCH}} 254\[ 255\frac{\Gamma\turn t_2} 256{\Gamma -\{t_1\} \turn t_1 \imp t_2} 257\] 258\begin{itemize} 259\item Dove $\Gamma -\{t_1\}$ � la sottrazione insiemistica di $\{t_1\}$ 260da $\Gamma$. 261\end{itemize} 262 263\subsubsection*{Modus Ponens [{\small\tt 264MP}]}\index{MP@\ml{MP}}\index{Modus Ponens, nella logica HOL@Modus Ponens, nella logica \HOL{}!forma astratta di} 265\[ 266\frac{\Gamma_1 \turn t_1 \imp t_2 \qquad\qquad \Gamma_2\turn t_1} 267{\Gamma_1 \cup \Gamma_2 \turn t_2} 268\] 269 270In aggiunta a queste otto regole, ci sono anche quattro {\it 271assiomi\/}\index{assiomi!come regole d'inferenza} che avrebbero potuto essere 272considerate come regole d'inferenza senza le ipotesi. Questo non � fatto, 273tuttavia, dal momento che � pi� naturale formulare gli assiomi usando qualche 274costante logica definita e il principio di definizione di costante non � 275stato ancora descritto. Gli assiomi sono dati nella Sezione~\ref{INIT} e 276le definizioni delle costanti logiche extra che essi coinvolgono sono date nella 277Sezione~\ref{LOG}. 278 279Il particolare insieme di regole e assiomi scelti per assiomatizzare la logica 280\HOL\ � piuttosto arbitrario. In parte � basato sulle regole che erano state 281utilizzate nella logica 282\LCF\index{LCF@\LCF}\ 283\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 284implementato modificando il sistema \LCF. In particolare, la 285regola di sostituzione\index{substitution rule, nella logica HOL@substitution rule, nella logica \HOL{}!implementation of} {\small\tt SUBST} � esattamente 286la stessa della corrispondente regola in \LCF; il codice che implementa questa regola 287fu scritto da Robin Milner ed � altamente ottimizzato. Poich� 288la sostituzione � un'attivit� cos� pervasiva nella dimostrazione, si � ritenuto 289importante che la primitiva di sistema fosse il pi� veloce possibile. Da un 290punto di vista logico sarebbe stato meglio avere una primitiva 291di sostituzione pi� semplice, come la `Regola R' della logica di Andrews ${\cal 292Q}_0$, e poi derivare regole pi� complicate da essa. 293 294\subsection{Teorema di validit�} 295\index{soundness!of HOL deductive system@of \HOL{} deductive system} 296\label{soundness} 297 298\index{inference rules, della logica HOL@inference rules, della logica \HOL{}!formal semantics of} 299\emph{Le regole del sistema deduttivo \HOL{} sono {\em valide} per 300 la nozione di soddisfacimento definita nella Sezione~\ref{sequents}: per 301 qualsiasi istanza di regole d'inferenza, se un modello (standard) 302 soddisfa le ipotesi della regola soddisfa anche la 303 conclusione.} 304 305\medskip 306 307\noindent{\bf Dimostrazione\ } 308La verifica della validit� delle regole � semplice. 309Le propriet� della semantica rispetto alla sostituzione date dai 310Lemmi 3 e 4 nella Sezione~\ref{term-substitution} sono necessari per le regole 311\ml{BETA\_CONV}, \ml{SUBST} and 312\ml{INST\_TYPE}\index{INST_TYPE@\ml{INST\_TYPE}}\footnote{Si noti in 313 particolare che la seconda restrizione su \ml{INST\_TYPE} permette 314 il risultato sulla semantica della sostituzione di tipi per variabili di tipo 315 nei termini da applicare}. Il fatto che $=$ e $\imp$ siano 316interpretate in modo standard (come nella Sezione~\ref{standard-signatures}) � 317necessario per le regole \ml{REFL}\index{REFL@\ml{REFL}}, 318\ml{BETA\_CONV}\index{BETA_CONV@\ml{BETA\_CONV}}, 319\ml{SUBST}\index{SUBST@\ml{SUBST}}, \ml{ABS}\index{ABS@\ml{ABS}}, 320\ml{DISCH}\index{DISCH@\ml{DISCH}} e \ml{MP}\index{MP@\ml{MP}}. 321 322\section{Teorie \HOL{}} 323\label{theories} 324 325Una {\it teoria\/}\index{theories, nella logica HOL@theories, nella logica \HOL{}!forma astratta di} \HOL{} ${\cal T}$ � una $4$-tupla: 326\begin{eqnarray*} 327{\cal T} & = & \langle{\sf Struc}_{\cal T},{\sf Sig}_{\cal T}, 328 {\sf Axioms}_{\cal T},{\sf Theorems}_{\cal T}\rangle 329\end{eqnarray*} 330dove 331\begin{myenumerate} 332 333\item ${\sf Struc}_{\cal T}$ � una struttura di tipo\index{type structures, of HOL theories@type structures, of \HOL{} theories} chiamata la 334struttura di tipo di ${\cal T}$; 335 336\item ${\sf Sig}_{\cal T}$ � una firma\index{signatures, della logica HOL@signatures, della logica \HOL{}!of HOL theories@of \HOL{} theories} 337su ${\sf Struc}_{\cal T}$ chiamata la firma di ${\cal T}$; 338 339\item ${\sf Axioms}_{\cal T}$ � un insieme di sequenti su ${\sf Sig}_{\cal T}$ 340chiamati gli assiomi\index{assiomi, in una teoria HOL@assiomi, in una teoria \HOL{}} 341 di ${\cal T}$; 342 343\item ${\sf Theorems}_{\cal T}$ � un insieme di sequenti su 344${\sf Sig}_{\cal T}$ chiamati i teoremi 345% 346\index{theorems, nella logica HOL@theorems, nella logica \HOL{}!forma astratta di} 347% 348di ${\cal T}$, con 349la propriet� che ogni membro segue da ${\sf Axioms}_{\cal T}$ per 350il sistema deduttivo \HOL{}. 351 352\end{myenumerate} 353 354Gli insiemi ${\sf Types}_{\cal T}$ e ${\sf Terms}_{\cal T}$ dei tipi e 355dei termini di una teoria ${\cal T}$ sono, rispettivamente, gli insiemi dei tipi e 356dei termini costruibili dalla struttura di tipo e dalla firma di ${\cal 357T}$, cio�: 358\begin{eqnarray*} 359{\sf Types}_{\cal T} & = & {\sf Types}_{{\sf Struc}_{\cal T}}\\ 360{\sf Terms}_{\cal T} & = & {\sf Terms}_{{\sf Sig}_{\cal T}} 361\end{eqnarray*} 362Un modello di una teoria $\cal T$ � specificato dando un modello (standard) 363$M$ della sottostante firma della teoria con la propriet� che 364$M$ soddisfa tutti i sequenti che sono assiomi di $\cal T$. A causa 365del Teorema di Validit�~\ref{soundness}, segue che $M$ soddisfa 366anche qualunque sequente nell'insieme dei teoremi dati, ${\sf 367Theorems}_{\cal T}$. 368 369\subsection{La teoria {\tt MIN}} 370\label{sec:min-thy} 371 372La {\it teoria minimale\/}\index{MIN@\ml{MIN}}\index{minimal theory, della logica HOL@minimal theory, della logica \HOL{}} \theory{MIN} � definita da: 373\[ 374\theory{MIN} = 375\langle\{(\bool,0),\ (\ind,0)\},\ 376 \{\imp_{\bool\fun\bool\fun\bool}, 377=_{\alpha\fun\alpha\fun\bool}, 378\hilbert_{(\alpha\fun\bool)\fun\alpha}\},\ 379\{\},\ \{\}\rangle 380\] 381Dal momento che la teoria \theory{MIN} ha una firma che consiste solo di 382elementi standard e non ha assiomi, essa possiede un unico modello standard, 383che sar� indicato con {\em Min}. 384 385Bench� la teoria \theory{MIN} contiene solo la sintassi standard 386minimale, sfruttando i costrutti di ordine superiore di \HOL{} si pu� 387costruire su di essa una collezione di termini piuttosto ricca. La seguente 388teoria introduce nomi per alcuni di questi termini che denotano utili 389operazioni logiche nel modello {\em Min}. 390 391Nell'implementazione, alla teoria \theory{MIN} � dato il nome 392\theoryimp{min}, e contiene anche il distinto operatore di tipo 393binario $\fun$, per costruire spazi di funzione. 394 395\subsection{La teoria {\tt LOG}} 396\index{LOG@\ml{LOG}} 397\label{LOG} 398 399La teoria \theory{LOG} ha la stessa struttura 400di tipo di \theory{MIN}. La sua firma contiene le costanti in 401\theory{MIN}. e le seguenti costanti: 402\[ 403\T_\ty{bool} 404\index{T@\holtxt{T}!forma astratta di} 405\index{truth values, nella logica HOL@truth values, nella logica \HOL{}!forma astratta di} 406\] 407\[ 408\forall_{(\alpha\fun\ty{bool})\fun\ty{bool}} 409\index{universal quantifier, nella logica HOL@universal quantifier, nella logica \HOL{}!forma astratta di} 410\] 411\[ 412\exists_{(\alpha\fun\ty{bool})\fun\ty{bool}} 413\index{existential quantifier, nella logica HOL@existential quantifier, nella logica \HOL{}!forma astratta di} 414\] 415\[ 416\F_\ty{bool} 417\index{F@\holtxt{F}!forma astratta di} 418\] 419\[ 420\neg_{\ty{bool}\fun\ty{bool}} 421\index{negation, nella logica HOL@negation, nella logica \HOL{}!forma astratta di} 422\] 423\[ 424\wedge_{\ty{bool}\fun\ty{bool}\fun\ty{bool}} 425\index{conjunction, nella logica HOL@conjunction, nella logica \HOL{}!forma astratta di} 426\] 427\[ 428\vee_{\ty{bool}\fun\ty{bool}\fun\ty{bool}} 429\index{disjunction, nella logica HOL@disjunction, nella logica \HOL{}!forma astratta di} 430\] 431\[ 432\OneOne_{(\alpha\fun\beta)\fun\ty\bool} 433\index{one-to-one predicate, nella logica HOL@one-to-one predicate, nella logica \HOL{}!forma astratta di} 434\] 435\[ 436\Onto_{(\alpha\fun\beta)\fun\ty\bool} 437\index{onto predicate, nella logica HOL@onto predicate, nella logica \HOL{}!forma astratta di} 438\] 439\[ 440\TyDef_{(\alpha\fun\ty{bool})\fun(\beta\fun\alpha)\fun\ty{bool}} 441\] 442In connessione con queste costanti � usata la seguente notazione speciale: 443\begin{center} 444\index{existential quantifier, nella logica HOL@existential quantifier, nella logica \HOL{}!abbreviation for multiple} 445\index{universal quantifier, nella logica HOL@universal quantifier, nella logica \HOL{}!abbreviation for multiple} 446\begin{tabular}{|l|l|}\hline 447{\rm Notation} & {\rm Meaning}\\ \hline $\uquant{x_{\sigma}}t$ & 448$\forall(\lambda x_{\sigma}.\ t)$\\ \hline $\uquant{x_1\ x_2\ \cdots\ 449x_n}t$ & $\uquant{x_1}(\uquant{x_2} \cdots\ (\uquant{x_n}t) 450\ \cdots\ )$\\ \hline 451$\equant{x_{\sigma}}t$ 452 & $\exists(\lambda x_{\sigma}.\ t)$\\ \hline 453$\equant{x_1\ x_2\ \cdots\ x_n}t$ 454 & $\equant{x_1}(\equant{x_2} \cdots\ (\equant{x_n}t) 455\ \cdots\ )$\\ \hline 456$t_1\ \wedge\ t_2$ & $\wedge\ t_1\ t_2$\\ \hline 457$t_1\ \vee\ t_2$ & $\vee\ t_1\ t_2$\\ \hline 458\end{tabular}\end{center} 459 460Gli assiomi della teoria \theory{LOG} consistono dei seguenti 461sequenti: 462\[ 463\begin{array}{l} 464 465\turn \T = ((\lquant{x_{\ty{bool}}}x) = 466 (\lquant{x_{\ty{bool}}}x)) \\ 467\turn \forall = \lquant{P_{\alpha\fun\ty{bool}}}\ P = 468 (\lquant{x}\T ) \\ 469\turn \exists = \lquant{P_{\alpha\fun\ty{bool}}}\ 470 P({\hilbert}\ P) \\ 471\turn \F = \uquant{b_{\ty{bool}}}\ b \\ 472\turn \neg = \lquant{b}\ b \imp \F \\ 473\turn {\wedge} = \lquant{b_1\ b_2}\uquant{b} 474 (b_1\imp (b_2 \imp b)) \imp b \\ 475\turn {\vee} = \lquant{b_1\ b_2}\uquant{b} 476 (b_1 \imp b)\imp ((b_2 \imp b) \imp b) \\ 477\turn \OneOne = \lquant{f_{\alpha \fun\beta}}\uquant{x_1\ x_2} 478 (f\ x_1 = f\ x_2) \imp (x_1 = x_2) \\ 479\turn \Onto = \lquant{f_{\alpha\fun\beta}} 480 \uquant{y}\equant{x} y = f\ x \\ 481\turn \TyDef = \begin{array}[t]{l} 482 \lambda P_{\alpha\fun\ty{bool}}\ 483 rep_{\beta\fun\alpha}. 484 \OneOne\ rep\ \ \wedge{}\\ 485 \quad(\uquant{x}P\ x \ =\ (\equant{y} x = rep\ y)) 486 \end{array} 487\end{array} 488\] 489Ininfe, come per la teoria \theory{MIN}, l'insieme ${\sf 490Theorems}_{\theory{LOG}}$ � considerato essere vuoto. 491 492Si noti che gli assiomi della teoria \theory{LOG} sono essenzialmente {\em 493definizioni\/} delle nuove costanti di \theory{LOG} come termini nella 494teoria originaria \theory{MIN}. (Il meccanismo per fare tali 495estensioni alle teorie attraverso definizioni di nuove costanti sar� riportato 496in generale nella Sezione~\ref{defs}.) I primi sette assiomi definiscono le 497costanti logiche per la verit�, la quantificazione universale, la quantificazione 498esistenziale, la falsit�, la negazione, la congiunzione e la disgiunzione. 499Bench� queste definizioni possano essere oscure a qualche lettore, esse sono di 500fatto definizioni standard di queste costanti logiche in termini di 501implicazione, uguaglianza e scelta all'interno della logica di ordine superiore. I 502due assiomi successivi definiscono le propriet� di una funzione di essere iniettiva e suriettiva; 503esse saranno usate per esprimere l'assioma dell'infinito (si veda 504la Sezione~\ref{INIT}), tra le altre cose. L'ultimo assioma definisce una 505costante usata per le definizioni di tipo (si veda la Sezione~\ref{tydefs}). 506 507L'unico modello standard {\em Min\/} di \theory{MIN} d� origine a un 508unico modello standard di 509\theory{LOG}\index{LOG@\ml{LOG}!formal semantics of}. Questo 510perch�, data la semantica dei termini formulata nella 511Sezione~\ref{semantics of terms}, per soddisfare le equazioni di sopra si � 512costretti ad interpretare le nuove costanti nel modo seguente: 513\index{assiomi!semantica formale degli assiomi della logic HOL@semantica formale degli assiomi della logic \HOL{}|(} 514\begin{itemize} 515 516\item $\den{\T_{\bool}}\index{T@\holtxt{T}!formal semantics of} = 1 \in \two$ 517 518\item \index{universal quantifier, nella logica HOL@universal quantifier, nella logica \HOL{}!formal semantics of} 519$\den{\forall_{(\alpha\fun\bool)\fun\bool}}\in\prod_{X\in{\cal 520 U}}(X\fun\two)\fun\two$ manda $X\in{\cal U}$ e $f\in X\fun\two$ a 521\[ 522\den{\forall}(X)(f) = \left\{ \begin{array}{ll} 1 & \mbox{se 523$f^{-1}\{1\}=X$} \\ 0 & \mbox{altrimenti} \end{array} \right. 524\] 525\index{universal quantifier, nella logica HOL@universal quantifier, nella logica \HOL{}!formal semantics of} 526 527\item \index{existential quantifier, nella logica HOL@existential quantifier, nella logica \HOL{}!formal semantics of} 528$\den{\exists_{(\alpha\fun\bool)\fun\bool}}\in\prod_{X\in{\cal 529 U}}(X\fun\two)\fun\two$ manda $X\in{\cal U}$ e $f\in X\fun\two$ a 530\[ 531\den{\exists}(X)(f) = \left\{ \begin{array}{ll} 532 1 & \mbox{se $f^{-1}\{1\}\not=\emptyset$} \\ 533 0 & \mbox{altrimenti} 534 \end{array} 535 \right. \] 536 537\item $\den{\F_{\bool}} = 0 \in \two$\index{F@\holtxt{F}!formal semantics of} 538 539\item $\den{\neg_{\bool\fun\bool}}\in\two\fun\two$ manda $b\in\two$ a 540 \[ \den{\neg}(b) = \left\{ \begin{array}{ll} 541 1 & \mbox{se $b=0$} \\ 542 0 & \mbox{altrimenti} 543 \end{array} 544 \right. \]\index{negation, nella logica HOL@negation, nella logica \HOL{}!formal semantics of} 545 546\item $\den{\wedge_{\bool\fun\bool\fun\bool}}\in\two\fun\two\fun\two$ manda 547$b,b'\in\two$ a 548 \[ \den{\wedge}(b)(b') = \left\{ \begin{array}{ll} 549 1 & \mbox{se $b=1=b'$} \\ 550 0 & \mbox{altrimenti} 551 \end{array} 552 \right. \]\index{conjunction, nella logica HOL@conjunction, nella logica \HOL{}!formal semantics of} 553 554\item $\den{\vee_{\bool\fun\bool\fun\bool}}\in\two\fun\two\fun\two$ manda 555$b,b'\in\two$ a 556 \[ \den{\vee}(b)(b') = \left\{ \begin{array}{ll} 557 0 & \mbox{se $b=0=b'$} \\ 558 1 & \mbox{altrimenti} 559 \end{array} 560 \right. \]\index{disjunction, nella logica HOL@disjunction, nella logica \HOL{}!formal semantics of} 561 562\item $\den{\OneOne_{(\alpha\fun\beta)\fun\bool}}\in\prod_{(X,Y)\in{\cal 563 U}^{2}} (X\fun Y)\fun \two$ manda $(X,Y)\in{\cal U}^{2}$ e 564 $f\in(X\fun Y)$ a 565 \[ \den{\OneOne}(X,Y)(f) = \left\{ \begin{array}{ll} 566 0 & \mbox{se $f(x)=f(x')$ 567 per qualche $x\not=x'$ in $X$} \\ 568 1 & \mbox{altrimenti} 569 \end{array} 570 \right. \]\index{one-to-one predicate, nella logica HOL@one-to-one predicate, nella logica \HOL{}!formal semantics of} 571 572\item $\den{\Onto_{(\alpha\fun\beta)\fun\bool}}\in\prod_{(X,Y)\in{\cal 573 U}^{2}} (X\fun Y)\fun \two$ manda $(X,Y)\in{\cal U}^{2}$ e 574 $f\in(X\fun Y)$ a 575 \[ \den{\Onto}(X,Y)(f) = \left\{ \begin{array}{ll} 576 1 & \mbox{se $\{f(x):x\in X\}=Y$} \\ 577 0 & \mbox{altrimenti} 578 \end{array} 579 \right. \]\index{onto predicate, nella logica HOL@onto predicate, nella logica \HOL{}!formal semantics of} 580 581\item $\den{\TyDef_{(\alpha\fun\bool)\fun(\beta\fun\alpha)\fun\bool}}\in 582 \prod_{(X,Y)\in{\cal U}^{2}} (X\fun\two)\fun(Y\fun X)\fun\two$ \\ 583 manda $(X,Y)\in{\cal U}^{2}$, $f\in(X\fun\two)$ and $g\in(Y\fun X)$ a 584 \[ \den{\TyDef}(X,Y)(f)(g) = \left\{ \begin{array}{ll} 585 1 & \mbox{se 586 $\den{\OneOne}(Y,X)(g)=1$}\\ 587 & \mbox{e $f^{-1}\{1\}= 588 \{g(y) : y\in Y\}$} \\ 589 0 & \mbox{altrimenti.} 590 \end{array} 591 \right. 592\] 593\end{itemize} 594\index{assiomi!semantica formale degli assiomi della logic HOL@semantica formale degli assiomi della logic \HOL{}|)} 595Dal momento che queste definizioni sono state ottenute applicando la semantica dei 596termini ai lati sinistri dell'equazioni che formano gli assiomi di 597\theory{LOG}, questi assiomi sono soddisfatti e si ottiene un modello della 598teoria \theory{LOG}. 599 600 601\subsection{La teoria {\tt INIT}} 602\label{INIT} 603 604La teoria \theory{INIT}\index{INIT@\ml{INIT}!forma astratta di} si 605ottiene aggiungendo i seguenti quattro assiomi\index{assiomi!della logica HOL@della logica \HOL{}} alla teoria 606\theory{LOG}. 607\[ 608\index{BOOL_CASES_AX@\ml{BOOL\_CASES\_AX}!forma astratta di} 609\index{ETA_AX@\ml{ETA\_AX}!forma astratta di} 610\index{SELECT_AX@\ml{SELECT\_AX}!forma astratta di} 611\index{INFINITY_AX@\ml{INFINITY\_AX}!forma astratta di} 612\index{assioma di scelta} 613\index{assioma dell'infinito} 614\begin{array}{@{}l@{\qquad}l} 615\mbox{\small\tt BOOL\_CASES\_AX}&\vdash \uquant{b} (b = \T ) \vee (b = \F )\\ 616 \\ 617\mbox{\small\tt ETA\_AX}& 618\vdash \uquant{f_{\alpha\fun\beta}}(\lquant{x}f\ x) = f\\ 619 \\ 620\mbox{\small\tt SELECT\_AX}& 621\vdash \uquant{P_{\alpha\fun\ty{bool}}\ x} P\ x \imp 622P({\hilbert}\ P)\\ 623 \\ 624\mbox{\small\tt INFINITY\_AX}& 625\vdash \equant{f_{\ind\fun \ind}} \OneOne \ f \conj \neg(\Onto \ f)\\ 626\end{array} 627\] 628 629L'unico modello standard di \theory{LOG} soddisfa questi quattro assiomi 630e di conseguenza � l'unico modello standard della teoria 631\theory{INIT}.\index{INIT@\ml{INIT}!formal semantics of} (Per l'assioma 632{\small\tt SELECT\_AX} � necessario usare la definizione di 633$\den{\hilbert}$ data nella Sezione~\ref{standard-signatures}; per l'assioma 634{\small\tt INFINITY\_AX} � ncessario il fatto che $\den{\ind}=\inds$ � 635un insieme infinito.) 636 637La teoria \theory{INIT} � la teoria iniziale\index{initial theory, 638 della logica HOL@initial theory, della logica \HOL{}!forma astratta di} della 639logica \HOL{}. Una teoria che estende \theory{INIT} sar� chiamata una 640{\em teoria standard}\index{teoria standard}. 641 642\subsection{Implementare le teorie \texttt{LOG} e \texttt{INIT}} 643\label{sec:implementing-log-init} 644 645L'implementazione combina le teorie \theory{LOG} e 646\theory{INIT} in una teoria \theoryimp{bool}. Essa include tutte le 647costanti e gli assiomi da queste teorie, e include un numero di 648risultati derivati circa queste costanti. Per maggiori informazioni sulla 649teoria \theoryimp{bool} d'implementazione, si veda \DESCRIPTION. 650 651\subsection{Coerenza} 652\label{consistency} 653 654Una teoria (standard) � {\em coerente\/}\index{teoria coerente} se 655non � il caso che ogni sequente nella sua firma possa essere 656derivato dagli assiomi della teoria usando la logica \HOL{}, o 657in modo equivalente, se non pu� essere derivato in questo modo il particolare sequente $\turn\F$. 658 659L'esistenza di un modello (standard) di una teoria � sufficiente per 660stabilire la sua coerenza. Perch� per il Teorema 661di Validit�~\ref{soundness}, qualsiasi sequente che possa essere derivato dagli 662assiomi della teoria sar� soddisfatto dal modello, mentre il sequente 663$\turn\F$ non � mai soddisfatto in alcun modello. Cos� in particolare, 664la teoria iniziale \theory{INIT} � coerente. 665 666Tuttavia, � possibile che una teoria sia coerente ma non 667possieda un modello standard. Questo avviene perch� la nozione di un 668modello {\em standard\/} � piuttosto restrittiva---in particolare non c'� alcuna 669scelta su come interpretare gli interi e la loro aritmetica in un tale 670modello. Il famoso teorema di incompletezza di G\"odel assicura che ci 671sono sequenti che sono soddisfatti in tutti i modelli standard (cio� che sono 672`veri'), ma che non sono dimostrabili nella logica \HOL{}. 673 674 675 676 677 678\section{Estensioni di teorie} 679\index{extension, della logica HOL@extension, della logica \HOL{}!forma astratta di} 680\label{extensions} 681 682Una teoria ${\cal T}'$ � detta essere un'{\em 683estensione\/}\index{extension, of theory} di una teoria ${\cal T}$ se: 684\begin{myenumerate} 685\item ${\sf Struc}_{{\cal T}}\subseteq{\sf Struc}_{{\cal T}'}$. 686\item ${\sf Sig}_{{\cal T}}\subseteq{\sf Sig}_{{\cal T}'}$. 687\item ${\sf Axioms}_{{\cal T}}\subseteq{\sf Axioms}_{{\cal T}'}$. 688\item ${\sf Theorems}_{{\cal T}}\subseteq{\sf Theorems}_{{\cal T}'}$. 689\end{myenumerate} 690In questo caso, qualsiasi modello $M'$ della teoria pi� grande ${\cal T}'$ pu� essere 691ristretto a un modello della teoria pi� piccola $\cal T$ nel modo 692seguente. Primo, $M'$ d� origine a un modello della struttura e della firma 693di $\cal T$ semplicemente dimenticando i valori di $M'$ alle costanti che non sono 694in ${\sf Struc}_{\cal T}$ or ${\sf Sig}_{\cal T}$. Indicando questo modello 695con $M$, si ha che per ogni $\sigma\in{\sf Types}_{\cal T}$, $t\in{\sf 696Terms}_{\cal T}$ e per tutti i contesti adatti che 697\begin{eqnarray*} 698\den{\alpha\!s.\sigma}_{M} & = & \den{\alpha\!s.\sigma}_{M'} \\ 699\den{\alpha\!s,\!x\!s.t}_{M} & = & \den{\alpha\!s,\!x\!s.t}_{M'}. 700\end{eqnarray*} 701Di conseguenza se $(\Gamma,t)$ � un sequente su ${\sf Sig}_{\cal T}$ 702(e di conseguenza anche su ${\sf Sig}_{{\cal T}'}$), allora $\Gamma 703\models_{M} t$ se e solo se $\Gamma \models_{M'} t$. Dal momento che ${\sf 704Axioms}_{\cal T}\subseteq{\sf Axioms}_{{\cal T}'}$ e $M'$ � un modello 705di ${\cal T}'$, segue che $M$ � un modello di $\cal T$. $M$ sar� 706chiamata la {\em restrizione}\index{restrictions, of models} del 707modello $M'$ della teoria ${\cal T}'$ alla sotto-teoria $\cal T$. 708 709\bigskip 710 711Ci sono due meccanismi principali per fare estensioni alle teorie in \HOL: 712\begin{itemize} 713 714\item Estensione attraverso la specifica di una costante (si veda la Sezione~\ref{specs}). 715 716\item Estensione attraverso la specifica di un tipo (si veda la 717Sezione~\ref{tyspecs}).\footnote{Questo meccanismo di estensione di teorie non � 718implementato nel sistema \HOL{}4.} 719 720\end{itemize} 721Il primo meccanismo permette la `specifica libera' di costanti (come nella 722notazione {\bf Z}~\cite{Z}, per esempio); la seconda permette di 723introdurre nuovi tipi e operatori di tipo. Come casi speciali (quando la 724cosa che si sta definendo � univocamente determinata) si hanno anche: 725\begin{itemize} 726 727\item Estensione attraverso la definizione di una costante (si veda la Sezione~\ref{defs}). 728 729\item Estensione attraverso la definizione di un tipo (si veda la Sezione~\ref{tydefs}). 730 731\end{itemize} 732Questi meccanismi sono descritti nelle seguenti sezioni. Essi producono 733tutti delle {\it estensioni definizionali\/} nel senso che essi estendono 734una teoria aggiungendo delle nuove costanti e dei nuovi tipi che sono definiti in termini 735di propriet� di quelli esistenti. La loro propriet� chiave � che la 736teoria estesa possiede un modello (standard) se la teoria originale 737lo ha. Cos� � garantito che una serie di queste estensioni che iniziano dalla teoria 738\theory{INIT} risulter� in una teoria con un modello 739standard, e di conseguenza in una teoria coerente. E' anche possibile estendere 740teorie semplicemente aggiungendo nuove costanti e tipi non interpretati. Questo 741preserva la coerenza, ma difficilmente sar� utile senza assiomi 742addizionali. Tuttavia, quando si aggiungono arbitrariamente nuovi 743assiomi\index{assiomi!non necessit� di aggiungere}, non c'� alcuna garanzia 744che la coerenza sia preservata. I vantaggi della postulazione rispetto 745alla definizione sono stati paragonati da Bertrand Russell ai vantaggi del 746furto rispetto al lavoro onesto\footnote{Si veda la pagina 71 del libro di Russel {\sl 747Introduction to Mathematical Philosophy\/}}. Dal momento che � sin troppo facile 748introdurre assiomatizzazioni incoerenti, gli utenti del sistema \HOL{} sono 749caldamente invitati a resistere alla tentazione di aggiungere assiomi, ma di lavorare 750onestamente attraverso teorie definizionali. 751 752 753 754 755\subsection{Estensione per definizione di costanti} 756\index{extension, della logica HOL@extension, della logica \HOL{}!by constant definition|(} 757\label{defs} 758 759Una {\it definizione di costante\/}\index{definizione di costante} su una 760firma $\Sigma_{\Omega}$ � una formula della forma 761$\con{c}_{\sigma} = t_{\sigma}$, tale che: 762\begin{myenumerate} 763 764\item 765$\con{c}$ non � il nome di alcuna costante in $\Sigma_{\Omega}$; 766 767\item 768$t_{\sigma}$ � un termine chiuso in ${\sf Terms}_{\Sigma_{\Omega}}$. 769 770\item 771tutte le variabili di tipo che occorrono in $t_\sigma$ occorrono anche in $\sigma$ 772 773\end{myenumerate} 774 775Data una teoria $\cal T$ e una tale definizione di costante su ${\sf 776Sig}_{\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}$ 777per $\con{c}_{\sigma}=t_{\sigma}$ � la teoria ${\cal T}{+_{\it 778def}}\langle 779\con{c}_{\sigma}=t_{\sigma}\rangle$ definita da: 780\[ 781{\cal T}{+_{\it def}}\langle 782\con{c}_{\sigma}=t_{\sigma}\rangle\ =\ \langle 783\begin{array}[t]{l} 784{\sf Struc}_{\cal T},\ 785{\sf Sig}_{\cal T}\cup\{(\con{c},\sigma)\},\\ 786{\sf Axioms}_{\cal T}\cup\{ 787\con{c}_{\sigma}=t_{\sigma} \},\ 788{\sf Theorems}_{\cal T}\rangle 789\end{array} 790\] 791 792Si noti che il meccanismo di estensione per definizione di costante � gi� 793stato usato implicitamente nel formare la teoria \theory{LOG} dalla 794teoria \theory{MIN} nella Sezione~\ref{LOG}. Cos� con la notazione 795di questa sezione si ha 796\[ 797\theory{LOG}\; =\; \theory{MIN}\;\begin{array}[t]{@{}l} 798 {+_{\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} \ =\ 799 ((\lquant{x_{\ty{bool}}}x) = (\lquant{x_{\ty{bool}}}x))\rangle\\ 800 {+_{\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 = 801 (\lquant{x}\T )\rangle\\ 802 {+_{\it def}}\langle {\exists}\index{existential quantifier, nella logica HOL@existential quantifier, nella logica \HOL{}!forma astratta di}\ =\ 803 \lquant{P_{\alpha\fun\ty{bool}}}\ P({\hilbert}\ P)\rangle\\ 804 {+_{\it def}}\langle \F\index{F@\holtxt{F}!forma astratta di} 805 \ =\ \uquant{b_{\ty{bool}}}\ b\rangle\\ 806 {+_{\it def}}\langle \neg\ =\ \lquant{b}\ b \imp \F \rangle\index{negation, nella logica HOL@negation, nella logica \HOL{}!forma astratta di}\\ 807 {+_{\it def}}\langle {\wedge}\index{conjunction, nella logica HOL@conjunction, nella logica \HOL{}!forma astratta di}\ =\ \lquant{b_1\ b_2}\uquant{b} 808 (b_1\imp (b_2 \imp b)) \imp b\rangle\\ 809 {+_{\it def}}\langle {\vee}\index{disjunction, nella logica HOL@disjunction, nella logica \HOL{}!forma astratta di}\ =\ \lquant{b_1\ b_2}\uquant{b} 810 (b_1 \imp b)\imp ((b_2 \imp b) \imp b)\rangle\\ 811 {+_{\it def}}\langle\OneOne \ =\ \lquant{f_{\alpha \fun\beta}} 812 \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}\\ 813 {+_{\it def}}\langle\Onto \ =\ \lquant{f_{\alpha\fun\beta}}\index{onto predicate, nella logica HOL@onto predicate, nella logica \HOL{}!forma astratta di} 814 \uquant{y}\equant{x} y = f\ x\rangle\\ 815 {+_{\it def}}\langle\TyDef \ =\ 816 \begin{array}[t]{@{}l} 817 \lambda P_{\alpha\fun\ty{bool}}\ rep_{\beta\fun\alpha}.\\ 818 \OneOne\ rep\ \ \wedge\\ 819 (\uquant{x}P\ x \ =\ (\equant{y} x = rep\ y)) \rangle\\ 820\end{array}\end{array} 821\] 822 823Se $\cal T$ possiede un modello standard allora lo ha anche l'estensione 824${\cal T}{+_{\it def}}\langle\con{c}_{\sigma}=t_{\sigma}\rangle$. Questo 825sar� dimostrato come un corollario del corrispondente risultato nella\linebreak 826Sezione~\ref{specs} mostrando che l'estensione per definizione di costante 827� di fatto un caso speciale di estensione per specifica di costante. 828(Questa riduzione richiede che si stia trattando con teorie 829{\em standard\/} nel senso della sezione~\ref{INIT}, dal momento che bench� 830la quantificazione esistenziale non sia necessaria per le definizioni di costanti, � 831necessaria per formulare il meccanismo di specifica di costante.) 832 833\medskip 834 835\noindent{\bf Nota\ } La condizione (iii) nella definizione di 836ci� che costituisce una definizione di costante corretta � una restrizione 837importante senza la quale la coerenza non potrebbe essere garantita. Per vedere 838questo, consideriamo il termine $\equant{f_{\alpha\fun\alpha}} \OneOne \ f 839\conj \neg(\Onto \ f)$, che esprime la proposizione che il (l'insieme 840di elementi denotati dal) tipo $\alpha$ � infinito. Il termine contiene 841la variabile di tipo $\alpha$, mentre il tipo del termine, $\ty{bool}$, 842no. Cos� per (iii) 843\[ 844\con{c}_\ty{bool} = 845\equant{f_{\alpha\fun\alpha}} \OneOne \ f \conj \neg(\Onto \ f) 846\] 847non � permessa come definizione di una costante. Il problema � che il 848significato del lato destro della definizione varia con $\alpha$, 849mentre il significato della costante sul lato sinistro � fissato, 850dal momento che non contiene $\alpha$. Di fatto, se ci fosse permesso di 851estendere la teoria coerente $\theory{INIT}$ con questa definizione, il 852risultato darebbe una teoria incoerente. Perch� istanziare $\alpha$ a 853$\ty{ind}$ nel lato destro risulta in un termine che � dimostrabile 854dagli assiomi di $\theory{INIT}$, e di conseguenza $\con{c}_\ty{bool}=\T$ � 855dimostrabile nella teoria estesa. Ma ugualmente, istanziare $\alpha$ 856a $\ty{bool}$ rende la negazione del lato destro dimostrabile 857dagli assiomi di $\theory{INIT}$, e di conseguenza anche $\con{c}_\ty{bool}=\F$ � 858dimostrabile nella teoria estesa. Combinando questi teoremi, si 859ha che $\T=\F$, cio� $\F$ � dimostrabile nella teoria estesa. 860\index{extension, della logica HOL@extension, della logica \HOL{}!by constant definition|)} 861 862\subsection{Estensione per specifica di costante} 863\index{extension, della logica HOL@extension, della logica \HOL{}!by constant specification|(} 864\label{specs} 865 866Le specifiche di costanti\index{constant specification extension, della logica HOL@constant specification extension, della logica \HOL{}!abstract form 867of} introducono costanti (o insiemi di costanti) 868che soddisfano propriet� (coerenti) arbitrariamente date. Per esempio, una 869teoria potrebbe essere estesa da una specifica di costante in modo da avere due nuove 870costanti $\con{b}_1$ e $\con{b}_2$ di tipo \ty{bool} tali che 871$\neg(\con{b}_1=\con{b}_2)$. Questa specifica non definisce 872in modo univoco $\con{b}_1$ e $\con{b}_2$, dal momento che � soddisfatta sia da 873$\con{b}_1=\T$ e $\con{b}_2=\F$, sia da $\con{b}_1=\F$ e 874$\con{b}_2=\T$. Per assicurare che tali specifiche sono 875coerenti\index{consistency, della logica HOL@consistency, della logica \HOL{}!under constant specification}, esse possono essere fatte solo se � 876gi� stato dimostrato che le propriet� che le nuove costanti devono 877avere sono coerenti. Questo impedisce, per esempio, di introdurre tre 878costanti booleane $\con{b}_1$, $\con{b}_2$ e $\con{b}_3$ tali che 879$\con{b}_1\neq \con{b}_2$, $\con{b}_1\neq \con{b}_3$ e 880$\con{b}_2\neq \con{b}_3$. 881 882Supponiamo che $\equant{x_1\cdots x_n}t$ sia una formula, con $x_1,\ldots, x_n$ 883variabili distinte. Se $\turn \equant{x_1 \cdots x_n}t$, allora una 884specifica di costante permette di introdurre le nuove costanti $\con{c}_1$, $\ldots$ , 885$\con{c}_n$ che soddisfano: 886\[ 887\turn t[\con{c}_1,\cdots,\con{c}_n/x_1,\cdots,x_n] 888\] 889dove $t[\con{c}_1,\cdots,\con{c}_n/x_1,\cdots,x_n]$ denota il 890risultato di sostituire simultaneamente $\con{c}_1, \ldots, \con{c}_n$ 891per $x_1, \ldots, x_n$ rispettivamente. Naturalmente il tipo di ciascuna 892costante $\con{c}_i$ deve essere lo stesso del tipo della corrispondente 893variabile $x_i$. Per assicurare che questo meccanismo di estensione preserva la 894propriet� di possedere un modello, � imposto su questi tipi un ulteriore 895requisito pi� tecnico: essi devono contenere ciascuno tutte le variabili 896di tipo che occorrono in $t$. Questa condizione � discussa ulteriormente nella 897Sezione~\ref{constants} di sotto. 898 899Formalmente, una {\em specifica di costante\/}\index{constant specification} 900per una teoria ${\cal T}$ � data da 901 902\medskip 903\noindent{\bf Dati} 904\[ 905\langle(\con{c}_1,\ldots,\con{c}_n), 906\lquant{{x_1}_{\sigma_1},\ldots,{x_n}_{\sigma_n}}t_{\ty{bool}}\rangle 907\] 908 909\noindent{\bf Condizioni} 910\begin{myenumerate} 911 912\item 913$\con{c}_1,\ldots,\con{c}_n$ sono nomi distinti che 914non sono i nomi di alcuna costante in ${\sf Sig}_{\cal T}$. 915 916\item 917$\lquant{{x_1}_{\sigma_1} 918\cdots {x_n}_{\sigma_n}}t_{\ty{bool}}\ \in\ {\sf Terms}_{\cal T}$. 919 920\item 921$tyvars(t_{\ty{bool}})\ =\ tyvars(\sigma_i)$ per $1\leq i\leq n$. 922 923\item 924$\equant{{x_1}_{\sigma_1}\ \cdots\ {x_n}_{\sigma_n}}t 925\ \in\ {\sf Theorems}_{\cal T}$. 926 927\end{myenumerate} 928L'estensione di una teoria standard ${\cal T}$ per mezzo di una tale specifica 929di costante � denotata da 930\[ 931{\cal T}{+_{\it spec}}\langle(\con{c}_1,\ldots,\con{c}_n), 932\lquant{{x_1}_{\sigma_1},\ldots,{x_n}_{\sigma_n}}t_{\ty{bool}} \rangle 933\] 934ed � definita essere la teoria: 935\[ 936\langle 937\begin{array}[t]{@{}l} 938{\sf Struc}_{\cal T},\\ 939{\sf Sig}_{\cal T} \cup 940\{{\con{c}_1}_{\sigma_1}, \ldots, 941{\con{c}_n}_{\sigma_n}\},\\ 942{\sf Axioms}_{\cal T}\cup 943\{ t[\con{c}_1,\ldots,\con{c}_n/x_1,\ldots,x_n] \},\\ 944{\sf Theorems}_{\cal T} 945\rangle 946\end{array} 947\] 948 949\noindent{\bf Proposizione\ }{\em 950La teoria ${\cal 951T}{+_{\it spec}}\langle(\con{c}_1,\ldots,\con{c}_n), 952\lquant{{x_1}_{\sigma_1},\ldots,{x_n}_{\sigma_n}}t_{\ty{bool}} 953\rangle$ ha un modello standard se la teoria ${\cal T}$ lo ha.} 954 955\medskip 956 957\noindent{\bf Dimostrazione\ } 958Supponiamo che $M$ sia un modello standard di ${\cal T}$. Sia 959$\alpha\!s=\alpha_{1},\ldots,\alpha_{m}$ la lista di variabili di tipo 960distinte che occorrono nella formula $t$. Allora $\alpha\!s,\!x\!s.t$ � un 961termine-in-contesto, dove $x\!s=x_{1},\ldots,x_{n}$. (Cambiando ogni variabile 962legata in $t$ in modo da renderle distinte da $x\!s$ se necessario.) 963Interpretando questo termine-in-contesto nel modello $M$ si ottiene 964\[ 965\den{\alpha\!s,\!x\!s.t}_{M} \in \prod_{X\!s\in{\cal U}^{m}} 966\left(\prod_{i=1}^{n}\den{\alpha\!s.\sigma_{i}}_{M}(X\!s)\right) 967\fun \two 968\] 969Ora $\equant{x\!s}t$ � in ${\sf Theorems}_{\cal T}$ e di conseguenza per il 970Teorema di Validit� \ref{soundness}\index{consistency, della logica HOL@consistency, della logica \HOL{}!under constant specification} questo 971sequente � soddisfatto da $M$. Usando la semantica di $\exists$ data nella 972Sezione~\ref{LOG}, questo significa che per ogni $X\!s\in{\cal 973U}^{m}$ l'insieme 974\[ 975S(X\!s) = \{y\!s\in\den{\alpha\!s.\sigma_{1}}_{M}(X\!s) \times\cdots\times 976 \den{\alpha\!s.\sigma_{n}}_{M}(X\!s)\; : \; 977 \den{\alpha\!s,\!x\!s.t}_{M}(X\!s)(y\!s)=1 \} 978\] 979non � vuoto. Dal momento che � anche un sottoinsieme di un prodotto finito di insiemi in 980$\cal U$, ne segue che � un elemento di $\cal U$ (usando le propriet� 981{\bf Sub} e {\bf Prod} dell'universo). Cos� si pu� applicare la funzione 982di scelta globale $\ch\in\prod_{X\in{\cal U}}X$ per selezionare un elemento specifico. 983\[ 984(s_{1}(X\!s),\ldots,s_{n}(X\!s)) = 985\ch(S(X\!s)) \in \prod_{i=1}^{n}\den{\alpha\!s.\sigma_{i}}_{M}(X\!s) 986\] 987per il quale $\den{\alpha\!s,\!x\!s.t}_{M}(X\!s)$ prende il valore $1$. Estendiamo 988$M$ a un modello $M'$ della firma di ${\cal 989T}{+_{\it spec}}\langle(\con{c}_1,\ldots,\con{c}_n), 990\lquant{{x_1}_{\sigma_1},\ldots,{x_n}_{\sigma_n}}t_{\ty{bool}} 991\rangle$ definendo che il suo valore per 992ogni nuova costante $(\con{c}_{i},\sigma_{i})$ sia 993\[ 994M'(\con{c}_{i},\sigma_{i}) = 995s_{i} \in \prod_{X\!s\in{\cal U}^{m}}\den{\sigma_{i}}_{M}(X\!s) . 996\] 997Si noti che la Condizione (iii) nella definizione di una specifica 998di costante assicura che $\alpha\!s$ � il contesto canonico di ogni 999tipo $\sigma_{i}$, cos� che 1000$\den{\sigma_{i}}=\den{\alpha\!s.\sigma_{i}}$ e quindi $s_{i}$ � 1001di fatto un elemento del prodotto di sopra. 1002 1003Dal momento che $t$ � un termine della sotto-teoria $\cal T$ di \linebreak${\cal 1004T}{+_{\it spec}}\langle(\con{c}_1,\ldots,\con{c}_n), 1005\lquant{{x_1}_{\sigma_1},\ldots,{x_n}_{\sigma_n}}t_{\ty{bool}} 1006\rangle$, 1007come notato all'inizio della Sezione~\ref{extensions}, si ha che 1008$\den{\alpha\!s,\!x\!s.t}_{M'} = \den{\alpha\!s,\!x\!s.t}_{M}$. Di conseguenza per 1009la definizione degli $s_{i}$, per tutti gli $X\!s\in{\cal U}^{m}$ 1010\[ 1011\den{\alpha\!s,\!x\!s.t}_{M'}(X\!s)(s_{1}(X\!s),\ldots,s_{n}(X\!s)) = 1 1012\] 1013Quindi usando il Lemma~4 nella 1014Sezione~\ref{term-substitution} sulla semantica della sostituzione insieme con 1015la definizione di $\den{\con{c}_{i}}_{M'}$, si ottiene infine che 1016per tutti gli $X\!s\in{\cal U}^{m}$ 1017\[ 1018\den{t[\con{c}_{1},\ldots,\con{c}_{n}/x_{1},\ldots,x_{n}]}_{M'}(X\!s)=1 1019\] 1020o in altre parole che $M'$ soddisfa 1021$t[\con{c}_{1},\ldots,\con{c}_{n}/x_{1},\ldots,x_{n}]$. 1022Quindi $M'$ � un modello di ${\cal T}{+_{\it 1023spec}}\langle(\con{c}_1,\ldots,\con{c}_n), 1024\lquant{{x_1}_{\sigma_1},\ldots,{x_n}_{\sigma_n}}t_{\ty{bool}} 1025\rangle$, come richiesto. 1026 1027\medskip 1028 1029Le costanti che sono affermate esistere in una specifica di costante 1030non sono necessariamente determinate in modo univoco. In modo corrispondente, ci possono 1031essere pi� modelli differenti di ${\cal T}{+_{\it 1032spec}}\langle(\con{c}_1,\ldots,\con{c}_n), 1033\lquant{{x_1}_{\sigma_1},\ldots,{x_n}_{\sigma_n}}t_{\ty{bool}} 1034\rangle$ la cui restrizione a $\cal T$ � $M$; la costruzione di sopra 1035produce un tale modello in una maniera uniforme facendo uso della funzione 1036di scelta globale sull'universo. 1037 1038L'estensione per mezzo di una definizione di costante, $\con{c}_\sigma=t_\sigma$, � un 1039caso speciale di estensione per specifica di costante. Perch� sia $t'$ 1040la formula $x_\sigma=t_\sigma$, dove $x_\sigma$ � una variabile che non 1041occorre in $t_\sigma$. Allora chiaramente $\turn 1042\equant{x_\sigma}t'$ e si pu� applicare il metodo della specifica 1043di costante per ottenere la teoria 1044\[ 1045{\cal T}{+_{\it spec}}\langle \con{c},\lquant{x_\sigma}t'\rangle 1046\] 1047Ma dal momento che $t'[\con{c}_\sigma/x_\sigma]$ � semplicemente 1048$\con{c}_\sigma=t_\sigma$, 1049questa estensione porta esattamente a ${\cal T}{+_{\it def}}\langle 1050\con{c}_{\sigma}=t_{\sigma}\rangle$. 1051Cos� come corollario della Proposizione, si ha che per ogni modello 1052standard $M$ di $\cal T$, c'� un modello standard $M'$ di ${\cal 1053T}{+_{\it def}}\langle\con{c}_{\sigma}=t_{\sigma}\rangle$ la cui 1054restrizione a $\cal T$ � $M$. In contrasto con il caso delle specifiche 1055di costante, $M'$ � determinato in modo univoco da $M$ e dalla definizione di 1056costante 1057\index{extension, della logica HOL@extension, della logica \HOL{}!by constant specification|)} 1058 1059\subsection{Note circa le costanti in \HOL{}} 1060\label{constants} 1061 1062Si noti come la Condizione (iii) nella definizione di una specifica di costante 1063sia stata necessaria nella dimostrazione che il meccanismo di estensione preserva la 1064propriet� di possedere un modello standard. Il suo ruolo � di assicurare che 1065le costanti introdotte abbiano, attraverso i loro tipi, la stessa dipendenza dalle 1066variabili di tipo che ha la formula che le specifica. La 1067situazione � la stessa di quella discussa nella Nota nella 1068Sezione~\ref{defs}. In un senso, ci� che causava il problema 1069nell'esempio dato in quella Nota non � tanto il metodo di estensione per mezzo 1070dell'introduzione di costanti, ma piuttosto la sintassi di \HOL{} che non 1071permette alle costanti di dipendere esplicitamente dalle variabili di tipo (nel modo 1072in cui lo fanno gli operatori di tipo). Cos� nell'esempio si vorrebbe 1073introdurre una costante `polimorfica' $\con{c}_\ty{bool}(\alpha)$ 1074che dipende esplicitamente da $\alpha$, e definirla essere 1075$\equant{f_{\alpha\fun\alpha}} \OneOne \ f \conj 1076\neg(\Onto \ f)$. Allora nella teoria estesa si potrebbe derivare 1077$\con{c}_\ty{bool}(\ty{ind})=\T$ e 1078$\con{c}_\ty{bool}(\ty{bool})=\F$, ma ora non risulta alcuna contraddizione dal momento che 1079$\con{c}_\ty{bool}(\ty{ind})$ e $\con{c}_\ty{bool}(\ty{bool})$ 1080sono differenti. 1081 1082Nella versione attuale di \HOL, le costanti sono coppie-(nome,tipo). 1083Si potrebbe immaginare una leggera estensione della sintassi di \HOL{} con 1084costanti `polimorfiche', specificate da coppie 1085$(\con{c},\alpha\!s.\sigma)$ dove ora $\alpha\!s.\sigma$ � un 1086tipo-in-contesto e la lista $\alpha\!s$ pu� ben contenere variabili di tipo 1087extra che non occorrono in $\sigma$. Una tale coppia darebbe origine 1088al particolare termine costante 1089$\con{c}_\sigma(\alpha\!s)$, e pi� in generale ai 1090termini costanti $\con{c}_{\sigma'}(\tau\!s)$ ottenuti da 1091questo istanziando le variabili di tipo $\alpha_i$ con i tipi 1092$\tau_i$ (cos� $\sigma'$ � l'istanza di $\sigma$ ottenuta 1093sostituendo $\tau\!s$ per $\alpha\!s$). Questa nuova sintassi di costanti 1094polimorfiche � paragonabile alla sintassi esistente dei tipi composti (si veda 1095la sezione~\ref{types}): un operatore di tipo $n$-ario $\textsl{op}$ da origine a un 1096tipo composto $(\alpha_1,\ldots,\alpha_n){\textsl{op}}$ che dipende da $n$ 1097variabili di tipo. Analogamente, la sintassi di sopra delle costanti polimorfiche 1098registra come esse dipendono dalle variabili di tipo (as well as which generic 1099type the constant has). 1100 1101Tuttavia, registrare esplicitamente la dipendenza delle costanti dalle variabili di tipo 1102da origine a una sintassi ingombrante che in pratica si preferirebbe 1103evitare laddove possibile. E' possibile evitarlo se il contesto 1104di tipo $\alpha\!s$ in $(\con{c},\alpha\!s.\sigma)$ � di fatto il 1105contesto {\em canonico\/} di $\sigma$, cio� contiene esattamente le variabili 1106di tipo di $\sigma$. Perch� allora si pu� applicare il Lemma~1 della 1107Sezione~\ref{instances-and-substitution} per dedurre che la 1108costante polimorfica $\con{c}_{\sigma'}(\tau\!s)$ pu� essere abbreviata 1109alla costante ordinaria $\con{c}_{\sigma'}$ senza ambiguit�---l'informazione 1110mancante $\tau\!s$ pu� essere ricostruita da $\sigma'$ e 1111dall'informazione circa la costante $\con{c}$ data nella firma. 1112Da questo prospettiva, il lato piuttosto tecnico delle Condizioni (iii) nelle 1113Sezioni~\ref{defs} e \ref{specs} diventano molto meno misteriose: 1114esse precisamente assicurano che nell'introdurre nuove costanti si stia sempre 1115trattando solo con i contesti canonici, e cos� si possano usare costanti ordinarie 1116piuttosto che quelle polimorfiche senza ambiguit�. In questo modo si evita 1117di complicare la sintassi esistente al costo di restringere 1118in qualche modo l'applicabilit� di questi meccanismi di estensioni delle teorie. 1119 1120 1121\subsection{Estensione per definizione di tipo} 1122\index{extension, della logica HOL@extension, della logica \HOL{}!by type definition|(} 1123\index{representing types, nella logica HOL@representing types, nella logica \HOL{}!forma astratta di|(} 1124\label{tydefs} 1125 1126Ogni tipo (monomorfico) $\sigma$ nella teoria iniziale \theory{INIT} 1127determina un insieme\linebreak $\den{\sigma}$ nell'universo $\cal U$. Tuttavia, 1128ci sono molti pi� insiemi in $\cal U$ dei tipi che sono in 1129\theory{INIT}. In particolare, mentre $\cal U$ � chiuso rispetto 1130all'operazione di prendere un sottoinsieme non-vuoto di $\den{\sigma}$, non c'� 1131alcun meccanismo corrispondente per formare un `sottotipo' di $\sigma$. Piuttosto, 1132i sottoinsiemi sono denotati indirettamente attraverso funzioni caratteristiche, per mezzo delle quali un 1133termine chiuso $p$ di tipo $\sigma\fun\ty{bool}$ determina il sottoinsieme 1134$\{x\in\den{\sigma} : \den{p}(x)=1\}$ (che � un insieme nell'universo 1135purch� non sia vuoto). Tuttavia, � utile avere un 1136meccanismo per introdurre nuovi tipi che sono sottotipi di quelli 1137esistenti. Tali tipi sono definiti\index{extension, della logica HOL@extension, della logica \HOL{}!by type definition} in \HOL{} introducendo una nuova costante 1138di tipo e asserendo un assioma che la caratterizza denotare un 1139insieme in biezione (cio� in corrispondenza uno-a-uno) con un sottoinsieme 1140non-vuoto di un tipo esistente (chiamato il {\em tipo rappresentante\/}). 1141Per esempio, il tipo \ml{num} � definito essere uguale a un sottoinsieme 1142numerabile del tipo \ml{ind}, che � garantito esistere dall'assioma 1143{\small\tt INFINITY\_AX} (si veda la Sezione~\ref{INIT}). 1144 1145Cos� come definire tipi, � anche conveniente essere in grado di definire 1146operatori di tipo. Un esempio sarebbe un operatore di tipo \ty{inj} che 1147mappasse un insieme all'insieme di funzioni uno-a-uno (cio� iniettive) su 1148di esso. Il sottoinsieme di $\sigma\fun\sigma$ che rappresenta $(\sigma)\ty{inj}$ 1149sarebbe definito dal predicato \OneOne. Un altro esempio sarebbe un 1150operatore di tipo per il prodotto cartesiano binario \ty{prod}. Questo � definito 1151scegliendo un tipo rappresentante che contiene due variabili di tipo, diciamo 1152$\sigma[\alpha_1;\alpha_2]$, tale che per ogni tipo $\sigma_1$ e 1153$\sigma_2$, un sottoinsieme di $\sigma[\sigma_1;\sigma_2]$ rappresenta il 1154prodotto cartesiano di $\sigma_1$ e $\sigma_2$. I dettagli di una tale 1155definizione sono dati nella sezione di \DESCRIPTION\/ sulla teoria dei 1156prodotti cartesiani. 1157 1158I tipi in \HOL{} devono denotare insiemi non-vuoti. Cos� � 1159coerente\index{consistency, della logica HOL@consistency, della logica \HOL{}!under type definition} definire un nuovo tipo isomorfo a un 1160sottoinsieme specificato da un predicato $p$, solo se c'� almeno una cosa 1161per cui $p$ vale, cio� $\turn\equant{x}p\ x$. Per esempio, 1162sarebbe incoerente definire un operatore di tipo binario \ty{iso} tale 1163che $(\sigma_1,\sigma_2)\ty{iso}$ denotasse l'insieme di funzioni 1164uno-a-uno da $\sigma_1$ {\em onto\/} $\sigma_2$ perch� per qualche 1165valore di $\sigma_1$ e $\sigma_2$ l'insieme sarebbe vuoto; per 1166esempio $(\ty{ind},\ty{bool})\ty{iso}$ denoterebbe l'insieme vuoto. Per 1167evitare questo, una precondizione di definire un nuovo tipo � che il 1168sottoinsieme rappresentante non sia vuoto. 1169 1170Riassumendo, un nuovo tipo � definito: 1171\begin{enumerate} 1172\item Specificando un tipo esistente. 1173\item Specificando un sottoinsieme di questo tipo. 1174\item Dimostrando che questo sottoinsieme non � vuoto. 1175\item Specificando che il nuovo tipo � isomorfo a questo sottoinsieme. 1176\end{enumerate} 1177 1178\noindent In maggiore dettaglio, 1179definire un nuovo tipo $(\alpha_1,\ldots,\alpha_n)\ty{op}$ consiste nel: 1180\begin{enumerate} 1181\item 1182Specificare un tipo-in-contesto, $\alpha_1,\ldots,\alpha_n.\sigma$ diciamo. 1183Il tipo 1184$\sigma$ � chiamato il {\it tipo rappresentante\/}, e il tipo 1185$(\alpha_1,\ldots,\alpha_n)\ty{op}$ � inteso essere isomorfo a un 1186sottoinsieme di $\sigma$. 1187 1188\item 1189Specificare un termine-in-contesto chiuso, $\alpha_1,\ldots,\alpha_n,.p$ 1190diciamo, di tipo $\sigma\fun\bool$. Il termine $p$ � chiamato la {\it 1191funzione caratteristica\/}\index{characteristic function, of type definitions}. Questo definisce il sottoinsieme di $\sigma$ al quale 1192$(\alpha_1,\ldots,\alpha_n)\ty{op}$ deve essere isomorfo\footnote{La 1193ragione per richiedere che $p$ sia chiuso, cio� non abbia variabili 1194libere, � che altrimenti per coerenza l'operatore di tipo definito 1195dovrebbe {\em dipendere\/} da (cio� essere una funzione di) queste 1196variabili. Tali tipi dipendenti non fanno (ancora!) parte del sistema \HOL{}}. 1197 1198\item 1199Dimostrare $\turn \equant{x_{\sigma}} p\ x$. 1200 1201\item 1202Asserire un assioma che dice che $(\alpha_1,\ldots,\alpha_n)\ty{op}$ � 1203isomorfo al sottoinsieme di $\sigma$ selezionato da $p$. 1204 1205\end{enumerate} 1206 1207Per rendere questo formale, la teoria \theory{LOG} fornisce 1208la costante polimorfica \TyDef\ definita nella Sezione~\ref{LOG}. 1209La formula 1210$\equant{f_{(\alpha_1,\ldots,\alpha_n)\ty{op}\fun\sigma}}\TyDef\ p\ f$ 1211asserisce che 1212esiste una funzione uno-a uno $f$ da $(\alpha_1,\ldots,\alpha_n)\ty{op}$ 1213al sottoinsieme di elementi di $\sigma$ per cui $p$ � vero. 1214Di conseguenza, l'assioma che caratterizza $(\alpha_1,\ldots,\alpha_n)\ty{op}$ �: 1215\[ 1216\turn \equant{f_{(\alpha_1,\ldots,\alpha_n)\ty{op}\fun\sigma}}\TyDef\ 1217p\ f 1218\] 1219 1220Definire un nuovo tipo $(\alpha_1,\ldots,\alpha_n)\ty{op}$ in una teoria 1221${\cal T}$ cos� consiste nell'introdurre $\ty{op}$ come un nuovo 1222operatore di tipo $n$-ario e l'assioma di sopra come un nuovo assioma. Formalmente, una {\em 1223definizione di tipo\/}\index{type definitions, nella logica HOL@type definitions, nella logica \HOL{}!abstract structure of} per una teoria ${\cal 1224T}$ � data da 1225 1226\medskip 1227 1228\noindent{\bf Dati} 1229\[ 1230\langle (\alpha_1,\ldots,\alpha_n)\ty{op},\ \sigma,\ 1231p_{\sigma\fun\ty{bool}}\rangle 1232\] 1233 1234\noindent{\bf Condizioni} 1235 1236\begin{myenumerate} 1237\item 1238$(\ty{op},n)$ non � il nome di una costante di tipo in ${\sf Struc}_{\cal T}$. 1239 1240\item 1241$\alpha_1,\ldots,\alpha_n.\sigma$ � un tipo-in-contesto con $\sigma 1242\in{\sf Types}_{\cal T}$. 1243 1244\item $p_{\sigma\fun\bool}$ � un termine chiuso in ${\sf Terms}_{\cal T}$ 1245le cui variabili di tipo occorrono in $\alpha_1,\ldots,\alpha_n$. 1246 1247\item 1248$\equant{x_{\sigma}}p\ x \ \in\ {\sf Theorems}_{\cal T}$. 1249\end{myenumerate} 1250 1251L'estensione di una teoria standard ${\cal T}$ per mezzo di una tale definizione di tipo 1252� denotata da 1253\[ 1254{\cal 1255T}{+_{tydef}}\langle(\alpha_1,\ldots,\alpha_n)\ty{op},\sigma,p\rangle 1256\] 1257e definita essere la teoria 1258\[ 1259\langle 1260\begin{array}[t]{@{}l} 1261{\sf Struc}_{\cal T}\cup\{(\ty{op},n)\},\\ 1262 {\sf Sig}_{\cal T},\\ 1263 {\sf Axioms}_{\cal T}\cup\{ 1264\equant{f_{(\alpha_1,\ldots,\alpha_n)\ty{op} 1265\fun\sigma}}\TyDef\ p\ f\},\\ 1266 {\sf Theorems}_{\cal T}\rangle\\ 1267\end{array} 1268\] 1269 1270\medskip 1271 1272\noindent{\bf Proposizione\ }{\em 1273La teoria ${\cal T}{+_{\it 1274tydef}}\langle(\alpha_1,\ldots,\alpha_n)\ty{op},\sigma,p\rangle$ ha un 1275modello standard se la teoria ${\cal T}$ lo ha.} 1276 1277\medskip 1278 1279Al posto di dare una dimostrazione diretta di questo risultato, esso sar� dedotto come 1280corollario della proposizione corrispondente nella prossima sezione. 1281\index{extension, della logica HOL@extension, della logica \HOL{}!by type definition|)} 1282\index{representing types, nella logica HOL@representing types, nella logica \HOL{}!forma astratta di|)} 1283 1284 1285\subsection{Estensione per specifica di tipo} 1286\index{extension, della logica HOL@extension, della logica \HOL{}!by type specification|(} 1287\label{tyspecs} 1288\noindent 1289(\textbf{Nota:} Questo meccanismo di estensione \emph{non} � 1290implementato nel sistema HOL4. Fu proposto da T.~Melham e 1291raffina una proposta di R.~Jones e R.~Arthan.) 1292 1293\smallskip 1294\noindent Il meccanismo di definizione di 1295tipo permette d'introdurre nuovi tipi dando una concreta 1296rappresentazione del tipo come un `sottotipo' di un tipo esistente. Si 1297potrebbe invece desiderare d'introdurre un nuovo tipo che soddisfa qualche propriet� 1298senza dare un'esplicita rappresentazione per il tipo. Per 1299esempio, si potrebbe volere estendere \theory{INIT} con un tipo atomico 1300$\ty{one}$ che soddisfa $\turn\uquant{f_{\alpha\fun\ty{one}}\ 1301 g_{\alpha\fun\ty{one}}}f=g$ senza scegliere un tipo specifico in 1302$\theory{INIT}$ e dicendo che $\ty{one}$ � in biezione con un 1303suo sottoinsieme di un elemento. (L'idea � quella che la scelta del 1304tipo rappresentante � irrilevante per le propriet� di $\ty{one}$ che 1305possono essere espresse in \HOL.) Il meccanismo descritto in questa sezione 1306fornisce un modo di ottenere questo preservando allo stesso tempo 1307la propriet� fondamentale di possedere un modello standard e quindi 1308di mantenere la coerenza. 1309 1310Ogni formula chiusa $q$ che coinvolge una singola variabile di tipo $\alpha$ pu� 1311essere pensata come se specificasse una propriet� $q[\tau/\alpha]$ dei tipi 1312$\tau$. La sua interpretazione in un modello � della forma 1313\[ 1314\den{\alpha,.q}\in \prod_{X\in{\cal U}}\den{\alpha.\bool}(X) 1315\;= \prod_{X\in{\cal U}}\two \;=\; {\cal U}\fun\two 1316\] 1317che � una funzione caratteristica sull'universo, che determina un 1318sottoinsieme $\{X\in{\cal U}:\den{\alpha,.q}(X)=1\}$ che consiste di quegli 1319insiemi nell'universo per cui vale la propriet� $q$. Il modo 1320pi� generale per assicurare la coerenza nell'introduzione di un nuovo tipo 1321atomico $\nu$ che soddisfa $q[\nu/\alpha]$ sarebbe dimostrare 1322`$\equant{\alpha}q$'. Tuttavia, una tale 1323formula con la quantificazione sui tipi non �\footnote{ancora!} parte della 1324logica \HOL{} e si potrebbe procedere in modo indiretto---sostituendo la 1325formula con una (logicamente pi� debole) che pu� essere espressa formalmente con 1326la sintassi \HOL{}. La formula usata � 1327\[ 1328(\equant{f_{\alpha\fun\sigma}}{\sf Type\_Definition}\ p\ f)\ \imp\ q 1329\] 1330dove $\sigma$ � un tipo, $p_{\sigma\fun\ty{bool}}$ � un termine chiuso 1331e non coinvolge la variabile di tipo $\alpha$. Questa formula dice `$q$ 1332vale di qualsiasi tipo che � in biezione con il sottotipo di $\sigma$ 1333determinato da $p$'. Se questa formula � dimostrabile e il sottotipo non � 1334vuoto, cio� se 1335\[ 1336\equant{x_\sigma}p\ x 1337\] 1338� dimostrabile, allora � coerente introdurre un'estensione con un nuovo 1339tipo atomico $\nu$ che soddisfa $q[\nu/\alpha]$. 1340 1341Nel dare la definizione formale di questo meccanismo di estensione, saranno 1342fatti due raffinamenti. Per prima cosa, a $\sigma$ � permesso essere 1343polimorfico e di conseguenza � introdotta una nuova costante di ripo di ariet� 1344appropriata, piuttosto che semplicemente un tipo atomico. In secondo luogo, alle formule 1345esistenziali di sopra � permesso di essere dimostrate (nella teoria che deve essere 1346estesa) da qualche ipotesi\footnote{Questo raffinamento accresce 1347l'applicabilit� del meccanismo di estensione senza accrescere il suo 1348potere espressivo. Avremmo potuto fare un raffinamento simile per l'altro 1349meccanismo di estensione di teoria.}. Cos� una {\em specifica 1350di tipo\/}\index{specifica di tipo} per una teoria $\cal T$ � 1351data da 1352 1353\medskip 1354 1355\noindent{\bf Dati} 1356\[ 1357\langle (\alpha_1,\ldots,\alpha_n)\ty{op},\sigma,p,\alpha,\Gamma,q\rangle 1358\] 1359 1360\noindent{\bf Condizioni} 1361 1362\begin{myenumerate} 1363\item 1364$(\ty{op},n)$ � una costante di tipo che non � in 1365${\sf Struc}_{\cal T}$. 1366 1367\item 1368$\alpha_1,\ldots,\alpha_n.\sigma$ � un tipo-in-contesto con 1369$\sigma\in{\sf Types}_{\cal T}$. 1370 1371\item $p_{\sigma\fun\bool}$ � un termine chiuso in ${\sf Terms}_{\cal T}$ 1372le cui variabili di tipo occorrono in $\alpha\!s=\alpha_1,\ldots,\alpha_n$. 1373 1374\item $\alpha$ � una variabile di tipo distinta da quelle in 1375$\alpha\!s$. 1376 1377\item $\Gamma$ � una lista di formule chiuse in ${\sf Terms}_{\cal T}$ 1378che non coinvolgono la variabile di tipo $\alpha$. 1379 1380\item $q$ � una formula chiusa in ${\sf Terms}_{\cal T}$. 1381 1382\item I sequenti 1383\begin{eqnarray*} 1384(\Gamma & , & \equant{x_\sigma}p\ x )\\ 1385(\Gamma & , & (\equant{f_{\alpha\fun\sigma}}{\sf Type\_Definition}\ 1386 p\ f)\ \imp\ q ) 1387\end{eqnarray*} 1388sono in ${\sf Theorems}_{\cal T}$. 1389 1390\end{myenumerate} 1391L'estensione di una teoria standard $\cal T$ per mezzo di una tale specifica 1392di tipo � denotata 1393\[ 1394{\cal T}{+_{\it tyspec}} \langle 1395(\alpha_1,\ldots,\alpha_n)\ty{op},\sigma,p,\alpha,\Gamma,q\rangle 1396\] 1397ed � definita essere la teoria 1398\[ 1399\langle 1400\begin{array}[t]{@{}l} 1401{\sf Struc}_{\cal T}\cup\{(\ty{op},n)\},\\ 1402 {\sf Sig}_{\cal T},\\ 1403 {\sf Axioms}_{\cal 1404 T}\cup\{(\Gamma , q[(\alpha_1,\ldots,\alpha_n)\ty{op}/\alpha])\},\\ 1405 {\sf Theorems}_{\cal T}\rangle 1406\end{array} 1407\] 1408 1409\noindent{\bf Esempio\ } Per eseguire l'estensione di \theory{INIT} 1410mensionata all'inizio di questa sezione, si forma 1411\[ 1412\theory{INIT}{+_{\it tyspec}} \langle 1413()\ty{one},\ty{bool},p,\alpha,\emptyset,q\rangle 1414\] 1415dove $p$ � il termine $\lquant{b_\bool}b$ e $q$ � la formula 1416$\uquant{f_{\beta\fun\alpha}\ g_{\beta\fun\alpha}}f=g$. Cos� il 1417risultato � una teoria che estende \theory{INIT} con una 1418nuova costante di tipo $\ty{one}$ che soddisfa l'assioma 1419$\uquant{f_{\beta\fun\ty{one}}\ g_{\beta\fun\ty{one}}}f=g$. 1420 1421Per verificare che questa � un'applicazione corretta del meccanismo 1422di estensione, si devono controllare le Condizioni da (i) a (vii) di sopra. Solo l'ultima 1423non � banale: essa impone l'obbligo di dimostrare 1424due sequenti dagli assiomi di \theory{INIT}. Il primo sequente dice 1425che $p$ definisce un sottoinsieme abitato di $\bool$, il che � certamente 1426vero dal momento che $\T$ testimonia questo fatto. Il secondo sequente dice 1427in effetti che qualsiasi tipo $\alpha$ che sia in biezione con il sottoinsieme di 1428$\bool$ definito da $p$ ha la propriet� che c'� al massimo una 1429funzione ad esso da qualsiasi tipo dato $\beta$; la dimostrazione di questo dagli 1430assiomi di \theory{INIT} � lasciata come esercizio. 1431 1432\medskip 1433 1434\noindent{\bf Proposizione\ }{\em 1435The theory ${\cal T}{+_{\it tyspec}}\langle 1436(\alpha_1,\ldots,\alpha_n)\ty{op},\sigma,p,\alpha,\Gamma,q 1437\rangle$ ha un modello standard se la teoria ${\cal T}$ lo ha.} 1438 1439\medskip 1440 1441\noindent{\bf Dimostrazione\ } 1442Scriviamo $\alpha\!s$ per $\alpha_1,\ldots,\alpha_n$, e supponiamo che 1443$\alpha\!s'={\alpha'}_1,\ldots,{\alpha'}_m$ sia la lista delle variabili 1444di tipo che occorrono in $\Gamma$ e $q$, ma che non sono ancora nella lista 1445$\alpha\!s,\alpha$. 1446 1447Supponiamo che $M$ sia un modello standard di ${\cal T}$. Dal momento che $\alpha\!s,.p$ � 1448un termine-in-contesto di tipo $\sigma\fun\ty{bool}$, interpretarlo in 1449$M$ porta a 1450\[ 1451\den{\alpha\!s,.p}_{M} 1452\in \prod_{X\!s\in{\cal U}^{n}}\den{\alpha\!s.\sigma\fun\ty{bool}}_M(X\!s) 1453= \prod_{X\!s\in{\cal U}^{n}} 1454 \den{\alpha\!s.\sigma}_M(X\!s)\fun\two . 1455\] 1456 1457Non c'� alcuna perdita di generalit� nell'assumere che $\Gamma$ consista di 1458una singola formula $\gamma$. (Semplicemente rimpiazziamo $\Gamma$ con la congiunzione delle 1459formula che esso contiene, con la convenzione che questa congiunzione sia 1460$\T$ se $\Gamma$ � vuoto.) Per l'assunzione su $\alpha\!s'$ e per la 1461Condizione~(iv), $\alpha\!s,\alpha\!s',.\gamma$ � un termine-in-contesto. 1462Interpretarlo in $M$ porta a 1463\[ 1464\den{\alpha\!s,\alpha\!s'.\gamma}_{M} 1465\in \prod_{(X\!s,X\!s')\in 1466{\cal U}^{n+m}}\den{\alpha\!s,\alpha\!s'.\ty{bool}}_M(X\!s,X\!s') 1467={\cal U}^{n+m}\fun\two 1468\] 1469 1470Ora $(\gamma,\equant{x_{\sigma}}p\ x)$ � in ${\sf Theorems}_{\cal T}$ 1471e di conseguenza per il Teorema di Validit�~\ref{soundness} questo sequente � 1472soddisfatto da $M$. Usando la semantica di $\exists$ data nella 1473Sezione~\ref{LOG} e la definizione di soddisfacimento di un sequente dalla 1474Sezione~\ref{sequents}, questo significa che per tutti gli $(X\!s,X\!s')\in{\cal U}^{n+m}$ 1475se $\den{\alpha\!s,\alpha\!s'.\gamma}_M(X\!s,X\!s')=1$, allora 1476l'insieme 1477\[ 1478\{y\in\den{\alpha\!s.\sigma}_{M}\: :\: \den{\alpha\!s,.p}(X\!s)(y)=1\} 1479\] 1480non � vuoto. (Questo usa il fatto che $p$ non coinvolge 1481le variabili di tipo $\alpha\!s'$, cos� per il Lemma~4 nella 1482Sezione~\ref{term-substitution} 1483$\den{\alpha\!s,\alpha\!s'.p}_M(X\!s,X\!s')=\den{\alpha\!s,.p}_M(X\!s)$.) 1484Dal momento che � anche un sottoinsieme di un insieme in $\cal U$, esso 1485segue per la propriet� {\bf Sub} dell'universo che questo insieme � un elemento di 1486$\cal U$. Cos� definendo 1487\[ 1488S(X\!s) = \left\{\hspace{-1mm} 1489\begin{array}{ll} 1490\{y\in\den{\alpha\!s.\sigma}_{M} : \den{\alpha\!s,.p}(X\!s)(y)=1\} 1491 & \mbox{\rm se $\den{\alpha\!s,.\gamma}_M(X\!s,X\!s')=1$, qualche $X\!s'$}\\ 14921 & \mbox{\rm altrimenti} 1493\end{array} 1494\right.%\} 1495\] 1496si ha che $S$ � una funzione ${\cal U}^n\fun{\cal U}$. Estendiamo $M$ 1497a un modello della firma di ${\cal T}'$ definendo che il suo valore alla 1498nuova costante di tipo $n$-aria $\ty{op}$ sia questa funzione $S$. Si noti 1499che i valori di $\sigma$, $p$, $\gamma$ e 1500$q$ in $M'$ sono gli stessi di quelli in $M$, dal momento che queste espressioni non 1501coinvolgono la nuova costante di tipo $\ty{op}$. 1502 1503Per ogni $X\!s\in{\cal U}^{n}$ definiamo $i_{X\!s}$ essere la funzione 1504d'inclusione per il sottoinsiem $S(X\!s)\subseteq\den{\alpha\!s.\sigma}_{M}$ 1505se $\den{\alpha\!s,\alpha\!s'.\gamma}_M(X\!s,X\!s')=1$ per qualche 1506$X\!s'$, e altrimenti essere la funzione 1507$1\fun\den{\alpha\!s.\sigma}_{M}$ che manda $0\in 1$ in 1508$\ch(\den{\alpha\!s.\sigma}_{M})$. Allora 1509$i_{X\!s}\in(S(X\!s)\fun\den{\alpha\!s.\sigma}_{M'}(X\!s))$ poich� 1510$\den{\alpha\!s.\sigma}_{M'}=\den{\alpha\!s.\sigma}_M$. Usando la 1511semantica di $\TyDef$ data nella Sezione~\ref{LOG}, si ha che per qualsiasi 1512$(X\!s,X\!s')\in{\cal U}^{n+m}$, se 1513$\den{\alpha\!s,\alpha\!s'.\gamma}_{M'}(X\!s,X\!s')=1$ allora 1514\[ 1515\den{\TyDef}_{M'}(\den{\alpha\!s.\sigma}_{M'} , 1516 S(X\!s))(\den{\alpha\!s,.p}_{M'})(i_{X\!s}) = 1. 1517\] 1518Cos� $M'$ soddisfa il sequente 1519\[ 1520(\gamma\ ,\ \equant{f_{(\alpha\!s)\ty{op}\fun\sigma}}\TyDef\ p\ f). 1521\] 1522Ma dal momento che il sequente $(\gamma,(\equant{f_{\alpha\fun\sigma}}{\sf 1523Type\_Definition}\ p\ f)\ \imp\ q )$ � in ${\sf Theorems}_{\cal T}$, 1524� soddisfatto dal modello $M$ e di conseguenza anche dal modello $M'$ 1525(dal momento che il sequente non coinvolge la nuova costante di tipo $\ty{op}$). 1526Istanziando $\alpha$ a $(\alpha\!s)\ty{op}$ in questo sequente (cosa che 1527� ammissibile dal momento che per la Condizione~(iv) $\alpha$ non occorre in 1528$\gamma$), si ha che $M'$ soddisfa il sequente 1529\[ 1530(\gamma\ ,\ 1531(\equant{f_{(\alpha\!s)\ty{op}\fun\sigma}}\TyDef\ p\ f)\imp 1532q[(\alpha\!s)\ty{op}/\alpha]). 1533\] 1534Applicando il Modus Ponens, si conclude che $M'$ soddisfa 1535$(\gamma\ ,\ q[(\alpha\!s)\ty{op}/\alpha])$ e 1536quindi $M'$ � un modello di ${\cal T}'$, come richiesto. 1537 1538\medskip 1539 1540Un'estensione per definizione di tipo � di fatto un caso speciale di estensione 1541per specifica di tipo. Per vedere questo, supponiamo che 1542$\langle (\alpha_1,\ldots,\alpha_n)\ty{op},\ \sigma,\ 1543p_{\sigma\fun\ty{bool}}\rangle$ sia una definizione di tipo per una teoria 1544$\cal T$. Scegliendo una variabile di tipo $\alpha$ differente da 1545$\alpha_1,\ldots,\alpha_n$, $q$ denoti la formula 1546\[ 1547\equant{f_{\alpha\fun\sigma}}{\sf Type\_Definition}\ p\ f 1548\] 1549Allora $\langle 1550(\alpha_1,\ldots,\alpha_n)\ty{op},\sigma,p,\alpha,\emptyset,q\rangle$ 1551soddisfa tutte le condizioni necessarie per essere una specifica di tipo per 1552$\cal T$. Dal momento che $q[(\alpha_1,\ldots,\alpha_n)\ty{op}/\alpha]$ � solo 1553$\equant{f_{(\alpha_1,\ldots,\alpha_n)\ty{op}\fun\sigma}}{\sf 1554Type\_Definition}\ p\ f$, si ha che 1555\[ 1556{\cal T}{+_{tydef}} 1557\langle(\alpha_1,\ldots,\alpha_n)\ty{op},\sigma,p\rangle 1558={\cal T}{+_{\it tyspec}} 1559\langle(\alpha_1,\ldots,\alpha_n)\ty{op},\sigma,p,\alpha,\emptyset,q\rangle 1560\] 1561Cos� la Proposizione nella Sezione~\ref{tydefs} � un caso speciale della 1562Proposizione di sopra. 1563 1564In un'estensione per specifica di tipo, la propriet� $q$ che � 1565affermata della nuova costante di tipo introdotta non ha bisogno di determinare la 1566costante di tipo in modo univoco (persino fino alla biezione). In modo corrispondente ci 1567possono essere molti modelli standard differenti della nuova teoria estesa la 1568cui restrizione a $\cal T$ � un dato modello $M$. Per contro, una definizione 1569di tipo determina la nuova costante di tipo in modo univoco fino alla biezione, 1570e due modelli qualsiasi della teoria estesa che si restringono allo stesso 1571modello della teoria originaria saranno isomorfi. 1572\index{extension, della logica HOL@extension, della logica \HOL{}!by type specification|)} 1573 1574 1575 1576%%% Local Variables: 1577%%% mode: latex 1578%%% TeX-master: "logic" 1579%%% End: 1580