Risultato di logica del prim'ordine

[mdoni]

Salve a tutti,
sto tentando di dimostrare un risultato di logica del prim'ordine, ma non ne vengo fuori. Si tratta di mostrare che:
Detto \(\Delta \subseteq Form_L \) per un certo linguaggio del prim'ordine \( L \), \( \varphi \in Form_L, x \) una variabile che non occorre libera in \( \Delta \) né in \( \varphi \), e \( c \) un simbolo di costante. Allora
\[
\Delta \vdash \varphi \Rightarrow \Delta[c/x] \vdash \varphi[c/x]
\]
Ora, immagino si debba procedere per induzione sull'insieme delle deduzioni (che è definito ricorsivamente), ma non capisco se considerare un insieme tipo
\[
\mathcal{D} = \{ D : \text{ se } D \text{ è derivazione con premessa } \Delta \text{ e conclusione } \varphi, \\ \text{ allora } D \text{ è derivazione con premessa } \Delta[c/x] \text{ e conclusione } \varphi[c/x] \}
\]
od invece una cosa tipo
\[
\mathcal{D} = \{ D : \text{ se } D \text{ è derivazione con premessa } \Delta \text{ e conclusione } \varphi, \\ \text{ allora esiste una derivazione } D' \text{con premessa } \Delta[c/x] \text{ e conclusione } \varphi[c/x] \}
\]

Personalmente credo si debba ragionare induttivamente sul primo insieme; ma in ogni caso poi mi fermo: non capisco come procedere nel caso in cui, per esempio, la deduzione considerata \( D \) sia quella che segue la regola \( ( \wedge I ) \), o ancora la regola \( ( \to I ) \) o tutte quelle regole in cui la conclusione non è della forma \( \varphi \).
Ringrazio tutti per l'aiuto

[perplesso1]

Ti dico una cosa, ma non sono proprio sicurissimo... allora, io credo che dovresti procedere per induzione sulla lunghezza di $\phi$. Se $\phi$ è una formula atomica la tesi è banalmente vera. Ora supponendo la tesi vera per tutte le formule che hanno una lunghezza strettamente minore di quella di $\phi$, procediamo per casi. Se $\phi := \psi \wedge \chi$ allora per l'ipotesi induttiva puoi derivare
\[ \psi[c/x] \] ed anche \[ \chi[c/x] \]
ed usando la giusta regola di inferenza cioe $(\wedge I)$ arrivi alla tesi. Analogamente devi trattare i casi

$\phi := \not \psi$
$\phi := \forall x (\psi)$
$\phi := \exists x (\psi)$