Logica matematica (dimostrazioni formali)

[Apofis]

Ciao a tutti.
Lunedi 19/9/2011 dovrò sostenere un esame di logica matematica...
purtroppo ci sono delle dimostrazioni formali che non riesco a fare.

Dare una dimostrazione formale della seguente regola logica:

PREMESSE:

Ϝ⊢P→Q∨R
Ϝ⊢-Q→S

CONCLUSIONE:

Ϝ⊢(((S ∧-R)→P)∧-R)→Q

dove il "-" è stato utilizzato come operatore di negazione.

Posso utilizzare le formule di derivazione formale presenti nel seguente link:
http://calvino.polito.it/~terzafac/Corsi/logica/pdf/regole.pdf

scusate se salto dei passaggi

1) ϜU{-((S ∧-R)→P)} ⊢-((S ∧-R)→P) assunzione + monotonia
2) ϜU{-((S ∧-R)→P)} ⊢-((S ∧-R)→P)∨R v-introduzione su 1
3) ϜU{-((S ∧-R)→P)} ⊢-(S ∧-R→P)∧-R) de morgan su 2 + eliminazione doppia negazione
4) ϜU{-((S ∧-R)→P)} ⊢-(S ∧-R→P)∧-R)∨Q v-introduzione su 3
5) ϜU{-((S ∧-R)→P)} ⊢(S ∧-R→P)∧-R)→Q →-definizione su 4

ora l'idea e di dimostrare grazie alle premesse che ϜU{((S ∧-R)→P)} ⊢(S ∧-R→P)∧-R)→Q in modo da eliminare le assunzioni/monotonie fatte attraverso la dimostrazione per casi....

idee su come fare?

[hamming_burst]

Ciao,
utilizzi qualche particolare tipo di induzione?

[Apofis]

In che senso?
Tutto ciò che fino ad ora ho utilizzato (e che posso utilizzare) deriva da un applicazione delle regole di derivazione prese dal formulario di cui ho messo il link, le quali a loro volta penso si possano ricavare da un sistema assiomatico tipo quello di Hilbert, o attraverso tavole di verità, nel caso di connettivi base.

L'insieme delle formule è un insieme costruito induttivamente.

Comunque io posso solo dimostrare la regola logica (la mia tesi), attraverso una dimostrazione formale (per derivazione).
Non posso dimostrarla con tavole di verità o altri espedienti.

[hamming_burst]

da quanto dici, a me ricorda troppo l'"induzione strutturale" secondo me le tue derviazioni sono strettamente collegate con questo metodo.
Comunque non conoscendo il tuo modo di procedere, posso aiutarti solo in parte, provo a darci un'occhiata alle regole di derivazione, vediamo che si può fare

[Apofis]

Ok allora ti aiuto ad aiutarmi:

ϜU{-(S ∧-R)→P)} ⊢-((S ∧-R)→P) assunzione + monotonia

assunzione (prima formula del formulario):
poichè se aggiungo una formula G = -((S ∧-R)→P) all'insieme di formule A
allora sicuramente G ∈ A ed A ⊢ G
dove A = {-((S ∧-R)→P)} ⊢ G = -((S ∧-R)→P) , ho dunque un assunzione.

monotonia (seconda formula del formulario):

Ϝ⊆ϜUA dove A= {-((S ∧-R)→P)} e A = {-((S ∧-R)→P)} ⊢ G = -((S ∧-R)→P)

che sono le ipotesi della seconda formula: Ϝ⊆ϜUA A ⊢ G
tesi: ϜUA⊢ G

dunque applicando quindi la 2 formula del formulario avrò:
ϜU{-(S ∧-R)→P)} ⊢-((S ∧-R)→P)

ecc....

[hamming_burst]

ok, così è meglio
Sì alla fine sono derivazioni sulle regole, e l'induzione strutturale si basa su questo.
Appena avrò un po' di tempo gli dò volentieri un'occhiata, sempre se qualcuno non ti risponda prima