The Gold Standard of Mathematical Logic | Logical Equivalence and Safe Formula Replacement

Agreement in one model means two formulas receive the same truth value there. Logical equivalence means they agree in every permitted model and assignment. One-way consequence means that whenever the first is true, the second is true; the reverse need not hold.

For propositional letters p and q, p ∧ q entails p. But p does not entail p ∧ q. The valuation p = true and q = false separates them.

Therefore replacing p with p ∧ q inside an arbitrary expression cannot be justified merely because the conjunction implies p. Equivalence requires both directions.

A numerical analogy with a clear limit

The conditions x = 2 and x² = 4 agree at x = 2. Over the real numbers they are not equivalent because x = −2 satisfies only the second. The first implies the second, while the reverse loses a sign possibility.

Over the nonnegative reals, they are equivalent. The domain restriction changes the comparison.

This is a useful bridge to formula reasoning: equivalence is always assessed within a specified semantic setting. A result relative to additional premises or a restricted domain should retain those conditions.

When comparing two expressions, ask three separate questions. Do they agree in the current example? Does each imply the other under the standing assumptions? Do they agree across the full intended class of interpretations?

A confident answer to the first does not establish the third. The repair is to state the scope of the evidence and either provide a general proof or search for a separating interpretation.

Contents · Next chapter

In classical propositional logic, p → q is equivalent to ¬p ∨ q. A complete two-letter truth table checks all four valuations.

The last two columns agree in every row, so the formulas are logically equivalent in this setting. The table is exhaustive for these two propositional letters, rather than a selection of favourable examples.

Now compare p → q with q → p. At p = false and q = true, the first is true and the second false. One separating valuation refutes their equivalence.

Structure matters more than familiar wording

The classical contrapositive ¬q → ¬p is equivalent to p → q. The converse q → p generally is not. The inverse ¬p → ¬q is equivalent to the converse, not generally to the original.

These are four distinct patterns. Reading “reverse it” or “make it negative” as one operation hides which pattern was produced.

A learner should be able to supply a separating valuation for an invalid equivalence. That gives the correction a mechanism: one expression allows a case that the other excludes.

For formulas with n independent propositional letters, a full truth table has 2ⁿ rows. It can establish equivalence when every valuation has been checked. A partial table may refute equivalence as soon as it finds disagreement, but absence of disagreement in selected rows is not yet exhaustive evidence.

Contents · Previous chapter · Next chapter

If A and B are logically equivalent, a truth-functional context receives the same truth value when A is replaced by B. The surrounding connective uses their truth value, not their spelling.

For example, replace p → q by ¬p ∨ q inside (p → q) ∧ r. The result is (¬p ∨ q) ∧ r, and the two larger formulas are equivalent.

The parentheses are important. Writing ¬p ∨ (q ∧ r) instead changes the grouping. At p = false and r = false, the correctly grouped expression (¬p ∨ q) ∧ r is false, while ¬p ∨ (q ∧ r) is true.

Identify the target boundary

Mark the exact occurrence of the subformula being replaced. A formula may contain several similar pieces. Replacing one, all, or only selected occurrences can each be a legitimate operation, but the result must match the operation described.

Do not perform a letter-level find-and-replace when the justification concerns a structured subformula. Symbols such as p or x can occur in different roles, and parentheses determine their boundaries.

A proof of replacement can be understood from inside out. Equivalent inputs supply the same truth value to the next connective, then to the next, until the whole formula receives the same value.

This explanation applies to truth-functional contexts. Statements about quotation, spelling or belief may depend on more than truth value. “The formula contains an arrow symbol” changes when p → q is rewritten as ¬p ∨ q, even though the represented propositions are equivalent.

The setting of the replacement matters. Equivalence of truth conditions does not make two written strings identical objects.

Contents · Previous chapter · Next chapter

A proof of A ↔ B can often be organised as two subproofs: assume A and derive B; then assume B and derive A. The two directions explain why neither formula is stronger than the other under the standing premises.

Consider p ∧ (q ∨ r) and (p ∧ q) ∨ (p ∧ r). From the first, obtain p and q ∨ r. In the q case, form p ∧ q and introduce the disjunction. In the r case, form p ∧ r and introduce the same disjunction.

For the reverse direction, split on the outer disjunction. Either conjunction supplies p and one of q or r, so each case gives p ∧ (q ∨ r).

Why a single direction is insufficient

