1178 lines
133 KiB
HTML
1178 lines
133 KiB
HTML
<!DOCTYPE html>
|
||
<html lang="italian">
|
||
<head>
|
||
<meta charset="utf-8">
|
||
<meta name="generator" content="pandoc">
|
||
<meta name="viewport" content="width=device-width, initial-scale=1.0, user-scalable=yes">
|
||
<meta name="author" content="Michele Guerini Rocco">
|
||
<title>I sistemi formali</title>
|
||
<style type="text/css">code{white-space: pre;}</style>
|
||
<style type="text/css">
|
||
div.sourceCode { overflow-x: auto; }
|
||
table.sourceCode, tr.sourceCode, td.lineNumbers, td.sourceCode {
|
||
margin: 0; padding: 0; vertical-align: baseline; border: none; }
|
||
table.sourceCode { width: 100%; line-height: 100%; }
|
||
td.lineNumbers { text-align: right; padding-right: 4px; padding-left: 4px; color: #aaaaaa; border-right: 1px solid #aaaaaa; }
|
||
td.sourceCode { padding-left: 5px; }
|
||
code > span.kw { color: #007020; font-weight: bold; } /* Keyword */
|
||
code > span.dt { color: #902000; } /* DataType */
|
||
code > span.dv { color: #40a070; } /* DecVal */
|
||
code > span.bn { color: #40a070; } /* BaseN */
|
||
code > span.fl { color: #40a070; } /* Float */
|
||
code > span.ch { color: #4070a0; } /* Char */
|
||
code > span.st { color: #4070a0; } /* String */
|
||
code > span.co { color: #60a0b0; font-style: italic; } /* Comment */
|
||
code > span.ot { color: #007020; } /* Other */
|
||
code > span.al { color: #ff0000; font-weight: bold; } /* Alert */
|
||
code > span.fu { color: #06287e; } /* Function */
|
||
code > span.er { color: #ff0000; font-weight: bold; } /* Error */
|
||
code > span.wa { color: #60a0b0; font-weight: bold; font-style: italic; } /* Warning */
|
||
code > span.cn { color: #880000; } /* Constant */
|
||
code > span.sc { color: #4070a0; } /* SpecialChar */
|
||
code > span.vs { color: #4070a0; } /* VerbatimString */
|
||
code > span.ss { color: #bb6688; } /* SpecialString */
|
||
code > span.im { } /* Import */
|
||
code > span.va { color: #19177c; } /* Variable */
|
||
code > span.cf { color: #007020; font-weight: bold; } /* ControlFlow */
|
||
code > span.op { color: #666666; } /* Operator */
|
||
code > span.bu { } /* BuiltIn */
|
||
code > span.ex { } /* Extension */
|
||
code > span.pp { color: #bc7a00; } /* Preprocessor */
|
||
code > span.at { color: #7d9029; } /* Attribute */
|
||
code > span.do { color: #ba2121; font-style: italic; } /* Documentation */
|
||
code > span.an { color: #60a0b0; font-weight: bold; font-style: italic; } /* Annotation */
|
||
code > span.cv { color: #60a0b0; font-weight: bold; font-style: italic; } /* CommentVar */
|
||
code > span.in { color: #60a0b0; font-weight: bold; font-style: italic; } /* Information */
|
||
</style>
|
||
<link rel="stylesheet" href="options/style.css">
|
||
<script src="" type="text/javascript"></script>
|
||
<!--[if lt IE 9]>
|
||
<script src="//cdnjs.cloudflare.com/ajax/libs/html5shiv/3.7.3/html5shiv-printshiv.min.js"></script>
|
||
<![endif]-->
|
||
<script type="text/javascript" src="http://cdn.mathjax.org/mathjax/latest/MathJax.js?config=TeX-AMS_HTML"></script>
|
||
<script type="text/x-mathjax-config">
|
||
MathJax.Hub.Config({
|
||
extensions: ["tex2jax.js"],
|
||
jax: ["input/TeX", "output/HTML-CSS"],
|
||
|
||
"HTML-CSS": { availableFonts: ["TeX"] }
|
||
});
|
||
</script>
|
||
<h1>I sistemi formali</h1>
|
||
</head>
|
||
<body>
|
||
<header>
|
||
<h1 class="title">I sistemi formali</h1>
|
||
<h2 class="author">Michele Guerini Rocco</h2>
|
||
<h3 class="date">25 Giugno 2015</h3>
|
||
</header>
|
||
<h2 id="introduzione-lindagine-sui-fondamenti"><span class="header-section-number">1.1</span> Introduzione: l’indagine sui fondamenti</h2>
|
||
<p>Nei cinquant’anni a cavallo tra XIX e XX secolo si è sviluppata un’importante <strong>riflessione</strong> e ricerca sui <strong>fondamenti della matematica</strong>. Partì dalla necessità di definire in modo rigoroso il calcolo infinitesimale nel quale rimanevano ancora poco chiari concetti come quello di <em>infinitesimo</em>, <em>limite</em> e <em>integrale</em>. Le spiegazioni intuitive fornite dai tempi di Leibniz che sfruttavano la geometria non potevano essere infatti le vere basi epistemologiche del calcolo ma queste andavano ricercate altrove.</p>
|
||
<h2 id="aritmetizzazione"><span class="header-section-number">1.2</span> Aritmetizzazione</h2>
|
||
<p>In una prima fase l’obbiettivo fu quello di <strong>ridurre</strong> tutte le nozioni della matematica ai concetti più semplici possibili dell’<strong>aritmetica</strong> a cui contribuirono matematici come Dedekind, Weierstrass e Cantor.</p>
|
||
<p>I <strong>numeri</strong> interi, razionali, reali e complessi furono ricondotti a numeri naturali. I complessi come coppia di numeri reali; i reali per esempio come <em>sezioni</em> nell’insieme dei razionali; i razionali come coppie di naturali.</p>
|
||
<h4 id="teoria-degli-insiemi"><span class="header-section-number">1.2.0.1</span> Teoria degli insiemi</h4>
|
||
<figure>
|
||
<img src="images/cantor.jpg" alt="Georg Cantor" /><figcaption>Georg Cantor</figcaption>
|
||
</figure>
|
||
<p>La teoria degli <strong>insiemi</strong> che era stata fino a quel momento molto generica e intuitiva venne studiata a fondo. Georg Cantor negli anni ’80 del XIX secolo fece chiarezza sugli insiemi di <strong>infiniti elementi</strong> (come i numeri naturali) dove la concezione intuitiva di insieme inizia ad avere problemi. Definì i concetti di cardinalità e numeri transfiniti arrivando alla rivoluzionaria scoperta dell’esistenza di <strong>infiniti di diverso ordine</strong>. I matematici Zermelo e Frankel a partire dal 1908 produssero la prima teoria <em>assiomatica</em> degli insiemi su cui si basa ancora oggi tutta la matematica ordinaria.</p>
|
||
<h3 id="logicizzazione"><span class="header-section-number">1.2.1</span> Logicizzazione</h3>
|
||
<p>In questi stessi anni c’è chi decise di andar oltre l’aritmetica nel processo di riduzione della matematica e cercò quindi di ricondurre tutto ai principi della logica, ancora più originari e indiscutibili.</p>
|
||
<h4 id="aritmetica-di-peano"><span class="header-section-number">1.2.1.1</span> Aritmetica di Peano</h4>
|
||
<p>Il matematico italiano Giuseppe Peano nel 1889, seguendo l’esempio della geometria di Euclide, individuò le caratteristiche fondamentali dei numeri naturali e le espresse in 5 proposizioni. Senza creare un complesso sistema formale si limitò a fornire le proprietà dei numeri dalle quali poi è possibile produrre tramite il ragionamento l’intera aritmetica. I cinque postulati di Peano possono essere espressi nel seguente modo:</p>
|
||
<ol type="1">
|
||
<li>Zero è un numero</li>
|
||
<li>Ogni numero ha un successore</li>
|
||
<li>Zero non è il successore di alcun numero</li>
|
||
<li>Numeri diversi hanno successori diversi</li>
|
||
<li>Se zero ha una proprietà <span class="math inline">\(X\)</span> e ogni numero conferisce <span class="math inline">\(X\)</span> al suo successore allora tutti i numeri hanno <span class="math inline">\(X\)</span></li>
|
||
</ol>
|
||
<p>Vedremo in seguito che questi postulati, specialmente l’ultimo, avranno un ruolo fondamentale, oltre che nel definire i sistemi formali e le loro caratteristiche, nella dimostrazione del teorema di Gödel.</p>
|
||
<h4 id="il-programma-di-frege"><span class="header-section-number">1.2.1.2</span> Il programma di Frege</h4>
|
||
<p>Il logico matematico <strong>Gottlob Frege</strong> tentò di ricondurre i numeri alla logica tramite l’uso del concetto logico di <strong>classe</strong> (o insieme) ed <strong>equinumerosità</strong>. Due classi sono equinumerose quando è possibile creare una relazione biunivoca tra gli elementi di esse. Definì quindi i <strong>numeri naturali</strong> in termini di <strong>classe di classi</strong>:</p>
|
||
<p>il numero della classe <span class="math inline">\(C\)</span> è la classe di tutte le classi equinumerose a <span class="math inline">\(C\)</span>. Per esempio il numero 2 è la classe di tutte le classi che hanno 2 elementi.</p>
|
||
<h3 id="la-crisi"><span class="header-section-number">1.2.2</span> La crisi</h3>
|
||
<figure>
|
||
<img src="images/russell.jpg" alt="Bertrand Russell" /><figcaption>Bertrand Russell</figcaption>
|
||
</figure>
|
||
<p>Il sistema logicista entrò ben presto in crisi quando il logico inglese <strong>Bertrand Russell</strong> scoprì un’<strong>antinomia</strong> legata al concetto stesso di insieme che ne evidenziò la contraddittorietà.</p>
|
||
<p>È infatti possibile costruire un insieme che porta inevitabilmente ad una <strong>contraddizione</strong>. Alcuni insiemi abbiamo visto possono contenerne altri (come la definizione di numero per esempio) e alcuni possono contenere sé stessi. Per esempio l’insieme di tutti gli insiemi contiene se stesso mentre l’insieme di tutte le persone non è una persona e quindi non contiene anche se stesso. Ora il <strong>paradosso di Russell</strong> dice questo: “L’insieme di tutti gli insiemi che non contengono se stessi contiene se stesso?”</p>
|
||
<p>Se non dovesse avere se stesso come elemento allora per la sua definizione dovrebbe contenere se stesso portando ad una contraddizione. Se invece contenesse se stesso significherebbe che per la sua definizione non dovrebbe contenere se stesso portando ugualmente ad una contraddizione.</p>
|
||
<p>Di fronte a questi risultati paradossali Frege stesso decise di abbandonare il programma logicista. Iniziò così la crisi dei fondamenti della matematica.</p>
|
||
<h3 id="principia-mathematica"><span class="header-section-number">1.2.3</span> Principia Mathematica</h3>
|
||
<p>Russell tuttavia non perse le speranze di dare un fondamento logico all’aritmetica e cercò di risolvere l’antinomia da lui stesso prodotta. Nell’immensa opera <em>Principia Mathematica</em> scritta da Russell in collaborazione con il matematico Alfred North Whitehead fu proposta la <strong>teoria dei tipi</strong> nel tentativo di eliminare l’autoreferenza delle classi.</p>
|
||
<p>Agli oggetti viene conferito un <em>tipo</em>: agli <strong>individui</strong> cioè numeri, oggetti fisici, elementi singoli viene dato il <strong>tipo 0</strong> mentre insiemi che contengono individui hanno <strong>tipo 1</strong>, insiemi di insiemi di tipo 1 hanno <strong>tipo 2</strong> e così via. Un insieme di tipo <span class="math inline">\(n\)</span> può contenere solo oggetti di tipo minore di <span class="math inline">\(n\)</span>.</p>
|
||
<p>Questa teoria non si limita agli insiemi: proibisce, per esempio, che io parli di questo documento in questo stesso documento come sto facendo ora: potrei parlarne solo in un metadocumento. Inoltre menzionare me stesso tramite il pronome “io” sarebbe del tutto impossibile. Persino la stessa discussione di questa teoria è una sua sfacciata violazione: questo fa capire, per quanto utile che sia, quanto la teoria dei tipi è limitante.</p>
|
||
<p>Con la teoria dei tipi viene eliminata la possibilità per un insieme di contenere se stesso e così anche il paradosso di Russell: tuttavia rimangono sempre possibili delle antinomie che sfruttano lo stesso principio ma legate al linguaggio come il <strong>paradosso del mentitore</strong> o il <strong>paradosso di Grelling-Nelson</strong>. Vedremo in seguito proprio queste saranno la causa del crollo dei <em>Principia</em> e in generale della ricerca di fondamenti formali della matematica.</p>
|
||
<h3 id="il-programma-di-hilbert"><span class="header-section-number">1.2.4</span> Il programma di Hilbert</h3>
|
||
<figure>
|
||
<img src="images/hilbert.jpg" alt="David Hilbert" /><figcaption>David Hilbert</figcaption>
|
||
</figure>
|
||
<p>Se un concetto così semplice come quello di insieme aveva potuto creare dei problemi così grandi non è allora possibile che ci siano altre contraddizione interne alla matematica? La preoccupazione era che i paradossi della logica potessero essere presenti anche altrove. I matematici del tempo iniziarono a chiedersi se il ragionamento e la matematica siano separati dalla logica. Il grande matematico del ’900 David Hilbert propose allora di dimostrare che il <strong>sistema formale</strong> dell’aritmetica fornito da Russell e Whitehead in Principia Mathematica fosse <strong>coerente</strong> (privo di contraddizioni) e <strong>completo</strong> (potesse produrre ogni possibile verità matematica) usando i metodi forniti dal sistema stesso. Quello che Hilbert sembra chiedere è che la matematica si tiri fuori da un pantano tirandosi per i capelli.</p>
|
||
<figure>
|
||
<img src="images/barone.jpg" alt="Il barone di Münchausen" /><figcaption>Il barone di Münchausen</figcaption>
|
||
</figure>
|
||
<p>In realtà Hilbert aveva previsto il possibile argomento circolare e aveva pensato perciò di aggirarlo dando una dimostrazione che usasse solo una parte ristretta dell’aritmetica, quella <em>finitista</em>: l’aritmetica elementare in cui solo ciò che è possibile esprimere tramite un numero finito di passaggi è valido. Sarebbe stato allora possibile fare questo in modo assolutamente intuitivo e certo: senza possibili contraddizioni o paradossi.</p>
|
||
<h3 id="i-teoremi-di-incompletezza"><span class="header-section-number">1.2.5</span> I teoremi di incompletezza</h3>
|
||
<figure>
|
||
<img src="images/godel.jpg" alt="Kurt Gödel a vent’anni" /><figcaption>Kurt Gödel a vent’anni</figcaption>
|
||
</figure>
|
||
<p>Nel 1931 tuttavia Kurt Gödel, divenuto in seguito uno dei più grandi logici di tutti i tempi, riuscì a dimostrare che un qualunque sistema formale che possa provare la coerenza di questa teoria è a sua volta potente come quest’ultima e quindi non è possibile aggirare l’argomento circolare rendendo vana ogni possibilità per una teoria di autogiustificarsi. Nonostante il risultato ottenuto da Gödel con i suoi due teoremi di incompletezza non vi è mai stata una fine dell’uso dei sistemi formali né tanto meno della ricerca di rigore che aveva animato all’inizio i matematici ma si è arrivati alla conclusione che <strong>le pretese di giustificare la matematica non sono razionali</strong>.</p>
|
||
<p>Vedremo quindi approfonditamente in cosa consistono i sistemi formali, come Gödel è arrivato a quanto abbiamo appena visto ed infine come e perché il formalismo è utilizzato ancora oggi.</p>
|
||
<h2 id="i-sistemi-formali"><span class="header-section-number">1.3</span> I Sistemi formali</h2>
|
||
<p>Esistono diverse definizioni di sistema formale: ne vedremo una in particolare ed utilizzeremo solamente quella da qui in avanti. Intuitivamente possiamo pensiamo ad un sistema formale in generale come ad un metodo rigoroso che permette di fornire una dimostrazioni ai teoremi.</p>
|
||
<h3 id="sistemi-di-produzione-di-post"><span class="header-section-number">1.3.1</span> Sistemi di produzione di Post</h3>
|
||
<p>I sistemi di produzione di Post o <em>sistemi canonici</em> sono un tipo di sistema formale ideato dal logico americano Emil Post negli anni ’20. Un sistema formale secondo questa definizione è costituito da un certo insieme di <strong>simboli</strong>, delle sequenze di simboli (<strong>stringhe</strong>) e delle <strong>regole</strong> per produrre nuove stringhe trasformando una stringa in un’altra tramite delle semplici manipolazioni di simboli, da questo il termine “di produzione”.</p>
|
||
<h3 id="miu"><span class="header-section-number">1.3.2</span> MIU</h3>
|
||
<p>Un esempio di semplice sistema formale di questo tipo è il sistema <strong>MIU</strong>, proposto da Hofstadter in “Gödel, Escher, Bach: An Ethernal Golden Braid”.</p>
|
||
<p>Il sistema ci sarà utile più volte, data la sua semplicità, per spiegare le caratteristiche dei sistemi formali, il loro utilizzo e la dimostrazione stessa del primo teorema di incompletezza.</p>
|
||
<h4 id="simboli"><span class="header-section-number">1.3.2.1</span> Simboli</h4>
|
||
<p>I simboli a disposizione sono le tre lettere: M, I, U.</p>
|
||
<h4 id="stringhe"><span class="header-section-number">1.3.2.2</span> Stringhe</h4>
|
||
<p>Sono stringhe del sistema MIU tutte le stringhe composte dei tre precedenti simboli. Esempi di stringhe MIU possono essere: MIU, MU, M, IMUUIUIUM, UMI, MIIIIII</p>
|
||
<h4 id="regole"><span class="header-section-number">1.3.2.3</span> Regole</h4>
|
||
<p>Le regole che possiamo utilizzare sono le seguenti:</p>
|
||
<ol type="1">
|
||
<li>Ad una stringa che termina con il simbolo <em>I</em> si può posporre il simbolo <em>U</em>. Per esempio la stringa <em>MII</em> può essere trasformata in <em>MIIU</em>.</li>
|
||
<li>Una stringa del tipo <em>Mx</em>, dove x indica una qualunque sequenza, può essere trasformata in <em>Mxx</em>. Cioè è possibile raddoppiarla. Per esempio <em>MIIU</em> può diventare <em>MIIUIIU</em>.</li>
|
||
<li>La sequenza <em>III</em> in una stringa, in una posizione qualunque, può essere sostituita con <em>U</em>. Per esempio <em>MIUIIIUI</em> diventa <em>MIUUI</em>.</li>
|
||
<li>La sequenza <em>UU</em> in una posizione qualunque in una stringa può essere cancellata. Per esempio <em>MIUUIU</em> diventa <em>MIIU</em>.</li>
|
||
</ol>
|
||
<p>Usando la notazione di Post possiamo enunciare così le regole:</p>
|
||
<ol type="1">
|
||
<li><span class="math inline">\(xI \to xIU\)</span></li>
|
||
<li><span class="math inline">\(Mx \to Mxx\)</span></li>
|
||
<li><span class="math inline">\(xIIIy \to xUy\)</span></li>
|
||
<li><span class="math inline">\(xUUy \to xy\)</span></li>
|
||
</ol>
|
||
<p>Da notare che la freccia va in una direzione sola. Le stringhe <strong>non</strong> sono intercambiabili.</p>
|
||
<h4 id="derivazione"><span class="header-section-number">1.3.2.4</span> Derivazione</h4>
|
||
<p>In questo sistema abbiamo a disposizione una sola stringa di partenza (<strong>assioma</strong>): <em>MI</em>. Applicando le regole di produzione a <em>MI</em> possiamo produrre tante nuove stringhe, infinite per la precisione.</p>
|
||
<p>Per esempio si può ottenere la stringa <em>MUIUI</em> in questo modo</p>
|
||
<table>
|
||
<thead>
|
||
<tr class="header">
|
||
<th style="text-align: left;">stringa</th>
|
||
<th style="text-align: left;">regola applicata</th>
|
||
</tr>
|
||
</thead>
|
||
<tbody>
|
||
<tr class="odd">
|
||
<td style="text-align: left;">1. MI</td>
|
||
<td style="text-align: left;">assioma</td>
|
||
</tr>
|
||
<tr class="even">
|
||
<td style="text-align: left;">2. MII</td>
|
||
<td style="text-align: left;">regola 2 con x=I</td>
|
||
</tr>
|
||
<tr class="odd">
|
||
<td style="text-align: left;">3. MIIII</td>
|
||
<td style="text-align: left;">regola 2 con x=II</td>
|
||
</tr>
|
||
<tr class="even">
|
||
<td style="text-align: left;">4. MUI</td>
|
||
<td style="text-align: left;">regola 3 con x=M e y=I</td>
|
||
</tr>
|
||
<tr class="odd">
|
||
<td style="text-align: left;">5. MUIUI</td>
|
||
<td style="text-align: left;">regola 2 con x=UI</td>
|
||
</tr>
|
||
</tbody>
|
||
</table>
|
||
<p>La sequenza di passaggi compiuti per ottenere una stringa si dice derivazione o <strong>dimostrazione</strong> di tale stringa. Poiché abbiamo dimostrato che possibile produrre questa stringa possiamo dire che <em>MUIUI</em> è un <strong>teorema</strong> del sistema MIU (lo sono anche gli intermedi <em>MII</em>, <em>MUI</em>…).</p>
|
||
<h3 id="procedure-di-decisione"><span class="header-section-number">1.3.3</span> Procedure di decisione</h3>
|
||
<p>In un sistema formale è possibile fare una prima distinzione fra tutte le possibili stringhe: stringhe <strong>ben formate</strong> e non. Le prime sono valide secondo le definizioni del sistema, le ultime invece non lo sono e vengono perciò definite “non sensate”.</p>
|
||
<p>Nel sistema MIU sono ben formate tutte le stringhe che contengono M,I e U: per esempio <em>IUIUM</em> o <em>MII</em> sono ben formate mentre <em>EII</em> non lo è.</p>
|
||
<p>Tra le stringhe ben formate possiamo individuare quali sono teoremi. Per esempio <em>MUIUI</em> è un teorema in quanto siamo stati in grado di derivarlo.</p>
|
||
<h4 id="è-possibile-stabilire-se-una-stringa-è-un-teorema"><span class="header-section-number">1.3.3.1</span> È possibile stabilire se una stringa è un teorema?</h4>
|
||
<p>Un <strong>criterio</strong> può essere questo: partendo dagli assiomi applichiamo tutte le possibile regole ottenendo nuovi teoremi che mettiamo da parte. Ripetiamo il processo su questi ultimi ottenendo altri nuovi teoremi e così via in modo da essere certi che tutti i teoremi saranno prima o poi ottenuti tra cui la stringa in questione. Se non la otteniamo significa perciò che non è un teorema.</p>
|
||
<p>Questo criterio però presuppone che si abbia un tempo potenzialmente infinito a disposizione per la verifica, il che non è molto ragionevole. Se un criterio di questo tipo richiede invece un tempo accettabile, se non immediato, viene detto <strong>procedura di decisione</strong></p>
|
||
<p>In un sistema formale esiste sempre almeno una procedura di decisione che è quella per riconoscere gli assiomi. In alcuni sistemi infatti esistono infiniti assiomi e non è possibile indicarli tutti: si procede quindi definendo una procedura di decisione per gli assiomi. Per i teoremi invece questa non esiste necessariamente.</p>
|
||
<h4 id="problema"><span class="header-section-number">1.3.3.2</span> Problema</h4>
|
||
<p>Questo sistema è stato pensato per essere un rompicapo: il problema posto è <strong>“<em>MU</em> è un teorema del sistema MIU?”</strong> Cioè se è possibile ottenere <em>MU</em> applicando ripetutamente le quattro regole partendo da <em>MI</em>.</p>
|
||
<p>Osservando bene le regole deduciamo che nessuna di essa modifica né il numero né la posizione delle <em>M</em> nelle stringhe. Quindi tutte le stringhe che possono essere prodotte, per l’assioma <em>MI</em>, iniziano inevitabilmente per <em>M</em>. Questo ci permette di scartare le stringhe come <em>IUIM</em> ma non <em>MU</em> che potrebbe essere ancora producibile.</p>
|
||
<p>Allo stesso modo osserviamo che il numero di <em>I</em> è lasciato invariato dalla regola 1 e 4, nella regola 2 viene sempre raddoppiato e nella regola 3 diminuito di 3. Poiché partiamo da <em>MI</em>, che contiene una <em>I</em>, possiamo ottenere stringhe con <span class="math inline">\(2^n\)</span> o <span class="math inline">\(2^n-3m\)</span> <em>I</em>, con <span class="math inline">\(n\)</span> il numero di applicazioni della regola 2 e <span class="math inline">\(m\)</span> della regola 3.</p>
|
||
<p>In <em>MU</em> il numero di <em>I</em> è zero: per eliminare tutte le <em>I</em> dovremmo avere <span class="math inline">\(2^n-3m=3x\)</span> che non ammette alcuna soluzione: non è possibile ottenere un multiplo di 3 sottraendo 3 da una potenza di 2.</p>
|
||
<p>La soluzione è quindi <strong>no</strong>: non è possibile ottenere <em>MU</em>.</p>
|
||
<h3 id="pq"><span class="header-section-number">1.3.4</span> pq•</h3>
|
||
<p>Il sistema pq• è un altro semplice sistema formale come MIU a cui tuttavia è possibile dare un’interpretazione che risulta familiare (in realtà anche più di una).</p>
|
||
<h4 id="simboli-1"><span class="header-section-number">1.3.4.1</span> Simboli</h4>
|
||
<p>Come risulta già chiaro dal nome i simboli consentiti dal sistema sono: p, q, •</p>
|
||
<h4 id="assiomi"><span class="header-section-number">1.3.4.2</span> Assiomi</h4>
|
||
<p>pq• ammette infiniti assiomi. Per caratterizzarli si utilizza la seguente definizione (una procedura di decisione):<br />
|
||
sono assiomi del sistema pq• tutte le stringhe del tipo <span class="math inline">\(x\)</span>p•q<span class="math inline">\(x\)</span>• dove <span class="math inline">\(x\)</span> rappresenta una stringa qualunque di “•”.</p>
|
||
<h4 id="regola"><span class="header-section-number">1.3.4.3</span> Regola</h4>
|
||
<p>pq• ha una sola regola di produzione:</p>
|
||
<ol type="1">
|
||
<li>se <span class="math inline">\(x\)</span>p<span class="math inline">\(y\)</span>q<span class="math inline">\(z\)</span> è un teorema allora anche <span class="math inline">\(x\)</span>p<span class="math inline">\(y\)</span>•q<span class="math inline">\(z\)</span>• è un teorema</li>
|
||
</ol>
|
||
<p>dove <span class="math inline">\(x\)</span>,<span class="math inline">\(y\)</span>,<span class="math inline">\(z\)</span> sono stringhe di “•” di lunghezza qualsiasi.</p>
|
||
<p>Prendiamo per esempio la stringa ••p•q••• (è un assioma infatti ha forma xp•qx•) e applichiamo la regola per ottenere: ••p••q••••. Di nuovo e si ottiene: ••p•••q•••••. Partendo invece da •••p•q•••• (altro assioma) produciamo •••p••q•••••, •••p•••q•••••• e così via.</p>
|
||
<h4 id="procedura-di-decisione"><span class="header-section-number">1.3.4.4</span> Procedura di decisione</h4>
|
||
<p>A differenza del precedente sistema MIU in cui a seconda della regola si produce una stringa più lunga o più corta della precedente si nota subito che nel sistema pq• si ricavano teoremi via via <strong>più lunghi</strong>. Questa caratteristica determina l’<strong>esistenza</strong> di una <strong>procedura di decisione</strong> per i propri teoremi.</p>
|
||
<p>A questo punto la procedura di decisione di pq• dovrebbe essere già stata individuata. È la seguente:<br />
|
||
<span class="math inline">\(x\)</span>p<span class="math inline">\(y\)</span>q<span class="math inline">\(z\)</span> è un teorema del sistema pq• se e solo se il numero di “•” in <span class="math inline">\(z\)</span> è uguale alla somma del numeri di “•” in <span class="math inline">\(x\)</span> e in <span class="math inline">\(y\)</span></p>
|
||
<p>Se indichiamo la lunghezza di una stringa x di “•” con <span class="math inline">\(\sharp x\)</span> allora possiamo riscrivere il criterio così:<br />
|
||
<span class="math inline">\(x\)</span>p<span class="math inline">\(y\)</span>q<span class="math inline">\(z\)</span> è un teorema del sistema pq• se e solo se <span class="math inline">\(\sharp x+\sharp y=\sharp z\)</span></p>
|
||
<h3 id="isomorfismo"><span class="header-section-number">1.3.5</span> Isomorfismo</h3>
|
||
<p>Il sistema pq• ha una proprietà particolare: produce solo teoremi che soddisfano i criteri dell’<strong>addizione</strong>. Possiamo interpretare il teorema “•••p••q•••••” come “3 più 2 uguale 5”. In generale xpyqz come <span class="math inline">\(x+y=z\)</span>. Non ha caso “p” è stato scelto perchè il suo suono ricorda “plus”e “q” “equals”. Questa relazione tra teoremi pq• e addizioni è un <em>isomorfismo</em>. Un isomorfismo è una particolare trasformazione tra strutture complesse in cui le relazioni interne tra le parti sono preservate.</p>
|
||
<h3 id="interpretazione-e-significato"><span class="header-section-number">1.3.6</span> Interpretazione e significato</h3>
|
||
<p>L’isomorfismo quindi causa l’acquisizione di un <strong>significato</strong> da parte dei simboli del sistema:</p>
|
||
<table>
|
||
<thead>
|
||
<tr class="header">
|
||
<th style="text-align: left;">simbolo</th>
|
||
<th style="text-align: left;">significato</th>
|
||
</tr>
|
||
</thead>
|
||
<tbody>
|
||
<tr class="odd">
|
||
<td style="text-align: left;">p</td>
|
||
<td style="text-align: left;">più</td>
|
||
</tr>
|
||
<tr class="even">
|
||
<td style="text-align: left;">q</td>
|
||
<td style="text-align: left;">è uguale a</td>
|
||
</tr>
|
||
<tr class="odd">
|
||
<td style="text-align: left;">•</td>
|
||
<td style="text-align: left;">uno</td>
|
||
</tr>
|
||
<tr class="even">
|
||
<td style="text-align: left;">••</td>
|
||
<td style="text-align: left;">due</td>
|
||
</tr>
|
||
<tr class="odd">
|
||
<td style="text-align: left;">•••</td>
|
||
<td style="text-align: left;">tre</td>
|
||
</tr>
|
||
<tr class="even">
|
||
<td style="text-align: left;">…</td>
|
||
<td style="text-align: left;">…</td>
|
||
</tr>
|
||
</tbody>
|
||
</table>
|
||
<p>Se potessimo leggere ogni possibile teorema pq in questo modo troveremmo che la sua interpretazione risulta immancabilmente vera. A questo punto viene naturale fare anche il processo contrario: cioè si potrebbe pensare che poichè “cinque più due è uguale a sette” la stringa “•••••p••q•••••••” è un teorema. Certamente lo è però questa non è una giustificazione valida infatti possiamo dire che una stringa è un teorema soltanto dopo averne trovato la dimostrazione seguendo le regole del sistema formale.</p>
|
||
<p>È ovviamente possibile uscire dalle costrizioni del sistema per ragionarci su, dare significati ai simboli, e quant’altro ma non ci è poi concesso di utilizzare nuove regole o considerare teoremi alcune stringhe sulla base delle interpretazioni trovate. Il significato conferito al sistema formale deve sempre rimanere <strong>passivo</strong>. Infatti si può trovare più di un isomorfismo e le interpretazioni da questi prodotte potrebbero essere anche contrastanti: per questo motivo bisogna sempre attenersi alle regole del sistema formale (<strong>requisito di formalità</strong>).</p>
|
||
<p>Un’altra interpretazione che risulta altrettanto valida del sistema pq è questa:</p>
|
||
<table>
|
||
<thead>
|
||
<tr class="header">
|
||
<th style="text-align: left;">simbolo</th>
|
||
<th style="text-align: left;">significato</th>
|
||
</tr>
|
||
</thead>
|
||
<tbody>
|
||
<tr class="odd">
|
||
<td style="text-align: left;">p</td>
|
||
<td style="text-align: left;">è uguale a</td>
|
||
</tr>
|
||
<tr class="even">
|
||
<td style="text-align: left;">q</td>
|
||
<td style="text-align: left;">sottratto da</td>
|
||
</tr>
|
||
<tr class="odd">
|
||
<td style="text-align: left;">•</td>
|
||
<td style="text-align: left;">uno</td>
|
||
</tr>
|
||
<tr class="even">
|
||
<td style="text-align: left;">••</td>
|
||
<td style="text-align: left;">due</td>
|
||
</tr>
|
||
<tr class="odd">
|
||
<td style="text-align: left;">•••</td>
|
||
<td style="text-align: left;">tre</td>
|
||
</tr>
|
||
<tr class="even">
|
||
<td style="text-align: left;">…</td>
|
||
<td style="text-align: left;">…</td>
|
||
</tr>
|
||
</tbody>
|
||
</table>
|
||
<p>•••p••q••••• <span class="math inline">\(\leftrightarrow\)</span> “tre è uguale a due sottratto da cinque”</p>
|
||
<h3 id="coerenza-e-completezza"><span class="header-section-number">1.3.7</span> Coerenza e Completezza</h3>
|
||
<p>Una volta introdotta un’interpretazione per un sistema formale si può parlare di <strong>coerenza</strong> del sistema. Esistono due diverse definizioni di coerenza:</p>
|
||
<ol type="1">
|
||
<li>Un sistema formale si dice <em>coerente</em> se ogni teorema una volta interpretato risulta essere una proposizione vera.</li>
|
||
<li>Un sistema formale si dice <em>coerente</em> se tutti i suoi teoremi una volta interpretati sono tra loro compatibili.</li>
|
||
</ol>
|
||
<p>Nel primo caso si parla di <strong>coerenza esterna</strong>. Il sistema formale risulta coerente se le affermazioni prodotte dalla sua interpretazione ottengono un riscontro nel mondo esterno, la nostra realtà. La seconda definizione è invece quella di <strong>coerenza interna</strong>. Questa coerenza non necessita di una conformità con il nostro mondo bensì con un qualunque possibile mondo immaginabile. È sufficiente che non vi siano <strong>contraddizioni</strong> al suo interno: non possono esistere per esempio due teoremi che si escludano a vicenda o uno che affermi l’opposto dell’altro. Sarà sempre intesa quest’ultimo tipo quando si parlerà di coerenza più avanti.</p>
|
||
<p>Complementare al concetto di coerenza vi è quello di <strong>completezza</strong> del sistema formale. È così definito:<br />
|
||
Un sistema formale è <em>completo</em> se qualunque proposizione vera <strong>esprimibile</strong> in una stringa ben formata risulta essere un teorema.</p>
|
||
<p>È importante evidenziare il fatto che debba essere esprimibile nei termini del sistema formale: il sistema si occupa solo di un certo ambito della realtà di sua competenza ed è completo se è in grado in esprimerla nella sua interezza. Altrimenti solo un sistema formale “universale” potrebbe essere completo.</p>
|
||
<p>Anche in questa definizione il valore di verità è riferibile alla nostra realtà ma si utilizzerà il termine “completo” sempre rispetto a mondo immaginabile coerente.</p>
|
||
<p>È fondamentale capire che entrambi i concetti di coerenza e completezza non sono proprietà del sistema formale ma <strong>relativi</strong> alla sua interpretazione: nonostante il sistema acquisisca inevitabilmente un significato passivo rimane comunque un insieme di regole di manipolazione di simboli di per sé senza senso.</p>
|
||
<h3 id="calcolo-proposizionale"><span class="header-section-number">1.3.8</span> Calcolo proposizionale</h3>
|
||
<p>Il calcolo proposizionale è una formalizzazione della <strong>logica delle proposizioni</strong>. Ovvero lo studio del valore di verità delle proposizioni complesse.</p>
|
||
<h4 id="simboli-2"><span class="header-section-number">1.3.8.1</span> Simboli</h4>
|
||
<p>Sono consentite le tre lettere <span class="math inline">\(P\)</span>, <span class="math inline">\(Q\)</span>, <span class="math inline">\(R\)</span>, i simboli <span class="math inline">\(\wedge\)</span>, <span class="math inline">\(\vee\)</span>, <span class="math inline">\(\rangle\)</span>, <span class="math inline">\(\langle\)</span>, <span class="math inline">\(\sim\)</span>, <span class="math inline">\(\supset\)</span> e l’apice <span class="math inline">\('\)</span>.</p>
|
||
<p>Le seguenti stringhe sono ben formate:</p>
|
||
<ol type="1">
|
||
<li><span class="math inline">\(\sim x\)</span></li>
|
||
<li><span class="math inline">\(\langle x\wedge y\rangle\)</span></li>
|
||
<li><span class="math inline">\(\langle x\vee y\rangle\)</span></li>
|
||
<li><span class="math inline">\(\langle x\supset y\rangle\)</span></li>
|
||
</ol>
|
||
<p>dove <span class="math inline">\(x\)</span> e <span class="math inline">\(y\)</span> sono stringhe ben formate.</p>
|
||
<p><span class="math inline">\(P\)</span>, <span class="math inline">\(Q\)</span> e <span class="math inline">\(R\)</span> sono detti <strong>atomi</strong> e corrispondono a proposizioni semplici. Si possono formare ulteriori atomi aggiungendo degli apici a quest’ultimi. Per esempio <span class="math inline">\(P'\)</span>, <span class="math inline">\(Q''\)</span>, <span class="math inline">\(R'\)</span>. Tutti gli atomi sono stringhe ben formate.</p>
|
||
<h4 id="regole-di-produzione"><span class="header-section-number">1.3.8.2</span> Regole di produzione</h4>
|
||
<ol type="1">
|
||
<li><strong>regola dell’unione</strong>: se <span class="math inline">\(x\)</span> e <span class="math inline">\(y\)</span> sono teoremi allora <span class="math inline">\(\langle x \wedge y \rangle\)</span> è un teorema</li>
|
||
<li><strong>regola della separazione</strong>: se <span class="math inline">\(\langle x \wedge y \rangle\)</span> è un teorema allora entrambi <span class="math inline">\(x\)</span> e <span class="math inline">\(y\)</span> sono teoremi.</li>
|
||
<li><strong>regola della doppia tilde</strong>: la stringa “<span class="math inline">\(\sim\sim\)</span>” può essere cancellata ovunque occorre in un teorema oppure inserita per ottenere una stringa ben formata.</li>
|
||
<li><strong>regola della fantasia</strong>: se è possibile dimostrare <span class="math inline">\(y\)</span> assumendo che <span class="math inline">\(x\)</span> sia un teorema allora <span class="math inline">\(\langle x \supset y \rangle\)</span> è un teorema.</li>
|
||
<li><strong>regola del riporto</strong>: all’interno di una <em>fantasia</em> si può utilizzare qualunque teorema del livello immediatamente esterno.</li>
|
||
<li><strong>regola del distaccamento</strong>: se sia <em><span class="math inline">\(x\)</span></em> che <span class="math inline">\(\langle x \supset y\rangle\)</span> sono teoremi allora <em><span class="math inline">\(y\)</span></em> è un teorema.</li>
|
||
<li><strong>regola dell’antitesi</strong>: <span class="math inline">\(\langle x\supset y\rangle\)</span> e <span class="math inline">\(\langle\sim y\supset\sim x\rangle\)</span> sono intercambiabili.</li>
|
||
<li><strong>regola di De Morgan</strong>: <span class="math inline">\(\langle \sim x\wedge\sim y\rangle\)</span> e <span class="math inline">\(\sim\langle x\vee y\rangle\)</span> sono intercambiabili.</li>
|
||
<li><strong>regola di Switcheroo</strong> (modus tollendo ponens): <span class="math inline">\(\langle x\vee y\rangle\)</span> e <span class="math inline">\(\langle\sim x\supset y\rangle\)</span> sono intercambiabili.</li>
|
||
</ol>
|
||
<h4 id="assiomi-1"><span class="header-section-number">1.3.8.3</span> Assiomi</h4>
|
||
<p>La particolarità di questo sistema è di non avere alcun assioma. A differenza dei sistemi precedenti, come pq il cui significato risiede quasi esclusivamente negli assiomi scelti, nel calcolo proposizionale sono le regole che determinano tutto il sistema. Come è possibile allora produrre teoremi se non abbiamo niente da cui partire? Semplice: usiamo la regola della <strong>fantasia</strong> che permette di produrre teoremi “dal nulla”.</p>
|
||
<h4 id="dimostrazioni"><span class="header-section-number">1.3.8.4</span> Dimostrazioni</h4>
|
||
<p>Ecco un esempio di dimostrazione:</p>
|
||
<p><span class="math display">\[
|
||
\begin{aligned}
|
||
1. \quad&[\\
|
||
2. \quad&\quad \langle P\vee Q\rangle &&\text{premessa}\\
|
||
3. \quad&\quad \langle \sim P\supset Q\rangle &&\text{Switcheroo}\\
|
||
4. \quad&\quad \langle\sim Q\supset\sim\sim P\rangle &&\text{antitesi}\\
|
||
5. \quad&\quad \langle\sim Q\supset P\rangle &&\text{doppia tilde}\\
|
||
6. \quad&\quad \langle Q\vee P\rangle &&\text{Switcheroo}\\
|
||
7. \quad&]\\
|
||
8. \quad& \langle\langle P\vee Q\rangle\supset\langle Q\vee P\rangle\rangle &&\text{fantasia}\\
|
||
\end{aligned}
|
||
\]</span></p>
|
||
<p>Le parentesi quadrate segnano l’inizio e il termine della fantasia. In questo caso partendo dalla premessa che <span class="math inline">\(\langle P\vee Q\rangle\)</span> sia un teorema abbiamo ottenuto che anche <span class="math inline">\(\langle Q\vee P\rangle\)</span> è un teorema. Quindi una volta fuori dalla fantasia possiamo riassumere il processo compiuto nel nuovo <strong>teorema</strong> <span class="math inline">\(\langle\langle P\vee Q\rangle\supset\langle Q\vee P\rangle\rangle\)</span> .</p>
|
||
<p>È possibile aprire più fantasie una nell’altra ed usare la regola del riporto così:</p>
|
||
<p><span class="math display">\[
|
||
\begin{aligned}
|
||
1. \quad&[\\
|
||
2. \quad&\quad \langle P\wedge\sim P\rangle &&\text{premessa}\\
|
||
3. \quad&\quad \sim P &&\text{separazione}\\
|
||
4. \quad&\quad P &&\text{separazione}\\
|
||
5. \quad&\quad [\\
|
||
6. \quad&\quad\quad \sim Q &&\text{premessa}\\
|
||
7. \quad&\quad\quad P &&\text{riporto da riga 3}\\
|
||
8. \quad&\quad\quad \sim\sim P &&\text{doppia tilde}\\
|
||
9. \quad&\quad ]\\
|
||
10. \quad&\quad \langle\sim Q\supset\sim\sim P\rangle &&\text{fantasia}\\
|
||
11. \quad&\quad \langle\sim P\supset\sim\sim Q\rangle &&\text{antitesi}\\
|
||
12. \quad&\quad \langle\sim P\supset Q\rangle &&\text{doppia tilde}\\
|
||
13. \quad&\quad Q &&\text{distaccamento riga 3 e 12}\\
|
||
14. \quad&]\\
|
||
15. \quad& \langle\langle P\wedge\sim P\rangle\supset Q\rangle &&\text{fantasia}\\
|
||
\end{aligned}
|
||
\]</span></p>
|
||
<h4 id="interpretazione-del-sistema"><span class="header-section-number">1.3.8.5</span> Interpretazione del sistema</h4>
|
||
<p>Come già detto questo sistema formalizza la logica proposizionale. Di seguito vi è un elenco di simboli e alcuni teoremi con le loro interpretazioni anche se a questo punto saranno già chiare:</p>
|
||
<table style="width:93%;">
|
||
<colgroup>
|
||
<col style="width: 45%" />
|
||
<col style="width: 47%" />
|
||
</colgroup>
|
||
<thead>
|
||
<tr class="header">
|
||
<th style="text-align: center;">sistema</th>
|
||
<th style="text-align: left;">significato</th>
|
||
</tr>
|
||
</thead>
|
||
<tbody>
|
||
<tr class="odd">
|
||
<td style="text-align: center;"><span class="math inline">\(P\)</span>, <span class="math inline">\(Q\)</span>, <span class="math inline">\(R\)</span></td>
|
||
<td style="text-align: left;">proposizioni semplici</td>
|
||
</tr>
|
||
<tr class="even">
|
||
<td style="text-align: center;"><span class="math inline">\(\sim\)</span></td>
|
||
<td style="text-align: left;">non, negazione</td>
|
||
</tr>
|
||
<tr class="odd">
|
||
<td style="text-align: center;"><span class="math inline">\(\wedge\)</span></td>
|
||
<td style="text-align: left;">e, congiunzione</td>
|
||
</tr>
|
||
<tr class="even">
|
||
<td style="text-align: center;"><span class="math inline">\(\vee\)</span></td>
|
||
<td style="text-align: left;">o, disgiunzione</td>
|
||
</tr>
|
||
<tr class="odd">
|
||
<td style="text-align: center;"><span class="math inline">\(\supset\)</span></td>
|
||
<td style="text-align: left;">implica che</td>
|
||
</tr>
|
||
<tr class="even">
|
||
<td style="text-align: center;"><span class="math inline">\(\sim\langle P\wedge Q\rangle\)</span></td>
|
||
<td style="text-align: left;">non P e Q</td>
|
||
</tr>
|
||
<tr class="odd">
|
||
<td style="text-align: center;"><span class="math inline">\(\sim\langle\langle P\vee\sim Q\rangle\supset\langle\sim P\vee Q\rangle\rangle\)</span></td>
|
||
<td style="text-align: left;">non P o non Q implica non P o Q</td>
|
||
</tr>
|
||
</tbody>
|
||
</table>
|
||
<p>Il teorema prima dimostrato <span class="math inline">\(\langle\langle P\wedge\sim P\rangle\supset Q\rangle\)</span> è il noto <strong>principio di esplosione</strong> o <em>ex falso quodlibet</em>; che è interpretabile come “P o non P implica Q”. Se ammettiamo che sia P sia sua negazione siano vere dobbiamo ammetere anche che qualunque altra proposizione Q sia vera! Aver dimostrato questo teorema significa che nel calcolo proposizionale non esistono contraddizioni. Se non fosse così sarebbe possibile dimostrare qualunque cosa e l’intero sistema (la sua interpretazione in realtà) cadrebbe. Dobbiamo sempre ricordare che per il sistema formale <span class="math inline">\(\langle\langle P \wedge\sim P\rangle\supset Q\rangle\)</span> è una semplice sequenza di simboli trasformabile secondo delle regole ed di per sè priva d’ogni significato.</p>
|
||
<h4 id="coerenza-e-metateorie"><span class="header-section-number">1.3.8.6</span> Coerenza e metateorie</h4>
|
||
<p>È sufficiente il fatto appena scoperto ad assicurarci che il calcolo proposizionale sia coerente? Assolutamente no, sarebbe necessaria una prova dell’assenza di contraddizioni. Tuttavia questa prova non è possibile tramite una derivazione di qualche teorema all’interno del calcolo proposizionale. C’è una grossa differenza tra una <em>derivazione</em> di un teorema e una <em>prova</em> (dimostrazione). Una dimostrazione è qualcosa di <strong>informale</strong>, una costruzione umana, mentre una derivazione è un’applicazione <strong>meccanica</strong> di regole.</p>
|
||
<p>Per dimostrare la coerenza e la completezza del calcolo proposizionale è necessario uscire dal sistema ed elaborare una teoria sulla teoria. Questa è una <strong>metateoria</strong> costituita da teoremi che parlano di teoremi. Anche una volta elaborata la metateoria e ottenuta la dimostrazione cercata chi ci assicura però che la metateoria sia coerente e completa? È necessaria una prova del fatto che va cercata in una <strong>metametateoria</strong> e di quest’ultima allora? Anche formalizzando le metateorie non si risolverebbe il problema: ad un certo punto è necessario arrendersi ed accettare il fatto che questa teoria sia coerente nella sua interpretazione in quanto evidente. In fondo dubitare del calcolo proposizionale è dubitare della logica stessa e della propria mente.</p>
|
||
<h3 id="teoria-dei-numeri-tipografica-tnt"><span class="header-section-number">1.3.9</span> Teoria dei Numeri Tipografica (TNT)</h3>
|
||
<p>Per poter scrivere la proposizione usata da Gödel nel primo teorema di incompletezza è necessario un sistema capace di esprimere le <strong>proprietà dei numeri</strong> oltre che a quelle della logica proposizionale. Per questo useremo una formalizzazione della teoria dei numeri: la teoria dei numeri tipografica (<strong>TNT</strong> in breve)</p>
|
||
<p>Questo sistema formale utilizza tutti i precedenti simboli e regole del calcolo proposizionale oltre a definire i numeri naturali e le loro proprietà tramite tramite <strong>l’arimetica di Peano</strong>.</p>
|
||
<h4 id="numerali"><span class="header-section-number">1.3.9.1</span> Numerali</h4>
|
||
<p>I numerali sono stringhe che rappresentano numeri. A differenza del familiare sistema posizionale e delle cifre indoarabe si ricorre soltanto a due simboli: <span class="math inline">\(S\)</span> e <span class="math inline">\(O\)</span> per poter scrivere qualsiasi numero naturale.</p>
|
||
<table>
|
||
<thead>
|
||
<tr class="header">
|
||
<th style="text-align: center;">Numerale</th>
|
||
<th style="text-align: center;">Interpretazione</th>
|
||
</tr>
|
||
</thead>
|
||
<tbody>
|
||
<tr class="odd">
|
||
<td style="text-align: center;"><span class="math inline">\(O\)</span></td>
|
||
<td style="text-align: center;">zero</td>
|
||
</tr>
|
||
<tr class="even">
|
||
<td style="text-align: center;"><span class="math inline">\(SO\)</span></td>
|
||
<td style="text-align: center;">uno</td>
|
||
</tr>
|
||
<tr class="odd">
|
||
<td style="text-align: center;"><span class="math inline">\(SSO\)</span></td>
|
||
<td style="text-align: center;">due</td>
|
||
</tr>
|
||
<tr class="even">
|
||
<td style="text-align: center;"><span class="math inline">\(SSSO\)</span></td>
|
||
<td style="text-align: center;">tre</td>
|
||
</tr>
|
||
<tr class="odd">
|
||
<td style="text-align: center;">…</td>
|
||
<td style="text-align: center;">…</td>
|
||
</tr>
|
||
</tbody>
|
||
</table>
|
||
<p><span class="math inline">\(O\)</span> rappresenta quindi il numero zero e <span class="math inline">\(S\)</span> e il numero successore di un qualunque numero.</p>
|
||
<h4 id="variabili"><span class="header-section-number">1.3.9.2</span> Variabili</h4>
|
||
<p>Per riferirsi a numeri non specifici in una formula si utilizzano delle variabili. Utilizziamo una lettera <span class="math inline">\(a\)</span> e come nel calcolo proposizionale l’apice <span class="math inline">\('\)</span> per produrre nuove variabili <span class="math inline">\(a'\)</span>, <span class="math inline">\(a''\)</span>, <span class="math inline">\(a'''\)</span>, …</p>
|
||
<h4 id="operazioni"><span class="header-section-number">1.3.9.3</span> Operazioni</h4>
|
||
<p>Le operazioni consentite sono l’addizione e la moltiplicazione. Si utilizzano i normali simboli <span class="math inline">\(+\)</span> e <span class="math inline">\(\times\)</span> e le parentesi tonde. Per esempio <span class="math inline">\(((a\times a'') + a')\)</span>.</p>
|
||
<p>Sono entrambe operazioni binarie e sono sempre necessarie le parentesi: non è possibile scrivere <span class="math inline">\(a+a'+a''\)</span> come si fa comunemente.</p>
|
||
<h4 id="formule-aperte-e-formule-chiuse"><span class="header-section-number">1.3.9.4</span> Formule aperte e formule chiuse</h4>
|
||
<p>Non tutte le stringhe TNT sono proposizioni. Le stringhe la cui interpretazione non ha un valore di verità sono dette <strong>formule aperte</strong> o predicati, in quanto sono analoghe ad una frase senza soggetto, e contengono sempre <strong>varibili libere</strong>.</p>
|
||
<p>Per esempio la stringa <span class="math inline">\(SSO=Sa\)</span> in cui <span class="math inline">\(a\)</span> è la variabile libera. La stringa fa un’ affermazione su un generico numero <span class="math inline">\(a\)</span> e non è né vera né falsa: esprime semplicemente una proprietà.</p>
|
||
<p>Una variabile è <strong>legata</strong> quando invece è associata ad un quantificatore. In questo caso la stringa fa un’affermazione sull’esistenza di un numero o una proprietà valida per tutti i numeri e si dice <strong>formula chiusa</strong>. Esistono due quantificatori: quello universale <span class="math inline">\(\forall\)</span> (pronunciato “per ogni”) e quello esistenziale <span class="math inline">\(\exists\)</span> (pronunciato “esiste almeno”).</p>
|
||
<p>Per esempio nella stringa <span class="math inline">\(\forall a:Sa=O\)</span> la variabile <span class="math inline">\(a\)</span> è legata e la stringa è sicuramente falsa.</p>
|
||
<h4 id="formule-ben-formate"><span class="header-section-number">1.3.9.5</span> Formule ben formate</h4>
|
||
<p>Ecco le regole per stabilire se una formula è ben formata:</p>
|
||
<ol type="1">
|
||
<li><strong>Numerali</strong>: sono formule ben formate tutti i numerali</li>
|
||
<li><strong>Variabili</strong>: sono formule ben formate tutte le variabili</li>
|
||
<li><strong>Termini</strong>:
|
||
<ul>
|
||
<li>sono termini tutti i numerali e le variabili</li>
|
||
<li>tutti i termini preceduti da <span class="math inline">\(S\)</span> sono termini</li>
|
||
<li><span class="math inline">\((x\times y)\)</span> e <span class="math inline">\((x+y)\)</span> sono termini se <span class="math inline">\(x\)</span> e <span class="math inline">\(y\)</span> sono termini</li>
|
||
<li>tutti i <strong>termini</strong> sono formule <strong>ben formate</strong></li>
|
||
</ul></li>
|
||
<li><strong>Atomi</strong>: se x e y sono termini allora x = y è un atomo</li>
|
||
<li><strong>Molecole</strong>: se x e y sono formule ben formate sono ben formate:
|
||
<ul>
|
||
<li><span class="math inline">\(\sim x\)</span></li>
|
||
<li><span class="math inline">\(\langle x\wedge y\rangle\)</span></li>
|
||
<li><span class="math inline">\(\langle x\vee y\rangle\)</span></li>
|
||
<li><span class="math inline">\(\langle x\supset y\rangle\)</span></li>
|
||
</ul></li>
|
||
<li><strong>Quantificazioni</strong>: sono ben formate le formule: <span class="math inline">\(\forall v:x\)</span> e <span class="math inline">\(\exists v:x\)</span> con <span class="math inline">\(v\)</span> una variabile e <span class="math inline">\(x\)</span> una formula aperte in cui compare <span class="math inline">\(v\)</span> come variabile libera</li>
|
||
</ol>
|
||
<h4 id="assiomi-2"><span class="header-section-number">1.3.9.6</span> Assiomi</h4>
|
||
<p>TNT definisce 5 assiomi:</p>
|
||
<ol type="1">
|
||
<li><span class="math inline">\(\forall a:\sim Sa=O\)</span></li>
|
||
<li><span class="math inline">\(\forall a:(a+O)=a\)</span></li>
|
||
<li><span class="math inline">\(\forall a:\forall a':(a+Sa')=S(a+a')\)</span></li>
|
||
<li><span class="math inline">\(\forall a:(a\times O)=O\)</span></li>
|
||
<li><span class="math inline">\(\forall a:\forall a':(a\times Sa')=((a\times a')+a)\)</span></li>
|
||
</ol>
|
||
<p>L’assioma 1 afferma che non esiste un numero il cui successore è zero: cioè non esistono numeri minori di zero. Gli assiomi 2 e 4 affermano che lo zero è l’elemento neutro dell’addizione e assorbente della moltiplicazione. Gli assiomi 3 e 5 affermano le proprietà dell’addizione e della moltiplicazione.</p>
|
||
<p>Da notare che il primo assioma è uno dei postulati di Peano.</p>
|
||
<h4 id="regole-di-produzione-1"><span class="header-section-number">1.3.9.7</span> Regole di produzione</h4>
|
||
<ol type="1">
|
||
<li><strong>regola della specificazione</strong>: sia <span class="math inline">\(x\)</span> una formula in cui compare la variabile <span class="math inline">\(v\)</span> e <span class="math inline">\(t\)</span> un termine in cui non compaiono variabile legate in <span class="math inline">\(x\)</span>: se <span class="math inline">\(\forall v:x\)</span> è un teorema allora <span class="math inline">\(x\)</span> e tutte le formule ottenute sostituendo <span class="math inline">\(v\)</span> con <span class="math inline">\(t\)</span> sono teoremi</li>
|
||
<li><strong>regola della generalizzazione</strong>: se <span class="math inline">\(x\)</span> è un teorema in cui compare la variabile libera <span class="math inline">\(v\)</span> allora <span class="math inline">\(\forall v:x\)</span> è un teorema. (Attenzione: <strong>Non</strong> è possibile generalizzare una variabile libera posta come premessa in una fantasia)</li>
|
||
<li><strong>regola dello scambio</strong>: sia <span class="math inline">\(v\)</span> una variabile: le stringhe “<span class="math inline">\(\forall v:\sim\)</span>” e “<span class="math inline">\(\sim\exists v:\)</span>” sono intercambiabili ovunque occorrano in un teorema</li>
|
||
<li><strong>regola dell’esistenza</strong>: sia <span class="math inline">\(x\)</span> un teorema in cui è presente un termine <span class="math inline">\(t\)</span> e <span class="math inline">\(y\)</span> la formula ottenuta sostituendo <span class="math inline">\(t\)</span> con una variabile <span class="math inline">\(v\)</span>: <span class="math inline">\(\exists v:y\)</span> è un teorema</li>
|
||
<li><strong>regole dell’uguaglianza</strong>:
|
||
<ol type="1">
|
||
<li>simmetria: siano <span class="math inline">\(t\)</span> e <span class="math inline">\(s\)</span> due termini: se <span class="math inline">\(t=s\)</span> è un teorema allora <span class="math inline">\(s=t\)</span> è un teorema</li>
|
||
<li>transitività: siano <span class="math inline">\(t\)</span>, <span class="math inline">\(s\)</span>, <span class="math inline">\(r\)</span> tre termini: se <span class="math inline">\(t=s\)</span> e <span class="math inline">\(s=r\)</span> sono teoremi allora <span class="math inline">\(t=r\)</span> è un teorema</li>
|
||
</ol></li>
|
||
<li><strong>regole del successore</strong>:
|
||
<ol type="1">
|
||
<li>siano <span class="math inline">\(t\)</span> e <span class="math inline">\(s\)</span> due termini: se <span class="math inline">\(t=s\)</span> è un teorema allora <span class="math inline">\(Ss=St\)</span> è un teorema</li>
|
||
<li>siano <span class="math inline">\(t\)</span> e <span class="math inline">\(s\)</span> due termini: se <span class="math inline">\(Ss=St\)</span> è un teorema allora <span class="math inline">\(s=t\)</span> è un teorema</li>
|
||
</ol></li>
|
||
</ol>
|
||
<h4 id="esempi-di-proposizioni-e-dimostrazioni"><span class="header-section-number">1.3.9.8</span> Esempi di proposizioni e dimostrazioni:</h4>
|
||
<p>La proposizione “esiste un numero pari diverso da zero” è traducibile in TNT come</p>
|
||
<p><span class="math display">\[\exists a:\exists a':Sa=(Sa'\times SSO)\]</span></p>
|
||
<p>Usando <span class="math inline">\(S\)</span> è possibile fissare un valore minimo che <span class="math inline">\(a\)</span> può assumere: in questo caso <span class="math inline">\(SSO\)</span>. Usiamo lo stesso metodo per scrivere “undici è un numero primo”:</p>
|
||
<p><span class="math display">\[\sim\exists a:\exists a': (SSa\times SSa')=SSSSSSSSSSSO\]</span></p>
|
||
<p>Una più complessa “non è possibile separare un cubo in due cubi”: <span class="math display">\[
|
||
\forall a:\forall a':\forall a'': \sim (((a\times a)\times a) + ((a'\times a')\times a')) = ((a''\times a'')\times a'')
|
||
\]</span></p>
|
||
<p>Il sistema è sicuramente molto espressivo tuttavia diventa già molto complicato scrivere proposizioni come “a è una potenza di b” per la mancanza di operatori.</p>
|
||
<p>Di seguito la dimostrazione di <span class="math inline">\(1 + 1 = 2\)</span>:</p>
|
||
<p><span class="math display">\[
|
||
\begin{aligned}
|
||
&1.\ \forall a:\forall a':(a+Sa')=S(a+a') &&\text{assioma 3} \\
|
||
&2.\ \forall a':(SSO+Sa')=S(SSO+a') &&\text{specificazione: $a$, $SSO$} \\
|
||
&3.\ (SSO+SO)=S(SSO+SO) &&\text{specificazione: $a'$, $SO$} \\
|
||
&4.\ \forall a:S(a+O)=a &&\text{assioma 2} \\
|
||
&5.\ S(SO+O)=SO &&\text{specificazione: $a$, $SO$} \\
|
||
&6.\ SS(SO+O)=SSO &&\text{successore 1} \\
|
||
&7.\ (SO+SO)=SSO &&\text{transitività linee 3, 6} \\
|
||
\end{aligned}
|
||
\]</span></p>
|
||
<h4 id="omega-incompletezza-e-omega-incoerenza"><span class="header-section-number">1.3.9.9</span> <span class="math inline">\(\omega\)</span>-incompletezza e <span class="math inline">\(\omega\)</span>-incoerenza</h4>
|
||
<p>Una cosa particolare di questa sistema è che spesso capita di poter dimostrare una serie di teoremi ma non è possibile dimostrare la formula che li riassume tutti. Per esempio potremmo riuscire a dimostrare:</p>
|
||
<p><span class="math display">\[ (SO\times SO)=SO \]</span> <span class="math display">\[ (SSO\times SO)=SSO \]</span> <span class="math display">\[ (SSSO\times SO)=SSSO \]</span> <span class="math display">\[ (SSSSO\times SO)=SSSSO \]</span> <span class="math display">\[ \cdots \]</span></p>
|
||
<p>ma non la formula <span class="math inline">\(\forall a:(a \times SO)=a\)</span>. Per questo fatto la teoria si dice <strong><span class="math inline">\(\omega\)</span>-incompleta</strong>.</p>
|
||
<p>In generale un sistema formale <span class="math inline">\(S\)</span> si dice <span class="math inline">\(\omega\)</span>-incompleto quando esiste una formula <span class="math inline">\(\varphi(x)\)</span> tale che <span class="math inline">\(\varphi(n)\)</span> è un teorema in <span class="math inline">\(S\)</span> per ogni numero naturale <span class="math inline">\(n\)</span> ma <span class="math inline">\(\forall x:\varphi(x)\)</span> non è un teorema. Con <span class="math inline">\(\omega\)</span> infatti si intende la totalità dei numeri naturali.</p>
|
||
<p>Se non dovesse essere un teorema neanche la sua negazione <span class="math inline">\(\forall x:\sim\varphi(x)\)</span> <span class="math inline">\(\varphi\)</span> è indecidibile nel sistema <span class="math inline">\(S\)</span> che si dice allora <strong><span class="math inline">\(\omega\)</span>-incoerente</strong>.</p>
|
||
<p>L’<span class="math inline">\(\omega\)</span>-incoerenza è essenzialmente diversa dall’incoerenza: solo una delle due formule tra <span class="math inline">\(\varphi(n)\)</span> e <span class="math inline">\(\sim\varphi(n)\)</span> risulta un teorema per tutti gli <span class="math inline">\(n\)</span> tuttavia nella loro espressione generica potremmo accettarle entrambe come assiomi. Per fare ciò dobbiamo ammettere che esistano alcuni numeri che verificano <span class="math inline">\(\sim\varphi\)</span> ma poichè <span class="math inline">\(\varphi\)</span> ci dice che nessun numero naturale ha tale la proprietà questi numeri non possono essere dei numeri normali.</p>
|
||
<p>Se ammettiamo l’esistenza di tali numeri, noti come numeri naturali generalizzati o <strong>soprannaturali</strong>, entriamo nel campo della <strong>teoria dei numeri non-standard</strong> in cui <span class="math inline">\(\sim\varphi\)</span> è un teorema mentre <span class="math inline">\(\varphi\)</span> è una proprietà di alcuni numeri (i naturali) e non c’è una contraddizione.</p>
|
||
<h4 id="induzione"><span class="header-section-number">1.3.9.10</span> Induzione</h4>
|
||
<p>Per rendere <span class="math inline">\(TNT\)</span> <span class="math inline">\(\omega\)</span>-completa è necessario un meccanismo che ci permetta di rendere <span class="math inline">\(\varphi\)</span> un teorema. Per fare ciò formalizziamo il quinto postulato di Peano noto come <strong>principio di induzione</strong> matematico e lo aggiungiamo alle regole. Quindi:</p>
|
||
<ol start="7" type="1">
|
||
<li><strong>regola di induzione</strong>: sia <span class="math inline">\(v\)</span> una variabile e <span class="math inline">\(\varphi(v)\)</span> una formula aperta che contiene <span class="math inline">\(v\)</span> libera: se <span class="math inline">\(\forall v:\langle \varphi(v)\supset \varphi(Sv)\rangle\)</span> e <span class="math inline">\(\varphi(O)\)</span> sono teoremi allora <span class="math inline">\(\forall v:\varphi(v)\)</span> è un teorema</li>
|
||
</ol>
|
||
<h3 id="conclusioni"><span class="header-section-number">1.3.10</span> Conclusioni</h3>
|
||
<p>Con quest’ultima regola TNT è diventata <span class="math inline">\(\omega\)</span>-completa ed equivalente al sistema formale di <em>Principia Mathematica</em>. Se TNT fosse anche completa ogni possibile proposizione vera della teoria dei numeri esprimibile in in una formula sarebbe un teorema e potremmo determinare meccanicamente tramite una procedura di decisione se una formula qualunque è un teorema. In altre parole i matematici rimarrebbero senza lavoro perché basterebbe una macchina che enumeri tutti i teoremi TNT e controlli che la stringa fornitale sia presente o no. Vediamo allora perché questo non è accaduto.</p>
|
||
<h2 id="la-dimostrazione"><span class="header-section-number">1.4</span> La dimostrazione</h2>
|
||
<p>Ora che abbiamo definito il sistema formale e le basi che ci servono possiamo passare a capire la dimostrazione del primo teorema di incompletezza in cui Gödel ha dimostrato che se una teoria è coerente non può essere anche completa.</p>
|
||
<h4 id="antinomie"><span class="header-section-number">1.4.0.1</span> Antinomie</h4>
|
||
<p>L’idea centrale è quella di costruire un’<strong>antinomia</strong> all’interno di TNT: cioè una proposizione che non può essere né vera né falsa, una contraddizione. In campo linguistico per esempio c’è l’antichissimo <em>Paradosso di Epimenide</em> o <strong>paradosso del mentitore</strong>: “Epimenide di Creta afferma che tutti i cretesi mentono” o la versione moderna “questa frase è falsa”. Se la frase fosse vera essa afferma di essere falsa portando ad una contraddizione, se fosse invece falsa di conseguenza l’opposto di quanto dice deve essere vero cioè che è vera portando ad una <strong>contraddizione</strong>.</p>
|
||
<p>Quindi, ironia della sorte, il principio scoperto da Russell con la sua antinomia nella teoria degli insiemi è lo stesso che è stato usato contro di lui da Gödel per far cadere <em>Principia Mathematica</em>.</p>
|
||
<p>Queste antinomie si basano sul fatto che il soggetto del predicato è la frase stessa: si dice che sono <strong>autoreferenziali</strong>. Per ottenere lo stesso effetto nella teoria dei numeri Gödel ha prima dovuto trovare un modo per scrivere formule TNT che parlano di formule TNT e poi ha potuto scrivere la famosa <strong>formula G</strong>, il cui significato è “<strong>G</strong> non è un teorema TNT”.</p>
|
||
<h3 id="numero-di-gödel"><span class="header-section-number">1.4.1</span> Numero di Gödel</h3>
|
||
<p>È possibile includere ogni problema di un qualunque sistema formale nella teoria dei numeri tramite uno speciale isomorfismo scoperto da Gödel noto come gödellizzazione o <em>numero di Gödel</em>.</p>
|
||
<h4 id="miu-1"><span class="header-section-number">1.4.1.1</span> MIU</h4>
|
||
<p>Si può per esempio compiere questa operazione con il problema “<em>MU</em> è un teorema del sistema MIU?”.</p>
|
||
<p>Il primo passo è <strong>associare un numero</strong>, scelto arbitrariamente, ad ogni simbolo del sistema.</p>
|
||
<p><span class="math display">\[
|
||
\begin{aligned}
|
||
M &\leftrightarrow 3 \\
|
||
I &\leftrightarrow 1 \\
|
||
U &\leftrightarrow 0 \\
|
||
\end{aligned}
|
||
\]</span></p>
|
||
<p>Così facendo si è creata una <strong>corrispondenza</strong> tra le <strong>stringhe</strong> MIU e <strong>numeri</strong>:</p>
|
||
<p><span class="math display">\[
|
||
\begin{aligned}
|
||
MIU &\leftrightarrow 310 \\
|
||
MU &\leftrightarrow 30 \\
|
||
MIII &\leftrightarrow 3111 \\
|
||
MIUI &\leftrightarrow 3101 \\
|
||
&\cdots
|
||
\end{aligned}
|
||
\]</span></p>
|
||
<p>Allo stesso modo possiamo riscrivere la <strong>regole</strong> di produzione tipografiche (Stringa <span class="math inline">\(\mapsto\)</span> Stringa) come regole aritmetiche, cioè <strong>funzioni</strong> (Numero <span class="math inline">\(\mapsto\)</span> Numero):</p>
|
||
<ol type="1">
|
||
<li><p>La regola “Se <span class="math inline">\(xI\)</span> è un teorema allora lo è anche <span class="math inline">\(xIU\)</span>” diventa “se <span class="math inline">\(10m+1\)</span> è un numero MIU lo è anche <span class="math inline">\(10(10m+1)\)</span>”. Scegliendo <span class="math inline">\(U \leftrightarrow 0\)</span> questa regola è una semplice moltiplicazione per 10.</p></li>
|
||
<li><p>“Se <span class="math inline">\(Mx\)</span> è un teorema allora lo è anche <span class="math inline">\(Mxx\)</span>” diventa “Se <span class="math inline">\(3 \cdot 10^m+n\)</span> è un numero MIU allora lo è anche <span class="math inline">\(10^m\cdot(3\cdot 10^m+n)+n\)</span>”</p></li>
|
||
<li><p>Questa regola è un po’ più complicata: “Se <span class="math inline">\(xIIIy\)</span> è un teorema allora lo è anche <span class="math inline">\(xUy\)</span>” viene riscritta come “Se <span class="math inline">\(k\cdot10^{m+3}+111\cdot 10^m+n\)</span> è un numero MIU lo è anche <span class="math inline">\(k\cdot 10^{m+1}+n\)</span>”.</p></li>
|
||
<li><p>In maniera simile alla precedente “Se <span class="math inline">\(xUUy\)</span> è un teorema allora lo è anche <span class="math inline">\(xy\)</span>” diventa “Se <span class="math inline">\(k\cdot 10^{m+2}+n\)</span> è un numero MIU allora lo è anche <span class="math inline">\(k\cdot 10^m+n\)</span>”.</p></li>
|
||
</ol>
|
||
<p>dove <span class="math inline">\(m\)</span> e <span class="math inline">\(k\)</span> sono numeri naturali qualsiasi e <span class="math inline">\(n<10^m\)</span></p>
|
||
<p>Il problema diventa quindi: <strong>“30 è un numero MIU?”</strong>. Poiché l’essere un numero MIU è una proprietà dei numeri definita in modo ricorsivo (tramite l’applicazione di funzioni) è sicuramente possibile <strong>esprimere in TNT</strong> (sebbene in modo incredibilmente complicato) questa proposizione tramite una formula e verificare se essa sia un teorema o meno. Possiamo quindi concludere che:<br />
|
||
<strong>ogni problema in un sistema formale può essere trasformato in un proposizione nella teoria dei numeri e convertito in una formula TNT.</strong></p>
|
||
<h4 id="tnt"><span class="header-section-number">1.4.1.2</span> TNT</h4>
|
||
<p>Poiché abbiamo detto che questa proprietà vale per qualsiasi sistema formale deve valere anche per TNT stessa. Possiamo quindi convertire un problema come il chiedersi se una formula TNT sia un teorema in una formula TNT e a sua volta quest’ultima e così via. Significa che TNT contiene stringhe che parlano di se stessa: il sistema si morde la coda!</p>
|
||
<p>Questa non è una particolarità di TNT ma avviene per tutti i sistemi abbastanza complessi da definire l’aritmetica.</p>
|
||
<p>Iniziamo come per MIU ad associare dei numeri ai simboli del sistema:</p>
|
||
<p><span class="math display">\[
|
||
\begin{aligned}
|
||
O &\leftrightarrow 10 \\
|
||
S &\leftrightarrow 11 \\
|
||
= &\leftrightarrow 12 \\
|
||
+ &\leftrightarrow 13 \\
|
||
\times &\leftrightarrow 14 \\
|
||
( &\leftrightarrow 15 \\
|
||
) &\leftrightarrow 16 \\
|
||
\langle &\leftrightarrow 17 \\
|
||
\rangle &\leftrightarrow 18 \\
|
||
a &\leftrightarrow 19 \\
|
||
' &\leftrightarrow 20 \\
|
||
\wedge &\leftrightarrow 21 \\
|
||
\vee &\leftrightarrow 22 \\
|
||
\supset &\leftrightarrow 23 \\
|
||
\sim &\leftrightarrow 24 \\
|
||
\exists &\leftrightarrow 25 \\
|
||
\forall &\leftrightarrow 26 \\
|
||
: &\leftrightarrow 27 \\
|
||
\end{aligned}
|
||
\]</span></p>
|
||
<p>Possiamo quindi associare un numero anche ad ogni formula. Per esempio sostituendo ogni simbolo della formula <span class="math inline">\(\sim\exists a:\exists a': \langle \sim a=a' \supset Sa=Sa'\rangle\)</span> si ottiene il numero:</p>
|
||
<p><span class="math display">\[24251927251920271724191219202311191211192018\]</span></p>
|
||
<p>Questo numero è il <em>numero di Gödel</em> della formula.</p>
|
||
<p>Possiamo trasformare tutte le regole di produzione in funzioni aritmetiche esattamente come per MIU tuttavia sarebbe un’ operazione veramente onerosa e di poco interesse: sappiamo già che esse svolgono esattamente lo stesso compito soltanto in maniera differente.</p>
|
||
<h4 id="coppie-dimostrative"><span class="header-section-number">1.4.1.3</span> Coppie dimostrative</h4>
|
||
<p>Nonostante tutto questo non siamo ancora in grado di esprimere in una formula “<span class="math inline">\(x\)</span> è un teorema”: per fare questo dobbiamo definire il concetto di <strong>coppia dimostrativa</strong>.</p>
|
||
<p>Sappiamo che una stringa in qualunque sistema formale è un teorema se è possibile derivarla utilizzando le regole di produzione, cioè se esiste una sua dimostrazione: una <strong>sequenza di stringhe e regole utilizzate</strong>. Poiché abbiamo associato numeri e funzioni corrispondenti a stringhe e regole tipografiche possiamo allo stesso modo creare un’ ulteriore relazione che consiste tra numeri e dimostrazioni. Una <strong>dimostrazione</strong> corrisponde semplicemente al <strong>numero</strong> di Gödel della stringa ottenuta concatenando tutti i suoi passaggi.</p>
|
||
<p>Una coppia dimostrativa è una coppia di numeri di cui uno è la dimostrazione dell’altro secondo la definizione precedente. Questa è quindi una <strong>proprietà</strong> di alcuni numeri e perciò può essere espressa da una formula aperta in TNT. Indichiamo tale formula con la notazione <span class="math inline">\(P(a,a')\)</span> dove <span class="math inline">\(a\)</span> e <span class="math inline">\(a'\)</span> sono le due variabili libere.</p>
|
||
<p>Per esempio per la dimostrazione di <span class="math inline">\(1+1=2\)</span> <span class="math display">\[
|
||
\begin{aligned}
|
||
&1.\ \forall a:\forall a':(a+Sa')=S(a+a') && 261927261920271519131119201612111519\dots \\
|
||
&2.\ \forall a':(SSO+Sa')=S(SSO+a') && 261920271511111013111920161211151111\dots \\
|
||
&3.\ (SSO+SO)=S(SSO+SO) && 151111101311101612111511111013111016 \\
|
||
&4.\ \forall a:S(a+O)=a && 2619271115191310161219 \\
|
||
&5.\ S(SO+O)=SO && 11151110131016121110 \\
|
||
&6.\ SS(SO+O)=SSO && 111115111013101612111110 \\
|
||
&7.\ (SO+SO)=SSO && 1511101311101612111110 \\
|
||
\end{aligned}
|
||
\]</span></p>
|
||
<p>il mostruoso numero 2619272619202715191311<span class="math inline">\(\dots\)</span> e 1511101311101612111110 formano una coppia dimostrativa.</p>
|
||
<p>Possiamo finalmente scrivere <span class="math inline">\(\exists a':P(a',x)\)</span> dove <span class="math inline">\(x\)</span> è il numerale di un numero di Gödel: interpretabile come <strong>“esiste una dimostrazione di <span class="math inline">\(x\)</span>”</strong>.</p>
|
||
<h4 id="sostituzione"><span class="header-section-number">1.4.1.4</span> Sostituzione</h4>
|
||
<p>Nel precedente esempio vediamo che a sinistra avviene il solito processo di applicazione di regole e trasformazione di stringhe e allo stesso modo avviene un analogo processo tra numeri e funzioni a destra. Nel primo passo della dimostrazione in particolare avviene la sostituzione di una variabile con un numerale per ottenere una nuova formula:</p>
|
||
<ol type="1">
|
||
<li><span class="math inline">\(\forall a:\forall a':(a+Sa')=S(a+a')\)</span></li>
|
||
<li><span class="math inline">\(SSO\)</span></li>
|
||
<li><span class="math inline">\(\forall a:\forall a':(SSO+Sa')=S(SSO+a')\)</span></li>
|
||
</ol>
|
||
<p>Lo stesso avviene secondo qualche procedimento aritmetico tra i corrispettivi numeri di Gödel:</p>
|
||
<ol type="1">
|
||
<li>26192726192027151913111920161211151913192016</li>
|
||
<li>111110</li>
|
||
<li>2619272619202715111110131119201612111511111013192016</li>
|
||
</ol>
|
||
<p>Possiamo dire, come per le coppie dimostrative, che questi tre numeri hanno la proprietà di essere una <strong>sostituzione</strong>. Poiché TNT può rappresentare ogni primitiva ricorsiva deve esistere una formula aperta anche per questa proprietà che chiamiamo <span class="math inline">\(S(a,a',a'')\)</span>.</p>
|
||
<h3 id="paradosso-di-quine"><span class="header-section-number">1.4.2</span> Paradosso di Quine</h3>
|
||
<p>Con il numero di Gödel abbiamo lo strumento che ci permette di scrivere una formula TNT che parla di altre formule o teoremi TNT. Tuttavia per poter scrivere la formula <strong>G</strong> ci serve un modo per fare che la formula <strong>parli di sé</strong>. Sfortunatamente questo non è fattibile in modo diretto: una formula che contenga il proprio numero di Gödel sarebbe di lunghezza infinita e quindi impossibile da costruire. È però possibile ottenere lo stesso risultato tramite un’<strong>autoreferenza indiretta</strong> scoperta dal logico americano Quine. Il paradosso da lui proposto è la seguente espressione:</p>
|
||
<p>“produce una falsità quando preceduto dalla sua citazione” produce una falsità quando preceduto dalla sua citazione.</p>
|
||
<p>Per capire dove sta la contraddizione analizziamo i componenti della frase.</p>
|
||
<h4 id="predicati"><span class="header-section-number">1.4.2.1</span> Predicati</h4>
|
||
<p>Un <strong>predicato</strong> è una frase in cui è assente il <strong>soggetto</strong>. Non è una proposizione completa e non ha un valore di verità (esattamente come le formule aperte in TNT). Per esempio “_____ è una città” a cui aggiungendo un soggetto es. “Roma” otteniamo “Roma è una città” che è un’affermazione vera.</p>
|
||
<p>Quindi un predicato diventa un’<strong>affermazione</strong> quando gli viene preposto un soggetto qualunque, fra i tanti possibili vi è anche il predicato stesso. È possibile quindi avere la frase: “è una città” è una città, che è un’affermazione sicuramente falsa (quando indichiamo tra virgolette una parola ci riferiamo alla parola stessa non al suo significato). Chiamiamo in generale <em>quine</em> un frase ottenuta ponendo come soggetto di un predicato la citazione del predicato stesso.</p>
|
||
<h4 id="autoreferenza-indiretta"><span class="header-section-number">1.4.2.2</span> Autoreferenza indiretta</h4>
|
||
<p>Nella frase proposta da Quine abbiamo un predicato che chiamiamo <strong>P</strong>:</p>
|
||
<p><span class="math display">\[\text{\_\_\_\_\_ produce una falsità quando preceduto dalla sua citazione.}\]</span></p>
|
||
<p>e la proposizione che è il quine di <strong>P</strong> che chiamiamo <strong>Q</strong>:</p>
|
||
<p>“produce una falsità quando preceduto dalla sua citazione” produce una falsità quando preceduto dalla sua citazione.</p>
|
||
<p><strong>P</strong> si riferisce al suo soggetto che ora è <strong>Q</strong> e la frase <strong>Q</strong> si riferisce al suo soggetto cioè <strong>P</strong>. Quindi <strong>Q</strong> tramite <strong>P</strong> parla di se stessa! E non finisce qui perché dicendo “produce una falsità” essa afferma anche di essere falsa. È quindi una proposizione equivalente a “Questa frase è falsa” ma che non usa direttamente un pronome per parlare di sé: proprio quello che dovrà essere la formula <strong>G</strong>.</p>
|
||
<h4 id="quine-aritmetico"><span class="header-section-number">1.4.2.3</span> Quine aritmetico</h4>
|
||
<p>L’analogo in TNT di porre come soggetto di un predicato il predicato stesso è <strong>sostituire</strong> in una variabile libera di una formula aperta il numero di Gödel (il suo numerale per la precisione) della formula stessa.</p>
|
||
<p>Per esempio prendiamo la formula aperta <span class="math inline">\(a=(SSO\times a')\)</span> e calcoliamone il numero di Gödel: 19121511111014192016. Il quine di tale formula è quindi</p>
|
||
<p><span class="math display">\[
|
||
\begin{aligned}
|
||
\underbrace{SSS\dots O}=(SSO\times a') \\
|
||
_{\text{19121511111014192016 volte }S}\qquad\qquad&
|
||
\end{aligned}
|
||
\]</span></p>
|
||
<p>Questa nuova formula ha ovviamente un numero (mostruosamente enorme) di Gödel:</p>
|
||
<p><span class="math display">\[
|
||
\begin{aligned}
|
||
\underbrace{11111111\dots}10121511111014192016 \\
|
||
_{38243022222028380000\text{ volte }1}\qquad\qquad\qquad\qquad&
|
||
\end{aligned}
|
||
\]</span></p>
|
||
<p>Il <strong>quine aritmetico</strong> è quindi una proprietà tra una coppia di numeri ed è un particolare tipo di sostituzione <span class="math inline">\(S(a,a,a')\)</span> dove <span class="math inline">\(a\)</span> è il numero di Gödel originale e <span class="math inline">\(a'\)</span> quello del quine. Indichiamo allora la formula TNT per questa proprietà come <span class="math inline">\(Q(a,a')\)</span>.</p>
|
||
<h3 id="g"><span class="header-section-number">1.4.3</span> G</h3>
|
||
<p>Finalmente abbiamo tutto il necessario per costruire la formula <strong>G</strong>. Partiamo dalla seguente proposizione:</p>
|
||
<p><span class="math display">\[\sim\exists a:\exists a':\langle P(a,a')\wedge Q(a'',a')\rangle\]</span></p>
|
||
<p>Chiamiamo <span class="math inline">\(g\)</span> il suo numero di Gödel. Dell’espansione decimale di <span class="math inline">\(g\)</span> conosciamo la parte iniziale, il centro e il termine:</p>
|
||
<p><span class="math display">\[g=242519272519202717\dots 21\dots 18\]</span></p>
|
||
<p><strong>G</strong> è il quine di tale proposizione che otteniamo quindi inserendo il numerale di <span class="math inline">\(g\)</span> al posto di <span class="math inline">\(a''\)</span>. Ed ecco <strong>G</strong>:</p>
|
||
<p><span class="math display">\[
|
||
\sim\exists a:\exists a':\langle P(a,a')\wedge Q(\underbrace{SSS\dots O}_\text{$g$ volte $S$},a')\rangle\]</span></p>
|
||
<h4 id="interpretazione"><span class="header-section-number">1.4.3.1</span> Interpretazione</h4>
|
||
<p>Una sua traduzione letterale è “Non esistono due numeri <span class="math inline">\(a\)</span> e <span class="math inline">\(a'\)</span> tali da formare una coppia dimostrativa di cui uno è il quine di <span class="math inline">\(g\)</span>”. Cioè non esiste alcun numero che forma una coppia dimostrativa con il quine di <span class="math inline">\(g\)</span>. Poiché il quine di <span class="math inline">\(g\)</span> è la formula stessa questo significa che <strong>G</strong> afferma che <strong>G</strong> <strong>non è dimostrabile</strong>.</p>
|
||
<p>A questo punto dobbiamo chiederci quali sono le implicazioni. Se <strong>G</strong> fosse un teorema significa che la sua interpretazione deve essere vera. Ma <strong>G</strong> afferma di non essere un teorema portando quindi ad una contraddizione. Allora significa che <strong>G</strong> non è un teorema. In questo caso non ci sarebbe alcuna contraddizione ma <strong>G</strong> sarebbe una proposizione vera che non è un teorema e quindi TNT non è più un sistema formale completo. Inoltre la formula <strong>G</strong> è indecidibile in TNT in quanto né <strong>G</strong> né <span class="math inline">\(\sim\)</span><strong>G</strong> possono essere teoremi.</p>
|
||
<h4 id="conclusione"><span class="header-section-number">1.4.3.2</span> Conclusione</h4>
|
||
<p>Ne concludiamo che <strong>qualsiasi sistema formale sufficientemente complesso da contenere l’aritmetica se è coerente non può essere anche completo</strong>. Esisterà sempre qualche verità che non può essere provata all’interno del sistema.</p>
|
||
<h4 id="osservazione"><span class="header-section-number">1.4.3.3</span> Osservazione</h4>
|
||
<p>Abbiamo visto che <strong>G</strong> è indecidibile: come TNT senza regola d’induzione anche questa formulazione della teoria dei numeri è <span class="math inline">\(\omega\)</span>-incoerente. Potremmo allora decidere di prendere <strong>G</strong> come assioma per eliminare il problema ma la teoria rimarrebbe ugualmente <span class="math inline">\(\omega\)</span>-incoerente: nel momento in cui abbiamo assunto <strong>G</strong> come verità possiamo costruire una nuova formula <strong>G<span class="math inline">\('\)</span></strong> anch’essa indecidibile. Se invece decidessimo di aggiungere <span class="math inline">\(\sim\)</span><strong>G</strong> agli assiomi ammetteremmo l’esistenza di alcuni numeri che “formano una dimostrativa con il quine di <span class="math inline">\(g\)</span>”. Questi numeri sarebbero dei numeri soprannaturali. In ogni caso TNT rimane <span class="math inline">\(\omega\)</span>-incoerente.</p>
|
||
<h3 id="il-secondo-teorema"><span class="header-section-number">1.4.4</span> Il secondo teorema</h3>
|
||
<p>Il secondo teorema di incompletezza è un corollario del teorema appena dimostrato che riguarda invece la <strong>coerenza</strong>.</p>
|
||
<p>Proviamo a costruire la proposizione “TNT è coerente” all’interno di TNT. Dire che una teoria è coerente significa che non possono essere teoremi sia <span class="math inline">\(x\)</span> che <span class="math inline">\(\sim x\)</span>. Se fossero entrambi veri, per il calcolo proposizionale (principio di esplosione), tutte le formule ben formate sarebbero teoremi. Per provare che TNT è coerente basterebbe quindi trovare per un solo non-teorema la dimostrazione che effettivamente non è un teorema. Per esempio di <span class="math inline">\(\forall a:Sa=O\)</span>.</p>
|
||
<p>Possiamo quindi scrivere: <span class="math display">\[\sim\exists a:P(a, \underbrace{SS\dots O}_\text{$g$ volte $S$})\]</span></p>
|
||
<p>dove <span class="math inline">\(g=26192711191210\)</span> (numero di Gödel di <span class="math inline">\(\forall a:Sa=O\)</span>)</p>
|
||
<p>Gödel è riuscito a dimostrare che una proposizione come questa per essere un teorema TNT deve necessariamente essere incoerente: cioè TNT è coerente se e solo se è incoerente. Quindi per assurdo ha dimostrato che <strong>non è possibile dimostrare la coerenza di un sistema formale al suo interno</strong>.</p>
|
||
<h2 id="allegati"><span class="header-section-number">1.5</span> Allegati</h2>
|
||
<h3 id="miu.hs"><span class="header-section-number">1.5.1</span> MIU.hs</h3>
|
||
<p>Un programma haskell che implementa la procedura di decisione “non molto ragionevole” per i teoremi MIU:</p>
|
||
<div class="sourceCode"><pre class="sourceCode haskell"><code class="sourceCode haskell"><span class="kw">import </span><span class="dt">Text.Regex</span> (subRegex, mkRegex)
|
||
|
||
<span class="kw">type</span> <span class="dt">Theorem</span> <span class="fu">=</span> <span class="dt">String</span>
|
||
<span class="kw">type</span> <span class="dt">Rule</span> <span class="fu">=</span> <span class="dt">String</span> <span class="ot">-></span> <span class="dt">String</span>
|
||
|
||
<span class="ot">axiom ::</span> <span class="dt">String</span>
|
||
axiom <span class="fu">=</span> <span class="st">"MI"</span>
|
||
|
||
<span class="ot">rules ::</span> [<span class="dt">Rule</span>]
|
||
rules <span class="fu">=</span> map (uncurry rewrite) transform
|
||
<span class="kw">where</span>
|
||
rewrite <span class="fu">=</span> flip <span class="fu">.</span> subRegex <span class="fu">.</span> mkRegex
|
||
transform <span class="fu">=</span> [ (<span class="st">"I$"</span> , <span class="st">"IU"</span>)
|
||
, (<span class="st">"M(.+)"</span>, <span class="st">"M\\1\\1"</span>)
|
||
, (<span class="st">"III"</span> , <span class="st">"U"</span>)
|
||
, (<span class="st">"UU"</span> , <span class="st">""</span>) ]
|
||
|
||
<span class="ot">theorems ::</span> [<span class="dt">Theorem</span>]
|
||
theorems <span class="fu">=</span> concat (deriveFrom [axiom])
|
||
<span class="kw">where</span> deriveFrom <span class="fu">=</span> iterate (rules <span class="fu"><*></span>)
|
||
|
||
<span class="ot">isTheorem ::</span> <span class="dt">String</span> <span class="ot">-></span> <span class="dt">Bool</span>
|
||
isTheorem <span class="fu">=</span> (<span class="ot">`elem`</span> theorems)
|
||
|
||
<span class="ot">main ::</span> <span class="dt">IO</span> ()
|
||
main <span class="fu">=</span> print (isTheorem <span class="st">"MIIUIIU"</span>)</code></pre></div>
|
||
<h4 id="miu-derive.hs"><span class="header-section-number">1.5.1.1</span> MIU-derive.hs</h4>
|
||
<p>Un altro programma relativo al sistema MIU che produce tutte le possibili dimostrazioni, specificata una lunghezza massima, per una stringa:</p>
|
||
<div class="sourceCode"><pre class="sourceCode haskell"><code class="sourceCode haskell"><span class="kw">import </span><span class="dt">Control.Monad.State</span>
|
||
<span class="kw">import </span><span class="dt">System.Random</span>
|
||
<span class="kw">import </span><span class="dt">Text.Regex</span> (subRegex, mkRegex)
|
||
<span class="kw">import </span><span class="dt">Text.Printf</span> (printf)
|
||
<span class="kw">import </span><span class="dt">Data.List</span> (nub)
|
||
|
||
<span class="kw">type</span> <span class="dt">Theorem</span> <span class="fu">=</span> <span class="dt">String</span>
|
||
<span class="kw">type</span> <span class="dt">Rule</span> <span class="fu">=</span> <span class="dt">String</span>
|
||
<span class="kw">type</span> <span class="dt">Rand</span> <span class="fu">=</span> <span class="dt">State</span> <span class="dt">StdGen</span>
|
||
|
||
<span class="ot">axiom ::</span> <span class="dt">String</span>
|
||
axiom <span class="fu">=</span> <span class="st">"MI"</span>
|
||
|
||
<span class="ot">rules ::</span> [(<span class="dt">String</span>, <span class="dt">String</span> <span class="ot">-></span> <span class="dt">String</span>)]
|
||
rules <span class="fu">=</span> zip [<span class="st">"I"</span>, <span class="st">"II"</span>, <span class="st">"III"</span>, <span class="st">"IV"</span>] fs
|
||
<span class="kw">where</span>
|
||
fs <span class="fu">=</span> map (uncurry rewrite) transform
|
||
rewrite <span class="fu">=</span> flip <span class="fu">.</span> subRegex <span class="fu">.</span> mkRegex
|
||
transform <span class="fu">=</span> [ (<span class="st">"I$"</span> , <span class="st">"IU"</span>)
|
||
, (<span class="st">"M(.+)"</span>, <span class="st">"M\\1\\1"</span>)
|
||
, (<span class="st">"III"</span> , <span class="st">"U"</span>)
|
||
, (<span class="st">"UU"</span> , <span class="st">""</span>) ]
|
||
|
||
<span class="ot">step ::</span> (<span class="dt">Rule</span>, <span class="dt">Theorem</span>) <span class="ot">-></span> <span class="dt">String</span>
|
||
step <span class="fu">=</span> uncurry (printf <span class="st">" -%s-> %s"</span>)
|
||
|
||
<span class="ot">choice ::</span> [a] <span class="ot">-></span> <span class="dt">Rand</span> a
|
||
choice xs <span class="fu">=</span> (xs <span class="fu">!!</span>) <span class="fu"><$></span> (state <span class="fu">.</span> randomR) (<span class="dv">0</span>, length xs <span class="fu">-</span> <span class="dv">1</span>)
|
||
|
||
<span class="ot">derive ::</span> <span class="dt">Theorem</span> <span class="ot">-></span> <span class="dt">Rand</span> [(<span class="dt">Rule</span>, <span class="dt">Theorem</span>)]
|
||
derive t <span class="fu">=</span> produceFrom axiom <span class="kw">where</span>
|
||
produceFrom s
|
||
<span class="fu">|</span> s <span class="fu">==</span> t <span class="fu">=</span> return []
|
||
<span class="fu">|</span> otherwise <span class="fu">=</span> <span class="kw">do</span>
|
||
(name, next) <span class="ot"><-</span> fmap (<span class="fu">$</span>s) <span class="fu"><$></span> choice rules
|
||
<span class="kw">if</span> next <span class="fu">/=</span> s
|
||
<span class="kw">then</span> (<span class="fu">:</span>) (name, next) <span class="fu"><$></span> produceFrom next
|
||
<span class="kw">else</span> produceFrom s
|
||
|
||
<span class="ot">main ::</span> <span class="dt">IO</span> ()
|
||
main <span class="fu">=</span>
|
||
<span class="kw">let</span> target <span class="fu">=</span> <span class="st">"MIIUIIU"</span>
|
||
valid <span class="fu">=</span> (<span class="fu">==</span>target) <span class="fu">.</span> snd <span class="fu">.</span> last <span class="fu">.</span> take <span class="dv">20</span>
|
||
show' <span class="fu">=</span> putStrLn <span class="fu">.</span> (<span class="fu">++</span><span class="st">"\n"</span>) <span class="fu">.</span> (axiom <span class="fu">++</span>) <span class="fu">.</span> concatMap step
|
||
proof <span class="fu">=</span> evalState (derive target) <span class="fu">.</span> mkStdGen
|
||
<span class="kw">in</span> mapM_ show' <span class="fu">.</span> (nub <span class="fu">.</span> filter valid <span class="fu">.</span> map proof) <span class="fu">$</span> [<span class="dv">1</span><span class="fu">..</span><span class="dv">100</span>]</code></pre></div>
|
||
<h4 id="number.py"><span class="header-section-number">1.5.1.2</span> number.py</h4>
|
||
<p>Il programma python utilizzato per calcolare il numero di Gödel delle formule in questo documento</p>
|
||
<div class="sourceCode"><pre class="sourceCode python"><code class="sourceCode python"><span class="im">from</span> functools <span class="im">import</span> <span class="bu">reduce</span>
|
||
|
||
symbols <span class="op">=</span> [<span class="st">"O"</span>,<span class="st">"S"</span>,<span class="st">"="</span>,<span class="st">"+"</span>,<span class="st">"</span><span class="ch">\\</span><span class="st">times"</span>,<span class="st">"("</span>,<span class="st">")"</span>,
|
||
<span class="co">"\\langle"</span>,<span class="st">"</span><span class="ch">\\</span><span class="st">rangle"</span>,<span class="st">"a"</span>,<span class="st">"'"</span>,
|
||
<span class="co">"\\wedge"</span>,<span class="st">"</span><span class="ch">\\</span><span class="st">vee"</span>,<span class="st">"</span><span class="ch">\\</span><span class="st">supset"</span>,
|
||
<span class="co">"\\sim"</span>,<span class="st">"</span><span class="ch">\\</span><span class="st">exists"</span>,<span class="st">"</span><span class="ch">\\</span><span class="st">forall"</span>,<span class="st">":"</span>]
|
||
|
||
numbers <span class="op">=</span> <span class="bu">dict</span>(<span class="bu">zip</span>(symbols, <span class="bu">range</span>(<span class="dv">10</span>,<span class="dv">30</span>)))
|
||
|
||
g <span class="op">=</span> <span class="kw">lambda</span> r: (
|
||
<span class="bu">map</span>(<span class="kw">lambda</span> s:
|
||
<span class="bu">reduce</span>(<span class="kw">lambda</span> x, y:
|
||
x.replace(y, <span class="bu">str</span>(numbers[y])), <span class="bu">sorted</span>(numbers), s.replace(<span class="st">' '</span>,<span class="st">''</span>)
|
||
),r.split(<span class="st">'</span><span class="ch">\n</span><span class="st">'</span>)
|
||
)
|
||
)
|
||
|
||
a<span class="op">=</span><span class="vs">r"""</span>
|
||
<span class="vs">\forall a:\forall a':(a+Sa')=S(a+a')</span>
|
||
<span class="vs">\forall a':(SSO+Sa')=S(SSO+a')</span>
|
||
<span class="vs">(SSO+SO)=S(SSO+SO)</span>
|
||
<span class="vs">\forall a:S(a+O)=a</span>
|
||
<span class="vs">S(SO+O)=SO</span>
|
||
<span class="vs">SS(SO+O)=SSO</span>
|
||
<span class="vs">(SO+SO)=SSO</span>
|
||
<span class="st">"""</span>
|
||
|
||
<span class="bu">print</span>(<span class="op">*</span>g(a), sep<span class="op">=</span><span class="st">'</span><span class="ch">\n</span><span class="st">'</span>)</code></pre></div>
|
||
<h2 id="bibliografia"><span class="header-section-number">1.6</span> Bibliografia</h2>
|
||
<ol type="1">
|
||
<li>Douglas R. Hofstadter, “Godel, Escher, Bach: An Eternal Golden Braid.” (1979).</li>
|
||
<li>Maria Rosaria, “Una costruzione del sistema dei numeri reali” (2012).</li>
|
||
<li>Enzo Ruffaldi, Gian Paolo Terravecchia, Andrea Sani, “Il Pensiero Plurale” (2008).</li>
|
||
</ol>
|
||
<h1 id="interessanti-applicazioni-il-lambda-calcolo"><span class="header-section-number">2</span> Interessanti applicazioni: il <span class="math inline">\(\lambda\)</span>-calcolo</h1>
|
||
<figure>
|
||
<img src="images/church.jpg" alt="Alonzo Church" /><figcaption>Alonzo Church</figcaption>
|
||
</figure>
|
||
<p>Il lambda calcolo o <span class="math inline">\(\lambda\)</span>-calcolo è un <strong>sistema formale</strong> inventato dal matematico e logico americano <strong>Alonzo Church</strong> negli anni ’30 che formalizza le computazioni di funzioni.</p>
|
||
<h2 id="il-problema-della-decisione"><span class="header-section-number">2.1</span> Il problema della decisione</h2>
|
||
<p>Questo sistema formale fu introdotto per risolvere un altro problema proposto da Hilbert nel suo programma: il cosiddetto <strong>Entscheidungsproblem</strong> o problema della decisione. Il problema è il seguente:</p>
|
||
<p><em>Esiste un algoritmo, un metodo completamente meccanico, per verificare se una qualunque stringa di un sistema formale è un teorema in quel sistema?</em></p>
|
||
<p>La risposta fu fornita indipendentemente da Church e <strong>Alan Turing</strong> nel 1936 e fu un deciso <strong>no</strong>. Church ci arrivò proprio tramite questo sistema formale mentre Turing attraverso un modello ideale di macchina che oggi è noto come <strong>macchina di Turing</strong>. Nello stesso anno poi Turing dimostrò che i sistemi da loro inventati erano equivalenti: cioè sono ugualmente potenti perché possono calcolare la stessa classe di funzioni.</p>
|
||
<figure>
|
||
<img src="images/turing.jpg" alt="Alan Turing" /><figcaption>Alan Turing</figcaption>
|
||
</figure>
|
||
<p>Il lambda calcolo e le macchine di Turing rendono formale la nozione intuitiva di <em>calcolabile</em> e <em>decidibile</em> che sono fondamentali per risolvere il problema.</p>
|
||
<h2 id="oggi"><span class="header-section-number">2.2</span> Oggi</h2>
|
||
<p>I computer moderni sono tuttora basati sul modello delle macchine di Turing e così anche i linguaggi di programmazione <strong>imperativi</strong> basati sul modo in cui si forniscono istruzioni a tali macchine.</p>
|
||
<h3 id="linguaggi-funzionali"><span class="header-section-number">2.2.1</span> Linguaggi funzionali</h3>
|
||
<p>Esiste tuttavia un’altra classe di linguaggi di programmazione i cosiddetti <strong>linguaggi funzionali</strong> che sono invece basati sul lambda calcolo. A differenza dei programmi imperativi che sono un elenco di istruzioni i programmi funzionali consistono di una singola <strong>espressione</strong> che contiene sia l’algoritmo che il suo input. Quest’espressione, tramite l’applicazione di regole, è <strong>ridotta</strong> più volte fino ad ottenere il risultato del programma. La riduzione consiste nel sostituire una parte dell’espressione con una più semplice come facciamo in matematica. Per esempio:</p>
|
||
<p><span class="math display">\[
|
||
\begin{aligned}
|
||
(1+2)\times(4\times 3) &\rightarrow 3\times (4\times 3) \\
|
||
&\rightarrow 3\times 12 \\
|
||
&\rightarrow 36 \\
|
||
\end{aligned}
|
||
\]</span></p>
|
||
<p>Partendo dall’espressione <span class="math inline">\(E\)</span> otteniamo alla fine l’espressione <span class="math inline">\(E^*\)</span> detta <em>forma normale</em>, ovvero il risultato. Il lambda calcolo fa esattamente questo.</p>
|
||
<h2 id="definizione"><span class="header-section-number">2.3</span> Definizione</h2>
|
||
<p>Vediamo ora la definizione del sistema formale.</p>
|
||
<h3 id="simboli-3"><span class="header-section-number">2.3.1</span> Simboli</h3>
|
||
<p>I simboli usati sono</p>
|
||
<ol type="1">
|
||
<li>la lettera <span class="math inline">\(\lambda\)</span></li>
|
||
<li>il punto .</li>
|
||
<li>le parentesi tonde ()</li>
|
||
<li>un insieme di lettere per le variabili</li>
|
||
</ol>
|
||
<h3 id="lambda-termini"><span class="header-section-number">2.3.2</span> Lambda termini</h3>
|
||
<p>Le espressioni (formule) ben formate del <span class="math inline">\(\lambda\)</span>-calcolo si chiamano <span class="math inline">\(\lambda\)</span>-termini.</p>
|
||
<p>I seguenti sono <span class="math inline">\(\lambda\)</span>-termini:</p>
|
||
<ol type="1">
|
||
<li><strong>variabili</strong>: si chiamano variabili tutti i simboli come <span class="math inline">\(x, y, z, \cdots\)</span></li>
|
||
<li><strong>applicazione</strong>: si dice applicazione <span class="math inline">\((t\ s)\)</span> dove <span class="math inline">\(s\)</span> e <span class="math inline">\(t\)</span> sono <span class="math inline">\(\lambda\)</span>-termini.</li>
|
||
<li><strong><span class="math inline">\(\lambda\)</span>-astrazione</strong> si dice <span class="math inline">\(\lambda\)</span>-astrazione <span class="math inline">\(\lambda v.t\)</span> dove <span class="math inline">\(t\)</span> è un <span class="math inline">\(\lambda\)</span>-termine e <span class="math inline">\(v\)</span> una variabile.</li>
|
||
</ol>
|
||
<p>Alcuni esempi di termini:</p>
|
||
<p><span class="math display">\[ x \]</span> <span class="math display">\[ y \]</span> <span class="math display">\[ (x\ y) \]</span> <span class="math display">\[ (\lambda x.(x\ y)) \]</span></p>
|
||
<p>Per comodità userò operatori come <span class="math inline">\(\times, +, -\)</span>, numeri e alcune metasintassi ma ricordiamoci che essi non fanno parte del sistema formale.</p>
|
||
<h3 id="applicazione"><span class="header-section-number">2.3.3</span> Applicazione</h3>
|
||
<p>La prima operazione di base del <span class="math inline">\(\lambda\)</span>-calcolo è l’<em>applicazione</em>: Se <span class="math inline">\(F\)</span> è un algoritmo e <span class="math inline">\(A\)</span> dei dati, indichiamo l’applicazione di <span class="math inline">\(F\)</span> al valore <span class="math inline">\(A\)</span> con:</p>
|
||
<p><span class="math display">\[F\ A\]</span></p>
|
||
<p>Con applicazione si può intendere sia il risultato dell’algoritmo sia il processo stesso di applicazione. Poiché il lambda calcolo non definisce i <strong>tipi</strong> possiamo anche applicare <span class="math inline">\(F\)</span> a se stesso (per fare una ricorsione per esempio) così:</p>
|
||
<p><span class="math display">\[F\ F\]</span></p>
|
||
<p>Un esempio di applicazione è</p>
|
||
<p><span class="math display">\[(\lambda x.x+2)2 \rightarrow 4\]</span></p>
|
||
<p>dove abbiamo applicato la <span class="math inline">\(\lambda\)</span>-espressione <span class="math inline">\((\lambda x.x+2)\)</span> al valore 2 e ottenuto 4.</p>
|
||
<h3 id="astrazione"><span class="header-section-number">2.3.4</span> Astrazione</h3>
|
||
<p>Un’altra operazione è l’<em>astrazione</em>: Se <span class="math inline">\(F[x]\)</span> è un espressione che contiene la variabile <span class="math inline">\(x\)</span>: <span class="math inline">\(\lambda x.F[x]\)</span> è un’espressione che denota la funzione <span class="math inline">\(x \mapsto F[x]\)</span>.</p>
|
||
<p>Quando applichiamo un valore ad un’astrazione facciamo una sostituzione:</p>
|
||
<p><span class="math inline">\((\lambda x.F[x])A\)</span> è uguale a <span class="math inline">\(F[A]\)</span>, scritto anche come:</p>
|
||
<p><span class="math display">\[(\lambda x.F[x])D = F[x:=D]\]</span></p>
|
||
<p>dove <span class="math inline">\(F[x:=D]\)</span> indica il <span class="math inline">\(\lambda\)</span>-termine ottenuto sostituendo tutte le occorrenze di <span class="math inline">\(x\)</span> con <span class="math inline">\(D\)</span>.</p>
|
||
<p>Un’astrazione quindi è la definizione di una funzione che non ha un nome specifico. Infatti vengono a volte chiamate <em>funzioni anonime</em>.</p>
|
||
<h3 id="variabili-libere-e-legate"><span class="header-section-number">2.3.5</span> Variabili libere e legate</h3>
|
||
<p>In un’espressione le variabili possono essere legate o libere. Per esempio in <span class="math inline">\(\lambda x.(y\ x)\)</span> <span class="math inline">\(y\)</span> è libera mentre <span class="math inline">\(x\)</span> è legata. Le variabili libere possono quindi essere legate da una <span class="math inline">\(\lambda\)</span>-astrazione con il simbolo <span class="math inline">\(\lambda\)</span>.</p>
|
||
<p>Quando applichiamo un valore facendo una sostituzione <span class="math inline">\([x:=D]\)</span> in un’astrazione questa avviene solo dove <span class="math inline">\(x\)</span> è libera. Esattamente come quando abbiamo una funzione integrale tipo <span class="math inline">\(F(x)=\int_0 ^x f(x)dx\)</span> e calcoliamo un suo valore come <span class="math inline">\(F(3)=\int_0 ^3 f(x)dx\)</span>.</p>
|
||
<p>Per esempio: <span class="math display">\[
|
||
\begin{aligned}
|
||
F[y] = \lambda y.(\lambda y.y\ y) &&F[y:=3] = (\lambda y.y\ 3)
|
||
\end{aligned}
|
||
\]</span></p>
|
||
<p>Se un <span class="math inline">\(\lambda\)</span>-termine non contiene variabili libere si che è un <strong>combinatore</strong> o termine <em>chiuso</em>.</p>
|
||
<h3 id="applicazione-parziale"><span class="header-section-number">2.3.6</span> Applicazione parziale</h3>
|
||
<figure>
|
||
<img src="images/curry.jpg" alt="Haskell Curry" /><figcaption>Haskell Curry</figcaption>
|
||
</figure>
|
||
<p>Abbiamo visto che con la <span class="math inline">\(\lambda\)</span>-astrazione possiamo produrre funzioni che accettano un parametro. Spesso però abbiamo la necessità di avere funzioni con <strong>argomenti multipli</strong> come <span class="math inline">\(f(x,y,z)\)</span> Si può rappresentare queste funzioni usando un metodo noto come applicazione parziale o <em>currying</em>, dal matematico <strong>Haskell Curry</strong> che lo utilizzò per primo.</p>
|
||
<p>Una funzione di più argomenti è rappresentata come una catena di funzioni in cui ciascuna genera a sua volta una funzione di un singolo argomento.</p>
|
||
<p>Per esempio la funzione <span class="math inline">\(f(x,y,z)=x\times y+z\)</span> viene così definita:</p>
|
||
<p><span class="math display">\[
|
||
\lambda x.\lambda y.\lambda z.(x\times y+z)
|
||
\]</span></p>
|
||
<p>Se vogliamo calcolare <span class="math inline">\(f(2,3,5)\)</span>:</p>
|
||
<ol type="1">
|
||
<li>applichiamo la prima volta 2 e otteniamo la funzione <span class="math inline">\(\lambda y.\lambda z.(2\times y+z)\)</span></li>
|
||
<li>applichiamo la seconda volta 3 e otteniamo la funzione <span class="math inline">\(\lambda z.(2\times 3+z)\)</span></li>
|
||
<li>applichiamo infine 5 e otteniamo il risultato <span class="math inline">\((2\times 3+5) \rightarrow 11\)</span></li>
|
||
</ol>
|
||
<p>complessivamente <span class="math inline">\(f(2,3,5) = (((\lambda x.\lambda y.\lambda z.(x\times y+z)\ 2)\ 3)\ 5)\)</span></p>
|
||
<h2 id="regole-1"><span class="header-section-number">2.4</span> Regole</h2>
|
||
<p>Vediamo ora le regole per ridurre o convertire una <span class="math inline">\(\lambda\)</span>-espressione.</p>
|
||
<h3 id="alpha-conversione"><span class="header-section-number">2.4.1</span> <span class="math inline">\(\alpha\)</span>-conversione</h3>
|
||
<p>L’<span class="math inline">\(\alpha\)</span>-conversione è una regola che permette di sostituire le variabili legate in un <span class="math inline">\(\lambda\)</span>-termine, cioè <strong>rinominarle</strong>. I <span class="math inline">\(\lambda\)</span>-termini ottenuti con questa conversione si dicono tra loro <strong><span class="math inline">\(\alpha\)</span>-equivalenti</strong>. L’<span class="math inline">\(\alpha\)</span>-conversione è una sostituzione del tipo <span class="math inline">\(F[u:=v]\)</span> dove <span class="math inline">\(u\)</span> è una variabile legate e <span class="math inline">\(v\)</span> una variabile qualsiasi.</p>
|
||
<p>Per esempio <span class="math inline">\(\lambda x.x \rightarrow_\alpha \lambda z.z\)</span>.</p>
|
||
<p>Non è sempre possibile effettuare un <span class="math inline">\(\alpha\)</span>-conversione. Per esempio non è possibile fare la sostituzione <span class="math inline">\((\lambda y.\lambda x.y)[y:=x]\)</span>. Infatti <span class="math inline">\(\lambda x.\lambda x.x\)</span> è un <span class="math inline">\(\lambda\)</span>-termine completamente diverso.</p>
|
||
<h3 id="beta-riduzione"><span class="header-section-number">2.4.2</span> <span class="math inline">\(\beta\)</span>-riduzione</h3>
|
||
<p>La <span class="math inline">\(\beta\)</span>-riduzione è un’applicazione del tipo <span class="math inline">\((\lambda x.M)N\)</span> dove <span class="math inline">\(M\)</span> e <span class="math inline">\(N\)</span> sono dei <span class="math inline">\(\lambda\)</span>-termini. Si può calcolare come una sostituzione <span class="math inline">\(M[x:=N]\)</span>.</p>
|
||
<p><span class="math inline">\((\lambda x.M)N\)</span> si dice <span class="math inline">\(\beta\)</span>-redex e <span class="math inline">\(M[x:=N]\)</span> la sua <span class="math inline">\(\beta\)</span>-contrazione. La riduzione si indica con <span class="math inline">\(g \rightarrow_\beta g'\)</span> e si legge “<span class="math inline">\(g\)</span> riduce a <span class="math inline">\(g'\)</span>”.</p>
|
||
<p>Per esempio <span class="math inline">\((\lambda x.x^3-1)3 \rightarrow_\beta 10\)</span></p>
|
||
<h3 id="eta-conversione"><span class="header-section-number">2.4.3</span> <span class="math inline">\(\eta\)</span>-conversione</h3>
|
||
<p>Quando abbiamo un <span class="math inline">\(\lambda\)</span>-termine del tipo <span class="math inline">\((\lambda x.M\ x)\)</span> l’<span class="math inline">\(\eta\)</span>-conversione ci permette di rimuovere la <span class="math inline">\(\lambda\)</span>-astrazione se <span class="math inline">\(x\)</span> non appare libera in <span class="math inline">\(M\)</span>. I termini prodotti si dicono <span class="math inline">\(\eta\)</span>-equivalenti e la conversione si indica con <span class="math inline">\(g \rightarrow_\eta g'\)</span>.</p>
|
||
<p>Per esempio <span class="math inline">\(\lambda y. \lambda x.y\ x \rightarrow_\eta \lambda y.y\)</span></p>
|
||
<h3 id="in-2-righe"><span class="header-section-number">2.4.4</span> In 2 righe</h3>
|
||
<p>Utilizzando la metasintassi di Backus-Naur possiamo riassumere la sintassi e la semantica del <span class="math inline">\(\lambda\)</span>-calcolo in appena 2 righe:</p>
|
||
<p><span class="math display">\[L ::= v\ |\ \lambda v.L\ |\ (L\ L)\]</span> <span class="math display">\[(\lambda v.L_\beta)L_\alpha \rightarrow L_\beta[v:=L_\alpha]\]</span></p>
|
||
<h2 id="utilità"><span class="header-section-number">2.5</span> Utilità</h2>
|
||
<p>Vediamo ora che abbiamo definito il sistema cosa ci permette di fare.</p>
|
||
<h3 id="aritmetica"><span class="header-section-number">2.5.1</span> Aritmetica</h3>
|
||
<p>Il <span class="math inline">\(\lambda\)</span>-calcolo calcolo contiene l’aritmetica di Peano. È possibile rappresentare i numeri naturali tramite i <strong>numerali di Church</strong> così definiti:</p>
|
||
<ol start="0" type="1">
|
||
<li><span class="math inline">\(\lambda y. \lambda x.x\)</span></li>
|
||
<li><span class="math inline">\(\lambda y. \lambda x. y\ x\)</span></li>
|
||
<li><span class="math inline">\(\lambda y. \lambda x. y\ (y\ x)\)</span></li>
|
||
<li><span class="math inline">\(\lambda y. \lambda x. y\ (y\ (y\ x))\)</span><br />
|
||
<span class="math inline">\(\cdots\)</span></li>
|
||
</ol>
|
||
<p>I numerali di Church sono <strong>funzioni di ordine maggiore</strong>: una funzione che accetta una funzione come parametro e ne genera un’altra. In particolare l’<span class="math inline">\(n\)</span>-esimo numerale prende una funzione <span class="math inline">\(y\)</span> e la applica <span class="math inline">\(n\)</span> volte a se stessa.</p>
|
||
<p>La funzione successore è definita come:</p>
|
||
<p><span class="math display">\[\text{succ} := \lambda n.\lambda y.\lambda x.y (n\ y\ x)\]</span></p>
|
||
<p><code>succ</code> semplicemente prende come argomento un numerale <span class="math inline">\(n\)</span> a cui applica nuovamente la funzione <span class="math inline">\(y\)</span> per ottenere <span class="math inline">\(n+1\)</span>.</p>
|
||
<p>È altrettanto semplice definire le operazioni aritmetiche. Per esempio:</p>
|
||
<p><span class="math display">\[
|
||
\begin{aligned}
|
||
\text{mult} &:= \lambda m.\lambda n.m\ \text{succ}\ n \\
|
||
\text{plus} &:= \lambda m.\lambda n.\lambda y.m\ (n\ y)
|
||
\end{aligned}
|
||
\]</span></p>
|
||
<h3 id="logica-booleana"><span class="header-section-number">2.5.2</span> Logica booleana</h3>
|
||
<p>I valori di vero e falso sono rappresentati per convenzione tramite i <strong>booleani di Church</strong>:</p>
|
||
<p><span class="math display">\[
|
||
\begin{aligned}
|
||
T := &\lambda x.\lambda y.x && \text{(vero)} \\
|
||
F := &\lambda x.\lambda y.y && \text{(falso)}
|
||
\end{aligned}
|
||
\]</span></p>
|
||
<p>È poi possibile formulare gli operatori logici così:</p>
|
||
<p><span class="math display">\[
|
||
\begin{aligned}
|
||
\text{and} &:= \lambda p.\lambda q.p\ q\ p \\
|
||
\text{or} &:= \lambda p.\lambda q.p\ p\ q \\
|
||
\text{not} &:= \lambda p.\lambda a.\lambda b.p\ b\ a \\
|
||
\end{aligned}
|
||
\]</span></p>
|
||
<p>Un esempio di uso: <span class="math display">\[
|
||
\begin{aligned}
|
||
\text{and}\ T\ F & \rightarrow (\lambda p.\lambda q.p\ q\ p)\ T\ F \\
|
||
& \rightarrow (T\ F)\ T \\
|
||
& \rightarrow (\lambda x.\lambda y.x\ F)\ T \\
|
||
& \rightarrow \lambda x.\lambda y.y \\
|
||
& \rightarrow F \\
|
||
\end{aligned}
|
||
\]</span></p>
|
||
<h3 id="ricorsione-anonima"><span class="header-section-number">2.5.3</span> Ricorsione anonima</h3>
|
||
<p>Una funzione ricorsiva essenzialmente è una funzione che nella sua definizione contiene se stessa. L’esempio più semplice è la funzione fattoriale <span class="math inline">\(n! = 1\cdot 2\cdot 3\dots (n-1)\cdot n\)</span> che può essere così definita:</p>
|
||
<p><span class="math display">\[
|
||
n! =
|
||
\begin{cases}
|
||
1 & x = 0 \\
|
||
n\cdot(n-1)! & \text{altrimenti}
|
||
\end{cases}
|
||
\]</span></p>
|
||
<p>È fondamentale quindi che la funzione abbia un <strong>nome</strong> associato. Nel <span class="math inline">\(\lambda\)</span>-calcolo nonostante le astrazioni siano anonime e quindi non possono riferirsi tramite un nome è possibile ottenere lo stesso risultato. Per fare ciò usiamo il <strong>combinatore <span class="math inline">\(Y\)</span></strong></p>
|
||
<p>Il combinatore <span class="math inline">\(Y\)</span>, o <em>di punto fisso</em>, è una qualunque funzione di ordine maggiore che soddisfa la relazione <span class="math inline">\(y\ f=f\ (y\ f)\)</span> per qualunque <span class="math inline">\(f\)</span>. Per esempio il <strong>combinatore di Curry</strong> è di punto fisso: <span class="math display">\[
|
||
Y := \lambda f.(\lambda x.f(x\ x))\ (\lambda x.f\ (x x))
|
||
\]</span></p>
|
||
<p>Possiamo dimostrare che vale la relazione del combinatore <span class="math inline">\(Y\)</span> tramite riduzione: <span class="math display">\[
|
||
\begin{aligned}
|
||
Y\ g &= \lambda f.(\lambda x.f(x\ x))\ (\lambda x.f\ (x\ x))\ g && \text {per definizione} \\
|
||
&\rightarrow_\beta (\lambda x.g(x\ x))\ (\lambda x.g\ (x\ x)) && \text {applicazione di $Y$ a $g$} \\
|
||
&\rightarrow_\beta g(\lambda x.g(x\ x))\ (\lambda x.g\ (x\ x)) && \text {applicazione del primo termine} \\
|
||
&= g\ (Y\ g) && \text {uguaglianza al secondo passaggio} \\
|
||
\end{aligned}
|
||
\]</span></p>
|
||
<p>Continuando ad applicare l’uguaglianza si ottiene: <span class="math display">\[g\ (Y\ g) = g\ (g\ (Y\ g)) = g\ (g\ (g\ (Y\ g))) = g\ (\dots(Y\ g)\dots)\]</span></p>
|
||
<p>Quindi il combinatore <span class="math inline">\(Y\)</span> continua ad applicare la funzione argomento e questo ci permette di scrivere una funzione ricorsiva tramite una <span class="math inline">\(\lambda\)</span>-astrazione senza la necessità di darle un nome.</p>
|
||
<p>Torniamo al nostro fattoriale: scriviamo subito la definizione di fattoriale nel modo classico:</p>
|
||
<p><span class="math display">\[
|
||
\text{fact} := \lambda n.(\text{if } n=0 \text{ then } 1 \text{ else } n\times \text{fact } (n-1))
|
||
\]</span></p>
|
||
<p>invece di chiamare fact usiamo una funzione <span class="math inline">\(f\)</span> tramite la <span class="math inline">\(\lambda\)</span>-astrazione <span class="math inline">\(\lambda f.\)</span>:</p>
|
||
<p><span class="math display">\[
|
||
\lambda f.\lambda n.(\text{if } n=0 \text{ then } 1 \text{ else } n\times f\ (n-1))
|
||
\]</span></p>
|
||
<p>infine applichiamo <span class="math inline">\(Y\)</span> all’espressione per ottenere:</p>
|
||
<p><span class="math display">\[
|
||
\text{fact} := Y\ (\lambda f.\lambda n.(\text{if } n=0 \text{ then } 1 \text{ else } n\times f\ (n-1)))
|
||
\]</span></p>
|
||
<p>In modo più formale usiamo i combinatori standard del lambda calcolo:</p>
|
||
<p><span class="math display">\[
|
||
\text{fact} := Y\ (\lambda f.\lambda n.(\text{isZero }n)\ 1\ (\text{mult }n\ (f\ (\text{pred }n))))
|
||
\]</span></p>
|
||
<h2 id="turing-equivalenza"><span class="header-section-number">2.6</span> Turing-equivalenza</h2>
|
||
<figure>
|
||
<img src="images/busy-beaver.png" alt="schema della macchina busy beaver 4,2" /><figcaption>schema della macchina busy beaver 4,2</figcaption>
|
||
</figure>
|
||
<p>Con la capacità di esprimere l’aritmetica, la logica ed infine anche la ricorsione il <span class="math inline">\(\lambda\)</span>-calcolo è diventato <strong>Turing-equivalente</strong>: può compiere qualunque operazione una macchina di Turing sia in grado di svolgere. Secondo la <strong>tesi di Church-Turing</strong> cioè può calcolare qualsiasi funzione intuitivamente calcolabile. È sicuramente sorprendente per un sistema che si può descrivere in solo due righe. Per accorgersi di quanto è semplice e potente basta fare un confronto con TNT che per poter esprimere ogni proprietà dei numeri necessita di ben 7 regole di inferenza, 5 assiomi ed ingloba un intero sistema formale a parte (il calcolo proposizionale).</p>
|
||
<h2 id="lambda-calcolo-tipizzato"><span class="header-section-number">2.7</span> <span class="math inline">\(\lambda\)</span>-calcolo tipizzato</h2>
|
||
<p>La versione che abbiamo visto del <span class="math inline">\(\lambda\)</span>-calcolo è senza tipi: cioè <strong>non ci sono limitazioni</strong> su cosa si può applicare a qualunque espressione. I termini possono persino essere applicati a se stessi. Questo permette una grande capacità di espressione ma porta agli stessi problemi individuati da Russell nella teoria <em>naive</em> degli insiemi. Per esempio il combinatore <span class="math inline">\(Y\)</span> che abbiamo utilizzato per la ricorsione può essere utilizzato per produrre un paradosso (<strong>paradosso di Curry</strong>) che permette di derivare qualsiasi <span class="math inline">\(\lambda\)</span>-termine. Lo stesso paradosso di Russel è presente in questa formulazione.</p>
|
||
<p>Questo si può risolvere introducendo una <strong>teoria dei tipi</strong> nel <span class="math inline">\(\lambda\)</span>-calcolo, esattamento quello che ha fatto Russel in <em>Principia mathematica</em>.</p>
|
||
<h3 id="tipi"><span class="header-section-number">2.7.1</span> Tipi</h3>
|
||
<p>Diciamo che <span class="math inline">\(\mathcal{G}\)</span> sia l’insieme dei tipi primitivi. Sono tipi:</p>
|
||
<ul>
|
||
<li>ogni <span class="math inline">\(A \in \mathcal{G}\)</span></li>
|
||
<li><span class="math inline">\(A \to B\)</span> dove <span class="math inline">\(A\)</span> e <span class="math inline">\(B\)</span> sono tipi</li>
|
||
</ul>
|
||
<h3 id="pre-termini"><span class="header-section-number">2.7.2</span> Pre-termini</h3>
|
||
<p>Modifichiamo la definizione precedente di termine per inserire i tipi:</p>
|
||
<p>I seguenti sono pre-termini:</p>
|
||
<ol type="1">
|
||
<li><strong>variabili</strong>: si chiamano variabili tutti i simboli come <span class="math inline">\(x, y, z, \cdots\)</span></li>
|
||
<li><strong>applicazione</strong>: si dice applicazione <span class="math inline">\((t\ s)\)</span> dove <span class="math inline">\(s\)</span> e <span class="math inline">\(t\)</span> sono pre-termini.</li>
|
||
<li><strong><span class="math inline">\(\lambda\)</span>-astrazione</strong> si dice <span class="math inline">\(\lambda\)</span>-astrazione <span class="math inline">\(\lambda v^A.t\)</span> dove <span class="math inline">\(t\)</span> è un pre-termine, <span class="math inline">\(v\)</span> una variabile e <span class="math inline">\(A\)</span> è un tipo.</li>
|
||
</ol>
|
||
<h3 id="test"><span class="header-section-number">2.7.3</span> Test</h3>
|
||
<p>Per confermare che un pre-termine sia un termine dobbiamo verificare che tutte le variabili presenti in esso abbiano i tipi corretti. Un test ha la seguente forma:</p>
|
||
<p><span class="math display">\[
|
||
\underbrace{x_1: A_1, x_2: A_2, \dots, x_n:A_n}_\text{contesto} \vdash \underbrace{M: A}_\text{termine}
|
||
\]</span></p>
|
||
<p>dove:</p>
|
||
<ul>
|
||
<li><span class="math inline">\(x_1, x_2, \dots, x_n\)</span> sono variabili presenti in <span class="math inline">\(M\)</span></li>
|
||
<li><span class="math inline">\(A_1, A_2, \dots, A_n\)</span> sono tipi</li>
|
||
<li>M è un pre-termine</li>
|
||
</ul>
|
||
<p>Se il tipo di ogni variabile in <span class="math inline">\(M\)</span> è confermato allora il test è passato e <span class="math inline">\(M\)</span> è un <span class="math inline">\(\lambda\)</span>-termine. Il processo con cui si determina il tipo delle variabili nel termine e se il tipo <span class="math inline">\(A\)</span> esiste si chiama <strong>type inference</strong> e l’insieme di regole che definiscono i tipi e come si assegnano ai termini si chiama <strong>type system</strong>.</p>
|
||
<p>L’assegnazione di tipi ai termini potrebbe sembrare un inutile complicazione e una limitazione ma rende impossibile la produzione di espressioni prive di significato e spesso evita di fare errori durante l’applicazione e la riduzione ma la cosa più importante è che è possibile fare una formulazione del lambda calcolo in non esistono problemi indecidibili.</p>
|
||
<h3 id="haskell"><span class="header-section-number">2.7.4</span> Haskell</h3>
|
||
<figure>
|
||
<img src="images/haskell.png" alt="Il logo del linguaggio" /><figcaption>Il logo del linguaggio</figcaption>
|
||
</figure>
|
||
<p>Haskell, che prende il nome da Haskell Curry, è un <strong>linguaggio</strong> di programmazione puramente funzionale staticamente tipizzato che si basa sulla <strong>teoria delle categorie</strong> e proprio sul <strong><span class="math inline">\(\lambda\)</span>-calcolo tipizzato</strong>. Il programma stesso utilizzato per generare questo documento è scritto interamente in haskell così come i vari programmi da me scritti allegati alla tesi.</p>
|
||
<p>Haskell usa un particolare type system noto come <strong>Hindley–Milner</strong> usato anche da altri linguaggi funzionali. HM permette di dedurre il tipo di ogni espressione anche in assenza di qualunque annotazione dei tipi e lo fa in tempo quasi-lineare rispetto alla dimensione del programma. Consente inoltre tipi polimorfici e funzioni di ordine maggiore.</p>
|
||
<p>Un programma in haskell è un’espressione costituita da una o più definizioni di funzioni e costanti. Essendo puramente funzionale le funzioni sono <strong>funzioni matematiche</strong>: un’associazione di un valore ad un altro valore. Non è possibile che fornendo lo stesso dato la funzioni produca risultati diversi nel tempo, né che la sua esecuzione possa modificare lo stato del programma o di altre funzioni (<strong>side effects</strong>). Non esistono stati variabili: tutte le strutture dati sono <strong>immutabili</strong>. Se è necessario fare delle modifiche semplicemente se ne producono di nuove.</p>
|
||
<p>Questa descrizione dà un idea di un linguaggio fortemente limitato ma in realtà le sue caratteristiche funzionali forniscono degli enormi vantaggi:</p>
|
||
<ul>
|
||
<li>Non essendoci possibili stati mutabili o side effects non possono esistere problemi dovuti all’accesso <strong>concorrente</strong> alla memoria. L’intero programma è <em>thread-safe</em>.</li>
|
||
<li>La gestione della memoria è basata sul <em>garbage collecting</em> ma a differenza di altri linguaggi l’immutabilità delle strutture rende il processo di cancellazione dei dati deferenziati estremamente semplice e rapido.</li>
|
||
<li>I risultati dell’applicazione di funzioni vengono calcolati solo quando necessario <em>lazy evaluation</em>. Questo permette di creare strutture dati <strong>infinite</strong> Per esempio <code class="sourceCode haskell">fib <span class="fu">=</span> <span class="dv">0</span> <span class="fu">:</span> scanl (<span class="fu">+</span>) <span class="dv">1</span> fib</code> è lista infinita di <em>tutti</em> i numeri di Fibonacci.</li>
|
||
<li>Anche quando non si vuole ragionare sui tipi il compilatore è in grado dedurli da sé e impedisce di fare errori in ogni caso. Con il type system di haskell è impossibile produrre un programma che compili ma che produca degli errori in <em>runtime</em> se non volutamente.</li>
|
||
<li>Per l’<strong>isomorfismo di Curry-Howard</strong> un programma haskell <em>type checked</em> è analogo ad una dimostrazione formale. Il type system può essere perciò usato per controllare la validità di una dimostrazione matematica.</li>
|
||
<li>Lo stile funzionale e il <em>pattern matching</em> sono molto espressivi e solitamente un programma è molto più conciso della controparte imperativa.</li>
|
||
</ul>
|
||
<h3 id="esempi-di-programma"><span class="header-section-number">2.7.5</span> Esempi di programma</h3>
|
||
<h4 id="game-of-life"><span class="header-section-number">2.7.5.1</span> Game of Life</h4>
|
||
<p>Un’implementazione del <a href="https://en.wikipedia.org/wiki/Conway%27s_Game_of_Life">Game of Life</a> di John Conway su una griglia rettangolare</p>
|
||
<div class="sourceCode"><pre class="sourceCode haskell"><code class="sourceCode haskell"><span class="kw">import </span><span class="dt">Control.Applicative</span>
|
||
<span class="kw">import </span><span class="dt">Data.List</span> ((\\))
|
||
<span class="kw">import </span><span class="dt">Data.Maybe</span> (fromMaybe)
|
||
<span class="kw">import </span><span class="dt">Matrix</span>
|
||
|
||
<span class="kw">type</span> <span class="dt">Cell</span> <span class="fu">=</span> <span class="dt">Int</span>
|
||
<span class="kw">type</span> <span class="dt">Grid</span> <span class="fu">=</span> <span class="dt">Mat</span> <span class="dt">Cell</span>
|
||
|
||
<span class="ot">(!) ::</span> <span class="dt">Grid</span> <span class="ot">-></span> <span class="dt">Pos</span> <span class="ot">-></span> <span class="dt">Cell</span>
|
||
(<span class="dt">Mat</span> g) <span class="fu">!</span> (x, y) <span class="fu">=</span> fromMaybe <span class="dv">0</span> (g <span class="fu">??</span> y <span class="fu">>>=</span> (<span class="fu">??</span> x))
|
||
|
||
<span class="ot">near ::</span> <span class="dt">Grid</span> <span class="ot">-></span> <span class="dt">Pos</span> <span class="ot">-></span> [<span class="dt">Cell</span>]
|
||
near g (x, y) <span class="fu">=</span> map state <span class="fu">$</span> neighbours \\ [(<span class="dv">0</span>,<span class="dv">0</span>)]
|
||
<span class="kw">where</span>
|
||
neighbours <span class="fu">=</span> liftA2 (,) [<span class="fu">-</span><span class="dv">1</span><span class="fu">..</span><span class="dv">1</span>] [<span class="fu">-</span><span class="dv">1</span><span class="fu">..</span><span class="dv">1</span>]
|
||
state (x', y') <span class="fu">=</span> g <span class="fu">!</span> (x<span class="fu">+</span>x', y<span class="fu">+</span>y')
|
||
|
||
<span class="ot">alive ::</span> <span class="dt">Grid</span> <span class="ot">-></span> <span class="dt">Pos</span> <span class="ot">-></span> <span class="dt">Cell</span>
|
||
alive g p
|
||
<span class="fu">|</span> v <span class="fu">==</span> <span class="dv">0</span> <span class="fu">&&</span> n <span class="fu">==</span> <span class="dv">3</span> <span class="fu">=</span> <span class="dv">1</span>
|
||
<span class="fu">|</span> v <span class="fu">==</span> <span class="dv">1</span> <span class="fu">&&</span> (n <span class="fu">==</span> <span class="dv">2</span> <span class="fu">||</span> n <span class="fu">==</span> <span class="dv">3</span>) <span class="fu">=</span> <span class="dv">1</span>
|
||
<span class="fu">|</span> otherwise <span class="fu">=</span> <span class="dv">0</span>
|
||
<span class="kw">where</span> (n, v) <span class="fu">=</span> (sum (near g p), g <span class="fu">!</span> p)
|
||
|
||
<span class="ot">next ::</span> <span class="dt">Grid</span> <span class="ot">-></span> <span class="dt">Grid</span>
|
||
next g <span class="fu">=</span> alive g <span class="fu"><$></span> indeces g
|
||
|
||
<span class="ot">main ::</span> <span class="dt">IO</span> ()
|
||
main <span class="fu">=</span> mapM_ print (iterate next grid)
|
||
|
||
grid <span class="fu">=</span> <span class="dt">Mat</span>
|
||
[ [<span class="dv">0</span>, <span class="dv">0</span>, <span class="dv">0</span>, <span class="dv">0</span>, <span class="dv">0</span>, <span class="dv">0</span>, <span class="dv">0</span>, <span class="dv">0</span>, <span class="dv">0</span>, <span class="dv">0</span>, <span class="dv">0</span>, <span class="dv">0</span>]
|
||
, [<span class="dv">0</span>, <span class="dv">0</span>, <span class="dv">1</span>, <span class="dv">0</span>, <span class="dv">0</span>, <span class="dv">0</span>, <span class="dv">0</span>, <span class="dv">0</span>, <span class="dv">0</span>, <span class="dv">0</span>, <span class="dv">0</span>, <span class="dv">0</span>]
|
||
, [<span class="dv">0</span>, <span class="dv">0</span>, <span class="dv">0</span>, <span class="dv">1</span>, <span class="dv">0</span>, <span class="dv">0</span>, <span class="dv">0</span>, <span class="dv">0</span>, <span class="dv">0</span>, <span class="dv">0</span>, <span class="dv">0</span>, <span class="dv">0</span>]
|
||
, [<span class="dv">0</span>, <span class="dv">1</span>, <span class="dv">1</span>, <span class="dv">1</span>, <span class="dv">0</span>, <span class="dv">0</span>, <span class="dv">0</span>, <span class="dv">0</span>, <span class="dv">0</span>, <span class="dv">0</span>, <span class="dv">0</span>, <span class="dv">0</span>]
|
||
, [<span class="dv">0</span>, <span class="dv">0</span>, <span class="dv">0</span>, <span class="dv">0</span>, <span class="dv">0</span>, <span class="dv">0</span>, <span class="dv">0</span>, <span class="dv">0</span>, <span class="dv">0</span>, <span class="dv">0</span>, <span class="dv">0</span>, <span class="dv">0</span>]
|
||
, [<span class="dv">0</span>, <span class="dv">0</span>, <span class="dv">0</span>, <span class="dv">0</span>, <span class="dv">0</span>, <span class="dv">0</span>, <span class="dv">0</span>, <span class="dv">0</span>, <span class="dv">0</span>, <span class="dv">0</span>, <span class="dv">0</span>, <span class="dv">0</span>]
|
||
, [<span class="dv">0</span>, <span class="dv">0</span>, <span class="dv">0</span>, <span class="dv">0</span>, <span class="dv">0</span>, <span class="dv">0</span>, <span class="dv">0</span>, <span class="dv">0</span>, <span class="dv">0</span>, <span class="dv">0</span>, <span class="dv">0</span>, <span class="dv">0</span>] ]</code></pre></div>
|
||
<h4 id="rpn"><span class="header-section-number">2.7.5.2</span> RPN</h4>
|
||
<p>Un programma che risolve espressioni in <a href="https://en.wikipedia.org/wiki/Reverse_Polish_notation">notazione polacca inversa</a></p>
|
||
<p>Per esempio:</p>
|
||
<pre><code>> 5 8 9 2 * cos ^ - 2 0.452 tan / +
|
||
= 5.1717299516</code></pre>
|
||
<div class="sourceCode"><pre class="sourceCode haskell"><code class="sourceCode haskell"><span class="ot">{-# LANGUAGE ViewPatterns #-}</span>
|
||
|
||
<span class="kw">import </span><span class="dt">Data.List</span>
|
||
<span class="kw">import </span><span class="dt">Data.Maybe</span>
|
||
<span class="kw">import </span><span class="dt">Text.Read</span>
|
||
<span class="kw">import </span><span class="dt">Text.Printf</span>
|
||
<span class="kw">import </span><span class="dt">Control.Monad</span>
|
||
<span class="kw">import </span><span class="dt">System.Console.Haskeline</span>
|
||
|
||
<span class="ot">main ::</span> <span class="dt">IO</span> ()
|
||
main <span class="fu">=</span> runInputT defaultSettings repl
|
||
|
||
<span class="ot">repl ::</span> <span class="dt">InputT</span> <span class="dt">IO</span> ()
|
||
repl <span class="fu">=</span> <span class="kw">do</span>
|
||
line <span class="ot"><-</span> getInputLine <span class="st">"> "</span>
|
||
<span class="kw">case</span> fromMaybe <span class="st">""</span> line <span class="kw">of</span>
|
||
<span class="st">"q"</span> <span class="ot">-></span> return ()
|
||
<span class="st">""</span> <span class="ot">-></span> outputStrLn <span class="st">""</span> <span class="fu">>></span> repl
|
||
exp <span class="ot">-></span> outputStrLn (result (rpn exp) <span class="fu">++</span> <span class="st">"\n"</span>) <span class="fu">>></span> repl
|
||
|
||
<span class="ot">result ::</span> <span class="dt">Either</span> <span class="dt">String</span> <span class="dt">Double</span> <span class="ot">-></span> <span class="dt">String</span>
|
||
result (<span class="dt">Left</span> err) <span class="fu">=</span> <span class="st">"!! "</span> <span class="fu">++</span> err
|
||
result (<span class="dt">Right</span> x) <span class="fu">=</span> printf format x <span class="kw">where</span>
|
||
format <span class="fu">|</span> ceiling x <span class="fu">==</span> floor x <span class="fu">=</span> <span class="st">"= %.0f"</span>
|
||
<span class="fu">|</span> otherwise <span class="fu">=</span> <span class="st">"= %.10f"</span>
|
||
|
||
<span class="ot">rpn ::</span> <span class="dt">String</span> <span class="ot">-></span> <span class="dt">Either</span> <span class="dt">String</span> <span class="dt">Double</span>
|
||
rpn <span class="fu">=</span> foldM parse [] <span class="fu">.</span> words <span class="fu">>=></span> return <span class="fu">.</span> head <span class="kw">where</span>
|
||
parse (y<span class="fu">:</span>x<span class="fu">:</span>xs) (flip lookup dyad <span class="ot">-></span> <span class="dt">Just</span> f) <span class="fu">=</span> <span class="dt">Right</span> (f x y <span class="fu">:</span> xs)
|
||
parse (x<span class="fu">:</span>xs) (flip lookup monad <span class="ot">-></span> <span class="dt">Just</span> f) <span class="fu">=</span> <span class="dt">Right</span> (f x <span class="fu">:</span> xs)
|
||
parse xs (flip lookup nilad <span class="ot">-></span> <span class="dt">Just</span> k) <span class="fu">=</span> <span class="dt">Right</span> (k <span class="fu">:</span> xs)
|
||
parse xs (readMaybe <span class="ot">-></span> <span class="dt">Just</span> x) <span class="fu">=</span> <span class="dt">Right</span> (x <span class="fu">:</span> xs)
|
||
parse _ _ <span class="fu">=</span> <span class="dt">Left</span> <span class="st">"syntax error"</span>
|
||
|
||
dyad <span class="fu">=</span> [ (<span class="st">"+"</span>, (<span class="fu">+</span>))
|
||
, (<span class="st">"-"</span>, (<span class="fu">-</span>))
|
||
, (<span class="st">"*"</span>, (<span class="fu">*</span>))
|
||
, (<span class="st">"/"</span>, (<span class="fu">/</span>))
|
||
, (<span class="st">"^"</span>, (<span class="fu">**</span>)) ]
|
||
|
||
monad <span class="fu">=</span> [ (<span class="st">"sin"</span> , sin )
|
||
, (<span class="st">"asin"</span> , asin)
|
||
, (<span class="st">"cos"</span> , cos )
|
||
, (<span class="st">"acos"</span> , acos)
|
||
, (<span class="st">"tan"</span> , tan )
|
||
, (<span class="st">"atan"</span> , atan)
|
||
, (<span class="st">"ln"</span> , log )
|
||
, (<span class="st">"sqrt"</span> , sqrt)
|
||
, (<span class="st">"sgn"</span> , signum)
|
||
, (<span class="st">"abs"</span> , abs)
|
||
, (<span class="st">"floor"</span>, fromIntegral <span class="fu">.</span> floor)
|
||
, (<span class="st">"ceil"</span> , fromIntegral <span class="fu">.</span> ceiling) ]
|
||
|
||
nilad <span class="fu">=</span> [ (<span class="st">"pi"</span> , pi)
|
||
, (<span class="st">"e"</span> , exp <span class="dv">1</span>)
|
||
, (<span class="st">"phi"</span>, (<span class="dv">1</span> <span class="fu">+</span> sqrt <span class="dv">5</span>)<span class="fu">/</span><span class="dv">2</span>) ]</code></pre></div>
|
||
<h2 id="bibliografia-1"><span class="header-section-number">2.8</span> Bibliografia</h2>
|
||
<ol type="1">
|
||
<li>Henk Barendregt, Erik Barendsen, “Introduction to Lambda Calculus” (1998).</li>
|
||
<li>Andrzej S. Murawski, “Typed lambda calculi” (2011).</li>
|
||
<li>Enrico Denti, “Introduzione ai linguaggi fondazionali” (2012).</li>
|
||
<li>Miran Lipovača, “Learn You a Haskell for Great Good” (2011).</li>
|
||
</ol>
|
||
<h1 id="unanalogia-pirandello-e-metateatro"><span class="header-section-number">3</span> Un’analogia: Pirandello e Metateatro</h1>
|
||
<h2 id="introduzione"><span class="header-section-number">3.1</span> Introduzione</h2>
|
||
<p>Uno dei metodi principali utilizzati da Gödel per dare la dimostrazione dei teoremi di incompletezza è quello produrre all’interno di una teoria matematica delle formule che parlino della teoria stessa, il cosiddetto numero di Gödel. Il fatto stesso che le teorie non possono mai essere complete deriva proprio dal fatto che possono <strong>contenere se stesse</strong>. Si può così dire che i sistemi formali nonostante imitino e si avvicinino per quanto si vuole alla realtà non sono mai in grado di raggiungerla completamente: esisteranno sempre delle verità che non possono essere da essi rappresentate. Troviamo questo stesso tema anche in letteratura e precisamente nell’opera di <strong>Luigi Pirandello</strong> (1867-1936) contemporaneo di Gödel.</p>
|
||
<figure>
|
||
<img src="images/pirandello.jpg" alt="Luigi Pirandello" /><figcaption>Luigi Pirandello</figcaption>
|
||
</figure>
|
||
<p>Nella sua opera mette in discussione l’immagine di un mondo ordinato, organico e interpretabile con certezza mediante gli strumenti razionali della ragione. Il risultato è un forte <strong>relativismo</strong>: la realtà è tanto complessa da non poter essere rappresentabile da un unico punto di vista né fissata in un unico sistema di regole come voleva Hilbert perché non esiste una sola verità ma ciascuno ne possiede una propria.</p>
|
||
<h2 id="sei-personaggi-in-cerca-dautore"><span class="header-section-number">3.2</span> Sei personaggi in cerca d’autore</h2>
|
||
<p>Esemplificativo di questo modo di intendere il mondo è il dramma “Sei personaggi in cerca d’autore”. Si tratta di un esempio di <strong>metateatro</strong>: o <em>teatro nel teatro</em>. Cioè un opera in cui arte e teatro mettono in scena se sessi. Si tratta di un opera buia, cupa ma di grande impatto intellettuale ed emotivo. Insieme a “Ciascuno a suo modo” (1924) e “Questa sera si recita a soggetto” (1929), “Sei personaggi in cerca d’autore” (1921) è il primo di una trilogia di drammi in cui l’autore affronta la tipica situazione metateatrale in cui gli attori/personaggi/autori utilizzano lo spazio del teatro per mettere in scena un’altra rappresentazione: come in una scatola cinese.</p>
|
||
<figure>
|
||
<img src="images/sei-personaggi.jpg" alt="I sei personaggi" /><figcaption>I sei personaggi</figcaption>
|
||
</figure>
|
||
<p>La trama è piuttosto complessa, il palco è spoglio perché in attesa di allestimento per la messa in scena della commedia “Il gioco delle parti”, sempre di Pirandello, affidata alla <em>Compagnia degli Attori</em>. Nel corso della prima parte dello spettacolo avviene quello che si definisce <em>sfondamento della quarta parete</em>. Gli attori infatti non si trovano sul palco ma in mezzo alla platea, tra il pubblico. Dal fondo della sala, e non dalle quinte, fanno il loro ingresso <em>La Prima Attrice</em> e gli stessi <em>Sei personaggi</em>: <em>Il Padre, La Madre, Il Figlio, La Figliastra, La Bambina e Il Giovinetto</em>. Essi in realtà non sono altro che ombre, idee di un fantomatico <em>Autore</em> che, dopo averli creati, li ha abbandonati rinunciando a scriverne il romanzo o la commedia. Bloccati in questa specie di limbo i sei personaggi chiedono aiuto alla <em>Compagnia degli Attori</em> perché mettano in scena il loro dramma affinché possano raggiungere la completezza della loro creazione. La <em>Compagnia</em> accetta ma il risultato è deludente. La natura della personalità di ciascun personaggio è tanto complessa, così ricche di sfaccettature sono le loro emozioni, che il lavoro degli attori risulta finto e forzato.</p>
|
||
<h3 id="tema"><span class="header-section-number">3.2.1</span> Tema</h3>
|
||
<p>Alla fine dello spettacolo sono i personaggi stessi ad autorappresentarsi trasformando anche gli attori in pubblico in un continuo gioco di specchi. Pirandello mette l’accento sull’impossibilità di comporre il conflitto tra vita reale e finzione scenica e in sintesi sull’incapacità intrinseca del teatro di rendere sulla scena ciò che l’autore ha ideato.</p>
|
||
<h3 id="critica"><span class="header-section-number">3.2.2</span> Critica</h3>
|
||
<p>Presentato per la prima volta a Roma nel 1921 “Sei personaggi in cerca d’autore” fu dapprima contestato ferocemente dal pubblico al grido di “Manicomio, manicomio!”, impreparato ad un discorso di avanguardia che di fatto distruggeva le forme classiche del teatro convenzionale. Successivamente però il colossale fiasco si trasformò in un grande successo anche su scala mondiale.</p>
|
||
</body>
|
||
</html>
|