Logica intuizionistica e logicamodale: legame semantico e

calcolo

r.vincelli@campus.unimib.it

Indice

1 Logica intuizionistica 21.1 Costruttivismo . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21.2 Logica intuizionistica . . . . . . . . . . . . . . . . . . . . . . . . . 2

1.2.1 No RAA . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41.3 Semantica proposizionale . . . . . . . . . . . . . . . . . . . . . . 51.4 Semantica predicativa . . . . . . . . . . . . . . . . . . . . . . . . 71.5 Un calcolo a tableaux per la logica intuizionistica . . . . . . . . . 81.6 Correttezza e Completezza . . . . . . . . . . . . . . . . . . . . . . 11

1.6.1 Correttezza . . . . . . . . . . . . . . . . . . . . . . . . . . 111.6.2 Completezza . . . . . . . . . . . . . . . . . . . . . . . . . 11

2 Logica modale 122.1 Un percorso antico . . . . . . . . . . . . . . . . . . . . . . . . . . 122.2 S4 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 132.3 Semantica . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 142.4 Un calcolo dei sequenti per la logica modale S4 proposizionale . . 15

2.4.1 Il calcolo dei sequenti . . . . . . . . . . . . . . . . . . . . 152.4.2 Il sistema S4∗ . . . . . . . . . . . . . . . . . . . . . . . . . 162.4.3 La regola Cut . . . . . . . . . . . . . . . . . . . . . . . . . 18

2.5 Correttezza e Completezza . . . . . . . . . . . . . . . . . . . . . . 19

Introduzione

Scopo della relazione e illustrare il legame semantico tra la logica intuizionistica,la principale logica costruttiva, e la logica modale, la logica che incorpora i con-cetti di possibilita e necessita, cosı come la disponibilita di calcoli per entrambe,adatti alla dimostrazione automatica. Per il primo ambito centrale e il lavoro diSaul Kripke il quale, nel celebre [1], adatta la propria semantica modale anchealla logica intuizionistica. Per il secondo esaminiamo il calcolo a tableaux e deisequenti, il primo nella logica intuizionistica, il secondo nella modale.

1

1 Logica intuizionistica

1.1 Costruttivismo

Una dimostrazione in matematica puo essere costruttiva o meno: l’esistenzadegli enti su cui essa si basa puo consistere in una costruzione esplicita che listabilisce oppure essere inferita.In tal senso una dimostrazione costruttiva dell’espressione 2+3 = 5, per esempionella teoria di Peano, non puo essere una semplice deduzione bensı, in ordine, lacostruzione di 2, di 3, di 5 seguita da una costruzione che somma 2 a 3 ed unache equivalga questa somma a 5, e quindi serve fornire anche un algoritmo adefinire la funzione successore, la funzione somma e la funzione di verifica.Nell’approccio classico invece ci si fa bastare il dire che un’ente e possibile co-struirlo o, con la dimostrazione per assurdo, che non potendo essere, fatte leassunzioni richieste, il caso che non-esista allora deve per forza esistere.Questa corrente della filosofia matematica ha varie forme, la maggiore delle qua-li e il programma intuizionista di Brouwer. Il termine deriva dal fatto che laverita matematica e da intendersi come frutto di una costruzione mentale, con-cretizzata con la dimostrazione, e verificata dal matematico con mezzi propri,consistenti in conoscenze pregresse, a priori, dette intuizioni in filosofia.La logica formulata da Arendt Heyting a supporto della teoria di Brouwer e lalogica intuizionistica. Essa incarna questa esigenza di, in qualche modo, nondare nulla per scontato, ed e percio adatta. In termini moderni una qualsiasilogica di questo tipo e detta costruttiva. Perche una logica sia tale, assumendoi consueti simboli, deve verificare entrambe le seguenti proprieta:

� proprieta di disgiunzione: se φ∨ψ e un teorema allora almeno uno traφ e ψ e un teorema

� esplicita definibilita: se ∃x : φ(x) e un teorema allora esiste un termine(costante) t per cui φ(t) e un teorema

La piu nota logica costruttiva e la logica intuizionistica. Essa e stata fornitada Heyting a Brouwer a supporto del suo programma intuizionista, maggiorefilosofia matematica costruttivista.L’aggettivo “intuizionistica” e famoso in associazione al nome della logica co-struttivista principale appunto, ma si ritrova anche in rispetto ad altre famigliedi logiche. Per esempio esiste la logica modale intuizionistica, nella quale le duemodalita non sono interdefinibili (vedi 2.1).

1.2 Logica intuizionistica

Come linguaggio del sistema formale prendiamo tutti i connettivi e quantificato-ri del predicativo classico; non se ne puo lasciare fuori nessuno poiche non si hainterdefinibilita tra essi: cio e diretta conseguenza dell’interpretazione che ve-dremo tra poco. Una formula e un teorema se e possibile fornire una costruzioneche la costituisca; per questa sezione intenderemo col termine “dimostrazione”allora una non specificata costruzione che prova il teorema in questo senso. Lalogica intuizionistica preserva la giustificabilita, attraverso l’esibizione di un teo-rema, piuttosto che la verita, fissata nella logica classica attraverso un’apposita

2

funzione.Il significato dei connettivi e dei quantificatori, e percio delle formule, e alloraradicalmente diverso rispetto a quel che e nel predicativo classico. L’interpre-tazione sintattica tradizionale e la BHK (Brouwer-Heyting-Kolmogorov). I casibase relativi alle due proprieta di disgiunzione e testimone sono:

� A dimostra φ ∨ ψ se A = (b, c) con C che dimostra φ se b = 0, chedimostra ψ altrimenti; posso cioe trovare una dimostrazione dell’una odell’altra formula

� A dimostra ∃x : φ(x) se A = (b, c) con b ∈ D, dominio del discorso, Cche dimostra φ(b); posso cioe trovare un particolare valore adatto e ladimostrazione del teorema istanziato su di esso

Queste sono esattamente le due proprieta costruttive declinate nella logica in-tuizionistica. Se la formula φ ∨ ψ e un teorema allora almeno una delle dueformule lo e, ed e necessario fornire una dimostrazione per esse, giacche solo leformule dimostrate sono teoremi; il discorso e analogo per l’esistenziale.

Possiamo utilizzare un sistema formale adatto alla deduzione naturale, alla Pra-witz, prendendo proprio quello che gia conosciamo per il predicativo classico etogliendo una regola, RAA, riduzione all’assurdo. Il sistema INT e allora for-mato dalle seguenti regole di inserimento:

φ ψ

φ ∧ ψφ

φ ∨ ψψ

φ ∨ ψ[φ]....ψ

(φ→ ψ)

⊥φ

A(u)

(∃xA(x))

A(u)

(∀xA(x))

applicabile se u non e occorsa in nessuna assunzione precedente non scaricata

e di eliminazione:

