Please enable JavaScript.
Coggle requires JavaScript to display documents.
Temi Avanzati di Logica (LK di Gentzen (Motivazione (Ricerca di una Forma…
Temi Avanzati di Logica
LK di Gentzen
Motivazione
Ricerca di una Forma Normale per le dimostrazioni:
- la conclusione contiene tutte e sole le proposizioni presenti nella dimostrazione (quindi eliminazione del CUT)
Simmetrizzazione: la legge del terzo escluso non è più un caso speciale (conseguenti multipli)
Definizioni
- Sequenza
- Antecedente, Conseguente
- Formula condizionale equivalente
- Calcolo:
- Assiomi (sequenze iniziali)
- Regole di inferenza:
- Regole strutturali (trasformazioni) (4)
- Regole logiche (introduzioni) (6)
- Formula principale, secondaria, contesto
- nel CUT le formule nella premessa non sono sottoformule di quelle nella conclusione
- Dimostrazione in LK:
- le foglie sono sequenze iniziali
- ciascun nodo è conclusione di un'inferenza di LK
Validità e Completezza
Definizioni:
- sequenza vera in una struttura
- sequenza universalmente valida
(:recycle:) Validità di LK
- diretta: per induzione
- indiretta con altri calcoli (es. CQ)
(:recycle:) Completezza di LK
- diretta
- indiretta con altri calcoli (es. CQ o NK)
Varianti di LK
Liste, multinsiemi, insiemiSequenze iniziali generalizzate
- eliminazione delle regole di attenuazione
Formulazione additiva/moltiplicativa delle regole sui connettori
Applicazioni
- Consistenza del calcolo proposizionale
- Decidibilità della logica proposizionale intuizionista
- [Sequenze ridotte a tre occorrenze]
Hauptsatz in LK
Ordinamento
Insieme ben ordinato:
- relazione <
- condizione wf
Proprietà W-progressiva:recycle:Principio di induzione transfinitaOrdine lessicografico
- ipotesi induttiva principale
- ipotesi induttiva secondaria
-
Teorema
(:recycle:) Lemma di sostituzione [induzione]
Definizione di derivazione distinta
Definizione di RED derivazione
:recycle: Lemma principale
- grado, rango di una derivazione, misura di complessità
- [induzione sulla complessità, per casi]
:recycle: Hauptsatz di Gentzen [induzione]
Percorso logico
- Rappresentazione in forma nornale (Hauptsatz)
- Introduzione del calcolo LK e sua equivalenza con CQ e NK
- Eliminazione del CUT (Hauptsatz)
- Rappresentazione bipartita (Hauptsatz rafforzato)
- Rappresentazione con esistenziale unico (Herbrand)
Herbrand
Definizioni:
- formula matrice
- formula in forma prenessa
- Σ-formule e П-formule
- sequenza normale
- Dimostrazione bipartita
- Dimostrazione proposizionale
:recycle: Lemma di sostituzione
:recycle: Lemma di attenuazione
:recycle: Lemma di contrazione
:recycle: Lemma di bipartizione
:recycle: Hauptsatz rafforzato
Definizioni:
- Const, Funct, Universo Herbrandiano HU, istanze Herbrandiane HI
- Calcolo LKc3p
:recycle: Teorema di equivalenza delle Σ-formule
:recycle: Teorema di prenessione
:recycle: Lemma della risoluzione herbrandiana
:recycle: Teorema di Herbrand
Craig/Robinson/Beth
Craig (interpolazione)
Partizione di una sequenza
Formula suitable
Formula interpolante
:recycle: Lemma di Maehara [induzione per casi]
:recycle: Teorema di interpolazione di Craig
-
Beth (definizione)
Definizioni:
- P definita esplicitamente
- P definita implicitamente
- P indipendente in T
:recycle: P esplicita <=> P indipendente
:recycle: P esplicita => P implicita
:recycle: Teorema di definibilità (Beth) P esplicita <= P implicita [da interpolazione]
Hauptsatz in LK3c
Calcolo LK3c
Sequenze iniziali
Regole logiche A, K
Differenze con LK:
- multinsiemi
- nessuna regola strutturale
- sequenze inziali attenuate
- regole a due premesse additive
- peculiarità di ∃ e ∀
Dimostrazioni in LK3c
Dimostrazioni in forma distinta
Equivalenza LKc e LK3c
Misura delle dimostrazioni: grado e rango
Definizione di iperesponenziale
-
Logica combinatoria
-
Introduzione
Funzioni:
- come grafo (estensionale
- come procedura, algoritmo (intensionale)
Currying (funzioni a n variabili ridotte a 1 variabile)
Calcolo non tipato (unico tipo per funzioni e dati)
- Combinatori (Schonfinkel)
- Logica combinatoria totale CL (Curry)
- Lambda-calcolo (Church)
Combinatori
Definizioni: K, I, B, S, C, W
Struttura applicativa
Linguaggio della struttura applicativa
:red_flag:Struttura combinatorialmente completa (chiusura sotto def. esplicite)
:recycle: comb.completa <=> |A| >1
[esistono K, S e da KKK(SKK)]
Schoenfinkel vuole eliminare le variabili vincolate
I quantificatori rendono la sostituzione problematica perché es. in VxRxy vale VxRxt solo se t non contiene x
L'operatore nextand Ra..b|Sc..d = -Ex(Ra..bx^Sc..dx)
Tutte le formule del primo ordine (FOL) possono essere scritte mediante il solo nextand (analogo alle formule proposizionali e NAND)
La costante U agisce come nextand ed "elimina" le variabili eventualmente con l'uso di altri combinatori
I combinatori di Schonfinkel permettono di scrivere le formule FOL come funzioni logiche dei predicati che contengono
-
-
-
Relazioni CL - lambda
Relazione sintattica tra CL e lambda:
- astrazione in CL
- K e S in lambda
Applicazioni C-Λ e Λ-C
- [:recycle:] 2 relazioni valide
- [:recycle:] 3 relazioni non valide
Algebre combinatorie e algebre lambda [Selinger]Teorema di equivalenza CL-lambda (Curry)
[Esistenza di uguaglianze come assiomi]Teorema di equivalenza CL+ext - lambda-eta
[equivalenza base/ equivalenza con uguaglianze come assiomi]
:recycle: Consistenza di λβ
Forma normale in λβ e λβη: essere in e avere NF
:recycle: Unicità NF => Consistenza di λβ e λβη
Definizione: redex e contractum, --> e -->>
:red_flag: Proprietà di Church-Rosser (diamond property)
:recycle:
- t= s sse esiste r
- t=s e s in NF allora t -->> s
- unicità di NF
Teorema di Church: l'insieme dei termini normalizzabili è semidecidible
Leftmost reduction strategy
Teorema: se t ha NF allora t -L->> NF(t)
Riduzione parallela
Definizione riduzione parallela per β e per βη (PARβ e PAR βη)
:recycle: Lemmi per PAR: t=t, t=s, eliminazione, chiusura transitiva, inversione
:recycle: =>β ha CR
:recycle: =>βη ha CR
:recycle: -->> è CR a la Takahashi