Inference with quantifiers Proving first-order sentences with inference rules is not too different than for propositional ones. We have two slight twists to add: upgrading propositions to relations, and quantifiers. We still keep all our original propositional inference rules, but declare they can now be used on first-order WFFs. For our quantifiers, we introduce new first-order inference rules for adding and eliminating quantifiers from formulas. These four new rules look surprisingly simple, but they do have a couple of subtleties we have to keep track of.

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 j1 k1 we can then conclude — using the inference rule ∃Intro — that the formula p p5 j k p jk j1 k1 is true. In general, to prove a formula 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 φ[p↦c] ⊢ pφ. The notation “φ[v↦w]” 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 sufficient to conclude p φ . 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 metalanguage!) While it seems like substitution should be a simple textual search-and-replace, it is sometimes more complicated. In the formula φ x 5 x Rx , we don't want φ[x↦6] to try to mention R6, 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 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 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 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) c, and end up concluding “c is a prime bigger than 5”. The caveats are that c 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 c along with universal formulas to get useful statements. Thus the general form of the rule is that pφ ⊢ φ[p↦c]. That is, we can rewrite the body of the exists, replacing the quantified variable p with any new variable name c, 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 n is prime, then we know that …” and “A person X who runs a business should always …”. Which n 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 n” or “For all [any] persons X”. 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: A variable is not arbitrary if it is free in (an enclosing) premise. A variable is not arbitrary if it is free after applying ∃Elim — either as the introduced witness c, or free anywhere else in the formula. The usual way to introduce arbitrary variables is during ∀Elim (w/o later using it in ∃Elim). The formal inference rule for introduction of universal quantification will use these cases as restrictions.

Forall-Elim Getting rid of universal quantifiers is easy: if you know xφ (where φ is a formula presumably involving x), well then you can replace x with anything you want, and the resulting formula will be true. We say xφ ⊢ φ[x↦t] where t is any term. Any variables in t are arbitrary, unless it is an already-existing non-arbitrary variable. For example, suppose we know that n primen n 2 oddn . We can replace n with some term like m4 to conclude prime m4 m 4 2 odd m4 . The variable m 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 (note the absence of the initial ∀); n 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.

Formal inference rules and proofs Recall the syllogisms from a previous lecture. The general form of a syllogism is x Px Qx [major premise] Pc [minor premise] Qc [conclusion] In our system, we don't have syllogism as a separate rule of inference, but it's easy to see how to translate any syllogism into our system: (for specific relations P and Q, and a specific constant c). 1x Px Qx Premise 2Pc Premise 3 Pc Qc ∀Elim, by line 1, with x c 4Qc ⇒Elim, by lines 2,3, with φ Pc and ψ Qc

Eliminating a quantifier via ∀Elim and ∃Elim is often merely an intermediate step, where the quantifier will be reintroduced later. This moves the quantification from being explicit to implicit, so that we can use other inference rules on the body of the formula. When this is done, it is very important to pay attention to the restrictions on ∀Intro, so that we don't accidentally “prove” anything too strong. x y φ ⊢ y x φ , for the particular case of φ Rxy (other cases all similar). 1x y Rxy Premise 2y Rpy ∃Elim, line 1 3Rpq ∀Elim, line 2 4x Rxq ∃Intro, line 3 5y x Rxy ∀Intro, line 4

Remember that in line 5, for ∀Intro, we must verify that q is arbitrary. It is, since it was introduced in line 3 by ∀Elim, and there hasn't been an intervening ∃Elim between lines 3 and 5. We cannot instead conclude in line 4 that x Rxq by ∀Intro, since variable p was introduced by ∃Elim in line 2, and therefore not arbitrary. Let's reverse the previous proof goal: y x φ ⊢ x y φ , for the particular case of φ Rxy (other cases all similar). This statement does not hold in general. So, what's the problem with the following “proof”? 1y x Rxy Premise 2x Rxq ∀Elim, line 1 3Rpq ∃Elim, line 2 4y Rpy ∀Intro, line 3 5x y Rxy ∃Intro, line 4

In line 4, ∀Intro requires that variable being generalized, q, be arbitrary. It was introduced in line 2 by ∀Elim, so that's OK. (E.g., we could've used ∀Intro on line 3 to reintroduce the quantifier just eliminated.) But, q was free when we used ∃Elim on line 3, and this makes the variable no longer arbitrary. Line 3's choice of p may depend on q, and a variable is only arbitrary if it is free of any such constraints. The ∀Intro principle is actually very familiar. For instance, after having shown a b ⊢ a b , we then claimed this was really true for arbitrary propositions instead of just a,b. (We actually went a bit further, generalizing individual propositions to entire (arbitrary) WFFs φ,ψ. This could only be done because in any particular interpretation, a formula φ will either be true or false, so replacing it by a proposition still preserves the important part of the proof-of-equivalence.) The ∀Intro is also used in many informal proofs. Consider: “If a number n is prime, then …”. This translates to “ primen … ”, where n is arbitrary. We are entirely used to thinking of this as “n primen … ” even though “n” was introduced as if it were a particular number.

Proofs and programming We previously saw that the inference rules of propositional logic are closely related to the process of type checking. The same holds here. For example, in many programming languages, we can write a sorting function that works on any type of data. It takes two arguments, a comparison function for the type and a collection (array, list, …) of data of that type. The type of the sorting function can then be described as “for all types T, given a function of type (T and T) → T, and data of type (collection T), it returns data of type (collection T)”. This polymorphic type-rule uses universal quantification. Note that the details about substitutions and capture noted here arise in any kind of program that manipulates expressions with bound variables. That includes not only automated theorem provers, but compilers. To avoid such issues, many systems essentially rename all variables by using pointers or some similar system of each variable referring to its binding-site. When people speak of proofs written by computer, they're talking about this style of inference rule proofs.