φ ∧ ψφ

φ ∧ ψψ

3

φ ∨ ψ

[φ]....χ

[ψ]....χ

χ

φ φ→ ψ

ψ

∀xA(x)

A(u)

∃xA(x)

[A(u)]....B

B

applicabile se u non e occorsa in nessuna assunzione precedente non scaricata e nemmeno in

B

Inoltre, definendo ¬φ ≡ φ → ⊥ si possono derivare dalle proposizionali le ag-giuntive:

[φ]....⊥

(¬φ)

φ ¬φ⊥

Se togliamo anche EFQ otteniamo una logica chiamata minimale.

A differenza della logica classica non c’e modo di scrivere un connettivo in fun-zione di altri. Se fosse per esempio φ∨ ψ := (φ→ ψ)→ ψ con l’interpretazioneBHK vorrebbe dire che avere una dimostrazione di φ oppure di ψ equivale adavere una costruzione che trasforma una dimostrazione di φ → ψ in una di ψ,fatto che non si intende.

1.2.1 No RAA

Perche la riduzione all’assurdo non e costruttiva? In deduzione naturale classi-ca, essa permette ` ¬¬φ→ φ; infatti:

¬φ1 ¬¬φ2⊥

i⊥

φRAA, 1

¬¬φ→ φi→ 2

[¬φ]....⊥φ

RAA

In ottica costruttivista la ¬¬φ → φ per essere un teorema richiede una costru-zione che trasformi una dimostrazione di ¬¬φ in una di φ. Ora A dimostra¬¬φ se trasforma ogni dimostrazione B di ¬φ in una di ⊥, il falso, e questaB a sua volta dimostra ¬φ se trasforma ogni dimostrazione C di φ in una di⊥, e cio e impossibile, perche ⊥, per definizione se il sistema e consistente, nonha dimostrazione e percio C non puo essere mandato che nella dimostrazionevuota. Tutto quel che abbiamo in mano non e la dimostrazione di C, sappiamo

4

solo che non e trasformabile in una di ⊥.RAA deriva conclusioni forti da premesse deboli. Sia per esempio ¬(φ ∧ ψ) `¬φ ∨ ¬ψ: la premessa non ha dimostrazione, la conclusione e effettivamenteuna scelta. Facendo a meno di RAA, molti teoremi classici non valgono: trai famosi, oltre all’eliminazione della doppia negazione, anche il terzo escluso,infatti non c’e garanzia di poter costruire qualsivoglia dimostrazione, potrei ri-trovarmi a non avere ne la dimostrazione di φ ne quella di ¬φ. D’altro cantovale il principio di non-contraddizione: non e possibile da una parte avere unadimostrazione per φ e dall’altra avere la possibilita con essa, trasformandola, didimostrare il falso, che e indimostrabile. Infine come visto sopra una legge diDe Morgan non vale, mentre le altre tre sı.

In generale per ritornare alla logica classica o si reintegra RAA come regolao si aggiunge come assiomi almeno una tra eliminazione della doppia negazione,terzo escluso o legge di Peirce, ((φ→ ψ)→ φ)→ φ

1.3 Semantica proposizionale

In logica classica abbiamo due valori di verita. Nella logica intuizionistica nonsi ha un insieme naturale di valori, perche le formule si valutano per la loro pro-vabilita piuttosto che per una verita intrinseca basata sugli assegnamenti agliatomi.Ad un sistema classico si puo associare l’algebra di Boole minima ed avere unastruttura compatibile col sistema, con cui provare correttezza e completezza. Lostesso si puo fare con l’intuizionistica ma associando un diverso reticolo, un’al-gebra di Heyting: cosı facendo e ancora possibile associare valori “di verita” alleformule, anche se indirettamente. Come ribadiremo meglio in seguito pero lalogica intuizionistica e infinite valued.

Un modello e un’interpretazione di una formula che la rende vera. Se il mo-dello M soddisfa la formula φ si scrive M � φ. Se posso definire una strutturacomune a qualsiasi modello allora e possibile studiare formalmente la semanticadel linguaggio. Ad esempio per la predicativa classica si hanno le algebre diBoole come detto e la formula φ ∨ ψ e soddisfatta interpretando φ oppure ψcome il top nell’adB minima, e la concordanza sta nel fatto che il connettivo orcoincide con la funzione join sul reticolo.Per la logica intuizionistica esiste il corrispettivo delle adB, le Heyting comedetto, ma modello piu semplice ed adottato e la semantica di Kripke, introdottada S. Kripke in [1]. Si propone qui la forma presente in [2]. E’ una 4-upla(G, R, Γ0, �) con:

� (G 6= ∅, R) qoset (quasi-ordered set; la r. di accesso e riflessiva e transitiva,ed e quindi un preordine)

� Γ0 = min((G, R))

� �⊆ G× FBF (r. di forzatura)

La forcing relation rispetta le seguenti regole:

1. Γ � >, Γ 2 ⊥

5

2. se Γ � A, ΓR∆ allora ∆ � A

3. Γ � (X ∨ Y ) sse (Γ � X o Γ � Y ) (e duale per ∧)

4. Γ � ¬X sse ∀∆ ∈ G : ΓR∆, ∆ 2 X

5. Γ � X → Y sse ∀∆ ∈ G : ΓR∆ se ∆ � X allora ∆ � Y

∀Γ ∈ GA atomo, ∀X, Y ∈ FBF .

G e l’insieme dei mondi possibili, espressione che gia di per se sa tipicamen-te di logica modale e risale a Leibniz, o meglio degli stati di conoscenza. QuindiΓ e una serie di fatti nota in un certo istante temporale. La relazione R puointendersi come possibile successione temporale e quindi causalita, e dalle regolequel che e noto in t lo sara ancora in t+ 1.Le formule valide sono quelle vere in qualsiasi modello di Kripke, e costitui-scono l’insieme dei teoremi intuizionistici. Una formula X e vera in G sse∀Γ ∈ GΓ � X. Se una formula non e vera in G allora e possibile costruire uncontromodello, ossia un modello in cui non e vera. Quel che si puo fare e, perogni stato, forzare od anti-forzare atomi; quindi la strategia prevede, fatto uncerto numero di forzature ed antiforzature, dedurre attraverso le regole dellasemantica in un particolare stato la non-forzatura della formula non vera. Peresempio:

� ΓR∆

� Γ 2 A (a), ∆ � A (b)

� (b)4⇒ Γ 2 ¬A 4⇒ Γ � ¬¬A 5⇒ Γ � ¬¬A → A

� quindi ¬¬A → A e un non-teorema (eliminazione doppia negazione)

