Prove the Dual-Converse Relationship

Question

Using a Hilbert-type system, given $ E \sim F ,E' \sim F', E \implies F $ prove $ F' \implies E' $ where a propositional formula A' is obtained by interchanging & and V in A. My answer is proving $ E' \implies F' $ and then use two replacements for both formulas. Would that suffice?

$ \sim $ is being used for equivalence.

Answer 1

If the question is relative to S.C.Kleene's Introduction to Metamathematics, page 122, it seems to me that you have slightly "altered" the sense of the exercise.

At page 122 it is proved the :

Corollary : if $E$ and $F$ are two propositional formulae built up from propositional letters $P_i$ and their negations $\lnot P_i$ with the only connectives : $\lor$ and $\land$ and we define as $E'$ and $F'$ the formulae obtained respectively from $E$ and $F$ applying the following transformation : interchange $\land$ and $\lor$ and each proposition letter $P_i$ with its negation, we have that :

if $\vdash E \sim F$, then $\vdash E' \sim F'$ [where $\sim$ stay for the equivalece, i.e. the bi-conditional : $A \sim B$ iff $(A \supset B) \land (B \supset A)$].

Then, Corallary page 124 ask to reexamine the previous proof in order to verify that :

if $\vdash E \supset F$, then $\vdash F' \supset E'$.

In order to prove it, we have to adapt the proof given at page 122, based on previous results :

• First step : assume $\vdash E \supset F$ and substitute each proposition letter $P_i$ with its negation : $\lnot P_i$; applying the substitution rule [Th.3, page 109] we get : $\vdash E^* \supset F^*$;

• Second step : apply the replacement property of equivalence [Th.6 and Coroll, page 117] using double negation to get $\vdash E^{*1} \supset F^{*1}$;

see Kleene, last line of page 122 : "the effect of these two operations is to interchange the proposition letters with their negations";

• Third step : intead of $*30$, we need here $*12$ : $A \supset B \vdash \lnot B \supset \lnot A$, to get : $\vdash \lnot F^{*1} \supset \lnot E^{*1}$;

• Finally, apply the preliminary result for duality [Th.8, page 121] to "move inside" the leading negation signs [applying De Morgan's laws] to get : $\vdash \lnot F^{*2} \supset \lnot E^{*2}$, which is : $\vdash F' \supset E'$;

see Kleene, second line page 123 : "these last two steps effect the interchange of $\land$ with $\lor$, and interchange the proposition letters with their negations a second time to restore them to their original condition".