0
$\begingroup$

According to ProofWiki, the principle of explosion says that:

$$p \implies (\lnot p \implies q)$$

but sometimes it's also stated as

$$(p \land \lnot p) \implies q$$

Can one be converted to the other? How do you prove or show these?

If we know that $(p \implies q) \equiv \lnot p \lor q$ by definition, then substituting the 2nd representation:

$$((p \land \lnot p) \implies q) \equiv \lnot(p \land \lnot p) \lor q \equiv \lnot p \lor p \lor q$$

Is this just true due to law of excluded middle? Like either $p$ or $\lnot p$ is true, i.e. $p \lor \lnot p \equiv \text{T}$ before we even get to whatever $q$ is. Is that why we're able to say it?

Then the first representation is weird too:

$$(p \implies (\lnot p \implies q)) \equiv (\lnot p \lor (\lnot p \implies q)) \equiv (\lnot p \lor (p \lor q)) \equiv \lnot p \lor p \lor q$$

I mean am I even on the right track here? How do you normally get these without "working backwards" and showing that they happen to be equivalent? Is there a more intuitive derivation of both of these?

|cite|improve this question
$\endgroup$
  • $\begingroup$ Yes, the two are equivalent. $\endgroup$ – Namaste Apr 5 '18 at 18:50
  • $\begingroup$ @amWhy Yes but I am asking something different than that $\endgroup$ – user525966 Apr 5 '18 at 18:52
  • 1
    $\begingroup$ @user525966 Those are just two ways to write that a false premise implies any conclusion. $\endgroup$ – dxiv Apr 5 '18 at 18:56
  • 1
    $\begingroup$ @Taroccoesbrocco you say the equivalence has nothing to do with excluded middle (and i don’t think it does) but you use the non intuitionistically valid demorgan law in your proof. $\endgroup$ – spaceisdarkgreen Apr 5 '18 at 19:28
  • 1
    $\begingroup$ @user525966 The “reason” behind the classical validity of a proposition can be difficult to untangle cause it all blends together. Intuitionistic logic is an example where excluded middle is not valid but explosion is. So inasmuch as intuitionistic logic is philosophically coherent for accepting one and not the other (there is another called “minimal logic” that rejects both), LEM cannot be the “reason” for explosion. $\endgroup$ – spaceisdarkgreen Apr 5 '18 at 19:49
2
$\begingroup$

The formulas $p \to (\lnot p \to q)$ and $(p \land \lnot p) \to q$ are equivalent because they are particular instances of a more general fact: the formulas $p \to (r \to q)$ and $(p \land r) \to q$ are equivalent. You can prove that checking that the two formulas actually have the same truth table. An alternative proof is the following:

\begin{align} p \to (r \to q) &\iff \lnot p \lor (\lnot r \lor q) &\text{by definition of } \to \\ &\iff (\lnot p \lor \lnot r) \lor q &\text{by associativity of } \lor \\ &\iff \lnot(p \land r) \lor q &\text{by De Morgan law} \\ &\iff (p \land r) \to q &\text{by definition of }\to \end{align}

|cite|improve this answer
$\endgroup$
  • $\begingroup$ @user525966 - Please, see my last edit. $\endgroup$ – Taroccoesbrocco Apr 5 '18 at 18:57
1
$\begingroup$

The two statements you post are logically equivalent.

$$\begin{align} p \to (\lnot p \to q) &\equiv \lnot p \lor (p \lor q) \tag{definion of $\to$}\\ \\ &\equiv (\lnot p \lor p) \lor q \tag{associativity of $\lor$}\\ \\ &\equiv \lnot (p \land \lnot p) \lor q \tag{DeMorgan's}\\ \\ &\equiv (p\land \lnot p)\to q\tag{definition of $\to$}\end{align}$$

You were heading in right direction, starting instead from $(p\land \lnot p)\to q$ and moving toward $p \to (\lnot p \to q)$. You just stopped too early. Note each direction can be proven, because we have a string of equivalencies: so to reverse the direction, just reverse the order of the steps.

$$\begin{align} (p\land \lnot p)\to q &\equiv \lnot (p \land \lnot p)\lor q\tag{definition of $\to$}\\ \\ &\equiv (\lnot p \lor p) \lor q\tag{DeMorgan's}\\ \\ &\equiv \lnot p\lor (p \lor q)\tag{associativity of $\lor$}\\ \\ &\equiv p\to (\lnot p \to q)\tag{definition of $\to$} \end{align}$$

First of all, we have $$p\to (q\to r) \vdash (p \land q) \to r\tag{importation}$$ and we have $$(p\land q) \to r \vdash p \to (q\to r)\tag{exportation}$$ Your question is a specific case of these, where $q = \lnot p$. See this link for more information.

|cite|improve this answer
$\endgroup$
  • $\begingroup$ How / why are you using $\vdash$ here? $\endgroup$ – user525966 Apr 5 '18 at 20:07
  • $\begingroup$ The turnstyle, $\vdash$ is the syntactic entailment operator. $\phi \vdash \psi$, symbolises that $\psi$ is derivable from $\phi$ ( or "...can be proven from..." ) using the syntactic transformations of some logic system. @user525966 $\endgroup$ – Graham Kemp Apr 6 '18 at 1:05
0
$\begingroup$

To get pernickety, we need to distinguish the principle about entailment what is usually called Explosion, i.e.

$(A \land \neg A) \vdash B$,

from the following principle that a conditional with a contradictory antecedent is always derivable:

$\vdash (A \land \neg A) \to B$.

You can have logics with one principle and not the other.

|cite|improve this answer
$\endgroup$
  • $\begingroup$ What's the difference between $\vdash$ and $\to$? I know the former is more "is derivable from" but I always thought that was what implies was, really $\endgroup$ – user525966 Apr 5 '18 at 19:42
  • $\begingroup$ @user525966 yes one is “derivable from” and is a metalogical relation (ie you use it to talk about the formal system) and the other is “implies” and is a logical connective (used within formal statements in the logic). They do oftentimes correspond exactly in the sense that we have $\vdash A\to B$ iff we have $A\vdash B$. One direction directly follows from the inference rule modus ponens if present. The other direction is called a deduction theorem and can be proved to apply to (for instance) one’s favorite deductive system for first order logic. $\endgroup$ – spaceisdarkgreen Apr 5 '18 at 20:05
  • $\begingroup$ @user525966 not sure why I forgot to add this yesterday but in natural deduction systems where this holds, the two directions are unified as introduction and elimination rules for implication. Whereas, the “deduction theorem” direction being a nontrivial metatheorem, as described above, is typical in Hilbert-style systems. $\endgroup$ – spaceisdarkgreen Apr 7 '18 at 2:07
  • $\begingroup$ What is metalogic, metatheory, exactly? $\endgroup$ – user525966 Apr 7 '18 at 2:39
  • $\begingroup$ @user525966 (You have to @ me so I get pinged). In logic, it is useful to distinguish between statements/proofs/theorems in formal systems and statements and results about formal systems (usually proven informally, using "ordinary mathematical reasoning", though we could formalize this too). The latter are called "meta_". "$\vdash A$" means "there is a formal proof of the statement $A$ in the deductive system under consideration"... that's a meta-statement about the system (and if true, $A$ is a (regular old) theorem of the system). See also: en.wikipedia.org/wiki/Metatheorem $\endgroup$ – spaceisdarkgreen Apr 7 '18 at 3:06

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.