If a proof establishes only p ∧ q → p, it has shown consequence but not equivalence. The omitted reverse direction is false in general.

A two-way layout therefore doubles as a diagnostic. If one direction repeatedly fails, look for a counterexample before attempting more complicated proof steps. The claim may simply be stronger than its proposed counterpart.

Some proof systems provide derived equivalence rules that allow a shorter solution. A shorter proof is useful when its rule and side conditions are known. During learning, expanding one example makes the dependencies easier to inspect.

The final statement should retain any assumptions used in both directions. If the derivation relies on r, the equivalence may hold only under r. Removing that premise from the report would strengthen the result beyond the proof.

Equivalence is a relation among formulas within a logical setting. The proof supplies a reason for it; a familiar-looking pattern is not itself that reason.

Contents · Previous chapter · Next chapter

In classical first-order logic, ¬∀x P(x) is equivalent to ∃x ¬P(x), and ¬∃x P(x) is equivalent to ∀x ¬P(x). The negation moves through the quantifier while changing its kind.

For a more structured example, negate ∀x(A(x) → B(x)). First obtain ∃x ¬(A(x) → B(x)). Then replace the negated conditional with A(x) ∧ ¬B(x). The result is ∃x(A(x) ∧ ¬B(x)).

This describes a counterexample: an A-object that lacks B. It is not the same as ∀x(A(x) → ¬B(x)), which says no A-object has B.

A mixed model separates the wrong replacement

Let domain {u,v}, with A true of both objects and B true only of u. “Not all A are B” is true because v is a counterexample. “No A are B” is false because u has both properties.

The exact scope of the negation matters. In ¬∀x P(x), the whole universal is negated. In ∀x ¬P(x), every individual instance is negated. These need not agree.

A reliable sequence writes one justified transformation per line. This is especially valuable when a formula contains nested quantifiers and implications. Moving every symbol at once can conceal where a negation was lost.

The guide uses classical equivalence. In an intuitionistic setting, not every classical quantifier-negation direction is available without additional assumptions. A learner should state the logic rather than treating every familiar rewrite as universally valid across proof systems.

Contents · Previous chapter · Next chapter

A common classical equivalence is (∀x P(x)) ∧ Q ≡ ∀x(P(x) ∧ Q), provided x is not free in Q and the domain is nonempty. Q must retain the same truth value as x varies.

If Q contains a free x, moving the quantifier can capture that occurrence. The original and rewritten formulas may disagree.

Consider (∀x P(x)) ∧ Q(x). Its x in Q is free. Let the domain be {0,1}, let P hold of both objects and let Q hold only of 0. Under assignment x = 0, the original formula is true.

The proposed replacement ∀x(P(x) ∧ Q(x)) is false because Q(1) fails. The edit has changed an assignment-dependent condition into a universal requirement.

Rename before moving when appropriate

If a bound variable conflicts with a free variable elsewhere, first rename the binder to a fresh z. The original becomes (∀z P(z)) ∧ Q(x). A safe moved version is ∀z(P(z) ∧ Q(x)), under the stated nonempty-domain convention.

The free x stays free, and z has no free occurrence in Q(x). The side condition is now satisfied.

Domain assumptions can also matter. With an empty domain, a universal sentence can be true even when Q is false, so some outward-movement equivalences need separate treatment. This guide keeps the standard nonempty-domain convention explicit.

A side condition is part of the theorem. Quoting the displayed pattern while omitting “x is not free in Q” removes the protection that makes the pattern valid. The correct rewrite includes both the shape and its applicability check.

Contents · Previous chapter · Next chapter

Universal quantification distributes over conjunction: ∀x(P(x) ∧ Q(x)) is equivalent to (∀x P(x)) ∧ (∀x Q(x)). Each object must satisfy both, which is the same as every object satisfying P and every object satisfying Q.

Existential quantification distributes over disjunction: ∃x(P(x) ∨ Q(x)) is equivalent to (∃x P(x)) ∨ (∃x Q(x)). A witness to either side supplies a witness to the disjunction.

The superficially parallel rules do not all work. ∃x(P(x) ∧ Q(x)) implies (∃x P(x)) ∧ (∃x Q(x)), but the reverse can fail because the witnesses may differ.

A two-object counterexample

Let P = {u} and Q = {v} on domain {u,v}. Both separate existential statements are true. No object has both properties, so the existential conjunction is false.

Likewise, ∀x(P(x) ∨ Q(x)) need not imply (∀x P(x)) ∨ (∀x Q(x)). In the same model, every object has at least one property, but neither property holds universally.

