Dimostrazione di un sillogismo tramite logica del I ord.
Ciao devo fare una dimostrazione molto semplice con la logica del I ordine, un sillogismo. Il problema è che formalmente non so come scriverlo.
So che:
1. Tutti gli sportivi hanno un corpo atletico
2. Marco fa sport
Provare che Marco ha un corpo atletico
Le 2 ipotesi sono:
1. { all x [NOT(x fa_sport) OR (x corpo_atletico)] }
2. { Marco fa_sport }
Tesi: { Marco corpo_atletico }
Il mio ragionamento è: pongo x = Marco, che vorrei sostituire nella 1., ma siccome Marco FA sport non posso metterlo al I termine dell'OR in quanto è NOT(x fa_sport) per cui la tesi. Ma come scriverlo??
So che:
1. Tutti gli sportivi hanno un corpo atletico
2. Marco fa sport
Provare che Marco ha un corpo atletico
Le 2 ipotesi sono:
1. { all x [NOT(x fa_sport) OR (x corpo_atletico)] }
2. { Marco fa_sport }
Tesi: { Marco corpo_atletico }
Il mio ragionamento è: pongo x = Marco, che vorrei sostituire nella 1., ma siccome Marco FA sport non posso metterlo al I termine dell'OR in quanto è NOT(x fa_sport) per cui la tesi. Ma come scriverlo??
Risposte
prima di tutto non esiste UNA logica (classica) del I ordine; dimostrare nella logica del I ordine significa derivare in un calcolo logico, e i tipi di calcolo logico principali nella logica contemporanea sono i sistemi assiomatici hilbertiani e la deduzione naturale. nonostante la deduzione naturale sia un caLCOlo logico molto agevole e intuitivo e nonostante il suo studio metamatematico sia fecondo di importanti implicazioni per la teoria della dimostrazione e la filosofia della matematica, l'assiomatica hilbertiana rimane di gran lunga il modello di calcolo logico più noto e impiegato anche nelle esposizione manualistiche; ovviamente esistono diverse assiomatizzazioni per il calcolo dei predicati del I ordine. costruiamone una assumendo una assiomatizzazione standard per il calcolo proposizionale e aggiungendo i seguenti schemi assiomatici:
ASS1 $ AA xArarr A[t/x] $
ASS2 $ AA x(Ararr B)rarr (Ararr AA xB) $
dove $ A $ e $ B $ sono metavariabili che stanno per formule (ben formate) qualsiasi e $ t $ sta per un termine singolare qualsiasi e $ A[t/x] $ sta per la formula ottenuta da $ A $ sostituendo tutte le occorrenze libere di $ x $ con occorrenze di $ t $; ASS2 è soggetto alla condizione che $ A $ non contenga occorrenze libere di $ x $; anche ASS1 è soggetto ad una restrizione, che però riguarda principalmente l'uso dei termini funtoriali: dato che nella nostra derivazione non ne avremo bisogno sorvoliamo.
assumiamo infine come regole di derivazione il modus ponens (da $ Ararr B $ e $ A $ segue $ B $ ) e la generalizzazione (da $ A $ segue $ AA xA $ )
prendiamo $ S $ per il predicato "fare sport" e $ C $ per "avere un corpo atletico" e $ m $ come costante individuale denotante Marco
Hp1 $ AA x(Sxrarr Cx) $
Hp2 $ Sm $
(1) $ AA x(Sxrarr Cx)rarr (Smrarr Cm) $ [istanza di ASS1]
(2) $ Smrarr Cm $ [applicazione del modus ponens a (1) e Hp1]
$ Cm $ [applicazione del modus ponens a (2) e Hp2]
QED
una piccola annotazione: lo schema
ogni A è B
a è A
______
a è B
NON è un sillogismo, almeno nel senso strettamente aristotelico del termine: la teoria aristotelica dell'inferenza sillogistica ammette soltanto enunciati nella forma "ogni A è B", "nessun A è B", "qualche A è B", "qualche A non è B", dove "A" e "B" sono termini generali; detto altrimenti, ammette soltanto enunciati universali o particolari, ma non enunciati singolari (in cui il soggetto è un nome proprio insomma, come appunto in "Marco fa sport" o "Marco è atletico")
il motivo, molto banalmente, è che Aristotele era interessato a sviluppare una teoria del ragionamento scientifico, e per l'epistemologia aristotelica "vi è scienza soltanto dell'universale": un enunciato su un individuo può essere vero o falso ma non riguarda la scienza; difficile dire se questa teoria epistemologica sia applicabile anche alle scienze naturali moderne: un enunciato che parla delle proprietà di una stella (di un individuo appunto) non è forse un enunciato scientifico? di certo non è un enunciato nomologico, ma saremmo disposti a negare a tutti gli effetti che sia un enunciato scientifico...? cmq questo esula dal presente problemA...
se ci sono passaggi nella derivazione che non hai capito, dimmelo, vedrò di chiarire
ASS1 $ AA xArarr A[t/x] $
ASS2 $ AA x(Ararr B)rarr (Ararr AA xB) $
dove $ A $ e $ B $ sono metavariabili che stanno per formule (ben formate) qualsiasi e $ t $ sta per un termine singolare qualsiasi e $ A[t/x] $ sta per la formula ottenuta da $ A $ sostituendo tutte le occorrenze libere di $ x $ con occorrenze di $ t $; ASS2 è soggetto alla condizione che $ A $ non contenga occorrenze libere di $ x $; anche ASS1 è soggetto ad una restrizione, che però riguarda principalmente l'uso dei termini funtoriali: dato che nella nostra derivazione non ne avremo bisogno sorvoliamo.
assumiamo infine come regole di derivazione il modus ponens (da $ Ararr B $ e $ A $ segue $ B $ ) e la generalizzazione (da $ A $ segue $ AA xA $ )
prendiamo $ S $ per il predicato "fare sport" e $ C $ per "avere un corpo atletico" e $ m $ come costante individuale denotante Marco
Hp1 $ AA x(Sxrarr Cx) $
Hp2 $ Sm $
(1) $ AA x(Sxrarr Cx)rarr (Smrarr Cm) $ [istanza di ASS1]
(2) $ Smrarr Cm $ [applicazione del modus ponens a (1) e Hp1]
$ Cm $ [applicazione del modus ponens a (2) e Hp2]
QED
una piccola annotazione: lo schema
ogni A è B
a è A
______
a è B
NON è un sillogismo, almeno nel senso strettamente aristotelico del termine: la teoria aristotelica dell'inferenza sillogistica ammette soltanto enunciati nella forma "ogni A è B", "nessun A è B", "qualche A è B", "qualche A non è B", dove "A" e "B" sono termini generali; detto altrimenti, ammette soltanto enunciati universali o particolari, ma non enunciati singolari (in cui il soggetto è un nome proprio insomma, come appunto in "Marco fa sport" o "Marco è atletico")
il motivo, molto banalmente, è che Aristotele era interessato a sviluppare una teoria del ragionamento scientifico, e per l'epistemologia aristotelica "vi è scienza soltanto dell'universale": un enunciato su un individuo può essere vero o falso ma non riguarda la scienza; difficile dire se questa teoria epistemologica sia applicabile anche alle scienze naturali moderne: un enunciato che parla delle proprietà di una stella (di un individuo appunto) non è forse un enunciato scientifico? di certo non è un enunciato nomologico, ma saremmo disposti a negare a tutti gli effetti che sia un enunciato scientifico...? cmq questo esula dal presente problemA...
se ci sono passaggi nella derivazione che non hai capito, dimmelo, vedrò di chiarire
"Tuttle":
Hp1 $ AA x(Sxrarr Cx) $
Hp2 $ Sm $
(1) $ AA x(Sxrarr Cx)rarr (Smrarr Cm) $ [istanza di ASS1]
(2) $ Smrarr Cm $ [applicazione del modus ponens a (1) e Hp1]
$ Cm $ [applicazione del modus ponens a (2) e Hp2]
QED
Innanzi tutto grazie per la risposta.
Non mi è chiaro il punto (1) forse per la notazione. Il modus ponens io lo conosco in questa forma:
$p, (p -> q) |= q$ come lo hai applicato?
Inoltre l'ipotesi Hp1 mi è già data ed è scritta come $AA x(-Sx$ $OR$ $Cm)$; mi conviene riscriverla come l'hai scritta tu?
il punto (1) è un'istanza dello schema assiomatico ASS1: ASS1 non è un assioma, anzi più in generale non è una formula del linguaggio, è quello che si dice uno schema di formula, cioè una stringa di simboli metateorici che funzionano come "segnaposto" per i simboli del linguaggio; mi spiego: in ASS1 compaiono metavariabili come $ A $ , che sta per una qualsiasi formula (ben formata); assumere questo schema assiomatico significa assumere come assioma ognuna delle (infinite) formule ottenute sostituendo ad $ A $ una qualsiasi formula, e così per tutte le altre metavariabili.
procedendo passo per passo, abbiamo lo schema $ AA xArarr A[t/x] $ ; sostituiamo alla lettera schematica $ A $ la formula $ Sxrarr Cx $ ; poi come ho spiegato sopra con $ A[t/x] $ intendiamo la formula ottenuta da $ A $ sostituendo tutte le occorrenze libere di $ x $ con occorrenze di un qualsiasi termine singolare: in questo caso la costante individuale $ m $ ; nel nostro caso quindi $ A[t/x] $ sarà $ Smrarr Cm $ ; in questo modo otteniamo l'assioma $ AA x(Sxrarr Cx)rarr (Smrarr Cm) $ .
per quanto riguarda il modus ponens, anche qui quando scriviamo $ Ararr B, A rArr B $ usiamo $ A $ e $ B $ come segnaposto per formule qualsiasi: in questo caso applichiamo il modus ponens sostituendo $ A $ con $ AA x(Sxrarr Cx) $ e $ B $ con $ Smrarr Cm $ .
per quanto riguarda Hp1:
$ AA x(Sxrarr Cx) $ come sappiamo è loGICAmente equivalente a $ AA x(-Sx vv Cx) $ ; da un punto di vista "euristico" diciamo, direi che ti conviene semplicemente riscriverla per poter applicare il modus ponens; se poi andiamo a guardare ai sistemi assiomatici, questa sostituzione è formalmente legittima? il discorso qui si complica: cioè, ovviamente possiamo dimostrare che le due formule sono logicamente equivalenti (anche perchè come sappiamo il calcolo dei predicati del I ordine è semanticamente completo, quindi tutte le formule valide sono dimostrabili), ma il modo in cui lo facciamo dipende dal sistema: in ogni caso, molti sistemi assiomatici assumono come connettivi primitivi solo la negazione $ - $ e il condizionale $ rarr $, e introducono gli altri connettivi con delle definizione contestuali, ovvero delle regole di riscrittura: si definisce $ A vv B $ come $ -Ararr B $ , $ A ^^ B $ come $ -(Ararr -B) $ e $ A harr B $ come $ (Ararr B) ^^ (Brarr A) $ ; in questo caso per derivare una formula dall'altra bastano un po' di sostituzioni.
procedendo passo per passo, abbiamo lo schema $ AA xArarr A[t/x] $ ; sostituiamo alla lettera schematica $ A $ la formula $ Sxrarr Cx $ ; poi come ho spiegato sopra con $ A[t/x] $ intendiamo la formula ottenuta da $ A $ sostituendo tutte le occorrenze libere di $ x $ con occorrenze di un qualsiasi termine singolare: in questo caso la costante individuale $ m $ ; nel nostro caso quindi $ A[t/x] $ sarà $ Smrarr Cm $ ; in questo modo otteniamo l'assioma $ AA x(Sxrarr Cx)rarr (Smrarr Cm) $ .
per quanto riguarda il modus ponens, anche qui quando scriviamo $ Ararr B, A rArr B $ usiamo $ A $ e $ B $ come segnaposto per formule qualsiasi: in questo caso applichiamo il modus ponens sostituendo $ A $ con $ AA x(Sxrarr Cx) $ e $ B $ con $ Smrarr Cm $ .
per quanto riguarda Hp1:
$ AA x(Sxrarr Cx) $ come sappiamo è loGICAmente equivalente a $ AA x(-Sx vv Cx) $ ; da un punto di vista "euristico" diciamo, direi che ti conviene semplicemente riscriverla per poter applicare il modus ponens; se poi andiamo a guardare ai sistemi assiomatici, questa sostituzione è formalmente legittima? il discorso qui si complica: cioè, ovviamente possiamo dimostrare che le due formule sono logicamente equivalenti (anche perchè come sappiamo il calcolo dei predicati del I ordine è semanticamente completo, quindi tutte le formule valide sono dimostrabili), ma il modo in cui lo facciamo dipende dal sistema: in ogni caso, molti sistemi assiomatici assumono come connettivi primitivi solo la negazione $ - $ e il condizionale $ rarr $, e introducono gli altri connettivi con delle definizione contestuali, ovvero delle regole di riscrittura: si definisce $ A vv B $ come $ -Ararr B $ , $ A ^^ B $ come $ -(Ararr -B) $ e $ A harr B $ come $ (Ararr B) ^^ (Brarr A) $ ; in questo caso per derivare una formula dall'altra bastano un po' di sostituzioni.
Prima di usare il MP, devo
particolarizzare (sorry, non ho letto
tutta la dimostrazione, non so se fatto): da "per tutti gli x, se A(x)allora B(x)" a "se A(Marco) allora B(Marco)".
particolarizzare (sorry, non ho letto
tutta la dimostrazione, non so se fatto): da "per tutti gli x, se A(x)allora B(x)" a "se A(Marco) allora B(Marco)".
"orazioster":
Prima di usare il MP, devo
particolarizzare (sorry, non ho letto
tutta la dimostrazione, non so se fatto): da "per tutti gli x, se A(x)allora B(x)" a "se A(Marco) allora B(Marco)".
la particolarizzazione io l'ho eseguita assumendo lo schema assiomatico $ AA xArarr A[t/x] $ (di cui $ AA x(Sxrarr Cx)rarr (Smrarr Cm) $ è un'instanza) e poi applicando il modus ponens, dato che per ipotesi vale $ AA x(Sxrarr Cx) $ ; ovviamente la stessa derivazione può essere eseguita, anzichè assumendo lo schema assiomatico $ AA xArarr A[t/x] $ , assumendo direttamente la particolarizzazione ( $ AA xA rArr A[t/x] $ ) tra le regole di derivazione primitive. come ho già scritto, dipende soltanto dal sistema deduttivo in cui decidiamo di eseguire la derivazione
ovviamente assumendo lo schema assiomatico possiamo dimostrare la validità della particolarizzazione come regola derivata:
Hp $ AA xA $
ASS1 $ AA xArarr A[t/x] $
$ A[t/x] $
derivando $ A[t/x] $ dall'ipotesi $ AA xA $ abbiamo appunto dimostrato la validità della regola di inferenza $ AA xA rArr A[t/x] $
cmq, raff5194, la tua richiesta mi ha da subito un po' disorientato: è un esercizio che ti ha assegnato un docente? perchè se è così, mi lascia molto perplesso il fatto che ti abbia assegnato una derivazione senza precisare il sistema formale in cui eseguirla
se è un esercizio tratto da un manuale, magari il testo propone un calcolo logico specifico e negli esercizi richiede implicitamente di usare quello.
si è l'esercizio che ci ha assegnato un prof e purtroppo non ho basi di logica. Infatti si è trattato di UNA SOLA lezione di un'ora sulla first-order predicate logic preceduta da un'altra sulla prepositional logic.
Infatti tutto il ragionamento che mi hai scritto l'ho dovuto leggere con molta attenzione per capirci qualcosa e nn ti nascondo che molte cose mi sono oscure
Infatti tutto il ragionamento che mi hai scritto l'ho dovuto leggere con molta attenzione per capirci qualcosa e nn ti nascondo che molte cose mi sono oscure
Curiosità: le
mie nozioni (ma alquanto "forti", in quel tempo! stante ora la dimenticanza dopo 20 anni...) su Logica/Calcolo Proposizionale risalgono
ai miei studi in....Filosofia. (già).
Erano esami altresì dal 'taglio' prettamente scientifico (per la disperazione
di alcuni colleghi): -proprio
Logica -e, l'anno dopo, Logica dei Sistemi Normativi.
Filosofia del Linguaggio furono altri insegnamenti.
mie nozioni (ma alquanto "forti", in quel tempo! stante ora la dimenticanza dopo 20 anni...) su Logica/Calcolo Proposizionale risalgono
ai miei studi in....Filosofia. (già).
Erano esami altresì dal 'taglio' prettamente scientifico (per la disperazione
di alcuni colleghi): -proprio
Logica -e, l'anno dopo, Logica dei Sistemi Normativi.
Filosofia del Linguaggio furono altri insegnamenti.
"orazioster":
Curiosità: le
mie nozioni (ma alquanto "forti", in quel tempo! stante ora la dimenticanza dopo 20 anni...) su Logica/Calcolo Proposizionale risalgono
ai miei studi in....Filosofia. (già).
anche le mie
tra le altre cose, la logica formale è il più potente strumento di analisi filosofica mai esistito
(affermazione volutamente iperbolica e anche un po' ruffiana in un forum di matematica... ma non così lontana dal vero...)
"Tuttle":
anche le mie
...
...affermazione volutamente iperbolica e anche un po' ruffiana in un forum di matematica...
@Tuttle
Fantastica!
Intervengo: a me sembra un semplice esercizio di logica dei predicati. Quindi il sistema assiomatico è "dato", per così dire, dalla forma (in fbf) delle premesse 1 e 2, dalle quali si deriva la tesi (cosa peraltro già ampiamente descritta nei precedenti post).
Accedi a tutti gli appunti
Tutor AI: studia meglio e in meno tempo