11 Il risultato, se ce n'� uno, di una sessione con il sistema \HOL{} � un oggetto
13 logico chiamerebbe una teoria\index{theories, nella logica HOL@teorie, nella logica \HOL{}!forma astratta di}, ma ci sono alcune differenze che sorgono
14 dalle necessit� della dimostrazione meccanica. Una teoria \HOL{}, come la teoria di
15 un logico, contiene insiemi di tipi, costanti, definizioni e assiomi. In
17 esplicita lista di teoremi che sono gi� stati dimostrati dagli
18 assiomi e dalle definizioni. I logici non hanno alcuna necessit� di distinguere i teoremi
19 attualmente dimostrati da quelli meramente dimostrabili; di conseguenza essi normalmente non
20 considerano insiemi di teoremi dimostrati come parte di una teoria; piuttosto, essi
21 considerano i teoremi di una teoria essere l'insieme (spesso infinito) di tutte
30 Lo scopo del sistema \HOL{} � di fornire strumenti per permettere
31 di costruire teorie ben-formate. La logica \HOL{} � tipizzata:
32 ogni teoria specifica una firma di constanti di tipo e individuali;
34 precedente. Tutti i teoremi di tali teorie sono conseguenze logiche
36 che solo teorie ben-formate possono essere costruite permettendo di creare
39 del sistema di dimostrazione di \HOL{}, che sar� dato di seguito. Esso � dimostrato essere {\em
40 valido\/} per la semantica insiemistica di \HOL{} descritta nel
50 preservare la propriet� di possedere un modello. Cos� le teorie costruite
58 La logica \HOL{} � formulata in termini di asserzioni ipotetiche chiamate
61 t)$ dove $\Gamma$ � un insieme finito di formule su $\Sigma_\Omega$
63 il sottoscritto di tipo � omesso dai termini quando � chiaro dal
64 contesto che essi sono formule, cio� hanno tipo \ty{bool}.}. L'insieme di
65 formule $\Gamma$ che formano il primo componente di un sequente � chiamato
66 il suo insieme di {\it assunzioni\/}\index{assunzioni!di sequenti} e il
68 conclusione\/}\index{conclusioni!di sequenti}. Quando non d� origine ad
72 Intuitivamente un modello $M$ di $\Sigma_\Omega$ {\em
73 soddisfa}\index{soddisfazione di sequenti, da parte di un modello} un sequente
75 elementi di $M$ che rendono le formule in $\Gamma$ vere, rendono vera
78 contesto contenente tutte le variabili di tipo e tutte le variabili libere
81 tipo di $x_{j}$ sia $\sigma_{j}$. Dal momento che le formule sono termini di tipo
105 Nel caso $p=0$, la soddisfazione di $(\{\},t)$ da parte di $M$ sar� scritta
116 ${\cal D}$ � un insieme di coppie $(L,(\Gamma,t))$ dove $L$ � una
117 lista (possibilmente vuota) di sequenti e $(\Gamma,t)$ � un sequente.
120 un insieme di sequenti
131 \item $(L_i,(\Gamma_i,t_i))\in{\cal D}$ per qualche lista $L_i$ di membri di
136 � chiamata una {\it dimostrazione\/}\index{dimostrazione!nella deduzione naturale} di
147 non ci siano ipotesi\index{ipotesi!di sequenti} (cio� $n=0$),
150 In pratica, un particolare sistema deduttivo � di solito specificato da un
151 numero di \emph{regole d'inferenza} (schematiche),
152 \index{regole d'inferenza, della logica HOL@regole d'inferenza, della logica \HOL{}!forma astratta di primitive}
159 ipotesi\/}\index{ipotesi!di regole d'inferenza} della regola e il
161 conclusione}\index{conclusioni!di regole d'inferenza}. Una tale regola �
164 queste meta-variabili con termini reali, si ottiene una lista di sequenti
175 d'inferenza, date di seguito. Le prime tre regole non hanno ipotesi;
179 condizioni a lato che restringano lo scopo di una regola sono date immediatamente
180 al di sotto di essa.
184 \subsubsection*{Introduzione di assunzione [{\small\tt
185 ASSUME}]}\index{introduzione di assunzione, nella logica HOL@Introduzione di assunzione, nella logica \HOL{}!forma astratta di}
191 REFL}]}\index{REFL@\ml{REFL}}\index{riflessivit�, nella logica HOL@riflessivit�, nella logica \HOL{}!forma astratta di}
197 \index{beta-conversione, nella logica HOL@beta-conversione, nella logica \HOL{}!forma astratta di}\index{BETA_CONV@\ml{BETA\_CONV}}
203 il risultato di sostituire $t_2$ per $x$
209 SUBST}]}\index{SUBST@\ml{SUBST}} \index{sostituzione regola, nella logica HOL@sostituzione, regola di, nella logica \HOL{}!forma astratta di}
217 libere di sottotermini $t_1$, $\ldots$ , $t_n$ isolati e
218 $t[t_1',\ldots,t_n']$ denota il risultato di sostituire ciascuna occorrenza
219 selezionata di $t_i$ per $t_i'$ (per $1{\leq}i{\leq}n$), con una rinomina
225 \index{ABS@\ml{ABS}}\index{regola di astrazione}
234 \subsubsection*{Istanziazione di tipo [{\small\tt INST\_TYPE}]}
235 \index{type instantiation, nella logica HOL@type instantiation, nella logica \HOL{}!forma astratta di}
242 \item Dove $t\insttysub$ � il risultato di sostituire, in parallelo,
243 	i tipi $\sigma_1$, $\dots$, $\sigma_n$ per le variabili di tipo
245 	� il risultato di eseguire la stessa sostituzione in tutte le
252 \subsubsection*{Scaricamento di assunzione [{\small\tt
253 DISCH}]}\index{discharging assumptions, nella logica HOL@discharging assumptions, nella logica \HOL{}!forma astratta di}\index{DISCH@\ml{DISCH}}
259 \item Dove $\Gamma -\{t_1\}$ � la sottrazione insiemistica di $\{t_1\}$
264 MP}]}\index{MP@\ml{MP}}\index{Modus Ponens, nella logica HOL@Modus Ponens, nella logica \HOL{}!forma astratta di}
274 costante logica definita e il principio di definizione di costante non �
279 Il particolare insieme di regole e assiomi scelti per assiomatizzare la logica
285 regola di sostituzione\index{substitution rule, nella logica HOL@substitution rule, nella logica \HOL{}!implementation of} {\small\tt SUBST} � esattamente
289 importante che la primitiva di sistema fosse il pi� veloce possibile. Da un
290 punto di vista logico sarebbe stato meglio avere una primitiva
291 di sostituzione pi� semplice, come la `Regola R' della logica di Andrews ${\cal
294 \subsection{Teorema di validit�}
300 	la nozione di soddisfacimento definita nella Sezione~\ref{sequents}: per
301 	qualsiasi istanza di regole d'inferenza, se un modello (standard)
314 	il risultato sulla semantica della sostituzione di tipi per variabili di tipo
325 Una {\it teoria\/}\index{theories, nella logica HOL@theories, nella logica \HOL{}!forma astratta di} \HOL{} ${\cal T}$ � una $4$-tupla:
333 \item ${\sf Struc}_{\cal T}$ � una struttura di tipo\index{type structures, of HOL theories@type structures, of \HOL{} theories}  chiamata la
334 struttura di tipo di ${\cal T}$;
337 su ${\sf Struc}_{\cal T}$ chiamata la firma di ${\cal T}$;
339 \item ${\sf Axioms}_{\cal T}$ � un insieme di sequenti su ${\sf Sig}_{\cal T}$
341  di  ${\cal T}$;
343 \item ${\sf Theorems}_{\cal T}$ � un insieme di sequenti su
346 \index{theorems, nella logica HOL@theorems, nella logica \HOL{}!forma astratta di}
348 di ${\cal T}$, con
355 dei termini di una teoria ${\cal T}$ sono, rispettivamente, gli insiemi dei tipi e
356 dei termini costruibili dalla struttura di tipo e dalla firma di ${\cal
362 Un modello di una teoria $\cal T$ � specificato dando un modello (standard)
364 $M$ soddisfa tutti i sequenti che sono assiomi di $\cal T$.  A causa
365 del Teorema di Validit�~\ref{soundness}, segue che $M$ soddisfa
381 Dal momento che la teoria \theory{MIN} ha una firma che consiste solo di
386 minimale, sfruttando i costrutti di ordine superiore di \HOL{} si pu�
387 costruire su di essa una collezione di termini piuttosto ricca. La seguente
388 teoria introduce nomi per alcuni di questi termini che denotano utili
392 \theoryimp{min}, e contiene anche il distinto operatore di tipo
393 binario $\fun$, per costruire spazi di funzione.
400 di tipo di \theory{MIN}. La sua firma contiene le costanti in
404 \index{T@\holtxt{T}!forma astratta di}
405 \index{truth values, nella logica HOL@truth values, nella logica \HOL{}!forma astratta di}
409 \index{universal quantifier, nella logica HOL@universal quantifier, nella logica \HOL{}!forma astratta di}
413 \index{existential quantifier, nella logica HOL@existential quantifier, nella logica \HOL{}!forma astratta di}
417 \index{F@\holtxt{F}!forma astratta di}
421 \index{negation, nella logica HOL@negation, nella logica \HOL{}!forma astratta di}
425 \index{conjunction, nella logica HOL@conjunction, nella logica \HOL{}!forma astratta di}
429 \index{disjunction, nella logica HOL@disjunction, nella logica \HOL{}!forma astratta di}
433 \index{one-to-one predicate, nella logica HOL@one-to-one predicate, nella logica \HOL{}!forma astratta di}
437 \index{onto predicate, nella logica HOL@onto predicate, nella logica \HOL{}!forma astratta di}
493 definizioni\/} delle nuove costanti di \theory{LOG} come termini nella
495 estensioni alle teorie attraverso definizioni di nuove costanti sar� riportato
499 Bench� queste definizioni possano essere oscure a qualche lettore, esse sono di
500 fatto definizioni standard di queste costanti logiche in termini di
501 implicazione, uguaglianza e scelta all'interno della logica di ordine superiore. I
502 due assiomi successivi definiscono le propriet� di una funzione di essere iniettiva e suriettiva;
505 costante usata per le definizioni di tipo (si veda la Sezione~\ref{tydefs}).
507 L'unico modello standard {\em Min\/} di \theory{MIN} d� origine a un
508 unico modello standard di
511 Sezione~\ref{semantics of terms}, per soddisfare le equazioni di sopra si �
596 termini ai lati sinistri dell'equazioni che formano gli assiomi di
604 La teoria \theory{INIT}\index{INIT@\ml{INIT}!forma astratta di} si
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}
629 L'unico modello standard di \theory{LOG} soddisfa questi quattro assiomi
630 e di conseguenza � l'unico modello standard della teoria
632 {\small\tt SELECT\_AX} � necessario usare la definizione di
638   della logica HOL@initial theory, della logica \HOL{}!forma astratta di} della
647 costanti e gli assiomi da queste teorie, e include un numero di
659 L'esistenza di un modello (standard) di una teoria � sufficiente per
661 di Validit�~\ref{soundness}, qualsiasi sequente che possa essere derivato dagli
667 possieda un modello standard. Questo avviene perch� la nozione di un
670 modello. Il famoso teorema di incompletezza di G\"odel assicura che ci
678 \section{Estensioni di teorie}
679 \index{extension, della logica HOL@extension, della logica \HOL{}!forma astratta di}
683 estensione\/}\index{extension, of theory} di una teoria ${\cal T}$ se:
693 di $\cal T$ semplicemente dimenticando i valori di $M'$ alle costanti che non sono
702 (e di conseguenza anche su ${\sf Sig}_{{\cal T}'}$), allora $\Gamma
705 di ${\cal T}'$, segue che $M$ � un modello di $\cal T$. $M$ sar�
714 \item Estensione attraverso la specifica di una costante   (si veda la Sezione~\ref{specs}).
716 \item Estensione attraverso la specifica di un tipo (si veda la
717 Sezione~\ref{tyspecs}).\footnote{Questo meccanismo di estensione di teorie non �
721 Il primo meccanismo permette la `specifica libera' di costanti (come nella
722 notazione {\bf Z}~\cite{Z}, per esempio); la seconda permette di
723 introdurre nuovi tipi e operatori di tipo. Come casi speciali (quando la
727 \item Estensione attraverso la definizione di una costante (si veda la Sezione~\ref{defs}).
729 \item Estensione attraverso la definizione di un tipo (si veda la Sezione~\ref{tydefs}).
735 di propriet� di quelli esistenti. La loro propriet� chiave � che la
737 lo ha. Cos� � garantito che una serie di queste estensioni che iniziano dalla teoria
739 standard, e di conseguenza in una teoria coerente. E' anche possibile estendere
743 assiomi\index{assiomi!non necessit� di aggiungere}, non c'� alcuna garanzia
746 furto rispetto al lavoro onesto\footnote{Si veda la pagina 71 del libro di Russel {\sl
749 caldamente invitati a resistere alla tentazione di aggiungere assiomi, ma di lavorare
755 \subsection{Estensione per definizione di costanti}
759 Una {\it definizione di costante\/}\index{definizione di costante} su una
765 $\con{c}$ non � il nome di alcuna costante in $\Sigma_{\Omega}$;
771 tutte le variabili di tipo che occorrono in $t_\sigma$ occorrono anche in $\sigma$
775 Data una teoria $\cal T$ e una tale definizione di costante su ${\sf
776 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}$
792 Si noti che il meccanismo di estensione per definizione di costante � gi�
795 di questa sezione si ha
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} \ =\
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 =
802    {+_{\it def}}\langle {\exists}\index{existential quantifier, nella logica HOL@existential quantifier, nella logica \HOL{}!forma astratta di}\ =\
804    {+_{\it def}}\langle \F\index{F@\holtxt{F}!forma astratta di}
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}
809    {+_{\it def}}\langle {\vee}\index{disjunction, nella logica HOL@disjunction, nella logica \HOL{}!forma astratta di}\ =\ \lquant{b_1\ b_2}\uquant{b}
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}
826 Sezione~\ref{specs} mostrando che l'estensione per definizione di costante
827 � di fatto un caso speciale di estensione per specifica di costante.
830 la quantificazione esistenziale non sia necessaria per le definizioni di costanti, �
831 necessaria per formulare il meccanismo di specifica di costante.)
835 \noindent{\bf Nota\ } La condizione (iii) nella definizione di
836 ci� che costituisce una definizione di costante corretta � una restrizione
840 di elementi denotati dal) tipo $\alpha$ � infinito. Il termine contiene
841 la variabile di tipo $\alpha$, mentre il tipo del termine, $\ty{bool}$,
847 non � permessa come definizione di una costante. Il problema � che il
850 dal momento che non contiene $\alpha$. Di fatto, se ci fosse permesso di
854 dagli assiomi di $\theory{INIT}$, e di conseguenza $\con{c}_\ty{bool}=\T$ �
857 dagli assiomi di $\theory{INIT}$, e di conseguenza anche $\con{c}_\ty{bool}=\F$ �
862 \subsection{Estensione per specifica di costante}
866 Le specifiche di costanti\index{constant specification extension, della logica HOL@constant specification extension, della logica \HOL{}!abstract form
867 of} introducono costanti (o insiemi di costanti)
869 teoria potrebbe essere estesa da una specifica di costante in modo da avere due nuove
870 costanti $\con{b}_1$ e $\con{b}_2$ di tipo \ty{bool} tali che
877 avere sono coerenti. Questo impedisce, per esempio, di introdurre tre
884 specifica di costante permette di introdurre le nuove costanti $\con{c}_1$, $\ldots$ ,
890 risultato di sostituire simultaneamente $\con{c}_1, \ldots, \con{c}_n$
891 per $x_1, \ldots, x_n$ rispettivamente. Naturalmente il tipo di ciascuna
893 variabile $x_i$. Per assicurare che questo meccanismo di estensione preserva la
894 propriet� di possedere un modello, � imposto su questi tipi un ulteriore
896 di tipo che occorrono in $t$. Questa condizione � discussa ulteriormente nella
897 Sezione~\ref{constants} di sotto.
899 Formalmente, una {\em specifica di costante\/}\index{constant specification}
914 non sono i nomi di alcuna costante in ${\sf Sig}_{\cal T}$.
928 L'estensione di una teoria standard ${\cal T}$ per mezzo di una tale specifica
929 di costante � denotata da
958 Supponiamo che $M$ sia un modello standard di ${\cal T}$. Sia
959 $\alpha\!s=\alpha_{1},\ldots,\alpha_{m}$ la lista di variabili di tipo
969 Ora $\equant{x\!s}t$ � in ${\sf Theorems}_{\cal T}$ e di conseguenza per il
970 Teorema di Validit� \ref{soundness}\index{consistency, della logica HOL@consistency, della logica \HOL{}!under constant specification} questo
971 sequente � soddisfatto da $M$. Usando la semantica di $\exists$ data nella
979 non � 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�
982 di scelta globale $\ch\in\prod_{X\in{\cal U}}X$ per selezionare un elemento specifico.
988 $M$ a un modello $M'$ della firma di ${\cal
997 Si noti che la Condizione (iii) nella definizione di una specifica
998 di costante assicura che $\alpha\!s$ � il contesto canonico di ogni
1001 di fatto un elemento del prodotto di sopra.
1003 Dal momento che $t$ � un termine della sotto-teoria $\cal T$ di \linebreak${\cal
1015 la definizione di $\den{\con{c}_{i}}_{M'}$, si ottiene infine che
1022 Quindi $M'$ � un modello di ${\cal T}{+_{\it
1029 Le costanti che sono affermate esistere in una specifica di costante
1031 essere pi� modelli differenti di ${\cal T}{+_{\it
1034 \rangle$ la cui restrizione a $\cal T$ � $M$; la costruzione di sopra
1036 di scelta globale sull'universo.
1038 L'estensione per mezzo di una definizione di costante, $\con{c}_\sigma=t_\sigma$, � un
1039 caso speciale di estensione per specifica di costante. Perch� sia $t'$
1043 di costante per ottenere la teoria
1052 standard $M$ di $\cal T$, c'� un modello standard $M'$ di ${\cal
1055 di costante, $M'$ � determinato in modo univoco da $M$ e dalla definizione di
1062 Si noti come la Condizione (iii) nella definizione di una specifica di costante
1063 sia stata necessaria nella dimostrazione che il meccanismo di estensione preserva la
1064 propriet� di possedere un modello standard. Il suo ruolo � di assicurare che
1066 variabili di tipo che ha la formula che le specifica. La
1067 situazione � la stessa di quella discussa nella Nota nella
1069 nell'esempio dato in quella Nota non � tanto il metodo di estensione per mezzo
1070 dell'introduzione di costanti, ma piuttosto la sintassi di \HOL{} che non
1071 permette alle costanti di dipendere esplicitamente dalle variabili di tipo (nel modo
1072 in cui lo fanno gli operatori di tipo). Cos� nell'esempio si vorrebbe
1082 Nella versione attuale di \HOL, le costanti sono coppie-(nome,tipo).
1083 Si potrebbe immaginare una leggera estensione della sintassi di \HOL{} con
1086 tipo-in-contesto e la lista $\alpha\!s$ pu� ben contenere variabili di tipo
1091 questo istanziando le variabili di tipo $\alpha_i$ con i tipi
1092 $\tau_i$ (cos� $\sigma'$ � l'istanza di $\sigma$ ottenuta
1093 sostituendo  $\tau\!s$ per $\alpha\!s$). Questa nuova sintassi di costanti
1095 la sezione~\ref{types}): un operatore di tipo $n$-ario $\textsl{op}$ da origine a un
1097 variabili di tipo. Analogamente, la sintassi di sopra delle costanti polimorfiche
1098 registra come esse dipendono dalle variabili di tipo (as well as which generic
1101 Tuttavia, registrare esplicitamente la dipendenza delle costanti dalle variabili di tipo
1104 di tipo $\alpha\!s$ in $(\con{c},\alpha\!s.\sigma)$ � di fatto il
1105 contesto {\em canonico\/} di $\sigma$, cio� contiene esattamente le variabili
1106 di tipo di $\sigma$. Perch� allora si pu� applicare il Lemma~1 della
1117 di complicare la sintassi esistente al costo di restringere
1118 in qualche modo l'applicabilit� di questi meccanismi di estensioni delle teorie.
1121 \subsection{Estensione per definizione di tipo}
1123 \index{representing types, nella logica HOL@representing types, nella logica \HOL{}!forma astratta di|(}
1130 all'operazione di prendere un sottoinsieme non-vuoto di $\den{\sigma}$, non c'�
1131 alcun meccanismo corrispondente per formare un `sottotipo' di $\sigma$. Piuttosto,
1133 termine chiuso $p$ di tipo $\sigma\fun\ty{bool}$ determina il sottoinsieme
1136 meccanismo per introdurre nuovi tipi che sono sottotipi di quelli
1138 di tipo e asserendo un assioma che la caratterizza denotare un
1140 non-vuoto di un tipo esistente (chiamato il {\em tipo rappresentante\/}).
1145 Cos� come definire tipi, � anche conveniente essere in grado di definire
1146 operatori di tipo. Un esempio sarebbe un operatore di tipo \ty{inj} che
1147 mappasse un insieme all'insieme di funzioni uno-a-uno (cio� iniettive) su
1148 di esso. Il sottoinsieme di $\sigma\fun\sigma$ che rappresenta $(\sigma)\ty{inj}$
1150 operatore di tipo per il prodotto cartesiano binario \ty{prod}. Questo � definito
1151 scegliendo un tipo rappresentante che contiene due variabili di tipo, diciamo
1153 $\sigma_2$, un sottoinsieme di $\sigma[\sigma_1;\sigma_2]$ rappresenta il
1154 prodotto cartesiano di $\sigma_1$ e $\sigma_2$. I dettagli di una tale
1155 definizione sono dati nella sezione di \DESCRIPTION\/ sulla teoria dei
1162 sarebbe incoerente definire un operatore di tipo binario \ty{iso} tale
1163 che $(\sigma_1,\sigma_2)\ty{iso}$ denotasse l'insieme di funzioni
1165 valore di $\sigma_1$ e $\sigma_2$ l'insieme sarebbe vuoto; per
1167 evitare questo, una precondizione di definire un nuovo tipo � che il
1173 \item Specificando un sottoinsieme di questo tipo.
1186 sottoinsieme di $\sigma$.
1190 diciamo, di tipo $\sigma\fun\bool$. Il termine $p$ � chiamato la {\it
1191 funzione caratteristica\/}\index{characteristic function, of type definitions}. Questo definisce il sottoinsieme di $\sigma$ al quale
1194 libere, � che altrimenti per coerenza l'operatore di tipo definito
1195 dovrebbe {\em dipendere\/} da (cio� essere una funzione di) queste
1203 isomorfo al sottoinsieme di $\sigma$ selezionato da $p$.
1213 al sottoinsieme di elementi di $\sigma$ per cui $p$ � vero.
1222 operatore di tipo $n$-ario e l'assioma di sopra come un nuovo assioma. Formalmente, una {\em
1223 definizione di tipo\/}\index{type definitions, nella logica HOL@type definitions, nella logica \HOL{}!abstract structure of} per una teoria ${\cal
1238 $(\ty{op},n)$ non � il nome di una costante di tipo in ${\sf Struc}_{\cal T}$.
1245 le cui variabili di tipo occorrono in $\alpha_1,\ldots,\alpha_n$.
1251 L'estensione di una teoria standard ${\cal T}$ per mezzo di una tale definizione di tipo
1279 Al posto di dare una dimostrazione diretta di questo risultato, esso sar� dedotto come
1282 \index{representing types, nella logica HOL@representing types, nella logica \HOL{}!forma astratta di|)}
1285 \subsection{Estensione per specifica di tipo}
1289 (\textbf{Nota:} Questo meccanismo di estensione \emph{non} �
1291 raffina una proposta di R.~Jones e R.~Arthan.)
1294 \noindent Il meccanismo di definizione di
1296 rappresentazione del tipo come un `sottotipo' di un tipo esistente. Si
1303 suo sottoinsieme di un elemento. (L'idea � quella che la scelta del
1304 tipo rappresentante � irrilevante per le propriet� di $\ty{one}$ che
1306 fornisce un modo di ottenere questo preservando allo stesso tempo
1307 la propriet� fondamentale di possedere un modello standard e quindi
1308 di mantenere la coerenza.
1310 Ogni formula chiusa $q$ che coinvolge una singola variabile di tipo $\alpha$ pu�
1318 sottoinsieme $\{X\in{\cal U}:\den{\alpha,.q}(X)=1\}$ che consiste di quegli
1320 pi� generale per assicurare la coerenza nell'introduzione di un nuovo tipo
1331 e non coinvolge la variabile di tipo $\alpha$. Questa formula dice `$q$
1332 vale di qualsiasi tipo che � in biezione con il sottotipo di $\sigma$
1341 Nel dare la definizione formale di questo meccanismo di estensione, saranno
1343 polimorfico e di conseguenza � introdotta una nuova costante di ripo di ariet�
1345 esistenziali di sopra � permesso di essere dimostrate (nella teoria che deve essere
1347 l'applicabilit� del meccanismo di estensione senza accrescere il suo
1349 meccanismo di estensione di teoria.}. Cos� una {\em specifica
1350 di tipo\/}\index{specifica di tipo} per una teoria $\cal T$ �
1364 $(\ty{op},n)$ � una costante di tipo che non � in
1372 le cui variabili di tipo occorrono in $\alpha\!s=\alpha_1,\ldots,\alpha_n$.
1374 \item $\alpha$ � una variabile di tipo distinta da quelle in
1377 \item $\Gamma$ � una lista di formule chiuse in ${\sf Terms}_{\cal T}$
1378 che non coinvolgono la variabile di tipo $\alpha$.
1391 L'estensione di una teoria standard $\cal T$ per mezzo di una tale specifica
1392 di tipo � denotata
1409 \noindent{\bf Esempio\ } Per eseguire l'estensione di \theory{INIT}
1410 mensionata all'inizio di questa sezione, si forma
1418 nuova costante di tipo $\ty{one}$ che soddisfa l'assioma
1422 di estensione, si devono controllare le Condizioni da (i) a (vii) di sopra. Solo l'ultima
1423 non � banale: essa impone l'obbligo di dimostrare
1424 due sequenti dagli assiomi di \theory{INIT}. Il primo sequente dice
1425 che $p$ definisce un sottoinsieme abitato di $\bool$, il che � certamente
1427 in effetti che qualsiasi tipo $\alpha$ che sia in biezione con il sottoinsieme di
1429 funzione ad esso da qualsiasi tipo dato $\beta$; la dimostrazione di questo dagli
1430 assiomi di \theory{INIT} � lasciata come esercizio.
1444 di tipo che occorrono in $\Gamma$ e $q$, ma che non sono ancora nella lista
1447 Supponiamo che $M$ sia un modello standard di ${\cal T}$. Dal momento che $\alpha\!s,.p$ �
1448 un termine-in-contesto di tipo $\sigma\fun\ty{bool}$, interpretarlo in
1457 Non c'� alcuna perdita di generalit� nell'assumere che $\Gamma$ consista di
1471 e di conseguenza per il Teorema di Validit�~\ref{soundness} questo sequente �
1472 soddisfatto da $M$. Usando la semantica di $\exists$ data nella
1473 Sezione~\ref{LOG} e la definizione di soddisfacimento di un sequente dalla
1481 le variabili di tipo $\alpha\!s'$, cos� per il Lemma~4 nella
1484 Dal momento che � anche un sottoinsieme di un insieme in $\cal U$, esso
1485 segue per la propriet� {\bf Sub} dell'universo che questo insieme � un elemento di
1497 a un modello della firma di ${\cal T}'$ definendo che il suo valore alla
1498 nuova costante di tipo $n$-aria $\ty{op}$ sia questa funzione $S$. Si noti
1499 che i valori di $\sigma$, $p$, $\gamma$ e
1500 $q$ in $M'$ sono gli stessi di quelli in $M$, dal momento che queste espressioni non
1501 coinvolgono la nuova costante di tipo $\ty{op}$.
1511 semantica di $\TyDef$ data nella Sezione~\ref{LOG}, si ha che per qualsiasi
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}$).
1536 quindi $M'$ � un modello di ${\cal T}'$, come richiesto.
1540 Un'estensione per definizione di tipo � di fatto un caso speciale di estensione
1541 per specifica di tipo. Per vedere questo, supponiamo che
1543 p_{\sigma\fun\ty{bool}}\rangle$ sia una definizione di tipo per una teoria
1544 $\cal T$. Scegliendo una variabile di tipo $\alpha$ differente da
1551 soddisfa tutte le condizioni necessarie per essere una specifica di tipo per
1562 Proposizione di sopra.
1564 In un'estensione per specifica di tipo, la propriet� $q$ che �
1565 affermata della nuova costante di tipo introdotta non ha bisogno di determinare la
1566 costante di tipo in modo univoco (persino fino alla biezione). In modo corrispondente ci
1569 di tipo determina la nuova costante di tipo in modo univoco fino alla biezione,

Indexes created Sun Jun 23 19:15:37 MDT 2024