Con lo stesso contromodello si puo anche mostrare Γ � ¬A ∨ A (tertium nondatur).Per dire invalida una fbf basta un modello che non la soddisfi, ed appunto lastrategia e forzare variabili e dedurre attraverso le regole.Un fatto criticato di questa semantica e che, nei singoli nodi, una formula edetta essere semanticamente deducibile o meno con un approccio classico, e noncostruttivista.Ad ogni modo questa semantica non e bivalente, in armonia con l’interpretazioneBHK e col fatto che l’intuizionistica non sia pero nemmeno a valori finiti. Non eper esempio il caso della logica trivalente adoperata in informatica nei database,per la quale si avrebbe provato teorema, provato non-teorema, ignoto. E’ statomostrato da Goedel che non v’e realizzazione a numero finito d’elementi per laquale solo le fbf dimostrabili intuizionisticamente, e solo queste, siano soddisfat-te. In pratica non ho V = {v1, . . . , vn} che assegno come valore agli atomi econ il quale possa costruire una f : FBF → V tc f(φ) = vi sse � φ. Goedelha inoltre mostrato che esistono infinite logiche proposizionali intermedie tral’intuizionistica e la classica; esse formano un reticolo con bottom la prima e topla seconda. In [3] si prova che delle logiche intermedie proposizionali quelle chesono costruttive tout-court secondo la proprieta di disgiunzione e massimali nelsottoreticolo delle costruttive hanno la cardinalita del continuo.

6

1.4 Semantica predicativa

Il modello di Kripke predicativo ha una definizione diversa: (G, R, Γ0, �, P )con P : G → P(D) r ∅, Γ∗ un qualsiasi ∆ tc ΓR∆, ¯P (Γ) l’insieme di tutte lefbf costruibili con costanti in P (Γ). Le condizioni soddisfatte sono:

1. P (Γ) ⊆ P (Γ∗)

2. se Γ � A allora A ∈ ¯P (Γ)

3. se Γ � A allora Γ∗ � A

4. Γ � (X ∧ Y ) sse (Γ � X e Γ � Y )

5. Γ � (X ∨ Y ) sse (X ∨ Y ∈ ¯P (Γ) e Γ � X o Γ � Y )

6. Γ � ¬X sse (¬X ∈ ¯P (Γ) e per tutti Γ∗, Γ∗ 2 X)

