Logo dell'Università di Catania: Siciliae Studium Generale 1434 Logo DMI, Fondamenti di informatica
matite e gomma
Loghi istituzionali: Siciliae Studium Generale 1434, Università di Catania, Facoltà di Scienze Matematiche, Fisiche, Naturali, Insegnamento di Fondamenti di Informatica

Logica predicativa, sintassi e semantica

Lezione 14 di Fondamenti di informatica

Docenti: Marina Madonia & Giuseppe Scollo

Università di Catania
Facoltà di Scienze Matematiche, Fisiche e Naturali
Corso di Laurea in Informatica, I livello, AA 2008-09

Logo di Conformità WCAG-1 di Livello Tripla A, W3C-WAI Web Content Accessibility Guidelines 1.0 Validazione XHTML 1.0 Validazione CSS 2

Indice

  1. Logica predicativa, sintassi e semantica
  2. definizioni ricorsive
  3. principio di induzione di Peano
  4. definizione induttiva di termini
  5. induzione strutturale
  6. induzione noetheriana
  7. sintassi predicativa
  8. variabili in termini e formule
  9. semantica predicativa
  10. teorie predicative
  11. semantica predicativa Tarskiana
  12. validità di formule predicative
  13. esercizi

definizioni ricorsive

una definizione, in un linguaggio, ha due costituenti:

una definizione è ricorsiva quando il definiendum occorre nel definiens

per l'inerente circolarità, una definizione ricorsiva rischia di essere semanticamente viziosa: inutilizzabile al fine di stabilire il significato dei suoi costituenti; tuttavia ...

... si può impedire la formazione di circoli viziosi se il definiendum è un termine parametrico, con un parametro che assume valori in un insieme ben ordinato

in tal caso, possiamo rendere costruttiva, anziché viziosa, la circolarità in una definizione ricorsiva assicurando che le occorrenze del definiendum nel definiens siano riferite a valori del parametro più piccoli di quello a cui è riferito il definiendum in quanto tale

principio di induzione di Peano

il principio di induzione naturale, dovuto a Giuseppe Peano (1889), ha due distinte, sebbene correlate, manifestazioni:

nella definizione dei numeri naturali, come principio di minimalità costruttiva, evidente nella terza clausola appresso:

nelle dimostrazioni di proprietà sui numeri naturali:

la minimalità costruttiva dei numeri naturali giustifica l'uso del principio di induzione naturale come regola di inferenza logica

definizione induttiva di termini

esempi di costruzioni induttive di largo impiego nella definizione di linguaggi formali, quali ad es. linguaggi logici, linguaggi di programmazione, etc., si hanno nelle definizioni degli insiemi dei termini, formule o espressioni del linguaggio

ecco, ad esempio, la definizione induttiva dell'insieme dei termini generato da una segnatura algebrica, ovvero famiglia di operatori, cioè simboli di operazione, dove ogni operatore ha una arietà: il numero di argomenti dell'operazione che esso designa

per una data interpretazione degli operatori quali costanti e operazioni di un'algebra, un termine privo di variabili descrive il calcolo di un valore nell'algebra, a partire da costanti

induzione strutturale

la costruzione induttiva dei termini ben si presta ad introdurre una tecnica di definizione e di dimostrazione molto utile nei linguaggi di programmazione: l'induzione strutturale

supponiamo di voler definire una nuova funzione, o dimostrare che una certa proprietà valga, per tutti i possibili valori assunti da una struttura dati:

in tali condizioni, l'induzione strutturale consiste nel

il principio di induzione strutturale può essere facilmente dedotto dal principio di induzione naturale di Peano, giacché altro non è che induzione naturale sulla complessità dei termini che rappresentano i valori delle strutture dati in gioco; il seguente principio di induzione, al contrario, è una generalizzazione propria del principio di Peano

induzione noetheriana

un ordinamento stretto < su un insieme S è detto ben fondato, e si dice che S è ben ordinato da <, se non esistono catene discendenti infinite a0 > a1 > ... an > ..., cioè se ogni catena discendente termina

una proprietà P definita per gli elementi di S, strettamente ordinato da <, è detta ereditaria se vale l'implicazione:     ( ∀y<x P(y) ) → P(x)

il seguente principio di induzione è dovuto a Emmy Noether:

