What is the definition of a statement implying or being equivalent to another statement given a background theory?

Solution 1:

Given some theory $T$, we can say that statement $P$ is '$T$-equivalent' to $Q$ if and only if $P \leftrightarrow Q$ is a theorem of $T$ (or if you want: can be derived from its axioms). Or formally: $T \vDash P \leftrightarrow Q$

Solution 2:

Bram28's answer is absolutely correct. However, I think it is worth pointing out a subtlety which arises if we look at weaker background logics than first-order logic. For simplicity I'll talk only about propositional logic(s) since already these present enough complexity for the situation to be interesting.

In classical propositional logic, it makes to say that (propositional) sentences $\alpha,\beta$ are equivalent modulo a (again, propositional) theory $T$ iff $$T\vdash \alpha\leftrightarrow\beta.$$ This is, however, dependent on having a particular connective ("$\leftrightarrow$") in our language. What if we don't have it?

Well, the following alternative definition leaps to mind: $\alpha$ is equivalent modulo $T$ to $\beta$ iff $$T\cup\{\alpha\}\vdash\beta\quad\mbox{and}\quad T\cup\{\beta\}\vdash\alpha.$$ In fact, this is really prior (in my opinion) to the $\leftrightarrow$-based definition, the two being connected by the deduction theorem. This gives us a notion of equivalence modulo a theory even in very limited situations - say, when we only have access to the connective "$\wedge$" (functional completeness is a privilege, not a right, and we may not have eaten sufficiently many lima beans recently :P).

However, this is really just the start of the story. Once we start questioning our underlying propositional apparatus, we will inevitably be led to the idea of algerbaic logic and in particular algebraization. It turns out that, broadly speaking, the following are equivalent for a logic (in the appropriate sense) $\mathcal{L}$:

• $\mathcal{L}$ has a "well-behaved" algebraic semantics (e.g. Boolean algebras for classical propositional logic).

• $\mathcal{L}$ has a "well-behaved" notion of logical equvialence (involving the so-called Leibniz operator $\Omega$).

See Blok/Pigozzi's Algebraizable logics or the introduction of Czelakowski's Protoalgebraic logics for more on this topic. Again, this type of subtlety does not arise when "working over $\mathsf{ZF}$" or similar, but for anyone interested in how logic works "under the hood" it's worth being aware of.