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

(♻) Validità di LK

  • diretta: per induzione
  • indiretta con altri calcoli (es. CQ)

(♻) Completezza di LK

  • diretta
  • indiretta con altri calcoli (es. CQ o NK)

Varianti di LK

Liste, multinsiemi, insiemi


Sequenze iniziali generalizzate

  • eliminazione delle regole di attenuazione

Formulazione additiva/moltiplicativa delle regole sui connettori

  • equivalenza

Hauptsatz in LK

Ordinamento

Insieme ben ordinato:

  • relazione <
  • condizione wf

Proprietà W-progressiva


♻Principio di induzione transfinita


Ordine lessicografico

  • ipotesi induttiva principale
  • ipotesi induttiva secondaria

Calcolo LKm

Multiinsiemi e regola MIX
Equivalenza MIX/CUT LKm/LK

Teorema

(♻) Lemma di sostituzione [induzione]
Definizione di derivazione distinta
Definizione di RED derivazione
♻ Lemma principale

  • grado, rango di una derivazione, misura di complessità
  • [induzione sulla complessità, per casi]

♻ 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

Craig/Robinson/Beth

Craig (interpolazione)

Partizione di una sequenza
Formula suitable
Formula interpolante
♻ Lemma di Maehara [induzione per casi]
♻ Teorema di interpolazione di Craig

Robinson (somma/Joint consistency)

Definizioni:

  • Teoria formale elementare
  • Teoria consistente
  • Teorie compatibili
  • Unione di teorie

♻ consistente (T1+T2) => compatibili (T1,T2)
♻ Teorema della somma /joint consistency (Robinson)
♻ Somma (Robinson) => Interpolazione (Craig)

Beth (definizione)

Definizioni:

  • P definita esplicitamente
  • P definita implicitamente
  • P indipendente in T

♻ P esplicita <=> P indipendente
♻ P esplicita => P implicita
♻ Teorema di definibilità (Beth) P esplicita <= P implicita [da interpolazione]

Definizioni:

  • formula matrice
  • formula in forma prenessa
  • Σ-formule e П-formule
  • sequenza normale
  • Dimostrazione bipartita
  • Dimostrazione proposizionale

♻ Lemma di sostituzione
♻ Lemma di attenuazione
♻ Lemma di contrazione
♻ Lemma di bipartizione
♻ Hauptsatz rafforzato

Definizioni:

  • Const, Funct, Universo Herbrandiano HU, istanze Herbrandiane HI
  • Calcolo LKc3p

♻ Teorema di equivalenza delle Σ-formule
♻ Teorema di prenessione
♻ Lemma della risoluzione herbrandiana
♻ Teorema di Herbrand

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

Hauptsatz alla Tait-Schwichtenberg

♻ Lemma di Sostituzione
♻ Lemma di Chiusura sotto Attenuazione
♻ Lemma di Inversione
♻ Lemma di Chiusura sotto Contrazione
♻ Lemma Principale
♻ Lemma di Riduzione
♻ Teorema di Eliminazione delle Cesure

Applicazioni

  • Consistenza del calcolo proposizionale
    • [Non si deriva => ]
  • Decidibilità della logica proposizionale intuizionista
    • [Sequenze ridotte a tre occorrenze]

Logica combinatoria

Motivazioni

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
🚩Struttura combinatorialmente completa (chiusura sotto def. esplicite)
♻ comb.completa <=> |A| >1
[esistono K, S e da KKK(SKK)]

Logica Combinatoria Totale (CL)

Linguaggio
Assiomi
Regole di inferenza
Es. definizioni di I, B,C,W
♻ si può costruire λ*x.t
[per induzione]
🚩 Algebra Conbinatoria
♻ AC è comb completa
[♻] AC è consistente
[|/- K=S per induzione]
[♻] AC è indecidibile (Scott-Curry)
[Rice?]
[♻] Teorema del Punto Fisso (Y)
redex/contractum
definibilità di booleani, numeri e funzioni ricorsive
Paradosso di Curry (indefinibilità del predicato di verità)

lambda-calcolo
[Selinger + notes on isomorphism]

lambda-termini:

  • alfabeto
  • termini
  • convenzioni
  • alfa congruenza (equivalenza con cambio di variabili vincolate)
  • sostituzione

[♻] Lemma di sostituzione

Calcoli:


Calcolo CONV(β):

  • formule e regole di inferenza

♻ Equivalenza [Ext] e [η]


Calcolo CONV(βη)


♻ Non estensionalità in λβ

Combinatori e booleani in λ
♻ Teorema del Punto Fisso

  • Versione non-uniforme (t*)
  • Versione uniforme Y
  • Theta di Turing

♻ Teorema della soluzione delle equazioni funzionali
Generalizzazione del Teorema del Punto Fisso

Relazioni CL - lambda

Relazione sintattica tra CL e lambda:

  • astrazione in CL
  • K e S in lambda

Applicazioni C-Λ e Λ-C

  • [♻] 2 relazioni valide
  • [♻] 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]

click to edit

♻ Consistenza di λβ
Forma normale in λβ e λβη: essere in e avere NF
♻ Unicità NF => Consistenza di λβ e λβη
Definizione: redex e contractum, --> e -->>
🚩 Proprietà di Church-Rosser (diamond property)
♻

  • 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 βη)
♻ Lemmi per PAR: t=t, t=s, eliminazione, chiusura transitiva, inversione
♻ =>β ha CR
♻ =>βη ha CR
♻ -->> è CR a la Takahashi

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

Problema semantico [Selinger p.39]
|X| < |X|^|X|
si usano algebre o spazi topologici