1

As an example, let's take the double negation elimination rule $$\neg \neg p\vdash p\ \ \ \text{and}\ \ \ p\vdash\neg \neg p$$

With this, we know that if $p$ is true, then $\neg\neg p$ is true, and vice versa. Now suppose we're given the formula $\phi(p)$, of which we are unaware if either of $p$ or $\phi(p)$ are true. By the double negation elimination rule, do we know if $\phi(p)$ is an equivalent statement to $\phi(\neg\neg p)$? That is to say, can we apply the transformation rule to $p$, even if it's nested within $\phi$?

In other words, does the transformation rule by itself allow us interchange any occurrence of $p$ with $\neg\neg p\ $, or can it only be applied when $p$ is on its own?

Graviton
  • 4,462
  • Yes, logically equivalent expressions can be freely substituted with each other in any part of a formula. (as long as we don't do something silly like use a variable name that's already being used somewhere else) – Greg Martin May 29 '21 at 04:53
  • @GregMartin, Great. Is the ability to do so inherent of the definition of '$\vdash$', or is substitution a separate rule? – Graviton May 29 '21 at 05:00
  • 1
    @Graviton It can be proved by induction on complexity. – Noah Schweber May 29 '21 at 05:01

1 Answers1

2

Yes, this is true and can be proved by induction on formula complexity. Specifically, the key point is that the connectives in classical propositional logic are truth functionals in the following sense:

For each connective $\mathfrak{C}(x_1,...,x_n)$ we have $$\{y_1\leftrightarrow x_1, ..., y_n\leftrightarrow x_n\}\vdash \mathfrak{C}(x_1,...,x_n)\leftrightarrow\mathfrak{C}(y_1,...,y_n).$$

Together with the deduction theorem (which tells us that $\varphi\dashv\vdash\psi$ iff $\vdash\varphi\leftrightarrow\psi$) and some induction on complexity, this gives the desired result. Note that both truth functionality in the above sense and the deduction theorem are nontrivial properties of a logic; that said, in my (limited) experience in algebraic logic we do tend to restrict attention to logics with the relevant substitutability property.

Noah Schweber
  • 245,398