l'ordinamento dei naturali è ben fondato, dal che discende una forma equivalente dell'induzione di Peano (la cui base deriva dalla validità vacua dell'implicazione di ereditarietà sui naturali quando x=0)

sintassi predicativa

costruzione di formule predicative (del I ordine), dati un insieme V di variabili e una segnatura algebrica (in senso lato) omogenea, o segnatura del I ordine, Σ=(Ω,Π):

l'insieme TΣ(V) dei termini su Σ e V è definito induttivamente come sopra, ma su una base più estesa, poiché anche le variabili sono termini di complessità 0

l'insieme delle formule atomiche su Σ e V è costituito dai simboli proposizionali in Π0 e dalle espressioni P(t1,...,tk) e (t1 = t2), dove PΠk e t1,t2,...,tkTΣ(V)

l'insieme FΣ(V) delle formule su Σ e V è definito induttivamente come segue:

variabili in termini e formule

sia i termini sia le formule di una segnatura del I ordine sono rappresentabili come alberi ordinati, ai cui nodi sono associati simboli della segnatura, variabili e, per le formule, i connettivi logici e i quantificatori introdotti nella loro definizione induttiva

Def.: un albero è ordinato se è radicato e con un ordine totale dei figli di ciascun nodo interno

N.B. una segnatura del I ordine come definita sopra è detta omogenea perché dà una sintassi per algebre (in senso lato) omogenee; una segnatura eterogenea, o multisortale ha inoltre un insieme di sorte (nomi per gli insiemi sostegno), e più articolate arietà dei simboli, che ne specificano le sorte degli argomenti (e dei risultati di operazioni); in tal caso anche le variabili hanno sorta; per semplicità, ci limitiamo al caso omogeneo

le variabili di un termine sono quelle che vi occorrono (associate a foglie del suo albero); per le formule, vanno distinte le occorrenze libere di variabili da quelle vincolate

un termine t è liberamente sostituibile a x in φ(x) se, sostituendo t in tutte le occorrenze libere di x in φ(x), nessuna variabile di t in tali sostituzioni viene quantificata

N.B. la libera sostituibilità di un termine a una variabile in una formula è necessaria alla correttezza della sostituzione, v. ad es. la sostituzione del termine x alla variabile y in x ¬(x=y)

semantica predicativa

definiamo innanzitutto la semantica degli enunciati, cioè formule prive di variabili libere

un enunciato di segnatura Σ trova significato in un modello che interpreta i simboli di Σ

l'interpretazione t M dei termini chiusi t TΣ è definita per induzione strutturale

qui conviene considerare una segnatura estesa Σ(D), in cui gli elementi del sostegno D di M sono aggiunti come simboli di costante (e interpretati come se stessi nella Σ(D)-struttura M)

la semantica è data dalla relazione di validità ⊨ di Σ-enunciati in Σ-modelli: M ⊨ φ

l'interpretazione di Π e TΣ(D) in M dà la validità degli enunciati atomici:

quella degli altri enunciati si definisce quindi per induzione strutturale (v. esercizio 9)

teorie predicative

ModΣ: la classe dei Σ-modelli ("classe di similarità")

ModΣ(φ): la sottoclasse di ModΣ caratterizzata dalla validità dell'enunciato φ

ModΣ(Ψ): la sottoclasse di ModΣ caratterizzata dalla validità di tutti gli enunciati dell'insieme Ψ in ciascun modello della classe

relazione di conseguenza semantica: Ψ  φ sse ModΣ(Ψ) ModΣ(φ)

Σ-teoria predicativa: un insieme di Σ-enunciati chiuso per conseguenza:

chiusura deduttiva di un insieme di Σ-enunciati Ψ: Th(Ψ) = {φ|Ψ  φ}

Ψ è soddisfacibile se ModΣ(Ψ) non è vuota, altrimenti è insoddisfacibile: Ψ  

principio di dimostrazione per assurdo: Ψ  φ    Ψ∪φ}  

φ è una verità logica o tautologia se ModΣ(φ= ModΣ (in tal caso si scrive ⊨ φ)

semantica predicativa Tarskiana

fissato un dominio D, la semantica dei Σ(D)-enunciati φ  FΣ(D) può essere specificata definendo ModΣ(D)(φ) per induzione sulla struttura di φ, come segue:

validità di formule predicative

per definire la validità di formule con variabili si ricorre al concetto di assegnamento:

notazione: l'assegnamento ρx=a coincide con ρ eccetto che associa a alla variabile x

un assegnamento ρ: V D nel sostegno D di un Σ-modello M viene induttivamente esteso ad una corrispondente funzione di valutazione, che estende ai termini con variabili l'interpretazione fornita dal modello: _ρM : TΣ(V)D

la definizione induttiva di validità di enunciati è così riproponibile per quella di validità di formule, relativa a un dato assegnamento ; N.B. per la semantica dei quantificatori si pone:

si ottiene anche una definizione di validità di formule indipendente dall'assegnamento stipulando che una formula (con variabili) è valida in un modello quando lo è, nel senso della definizione precedente, per tutti gli assegnamenti

esercizi

  1. definire ricorsivamente il prodotto di due numeri naturali, usando la somma
    • suggerimento: definire per induzione su uno dei due argomenti del prodotto
  2. dimostrare per induzione la validità della formula di Gauss per il calcolo della somma dei primi n numeri naturali positivi: n(n+1)/2
  3. dimostrare per induzione che la somma dei primi n numeri naturali dispari è n2
  4. definire ricorsivamente la funzione lgf(n) = lg(n!)
  5. definire ricorsivamente la funzione lgmk(n) = (lg n) mod k, dove k>1 è una costante
  6. dimostrare per induzione che un insieme di n elementi ha 2n sottoinsiemi
  7. dimostrare per induzione che esistono mn funzioni totali da un insieme di n elementi in uno di m elementi (considerare anche i casi m=0 e n=0)
  8. data una segnatura omogenea del I ordine Σ=(Ω,Π) e un insieme di variabili V, definire per induzione strutturale l'insieme Var(t) delle variabili di un termine t e l'insieme Free(φ) delle variabili libere di una formula φ
  9. completare per induzione strutturale la definizione della relazione di validità ⊨ introdotta a lezione (suggerimento: considerare le tavole di verità dei connettivi booleani e il significato intuitivo dei quantificatori; è chiara ora la convenienza di estendere la segnatura del modello con gli elementi del suo dominio come costanti?)