You are here


16 June, 2015 - 16:21
Available under Creative Commons-ShareAlike 4.0 International License. Download for free at

What is the most natural way to prove an existential sentence, like "there exists a prime num ber greater than 5"? That's easy you just mention such a number, like 11, and show that it is indeed prime and greater than 5. In other words, once we prove

(11>5)\wedge \forall j:(\forall k:((11=jk)\Rightarrow (j=1)\vee (k=1)))

we can then conclude --  using the inference rule ∃Intro that the formula ∃p : ((p> 5) ∧∀j :(∀k : ((p = jk) ⇒ (j = 1) ∨ (k = 1)))) is true. In general, to prove a for mula of the form ∃x :(φ), we show that φ holds when x is replaced with some particular witness. (The witness was 11 in this example.) The inference rule is \phi\begin{bmatrix} p\leftrightarrow c \end{bmatrix}\vdash \exists p:\left ( \phi \right ).The notation "φ[vw]" means the formula φ but with every occurrence of v replaced by w. For example, we earlier wrote down the formula φ[p→11], and then decided that this was sufcient to conclude ∃p :(φ).

Note: Observe that you'll never use the substitution-notation " φ[...→...]" as part of a literal formula it is only used in the inference rule, as a shorthand to describe the actual formula. (It's a pattern-matching metalanguagel)
Note: While it seems like substitution should be a simple textual search-and-replace, it is sometimes more complicated. In the formula φ =(x> 5) ∧∃x :(R (x)), we don't want φ[x→6] to try to mention R (6), much less generate something nonsensical like ∀6:(... ). In programming languages, we say we want "hygienic macros", to respect our the language's notions of variables and scope. E.g., the C pre-processor's #define and #include notably does not respect hygiene, and can inadvertently lead to hard-to-find bugs. Solution: For simplicity, we will always consistently rename variables (p. 94) so that each quantifier binds a distinct variable.

How do you find a witness? That's the difficult part. You, the person creating the proof, must grab a suitable example out of thin air, based on your knowledge of what you want to prove about it. In our previous example, we used our knowledge about prime numbers and about the greater-than relation to pick a witness that would work. In essence, we fgured out what facts needed to be true about the witness for the formula to hold, and used that to guide our choice of witness. Of course, this can easily be more difcult, as when proving that there exists a prime greater than 6971 of the form 4x 1. (It turns out that 796751 will sufce as a witness here.) Another approach is trial-and-error: Pick some candidate value, and see if it does indeed witness what you're trying to prove. If you succeed, you're done. If not, pick another candidate.