Induzione strutturale e teorema del rimpiazzamento.

[Michele.c93]

Buonasera ragazzi ho iniziato lo studio della logica proposizionale e per ora ho affrontato l'induzione strutturale e il teorema del rimpiazzamento. Allora a grandi linee ho capito l'induzione strutturale ma non ho capito come applicarla per spiegare un teorema, nel mio caso quello del rimpiazzamento.
Allora l'induzione come spiegata dalle dispense del mio Prof. che dice data una formula $ F $ con una proprietà $ E $ .
1 PASSO BASE) Tutti gli atomi hanno la proprietà $E$.
2 PASSO INDUTTIVO) Se $ F $ gode della proprietà $ E$ allora anche $ neg F $ e $ (F@ G) $ godono di tale proprietà.

Il teorema del rimpiazzamento è spiegato in questo modo:
Sia $F$ una formula, $ pi in P (F)$, $F[pi]=G $ e G $ -= H $ dove $P(F)$ indica l'insieme di posizioni in una formula logica proposizionale ${1,2}$ e $Delta$ denota una parola vuota . Poi $F-=F[pirarr H] $.
Dove per $F-=F[pirarr H] $ si intende la sostituzione di una sottoformula di $F$ in posizione $pi$ con una $H$ nel modo seguente:
1) $F[Delta rarr H]=H$

2) $F[1pi rarr H]=neg(G[pi rarr H])$ se $F$ è nella forma$ negG$

3) $F[1pi rarr H]=(G1[pi rarr H] @ G2)$ se $F$ è nella forma $(G1 @ G2) $

4) $F[2pi rarr H]=(G1@ G2[pi rarr H])$ se $F$ è nella forma $(G1 @ G2) $

1. PASSO BASE Dato $pi=Delta$
$F-=F[Delta]=G-=H=F[Delta rarr H]$
2. PASSO INDUTTIVO
Dato $pi=ipi'$ ci sono due casi
2.1 $i=1 pi=1pi' in P(F)$, quindi F deve essere nella forma $negF'$ o $(G1 @ G2)$
caso $negF'$ dimostrato cosi $ F[1pi' rarr H]=(negF')[1pi' rarr H]= neg(F'[pi' rarr H])$ e si conclude che $F'-=F'[pi' rarr H]$.

Il caso $G1 @ G2$ e il caso in cui $i=2$ è dimostrato analogamente.

Quali sono i collegamenti tra l'induzione e questa dimostrazione? Io non riesco a capire come impostare i passi che nel mio caso sono $pi=Delta$ e $pi=1pi'$ per $pi=Delta$ intende dimostrare la proprietà sull'atomo? e cioè sulla formula vuota? Nel caso come dimostro il caso $(G1@G2)$?

Io ho provato cosi Dato che $F=(G1@G2)$ allora $F[1pi']=(G1@G2)[1pi']=G1[pi'] @ G2 = G1[1pi' rarr H] @ G2=(G1 @ G2)[1pi' rarr H]=F[1pi' rarr H]$
E dimostro quindi che $F[1pi']=F[1pi' rarr H]$ nello stesso modo in cui nel passo induttivo è stato dimostrato che $F[Delta]=F[Delta rarr H]$