Defining a formula inductively using structural induction

Question

If I'm given a well formed formula $\varphi$ that only has the logic symbols $\land,\lor,\neg$. I want to define a formula $\varphi^*$ that is a result of switching every sign $\land$ to $\lor$ and every $\lor$ to $\land$ and every atom to its negation in $\varphi$.

So, I thought defining $\varphi^*$ will be :

Base step: $\varphi$ is an atom then $\varphi^*=\neg{\varphi}$.

Induction step: Here I'm not having a clear thought about defining this so i was thinking of letting $\alpha,\beta\in{WFF}$ that satisfy $\varphi$ .then i gave my self some examples and saw that i need to apply negation to the formulas $\alpha,\beta$ that construct $\varphi$ based on counting $\land$,$\lor$.

My examples:

$\varphi=(p_1\land p_2)\implies \varphi^*=\neg\varphi$.

$\varphi=(p_1\land p_2)\lor p_3 \implies\varphi^*=\neg\neg\varphi$

Is this correct?

Answer 1

The induction step corresponds to the cases $\varphi = \lnot \varphi_1$, $\varphi = \varphi_1 \lor \varphi_2$ and $\varphi = \varphi_1 \land \varphi_2$, where $\varphi_1$ and $\varphi_2$ are well-formed formulas that only have the logic symbols $\lnot$, $\lor$ and $\land$. By induction hypothesis, $\varphi_1^*$ and $\varphi_2^*$ is already defined (this is the "magic" aspect of definitions by induction), so you just have to set:

1. $\varphi^* := \lnot (\varphi_1^*)$ if $\varphi = \lnot \varphi_1$,
2. $\varphi^* := \varphi_1^* \land \varphi_2^*$ if $\varphi = \varphi_1 \lor \varphi_2$,
3. $\varphi^* := \varphi_1^* \lor \varphi_2^*$ if $\varphi = \varphi_1 \land \varphi_2$.

Answer 2

Terminological note: There isn't really such a thing as an 'inductive definition'. Rather, what you are trying to do is to come up with a recursive definition.

However, once such a recursive definition is in place, you can use structural induction to prove things about it.

For example, using the recursive definition as given by @Taroccoesbrocco, we can now prove by structural induction that $\varphi^* \Leftrightarrow \neg \varphi$ (I wouldn't say $\varphi^* = \neg \varphi$, since within the context of metalogic the '$=$' is used to indicate that the two formulas are syntactically/symbolically the same symbol string, whereas of course you just want to prove logical equivalence, for which we use $\Leftrightarrow$)

OK, so here goes that proof:

Base: $\varphi$ is atomic. Then by definition, $\varphi^* = \neg \varphi$

Step: There are three cases to consider:

Suppose $\varphi = \neg \varphi_1$. By inductive hypothesis we can assume $\varphi_1^* \Leftrightarrow \neg \varphi_1$. But that means that $\varphi^* = (\neg \varphi_1)^* = \neg \varphi_1* \Leftrightarrow \neg \neg \varphi_1 = \neg \varphi$

Suppose $\varphi = \varphi_1 \land \varphi_2$. By inductive hypothesis we can assume $\varphi_1^* \Leftrightarrow \neg \varphi_1$ and $\varphi_2^* \Leftrightarrow \neg \varphi_2$. Hence: $\varphi^* = (\varphi_1 \land \varphi_2)^* = \varphi_1^* \lor \varphi_2^* \Leftrightarrow \neg \varphi_1 \lor \neg \varphi_2 \Leftrightarrow \neg (\varphi_1 \land \varphi_2) = \neg \varphi $

Suppose $\varphi = \varphi_1 \lor \varphi_2$. By inductive hypothesis we can assume $\varphi_1^* \Leftrightarrow \neg \varphi_1$ and $\varphi_2^* \Leftrightarrow \neg \varphi_2$. Hence: $\varphi^* = (\varphi_1 \lor \varphi_2)^* = \varphi_1^* \land \varphi_2^* \Leftrightarrow \neg \varphi_1 \land \neg \varphi_2 \Leftrightarrow \neg (\varphi_1 \lor \varphi_2) = \neg \varphi $