7. Γ � (X → Y ) sse ((X → Y ) ∈ ¯P (Γ) e per tutti Γ∗ se Γ∗ � X allora Γ∗ � Y

8. Γ � ∃xX(x) sse per un qualche a ∈ P (Γ) Γ � X(a)

9. Γ � ∀xX(x) sse per tutti Γ∗ a ∈ P (Γ∗) Γ∗ � X(a)

La soddisfazione di una formula in un modello e analoga: ∀Γ ∈ G : X ∈¯P (Γ) Γ � X.

Il significato di P e quello di assegnare ad ogni stato di conoscenza tutte e solele costanti note in esso; si assume che non sia possibile non conoscere costantealcuna, si ha infatti r∅ nella posizione, anche nello stato di partenza Γ0. Questeregole includono le proposizionali ed in particolare osserviamo che:

� con la 1 diciamo che le costanti, una volta note, rimangono sempre

� con la 2 che un atomo, che e un predicato su m costanti, se e forzato allorao m = 0 o sono tutte note

� 8: i parametri possono assumere solo valori di costante noti

� 9: si richiede che la formula non solo valga per le costanti gia note maanche per tutte quelle a venire

Es. di contromodello per ∀x(A ∨B(x))→ (A ∨ ∀xB(x)):

� Γ1RΓ2

� P (Γ1) = {1} Γ1 = B(1); P (Γ2) = {1, 2} Γ2 � B(1), A

� vale Γ1 � ∀x(A ∨B(x)) infatti:

– Γ1 � A ∨B(1) poiche Γ1 � B1

– Γ1 � A ∨B(2) poiche Γ1 � A

� e vero anche che Γ1 2 A, Γ1 2 ∀xB(x) (infatti Γ2 2 B(2)) e quindi risultaΓ1 2 A ∨ ∀xB(x)

� e percio Γ1 2 ∀x(A ∨B(x))→ (A ∨ ∀xB(x))

7

1.5 Un calcolo a tableaux per la logica intuizionistica

Per la dimostrazione automatica di teoremi la deduzione naturale non si riveladi facile utilizzo, anzitutto per il non essere goal-oriented e basarsi su euristi-che per la scelta della strategia. Il calcolo dei tableaux analitici e, assiemeal calcolo dei sequenti, la scelta nel caso si voglia costruire un dimostratoreautomatico sufficientemente efficace. La dimostrazione nel calcolo a tabelle eun processo di refutazione: l’obiettivo e mostrare, informalmente, che indicarecome falsa la formula porta ad una contraddizione ed e quindi il caso che essae un teorema. Il processo e incentrato sulla riduzione all’assurdo ma cio non eovviamente un problema dato che si opera a livello superiore. I metodi a tabellehanno il vantaggio di poter incorporare l’interpretazione e la natura della logicaattraverso regole facilmente implementabili. L’obiettivo e, partiti dalla formulada dimostrare, arrivare ad una contraddizione sui letterali, es {A, ¬A} da cuidedurre il falso e quindi il teorema.

Per la logica intuizionistica si ha un calcolo base in [2]. Tale calcolo pero hail problema di assumere, per ogni regola, la possibilita di dover riutilizzare laformula cui la si applica, il cosiddetto problema della duplicazione. Volendoimplementare il metodo in un dimostratore automatico al calcolatore la dupli-cazione e un impatto sulle prestazioni del programma. Un calcolo che mitiga laproblematica e quello di [4]:T-regole:

S, T (A ∧B)

S, TA, TB

S, T (A ∨B)

S, TA/S, TB

S, T (A→ B)

S, FA/S, TB

con A atomo o negata

S, T ((A ∧B)→ C)

S, T (A→ (B → C))

S, T ((A ∨B)→ C)

S, T (A→ C), T (B → C)

S, T ((A→ B)→ C)

S, F (A→ B), T (B → C)/S, TC

S, T (∃xA(x)→ B)

S, T (∀x (A(x)→ B))

S, T (∀x, A(x)→ B)

S, F∀xA(x), T (∀x, A(x)→ B)/S, TB

F -regole:

S, F (A ∧B)

S, FA/S, FB

8

S, F (A ∨B)

S, FA‖S, FBS, F (A→ B)

Sc, TA, FB

S, F (¬A)

Sc, TA

S, F∀xA(x)

Sc, FA(a)

con a nuovo

S, F∃x, A(x)

S, FA(a)

Fc-regole:

S, Fc(A ∧B)

Sc, FcA/Sc, FcB

S, Fc(A ∨B)

S, FcA, FcB

S, Fc(A→ B)

Sc, TA, FcB

S, Fc(¬A)

Sc, TA

S, Fc∀xA(x)

Sc, FA(a), Fc∀xA(x)

con a nuovo

S, Fc∃xA(x)

S, FcA(a), Fc∃xA(x)

In classica T ed F indicano una formula vera, falsa e le conclusioni di unasingola regola seguono in necessita dalla premessa: se e il caso di queste, lo eanche delle prime. La dimostrazione e per refutazione: per mostrare TX assu-mo FX ed arrivo a {TY, FY } (chiusura tavola).In intuizionistica, TX sta per il fatto che X e provata, FX non si sa, puo ancheessere dimostrabile ma la prova non la si possiede ancora. Le conclusioni sonocompatibili con le premesse, sono possibili. La refutazione sta nell’asserire unaformula sia come gia sia come non provata, e cio si puo fare anche arrivando aTX, FcX.Il segno FcX e stato introdotto durante il percorso di avvicinamento ad un cal-colo ottimale rispetto al problema della duplicazione di cui sopra, ed e la falsitacerta: FcX ⇔ Γ � ¬X. Sapendo che TX ⇔ Γ � A, FX ⇔ Γ 2 X, Fc e piuforte di F e quindi pure {TX, FcX} e una chiusura. La falsita di F e locale:so che nel nodo corrente la formula non e presente, ma in un Γ∗ puo diventarlo.

9

La falsita di Fc e invece globale: essendo FcX ⇔ Γ � ¬X, per la regola sul ¬ e∆ 2 X ∀∆ : ΓR∆.Questo segno rende allora esplicita una importante differenza tra due diversenon-validita: la sintassi illumina la semantica, svelando la natura three-valueddella semantica la logica di per se essendo pero, ribadiamo, a valori infiniti.La regola F∨ richiede una scelta tra uno dei due rami: non un branch maun’operazione nondeterministica. Suo spirito e incorporare il principio di di-sgiunzione forzando a provare una delle due formule, ed una sola, entrambe esuperfluo: Se X ∨Y e dimostrabile allora mi basta una tra X ed Y dimostrabilee percio nella tabella perseguo FX per arrivare alla chiusura (o in alternativaFY ). Cosı facendo e eliminata una ridondanza-ripetizione implicita nella FVsenza scelta.Per →, ad ognuna delle classi di antecedente individuata si associa una formu-la diversa. La scelta ha come obiettivo minimizzare le duplicazioni. Le regoleT → ∧, T → ∨ sono trasformazioni nel senso che la formula derivata e intui-zionisticamente equivalente all’antecedente; la duplicazione e evitata poiche lederivate hanno antecedenti di grado minore che le premesse, dove il grado e ilnumero di connettivi. La regola T →→ e classica, decompone non trasforma,ed anche qui le formule derivate sono inferiori in grado di uno. La natura dellesottoregole T → e percio piu sintattica che semantica, nell’ottica dell’ottimiz-zazione.Infine consideriamo, a titolo d’esempio della diversita del tableaux intuizionisti-co rispetto al classico, il significato di F →. Se non abbiamo ancora provatoX → Y e lecito pensare che si riesca a provare X ma non Y , che la prova delprimo non si possa trasformare in una del secondo, seguendo la definizione in-tuizionistica di →. Assumendo questo scenario dimostrare X puo portare, perS l’insieme delle formule segnate correnti, alla dimostrazione di S ∈ S (es. valeX → S). Siccome cio e solo possibile, non necessario, portiamo avanti solo leformule T ed Fc segnate, tutte e sole le formule in S stabili al momento dell’ap-plicazione, formule di cui si ha gia prova o controprova.Il calcolo e facilmente interpretabile rispetto alla semantica di Kripke: le T-segnate sono forzate nel nodo ed in tutti gli accessibili, le Fc sono non-forzatein esso ed in tutti gli accessibili, le F sono non-forzate nel nodo. Per un setS realizzato nel nodo corrente, applicare una regola da un S′ realizzato nellostesso o in altri, per esempio:

� Γ = St

⋃{X ∨ Y } T∨⇒ ∆′ = St

⋃{X}, ∆′′ = St

⋃{Y }

� Γ = StF→⇒ ∆ = St

⋃{X}

Come sistema di riscrittura, il calcolo non gode della proprieta di Church-Rosserneanche al proposizionale: l’ordine di esecuzione delle mosse conta, non c’e ne-cessariamente confluenza. In caso di scelta e allora necessario annotare il puntoper un eventuale backtrack. Questo calcolo solleva, a livello proposizionale, dallanecessita di duplicare. Esso e alla base del theorem prover predicativo PITP([5]), il cui calcolo pero e differente principalmente nei seguenti punti:

� ritorno alla F∨ classica: la versione nondeterministica ha probabilita, apriori, .5 di determinare backtrack

10

� modifica delle T → regole, specie la T →→ alfine di migliorare la com-plessita spaziale

� regole repl e simpl: queste nuove regole riducono branching e backtrackinge sostituiscono T∨ e T∧ con una particolare regola detta di bivalenza

� principio di simmetria: permette d’inferire sul segno di una formula apartire da quello di un’altra ad essa uguale a meno di una permutazionedelle sue variabili; ha rilevanza semantica

1.6 Correttezza e Completezza

Illustriamo a grandi linee la dimostrazione della correttezza e completezza delcalcolo fornito, seguendo la linea dei lavori che descrivono il calcolo stesso nellasua evoluzione, [6], [4], [5]; il calcolo basico e quello di [2].

1.6.1 Correttezza

Correttezza: se una tavola per FA e chiusa allora A e intuizionisticamente va-lida.Un insieme {TX1, . . . TXn, FY1, . . . FYm} e realizzabile se esiste un modello conΓ tc Γ � Xi, Γ 2 Yj ∀i, j. Una configurazione C e una famiglia di insiemi diquesto tipo ed e realizzabile se almeno uno di essi lo e.Sia C1 . . . Cn un tableau; se Ci e realizzabile allora anche Ci+1 lo e. Per dimo-strarlo si hanno tanti casi quante sono le regole, poiche Ci+1 puo essere generatoda una qualsiasi.Per T∨ ad esempio si ha Ci = {. . . , {S, T (X∨Y )}, . . .}, Ci+1 = {. . . , {S TX}, {S, TY }, . . .}(ho applicato T∨). Poiche Ci e realizzabile un suo elemento lo e. Se non e{S, T (X ∨ Y )} allora quello che e lo e pure in Ci+1, la regola non lo tocca. Selo e allora Γ realizza {S, T (X ∨ Y )} ossia S e T (X ∨ Y ). Per il secondo valeΓ � X, Γ � Y seguendo la regola del modello, e dev’essere, combinando, che Γrealizza {S, TX} oppure {S, TY }.Esaminiamo ora Ci = {. . . , {S, T (X → Y )}, . . .} con X atomo o negato; ap-plicando la regola otteniamo Ci+1 = {. . . , {S, TY }, {S, FX}, . . .}. Sia subito{S, T (X → Y )} la realizzata: vale Γ � S, Γ � X → Y . Seguendo la regola per→ abbiamo due casi. Uno e Γ � X ossia TX ∈ S: necessariamente Γ � Y equindi ho {S, TY } realizzato. L’altro e Γ 2 X ossia FX ∈ S (ricordando chedobbiamo sostituire al ∆ della regola il presente Γ).

Se `Int X allora X e valida. Dimostriamolo per contrapposizione: se X non evalida allora 0Int X. Se non e valida esiste almeno un Γ tc Γ 2 X ossia {FX} erealizzabile. Una derivazione per X sarebbe una tavola C1, . . . , Cn chiusa, conC1 = {FX}. C1 e realizzabile, ed abbiamo appena mostrato che se lo e alloraanche Ci>1 lo e. Non ci puo essere allora una dimostrazione di X, perche dovreiavere una Cn realizzabile ma chiusa cioe tale per cui, per una certa φ ho un∆ : ΓR∆ ∆ � φ, ∆ 2 φ �

1.6.2 Completezza

Come per qualsiasi altro calcolo su qualsiasi altra logica, dato un insieme con-sistente, cioe non contraddittorio, di formule, se ne costruisce un modello. Per

11

esempio Goedel dimostra la completezza predicativa basandosi su un sistemadeduttivo dato corretto ed un modello generico, ma e possibile declinare.

La dimostrazione risulta complessa. Il primo teorema da mostrare e il seguente:se I e un insieme di segnate consistente allora esiste un modello K con radiceΓ0 tale che I sia realizzato in esso. La dimostrazione consiste nella costruzionedi K e si divide in due fasi:

� costruzione di Γ0 suddividendo le formule in gruppi

� costruzione del successore, in stile analogo

La procedura e ripetuta ricorsivamente a costruire l’albero.Il secondo e invece: per ogni insieme di segnate consistente I, per ogni modellocostruibile con tale algoritmo KI , per ogni suo nodo S ed ogni formula H ∈ S∗nei successori rispetto a S, H e realizzata in S. La dimostrazione e per indu-zione sul grado delle formule, ancora con un caso per ciascuna regola.Si puo ora dimostrare la completezza: supponendo il contrario, X e intuizioni-sticamente valida e non c’e una tavola chiusa per FX ossia non e dimostrabilenel calcolo; se cosı e allora {FX} e un insieme consistente ma il risultato diceche ogni insieme di segnate consistente e realizzabile, quindi anche {FX}, il checontrasta con fatto che X e intuizionisticamente valida �Con il teorema abbiamo una strategia che consente, per ogni insieme I di formu-le segnate consistenti, di costruire un modello la cui radice lo realizza. Inoltre,siccome per ogni X non-teorema {FX} e consistente e possibile ottenere uncontromodello; nel caso predicativo, essendo la predicativa indecidibile, essopuo essere infinito, anche se regolare. Il modello/contromodello ottenuto non enecessariamente minimale.

2 Logica modale

2.1 Un percorso antico

Aristotele e comunemente indicato come l’iniziatore della logica modale: nelsuo sillogismo categorico, formato da tre cosiddette proposizioni categoriche,ossia di struttura affermativa o negativa soggetto+predicato, contempla ancheil modo della proposizione, che definisce in che termini il predicato e verifica-to. I modi previsti da Aristotele sono l’effettivita, la necessita, la possibilita,la contingenza e l’impossibilita. I sillogismi modali nell’Organon sono 125. Ilpensiero modale aristotelico e ripreso ed approfondito nella scolastica, per laquale Aristotele e certamente pensatore di riferimento: a questo proposito e daricordare sicuramente il lavoro di S. Tommaso d’Aquino ma anche S. Anselmoche, con la propria prova ontologica e iniziatore di un filo rosso il cui legamecon la modalita si spinge fino alla logica formale moderna con Goedel, che neassiomatizza l’argomento. Infine, Guglielmo di Occam, il pensatore cui si attri-buisce il principio di semplificazione noto come Ockham’s razor, offre circa 1000sillogismi modali ed elabora circa la distinzione tra modalita intesa sensu com-posito, in cui il modo della possibilita coincide effettivamente con la contingenzaaristotelica e sensu diviso per la quale la modalita e predicata direttamente sulsoggetto in atto, intendendo atto alla aristotele. La logica modale e ripresa do-po un lungo iato nell’ ’800, con il presentarsi della logica formale: e registrato

12

principalmente interesse da una parte alla definibilita delle modalita in terminifilosofici, evitando circoli viziosi, dall’altra alla formalizzazione ed alle relazionicon l’algebra di tali formalizzazioni. Questo secondo aspetto culmina con la de-finizione dei sistemi S1,. . . , S5 ad opera di C. I. Lewis ([7]). Oltre alle modalitaaristoteliche, chiamate aletiche poiche concernenti la verita del predicato, sonostate discusse e formalizzate anche modalita deontiche, “e o meno obbligatorioche”, epistemiche, “e noto o meno che”, le quali sono state messe in relazio-ne concettualmente con l’interpretazione intuizionistica della logica BHK cheabbiamo dato in 1.2, ed infine d’apparenza, “e creduto o meno che”. Particola-re importanza applicativa riveste la modalita temporale: sono state sviluppatevarie logiche temporali adatte al model checking, cioe alla verifica formale di pro-prieta nella specifica di un programma; famosa e la logica CTL (computationtree logic), appartenente alla famiglia delle branching-time logic per la quale esi-ste un calcolo a tableau sia proposizionale sia predicativo [8]. La varieta modalepiu nota resta l’aletica: nella sua sotto-variante classica necessita e possibilitasono definibili l’una in termini dell’altra attraverso negazione; cio non vale perla logica modale intuizionistica. Per una panoramica sulla storia della logicamodale non parca di riferimenti dettagliati ci si puo riferire all’Introduzione di[9] e complementarmente a [10].

2.2 S4

La famiglia delle logiche formali modali e, come possiamo intuire, vasta. Lanostra attenzione e rivolta alla S4 di Lewis, che la propose in forma alla Hilbert.Ci limitiamo alla versione proposizionale; R. C. Barcan ha in seguito estesoanche al predicativo essa assieme ad S2 ed S5. Questa scelta e in virtu delleseguenti motivazioni:

� S4 e la logica intuizionistica presentata sono fortemente legate dal puntodi vista semantico

� ne esistono molti calcoli dei sequenti e si puo cogliere l’occasione per con-frontare questo tipo di calcolo con il calcolo a tabelle; oltre a quello chediscuteremo un’ampia trattazione si ha in [11]

La logica S4 e solitamente definita in uno dei due modi equivalenti:

� estendendo la S1

� estendendo la K

La seconda definizione esplicita per S4 l’attributo di logica modale normale; ilfatto che S4 e invece classica nel senso anticipato alla fine di 1.1 e chiaro giaestendendo da S1. Definiamo S4 nel secondo modo.

A livello di linguaggio introduciamo due nuovi simboli, 2, che denota la moda-lita della necessita, e 3 per la possibilita; poniamo 2 ≡ ¬3¬ (e viceversa). Ke la logica di Kripke, la piu piccola logica che soddisfa le seguenti:

� contiene tutti i teoremi proposizionali classici

� contiene tutte le istanze dello schema 2(A → B) → (2A → 2B) (distri-butivita di 2 su →)

13

� e chiusa rispetto al modus ponens

� e chiusa rispetto alla necessitation rule ` A⇒` 2A

In K e lasciata liberta circa quel che segue da 2A: per esempio la necessitasemplice non determina una “necessita necessaria”, e la proposizione potrebbeessere solo contingentemente necessaria. Si aprono allora varie possibilita. Se ilrimedio scelto e aggiungere l’assioma di riflessivita

2A→ A

la logica modale che si ottiene e chiamata T, e contiene K. Se 2 in T e ulte-riormente caratterizzato aggiungendo la legge di transitivita

2A→ 22A

la logica ottenuta e S4. Questi due assiomi hanno un forte legame con lasemantica di Kripke, come vedremo tra poco. Il numero di modalita, ossiasequenze di ¬, 2, 3, distinte di S4 e pari a 7 senza contarne le negazioni:cio e possibile solo avendo introdotto la precedente, infatti in T sono infinite([9]). La costruzione di diverse logiche modali e le loro relazioni sono trattateesaustivamente in [13].

2.3 Semantica

La semantica di Kripke che abbiamo visto per la logica intuizionistica in 1.3 fucome detto originariamente pensata dall’autore per una logica modale. Per S4la definizione e ([2]): (G, R, Γ0, �) con:

� (G 6= ∅, R) qoset (quasi-ordered set; la r. di accesso e riflessiva e transitiva,ed e quindi un preordine)

� Γ0 = min((G, R))

� �⊆ G× FBF (r. di forzatura)

La forcing relation rispetta le seguenti regole:

1. Γ � >, Γ 2 ⊥

2. Γ � (X ∨ Y ) sse (Γ � X o Γ � Y ) (e duale per ∧)

3. Γ � ¬X sse Γ 2 X

4. Γ � X → Y sse (Γ 2 X o Γ � Y )

5. Γ � 2X sse per tutti Γ∗, Γ∗ � X

∀Γ ∈ G; ∀X, Y ∈ FBF .

Osserviamo che, esattamente come per l’intuizionistica, la relazione R e unpreordine. Le regole per ∨ e ∧ sono invariate. La persistenza degli atomi non

14

e esplicita poiche, grazie alla regola di necessita, ogni atomo vero e mantenutoattraverso la regola per 2. La 3 e equivalente alla controparte in modo analo-go. La 4 invece e in questa forma sfruttando il fatto che in logica classica valeX → Y ↔ ¬X ∨ Y .Tale “parentela” e formalizzata nella seguente (vedi [2]): se X e una formula inInt, X e valida se e solo se M(X) e valida in S4 dove M mappa formule dellaprima in formule della seconda attraverso tale schema:

M(A) = 2A

M(X ∨ Y ) = M(X) ∨M(Y )

M(X ∧ Y ) = M(X) ∧M(Y )

M(¬X) = 2¬M(X)

M(X → Y ) = 2(M(X)→M(Y )

∀A atomo; ∀X, Y ∈ FBFQuesta traduzione e nota come traduzione di Goedel-McKinsey-Tarski. Puoessere applicata anche alle regole d’inferenza applicando a ciascuna formula cheappare la mappa M . Ricordando la traduzione da Cl ad Int a livello proposizio-nale attraverso la doppia negazione del teorema di Glivenko, una formula di Clpuo essere mandata in S4. La traduzione GMT puo essere estesa al primordine([14]).Infine, 2X → X richiede R riflessiva, come possiamo vedere dalla regola 5.2X → 22X la vuole transitiva; poniamoci in un Γ tale che Γ � 2X ed indivi-duiamo ∆ e Σ tali che ΓR∆, ∆RΣ; per la transitivita vale ΓRΣ e leggendo il⇐ nella 5 vale ∆ � 2X, Γ � 22X.

2.4 Un calcolo dei sequenti per la logica modale S4 pro-posizionale

2.4.1 Il calcolo dei sequenti

Il calcolo dei sequenti fu introdotto da G. Gentzen nel ’34 come evoluzione delladeduzione naturale e da egli stesso formalizzato nei sistemi LK ed LJ per lalogica classica ed intuizionistica predicative rispettivamente.Per meglio comprendere la natura del calcolo dei sequenti, tracciamo un bre-ve confronto con il calcolo alla Hilbert e la deduzione naturale. Un confrontoesclusivo con il calcolo a tableau e invece in 2.5.

Il task principale di un sistema alla Hilbert e la deduzione di teoremi, leformule che sono tautologie. L’insieme dei giudizi, ossia delle asserzioni otteni-bili sulle formule a partire dalle derivazioni in cui esse compaiono, coincide conle formule stesse: infatti la natura stessa dei sistemi alla Hilbert, sbilanciati sul-l’assiomatizzazione, non permette il ragionamento ipotetico. Detto altrimenti,ad ogni passo di una dimostrazione in questo calcolo siamo sicuri di avere unteorema, sia esso vecchio o nuovo, cioe assioma del sistema o nuovo risultato.In essi si fa forte uso del teorema di deduzione.Il calcolo della deduzione naturale, che incorpora nella regola i → questometateorema, si presenta come espressivamente piu ricco: e possibile esplicita-mente porre assunzioni e derivare formule che non sono teoremi della logica ma

15

sono vere solo in virtu delle assunzioni stesse, un ragionamento ipotetico. Cio ediretta conseguenza del fatto che le regole della deduzione naturale permettono,con la loro maggiore complessita, una gestione dinamica del contesto, ossia delnumero di assunzioni correnti. I giudizi sono di forma S ` φ dove S e un insiemedi formule vuoto se φ e un teorema, mentre se e teorema perche sia tautologiatutte le formule di S devono essere vere.Nella deduzione naturale il succedente e al massimo una formula, e cio e esatta-mente quel che ci aspettiamo per la forma delle regole. Il calcolo dei sequentiinvece supera questa limitazione ed ha giudizi di forma S ` T dove S e T sonosequenze di formule di cardinalita qualsiasi, anche vuota; piu comodamente as-sumiamo S e T multinsiemi. La semantica e la seguente: ogni volta che tutte leformule di S sono vere, almeno una formula di T lo e pure; l’intera scrittura edetta sequente e da questo fatto osserviamo che in S le formule sono congiunte,in T disgiunte. Se S = ∅ allora la disgiunzione rappresentata da T e un teorema;se invece T = ∅ allora la congiunzione delle formule in S e una contraddizione.

2.4.2 Il sistema S4∗

In precedenza abbiamo mostrato come costruire S4 a partire dalla logica classi-ca, e queste radici della logica saranno esplicitate anche nel calcolo. Per meglioapprezzare il calcolo dei sequenti poniamo esplicitamente l’LK di Gentzen comebase; alternativamente e possibile costruire per ogni φ teorema classico l’assio-

ma ` φ ed aggiungere poi solo la caratterizzazione modale.Iniziamo con l’esaminare LK. In esso si hanno tre tipi di regole:

� assiomi: come consueto, sono regole dalla premessa vuota

� regole speciali: LK ha una sola regola speciale, Cut, che discutiamo in2.4.3; talvolta comprese nelle strutturali

� regole logiche: introducono una nuova formula in S (sinistre) o T (destre)

� regole strutturali: modificano la struttura dell’antecedente o del succeden-te modificandone la sequenza

Assiomi:

A ` Aid

Regole speciali:Γ ` ∆, A A, Σ ` Π

Γ, Σ ` ∆, ΠCut

Regole logiche classiche:

Γ, A ` ∆

Γ, A ∧B ` ∆∧L1

Γ, B ` ∆

Γ, A ∧B ` ∆∧L2

Γ ` A, ∆

Γ ` A ∨B, ∆∨R1

Γ ` B, ∆

Γ ` A ∨B, ∆∨R2

Γ, A ` ∆ Σ, B ` Π

Γ, Σ, A ∨B ` ∆, Π∨L

Γ ` A, ∆ Σ ` B, Π

Γ, Σ ` A ∧B, ∆, Π∧R

Γ, A ` ∆ Σ, B ` Π

Γ, Σ, A→ B ` ∆, Π→L

Γ, A ` B, ∆

Γ ` A→ B, ∆→R

16

Γ ` A, ∆

Γ, ¬A ` ∆¬L

Γ, A ` ∆

Γ ` ¬A, ∆¬R

Regole strutturali:Γ ` ∆

Γ, A ` ∆WL

Γ ` A, ∆

Γ ` ∆WR

Γ, A, A ` ∆

Γ, A ` ∆CL

Γ ` A, A, ∆

Γ ` A, ∆CR

Qualche considerazione sulle regole:

� l’assioma d’identita e dimostrabile in deduzione naturale assumendo A edusando i→

� ∧L1, ∧L2, ∨R1, ∨R2 sono tipiche regole classiche, semplicemente viste alivello di contesto; trasformano la formula dalla quale sono richiamate

� ∨L, ∧R, → L si possono utilizzare per collegare due rami separati nelladimostrazione, un uso comune e usarli sul ramo principale e l’assioma;alternativamente, il sequente corrente puo essere mappato in entrambiquelli della regola

� → R e il teorema di deduzione

� ¬L: Γ ∧ ¬A → ∆ e un teorema sia se A e ∆ sono entrambi veri, sia sesolo uno dei due lo e; analogamente per ¬R

� WL e una regola di indebolimento, cui scopo e poter aggiungere ipote-si arbitrarie ed incarna la monotonicita classica; osserviamo che non eun problema rendere l’antecedente contraddittorio (aggiungere A ma vale¬A ∈ Γ) perche la formula ottenibile via t. di deduzione e comunque siaun teorema (eg ¬(A ∧A)→ B); il discorso e speculare per WR

� CL e CR permettono di eliminare risorse duplicate dal multinsieme

Siamo ora pronti per evolvere ad S4. Il primo famoso calcolo dei sequentimodale risale al ’51 con in un lavoro di von Wright. Il calcolo che presentiamoe quello discusso in [12], che nello stesso lavoro e mostrato essere equivalente eper il quale e dato anche un Haupsatz (vedi 2.4.3. Richiede semplicemente diaggiungere le seguenti regole logiche:

A, ∆ ` Γ

2A, ∆ ` Γ2L

2∆ ` A2∆ ` 2A

2R

Sono importanti le seguenti osservazioni:

� 2∆ richiede di prefiggere 2 ad ogni formula di ∆

� non e necessario aggiungere esplicitamente il modus ponens; il perche ediscusso in 2.4.3

� la regola di necessitazione e istanza particolare di 2R per ∆ = ∅

17

� riflessivita e transitivita sono presenti come teoremi: la prima si ottienecon < id, 2L, → R > la seconda con < id, 2R, → R >

� la distributivita di 2 e anch’essa teorema con la seguente derivazione, chepresentiamo anche ad esempio; la sua costruzione e illustrata in 2.5:

A ` Aid B ` B

id

A, B ` BWL

A, A→ B ` A, B→L

A, A→ B ` BWR

2A, A→ B ` B2L

2A, 2(A→ B) ` B2L

2A, 2(A→ B) ` 2B2R

2(A→ B) ` 2A→ 2B→R

` 2(A→ B)→ (2A→ 2B)→R

ponendo in → L ∆ = Σ = {A}, Π = {B}, Γ = ∅

2.4.3 La regola Cut

La regola di (short)cut ci dice che quando una formula A puo essere conclusa eservire anche da premessa per concluderne altre, allora A puo essere “tagliatafuori” e si puo collegare direttamente le derivazioni, prendere una scorciatoia.Nel ’34 Gentzen dimostro un teorema conosciuto come Hauptsatz (proposizioneprincipale), per il quale, per ogni dimostrazione che nel calcolo dei sequenti LJo LK fa uso di questa regola ne esiste una equivalente (forma normale), ossiache dimostra lo stesso teorema, che non ne fa uso; inoltre il metateorema e co-struttivo poiche e illustrata una procedura algoritmica per costruire tale formulacut-free. Cio fa della regola una regola ammissibile, ossia in pratica da include-re facoltativamente poiche semplifica (e di molto, per curiosita possiamo vedereun teorema “patologico” in [15]) ma e invariante alla completezza del sistema.Osserviamo che essendo la regola ammissibile sia in LJ sia in LK rappresentaun legame notevole tra le due logiche. Il cut e ammissibile anche nel sistemapresentato (cio e mostrato direttamente in [12]).

In generale per i sequenti in cui vale la cesura e uno strumento per verificarela consistenza del sistema. L’ammissibilita del cut si puo mostrare che implicauna proprieta di sottoformula che ci dice che ogni formula in una derivazionecut-free e sottoformula di una che appare nella conclusione. Ipotizziamo che `sia derivabile; allora per l’Haupsatz ne esiste una derivazione cut-free, ed es-sendo tale rispetta la proprieta di sottoformula. Ma cio non e possibile, nonsapremmo letteralmente cosa mettere ai piani sopra ` perche sarebbero lecitesolo formule vuote, una sequenza e incostruibile; percio rifiutiamo l’ipotesi ed ilcalcolo viene ad essere consistente.Come detto, e possibile ottenere algoritmicamente una derivazione cut-free dauna che presenta l’uso della regola. La corrispondenza di Curry-Howarde un complesso ma assai rilevante e significativo framework con il quale met-tere in relazione diretta dimostrazione e computazione ed aprirsi per esempioalla stesura automatica di programmi corretti per costruzione, dove la specifi-ca rispettata e quella codificata dalla dimostrazione. Per il calcolo dei sequenti,

18

l’interpretazione di una singola eliminazione di cut e l’essere un passo di compu-tazione in una qualche macchina astratta scelta. Se prendiamo in considerazioneil Lambda calcolo piu precisamente abbiamo una β-riduzione, cioe il posizio-namento dell’argomento λx.fa . f [a/x], e la successiva valutazione.

Nel definire un calcolo dei sequenti per S4 la logica modale di Kripke richiedela chiusura dell’insieme dei teoremi rispetto al modus ponens ma in realta lacesura e gia sua generalizzazione. Consideriamo la regola:

Γ ` A A, ∆ ` BΓ, ∆ ` B

essa e istanza di Cut. D’altro canto se applichiamo → R a A, ∆ ` B otteniamo∆ ` A→ B e la regola di sopra e il modus ponens nei sequenti.

2.5 Correttezza e Completezza

La chiave alla correttezza delle formule di S4∗ e ricordare che i sequentiA1, . . . , An `B1, . . . Bn e ` (A1∧, . . . , An)→ (B1∨, . . . , Bn) sono equivalenti data l’interpre-tazione e la presenza del teorema di deduzione sotto forma di regola d’inferenza.Le regole strutturali in quest’ottica permettono di rilassare le ipotesi, aggiungen-do formule a sinistra, cosı come le tesi, aggiungendone a destra, o di considerarnepiu volte una stessa, come e lecito e comune in logica classica.

Per la completezza abbiamo una dimostrazione costruttiva che, analogamen-te a quanto abbiamo visto per il calcolo a tabelle ma in modo piu diretto, dauna esplicita procedura per la costruzione della dimostrazione in sequenti diun teorema dato. Essa permette agevolmente di costruire una dimostrazionebottom-up, e consiste nell’applicazione all’indietro delle regole d’inferenza, finoad arrivare a sequenti dove appaiono solo atomi. Sia S ` T un sequente di que-sto tipo; la dimostrazione e terminata aggiungendo un assioma id per ciascunatomo A ∈ S∩T , e questo passo e permesso dalle regole di rilassamento. Questoprocesso risulta facilmente automatizzabile. Infine vale la pena di osservare cheanche se in regole complesse come → L la liberta nella formazione dei multin-siemi puo essere un problema, essendo antecedente e conseguente finiti, cosı elo spazio delle possibilita.

Conclusioni

Abbiamo presentato brevemente la natura delle logiche intuizionistica e modaleassieme a due sistemi di calcolo per esse, a tabelle ed ai sequenti rispettivamente.Esistono ovviamente sia calcoli a tabelle modali sia ai sequenti intuizionistici:un esempio dei primi si ha in [16] e l’esempio maggiore per i secondi proprio nelsistema LJ originale di Gentzen.Volendo tracciare qualche paragone generale tra i due metodi di calcolo, anzi-tutto possiamo dire che entrambi si prestano ad un approccio g.o., i tableauxdirettamente per la propria natura formale, i sequenti in virtu della dimostrazio-ne di completezza originale di Gentzen con cui la dimostrazione e costruita dalbasso all’alto; coi tableaux si arriva ad una contraddizione mentre coi sequen-ti ad una serie di istanze dell’assioma id. Entrambi calcoli discussi risultano

19

poi computationally feasible: per quello a tabelle, apportando le opportune mo-difiche si arriva al calcolo presentato in [5] che ha lunghezza delle formule inO(n log n), mentre per LK abbiamo, adoperando la cesura, O(n2).

Riferimenti bibliografici

[1] S. A. Kripke. Semantical analysis of intuitionistic logic I. Studies in Logicand the Foundations of Mathematics, January 1965.

[2] Melvin Fitting. Intuitionistic Logic, Model Theory and Forcing. Studies inLogic and the Foundations of Mathematics. North-Holland, 1969.

[3] Mauro Ferrari and Pierangelo Miglioli. Counting the maximal intermediateconstructive logics. The Journal of Symbolic Logic, 58(4):pp. 1365–1401,1993.

[4] Pierangelo Miglioli, Ugo Moscato, and Mario Ornaghi. Avoiding duplica-tions in tableau systems for intuitionistic logic and kuroda logic. LogicJournal of the IGPL, 5(1):145–167, 1997.

[5] Alessandro Avellone, Guido Fiorino, and Ugo Moscato. Optimizationtechniques for propositional intuitionistic logic and their implementation.Theor. Comput. Sci., 409(1):41–58, 2008.

[6] Pierangelo Miglioli, Ugo Moscato, and Mario Ornaghi. An improved re-futation system for intuitionistic predicate logic. J. Autom. Reasoning,13(3):361–373, 1994.

[7] C. I. Lewis and Langford C. H. Symbolic logic. Macmillian and Co., 1932.

[8] Wolfgang May and Peter H. Schmitt. A tableau calculus for first-order bran-ching time logic. In Intl. Conf. on Formal and Applied Practical Reasoning,FAPR’96, Springer LNCS 1085, pages 399–413, 1996.

[9] G. E. Hughes and M. J. Cresswell. A New Introduction To Modal Logic.Routledge, 1996.

[10] Susanne Bobzien. Ancient logic. In Edward N. Zalta, editor, The StanfordEncyclopedia of Philosophy. -, fall 2008 edition, 2008.

[11] Alain Heuerding. Sequent Calculi for Proof Search in some Modal Logics.phd, Bern University, Institut fur Informatik und angewandte Mathematik,1998.

[12] M. Ohnishi and K. Matsumoto. Gentzen method in modal calculi. OsakaMathematical Journal, 9:113–130, 1957.

[13] Roberta Ballarin. Modern origins of modal logic. In Edward N. Zalta,editor, The Stanford Encyclopedia of Philosophy. -, winter 2010 edition,2010.

[14] H. Rasiowa and R. Sikorski. The mathematics of metamathematics.Panstwowe Wydawn, 1963.

20

[15] George Boolos. Don’t eliminate cut. Journal of Philosophical Logic,13(4):373–378, November 1984.

[16] Pierangelo Miglioli, Ugo Moscato, and Mario Ornaghi. Refutation systemsfor prepositional modal logics. In Peter Baumgartner, Reiner Haehnle, andJoachim Possega, editors, Theorem Proving with Analytic Tableaux andRelated Methods, volume 918 of Lecture Notes in Computer Science, pages95–105. Springer Berlin / Heidelberg, 1995.

21