0

How do I formalize this phrase from an informal proof using some form of natural deduction:

We claim that X. To obtain a contradiction, assume that Y.

https://digitalcommons.kennesaw.edu/cgi/viewcontent.cgi?article=2161&context=facpubs (p.2 of pdf)

Maybe something like:

  1. $X~~~$(Assume)
  2. $Y~~~$(Assume)

$~~~~~~~\vdots$

$~~~~$n. $Z \land \neg Z$

$~~~~$???

Doesn't make sense.

Dan Christensen
  • 14,529
  • If you claim that statement $X$ holds true and you want to derive a contradiction to prove $X$, then this means that $X$ has the form $p \rightarrow q$. Then to get the contradiction you assume $p \wedge \neg q$, so if your $X$ is $p \rightarrow q$, then your $Y$ must be $p \wedge \neg q$, and the contradiction will come in the form $Z \wedge \neg Z$ as you said, for some statement $Z$. – Rick May 21 '20 at 20:07

1 Answers1

1

You're leaping too quickly to the attempted formalization; the informal passage in question needs further analysis.

Basically, a passage like

"We claim that $X$. To obtain a contradiction, assume $Y$"

is shorthand for

"We claim that $X$. To prove this, suppose $\neg X$. Then because [reasons], we have $Y$."

The original passage has two implicit claims:

  • The way we're going to prove $X$ is via contradiction.

  • The claim $Y$ is a consequence of $\neg X$.

The first point is simple enough, but the latter can be problematic: it's only really appropriate if we can "easily" prove $\neg X\rightarrow Y$ to the point that it's not worth mentioning. Whether or not a given usage is appropriate is of course subjective.

So, for example, the first argument in the linked text "unfolds" to the following:

Claim: If $X$ is a poset in which every chain has an upper bound, then $X$ has a maximal element.

Proof: Suppose not. Let $X$ be a counterexample. Then $X$ has no maximal element, so $[\mathit{stuff}]$. But that gives us a chain in $X$ with no upper bound, which can't happen because $X$ - being a counterexample to the claim - must have the property that every chain has an upper bound.

Somewhat more formally, this amounts to something like the following:

  • Begin subproof:

    • Assume $\neg(\forall X[\mathit{chainbound(X)}\rightarrow\mathit{maxelt(X)}])$.

    • Then $\exists X[\mathit{chainbound(X)\wedge\neg maxelt(X)}]$.

    • Do existential instantiation - introducing a specific counterexample $C$.

    • In particular, $C$ has no maximal element.

    • Deduce $\perp$.

  • Discharge the assumption so that we get $\neg(\forall X[\mathit{chainbound(X)}\rightarrow\mathit{maxelt(X)}])\rightarrow\perp$.

  • From that, conclude $\forall X[\mathit{chainbound(X)}\rightarrow\mathit{maxelt(X)}]$.

Of course that's neither complete ("Deduce $\perp$" :P) nor correctly formed (exactly how subproofs/discharging assumptions are presented will be determined by the system you're using), but it should suggest how to proceed.

Noah Schweber
  • 245,398