[Logica Matematica] Aiuto per dimostrazione formale (applicazione monotonia)

[Crystal Dragon]

Mi sto preparando per l'esame di logica matematica, e dopo aver risolto i più semplici esempi di dimostrazione formale trovati sul libro mi sono buttato sul primo tema d'esame che ho trovato, che chiedeva ciò:

\(Premessa: \digamma \vdash (F \rightarrow H)\wedge G\)
\(Conclusione: \digamma \vdash (F \vee \neg G) \rightarrow H \)

Ecco la mia risoluzione:

\( 1)\digamma \vdash (F \rightarrow H)\wedge G\) pre
\( 2)\digamma \vdash F \rightarrow H \) ∧-elim a 1
\( 3)\digamma \cup \{F\} \vdash F \rightarrow H \) mon a 2
\( 4)\digamma \cup \{F\} \vdash F \) ass
\( 5)\digamma \cup \{F\} \vdash H \) →-elim a 3,4

Da qui in poi sono rimasto abbastanza bloccato, l'unica idea che mi è venuta in mente è di applicare la monotonia in questo modo:

\( 6)\digamma \cup \{F \vee \neg G\} \vdash H \) mon a 5
\( 7)\digamma \vdash (F \vee \neg G) \rightarrow H \) ->-intro a 6

Solo che non sono assolutamente sicuro di aver fatto qualcosa di lecito, di solito ho sempre visto applicare queste regole a destra del simbolo di conseguenza logica. Si può fare una cosa del genere? In alternativa, ci sono altri modi per arrivare alla soluzione?

[Crystal Dragon]

Van bene anche idee su cui non siete sicuri, mi serve una mano

[Crystal Dragon]

Aggiornamento, son riuscito in questo altro modo:

\( 1)\digamma \vdash (F \rightarrow H)\wedge G\) pre
\( 2)\digamma \vdash F \rightarrow H \) ∧-elim a 1
\( 3)\digamma \cup \{F\} \vdash F \rightarrow H \) mon a 2
\( 4)\digamma \cup \{F\} \vdash F \) ass
\( 5)\digamma \cup \{F\} \vdash H \) →-elim a 3,4
\( 6)\digamma \cup \{F\} \vdash H \vee \neg(F \vee \neg G)\) v-intro a 5
\( 7)\digamma \cup \{F\} \vdash \neg(F \vee \neg G) \vee H\) v-simm a 6
\( 8)\digamma \cup \{F\} \vdash (F \vee \neg G) \rightarrow H\) →-intro a 7
\( 9)\digamma \cup \{\neg F\} \vdash \neg F \) ass
\( 9)\digamma \vdash G \wedge (F \rightarrow H) \) ∧-simm a 1
\( 10)\digamma \vdash G \) ∧-elim a 9
\( 11)\digamma \vdash \neg\neg G \) DN-I a 10
\( 12)\digamma \cup \{\neg F\} \vdash \neg\neg G \) mon a 11
\( 13)\digamma \cup \{\neg F\} \vdash \neg F \wedge \neg \neg G \) ∧-intro a 9,12
\( 14)\digamma \cup \{\neg F\} \vdash \neg (F \vee \neg G) \) De Morgan a 13
\( 15)\digamma \cup \{\neg F\} \vdash \neg (F \vee \neg G ) \vee H \) v-intro a 14
\( 16)\digamma \cup \{\neg F\} \vdash (F \vee \neg G) \rightarrow H\) →-intro a 15
\( 17)\digamma \vdash (F \vee \neg G) \rightarrow H\) Casi a 8,16

Forse le v-introduzioni 6 e 15 andavano fatte in più passi, ma almeno qui mi sembra di aver rispettato ogni regola.