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