Exists-intro

What is the most natural way to prove an existential sentence, like “there exists a prime number 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∧∀j:∀k:11=jk⇒j=1∨k=1 11 5 j k 11 jk j1 k1 we can then conclude — using the inference rule ∃∃Intro — that the formula ∃p:p>5∧∀j:∀k:p=jk⇒j=1∨k=1p p5 j k p jk j1 k1 is true. In general, to prove a formula of the form ∃x:φx φ , we show that φφ holds when xx is replaced with some particular witness. (The witness was 11 in this example.) The inference rule is φ[p↦c] ⊢ ∃p:φφ[p↦c] ⊢ pφ. The notation “φ[v↦w]φ[v↦w]” means the formula φφ but with every occurrence of vv replaced by ww. For example, we earlier wrote down the formula φ[p↦11]φ[p↦11], and then decided that this was sufficient to conclude ∃p:φp φ .

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 figured 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 difficult, as when proving that there exists a prime greater than 6971 of the form 4x−1 4 x 1 . (It turns out that 796751 will suffice 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.

Exists-Elim

The complementary ∃∃Elim rule corresponds to giving a (new) name to a witness. Thus if you know “there exists some prime bigger than 5”, then by ∃∃Elim we can think of giving some witness the name (say) cc, and end up concluding “cc is a prime bigger than 5”. The caveats are that cc must be a new name not already used in the proof, and different from any variables free in the conclusion we're aiming for. However, we will be able to use that variable cc along with universal formulas to get useful statements.

Thus the general form of the rule is that ∃p:φ ⊢ φ[p↦c]pφ ⊢ φ[p↦c]. That is, we can rewrite the body of the exists, replacing the quantified variable pp with any new variable name cc, subject to the restrictions just mentioned.

Forall-Intro

Can we extend that idea to proving a universal sentence? One witness is certainly not enough. We'd need to work with lots of witnesses, in fact, every single member of our domain. That's not very practical, especially with infinitely large domains. We need to show that no matter what domain element you choose, the formula holds.

Consider the statements “If nn is prime, then we know that …” and “A person XX who runs a business should always …”. Which nn is being talked about, and which person? Well, any number or person, respectively. After learning about quantifiers, you may want to preface these sentences with “For all nn” or “For all [any] persons XX”. But a linguist might point out that while yes “for all” is related to the speaker's thought, they are actually using a subtly different mode — that of referring to a single person or number, albeit an anonymous, arbitrary one. If “an arbitrary element” really is a natural mode of thought, should our proof system reflect that?

If we choose an arbitrary member of the domain, and show that the sentence holds for it, that is sufficient. But, what do we mean by “arbitrary”? In short, it means that we have no control over what element is picked, or equivalently, that the proof must hold regardless of what element is picked. More precisely, a variable is arbitrary unless:

Forall-Elim

Getting rid of universal quantifiers is easy: if you know ∀x:φxφ (where φφ is a formula presumably involving xx), well then you can replace xx with anything you want, and the resulting formula will be true. We say ∀x:φ ⊢ φ[x↦t]xφ ⊢ φ[x↦t] where tt is any term. Any variables in tt are arbitrary, unless it is an already-existing non-arbitrary variable.

For example, suppose we know that ∀n:primen∧n>2⇒oddnn primen n 2 oddn . We can replace nn with some term like m+4m4 to conclude primem+4∧m+4>2⇒oddm+4 prime m4 m 4 2 odd m4 . The variable mm is arbitrary, unless it already occurred in non-arbitrary in a previous line of the proof (perhaps introduced via ∃∃Elim). A more usual step is to use a term which is just a single variable, and (by coincidence) happens to have the same name as the quantified variable we are eliminating. Thus we often conclude primen∧n>2⇒oddn primen n 2 oddn (note the absence of the initial ∀∀); nn is arbitrary (unless it had already been confusingly in use as a non-arbitrary variable earlier). This is helpful when we'll be later re-introducing the ∀∀ in a later step; see the example below.