The reverse implication in that last comparison does hold. If every object has P, then every object has P or Q; similarly if every object has Q.

The pattern therefore contains equivalences and one-way implications. A list of symbols alone can make them look symmetric, so mark each arrow carefully.

The repair is to ask about witnesses and coverage. A conjunction under an existential needs one shared witness. A disjunction under a universal allows different objects to satisfy different alternatives. These semantic explanations expose the precise reason the tempting distribution fails.

Contents · Previous chapter · Next chapter

Two formulas may be equivalent under an additional premise without being logically equivalent on their own. If Γ is the standing premise set, Γ entails A ↔ B means they agree in every interpretation satisfying Γ.

For example, under the premise q, p and p ∧ q agree. Without q, they differ when p is true and q false.

A replacement justified relative to q is safe only while that assumption remains available in the context of the reasoning. Reporting it as an unconditional logical identity loses the condition.

Track the scope of the premise

In a subproof assuming q, one may use the resulting equivalence locally. After discharging q, the final statement must incorporate that dependence, for example as q → (p ↔ (p ∧ q)).

The formula q → (p ↔ (p ∧ q)) is classically valid. The formula p ↔ (p ∧ q) alone is not.

A similar distinction appears in mathematical domains. x² = 4 and x = 2 are equivalent under x ≥ 0 over the reals. That condition must remain part of the problem or the reported conclusion.

When editing a proof, record the reason for each replacement: unconditional logical equivalence, equivalence under a premise, or an algebraic equivalence under a domain restriction. Each permits a different scope of use.

A practical reading check

If a source says “under these assumptions,” underline the assumptions before copying the formula. The words are doing mathematical work. A theorem with a condition is not a weaker presentation of an unconditional theorem; it is a different statement.

This habit prevents a common transfer error: remembering the attractive central equation while dropping the clause that made it true.

Contents · Previous chapter · Next chapter

Exercise 1: one-way consequence

Are p and p ∧ q equivalent? No. Use p = true, q = false. State the valid direction: p ∧ q entails p.

Exercise 2: a safe context replacement

Replace p → q in (p → q) ∧ r. The result is (¬p ∨ q) ∧ r. Keep the grouping. The expression ¬p ∨ (q ∧ r) is not generally equivalent.

Exercise 3: negate a restricted universal

Negate ∀x(A(x) → B(x)). The classically equivalent result is ∃x(A(x) ∧ ¬B(x)). Identify the witness as an A-object that fails B.

Exercise 4: preserve a free variable

Rewrite (∀x P(x)) ∧ Q(x) by moving a quantifier safely. First rename the bound x to fresh z, then use ∀z(P(z) ∧ Q(x)). The x remains free.

Exercise 5: distribution with separate witnesses

Over {u,v}, let P = {u} and Q = {v}. Evaluate ∃x(P(x) ∧ Q(x)) and (∃x P(x)) ∧ (∃x Q(x)). The first is false and the second true, so the proposed equivalence fails.

Transfer check

Choose a formula rewrite from a lesson. Identify its logical setting, exact target subformula and every side condition. Prove both directions or provide a complete truth table when appropriate.

Then deliberately remove one condition and seek a separating interpretation. A strong answer explains not only that the replacement failed, but which dependency, witness or scope boundary the omitted condition had protected.

Contents · Previous chapter · Next chapter

Frequently asked questions

If two formulas are true in the same model, are they equivalent? Not necessarily. Logical equivalence requires agreement across the full permitted class.

Can one implication justify arbitrary replacement? No. Equivalence supplies two-way truth preservation; a one-way implication needs more careful context reasoning.

Can bound-variable renaming preserve meaning? Yes, when it preserves binding and avoids capture. It is a different operation from changing a free variable’s assigned role.

Do classical equivalences hold in every logic? No. State the logic and use its permitted rules.

Connected reading

Return to Mathematical Logic for the full subject. The quantifier guide develops shared and dependent witnesses. The countermodel guide explains why a separating interpretation is decisive.

Sources and scope

Truth-functional replacement was checked against forall x: Calgary, Proving Equivalences. Variable and quantifier conventions follow Sentences of FOL and the Open Logic Project syntax and semantics reference. Accessed 22 October 2026. Tables, two-way arguments and counterexamples here are original teaching constructions in the explicitly stated classical setting.

Contents · Previous chapter · Continue to Mathematical Logic