# Thread: Proving a Theorem (Predicate Logic)

1. ## Proving a Theorem (Predicate Logic)

Prove the case for the following theorem when C has the form $\displaystyle F \to G$:
"Let A and B be predicate forms with $\displaystyle A \iff B$, and let C be a predicate form which contains (one or more instances of) A. Let D be a predicate form obtained from C by replacing some instances of A with B. Then $\displaystyle C \iff D$."

Attempt:

We apply induction on the complexity of C.

Base: the simplest case, C is C=A. In this case we have D=B so C \iff D by hypothesis. So, for the insuctive case we can consider different cases like $\displaystyle \neg F$, $\displaystyle (F \wedge G)$, etc. But I'm only required to prove the case case F-->G (F implies G).

So, $\displaystyle C$ has the form $\displaystyle (F \to G)$. Then $\displaystyle D$ is $\displaystyle (F’ \to G’)$, where either$\displaystyle F=F’$ or $\displaystyle F’$ is obtained from $\displaystyle F$ by replacing one or more instances of A with B. Similarly $\displaystyle G’=G$ or $\displaystyle G’$ is obtained from $\displaystyle G$ by replacing one or more instances of A with B. I think we need to show for any interpretation I and any I-assignment v, something like this holds:

$\displaystyle I \models_v C \iff (I \models_v F \to I \models_v G)$
$\displaystyle \iff ((I \models_v F’) \to (I \models_v G’))$
$\displaystyle \iff I \models_v D$

But that requires us to show that we have $\displaystyle (F \iff F’) \to (F \iff G’)$. How do we show that? Any help and suggestion is really appreciated.

2. ## Re: Proving a Theorem (Predicate Logic)

Originally Posted by demode
$\displaystyle I \models_v C \iff (I \models_v F \to I \models_v G)$
$\displaystyle \iff ((I \models_v F’) \to (I \models_v G’))$
$\displaystyle \iff I \models_v D$

But that requires us to show that we have $\displaystyle (F \iff F’) \to (F \iff G’)$.
I don't see why this is required. By induction hypothesis, for every $\displaystyle I$ and $\displaystyle v$ we have $\displaystyle I\models_v F$ iff $\displaystyle I\models_v F'$, and also $\displaystyle I\models_v G$ iff $\displaystyle I\models_v G'$. Thus, for any $\displaystyle I$ and $\displaystyle v$,

$\displaystyle I\models_v C$ iff
$\displaystyle I\models_v (F\to G)$ iff
($\displaystyle I\models_v F$ implies $\displaystyle I\models_v G$) iff
($\displaystyle I\models_v F'$ implies $\displaystyle I\models_v G'$) iff
$\displaystyle I\models_v (F'\to G')$ iff
$\displaystyle I\models_v D$.

3. ## Re: Proving a Theorem (Predicate Logic)

Originally Posted by emakarov
I don't see why this is required. By induction hypothesis, for every $\displaystyle I$ and $\displaystyle v$ we have $\displaystyle I\models_v F$ iff $\displaystyle I\models_v F'$, and also $\displaystyle I\models_v G$ iff $\displaystyle I\models_v G'$. Thus, for any $\displaystyle I$ and $\displaystyle v$,

$\displaystyle I\models_v C$ iff
$\displaystyle I\models_v (F\to G)$ iff
($\displaystyle I\models_v F$ implies $\displaystyle I\models_v G$) iff
($\displaystyle I\models_v F'$ implies $\displaystyle I\models_v G'$) iff
$\displaystyle I\models_v (F'\to G')$ iff
$\displaystyle I\models_v D$.
I see. Yes, either way, by inductive hypothesis we have $\displaystyle F \iff F'$ and $\displaystyle G \iff G'$. But thank you for confirming, I appreciate that.