Loading [MathJax]/jax/output/HTML-CSS/jax.js
Skip to main content
Library homepage
 

Text Color

Text Size

 

Margin Size

 

Font Type

Enable Dyslexic Font
Mathematics LibreTexts

2.4: Rules of Inference

( \newcommand{\kernel}{\mathrm{null}\,}\)

Having established our set Λ of logical axioms, we must now fix our rules of inference. There will be two types of rules, one dealing with propositional consequence and one dealing with quantifiers.

Propositional Consequence

In all likelihood you are familiar with tautologies of propositional logic. They are simply formulas like (AB)(¬B¬A). If you are comfortable with tautologies, feel free to skip over the next couple of paragraphs. If not, what follows is a very brief review of a portion of propositional logic.

We work with a restricted language P, consisting only of a set of propositional variables A,B,C, and the connectives and ¬. Notice there are no quantifiers, no relation symbols, no function symbols, and no constants. Formulas of propositional logic are defined as being the collection of all ϕ such that either ϕ is a propositional variable, or ϕ is (¬α), or ϕ is (αβ), with α and β being formulas of propositional logic.

Each propositional variable can be assigned one of two truth values, T or F, corresponding to truth or falsity. Given such an assignment (which is really a function v:propositional variables{T,F}), we can extend v to a function ˉv assigning a truth value to any propositional formula as follows:

ˉv(ϕ){v(ϕ)ifϕis a propositional variableFifϕ:≡(¬α)andˉv(α)=TFifϕ:≡(αβ)andˉv(α)=ˉv(β)=FTotherwise

Now we say that a propositional formula ϕ is a tautology if and only if ˉv(ϕ)=T for any truth assignment v.

One way that you can check whether a given ϕ is a tautology is by constructing a truth table with one row for each possible combination of truth values for the propositional variables that occur in ϕ. Then you fill in the truth table and see whether the truth value associated with the main connective is always true. For example, consider the propositional formula A(BA), which is translated to ¬A(¬BA). The truth table verifying that this formula is a tautology is

AB¬A(¬BA)TTFTFTTTFFTTTTFTTTFFFFFTTTTF

To discuss propositional consequence in first-order logic, we will transfer our formulas to the realm of propositional logic and use the idea of tautology in that area. To be specific, given β, an L-formula of first-order logic, here is a procedure that will convert β to a formula βP of propositional logic corresponding to β:

  1. Find all subformulas of β of the form xα that are not in the scope of another quantifier. Replace them with propositional variables in a systematic fashion. This means that if yQ(y,c) appears twice in β, it is replaced by the same letter both times, and distinct subformulas are replaced with distinct letters.
  2. Find all atomic formulas that remain, and replace them systematically with new propositional variables.
  3. At this point, β will have been replaced with a propositional formula βP.

For example, suppose that we look at the L-formula

(xP(x)Q(c,z))(Q(c,z)xP(x)).

For the first step of the procedure above, we replace the quantified subformulas with the propositional letter B:

(BQ(c,z))(Q(c,z)B).

To finish the transformation to a propositional formula, replace the atomic formula with a propositional letter:

(BA)(AB).

Notice that if βP is a tautology, the β is valid, but the converse of this statement fails. For example, if β is

[(x)(θ)(x)(θρ)](x)(ρ),

then β is valid, but βP would be [AB]C, which is certainly not a tautology.

We are now almost at a point where we can state our propositional rule of inference. Recall that a rule of inference is an ordered pair (Γ,ϕ), where Γ is a set of L-formulas and ϕ is an L-formula.

Definition 2.4.1. Suppose that ΓP is a set of propositional formulas and ϕP is a propositional formula. We will say that ϕP is a propositional consequence of ΓP if every truth assignment that makes each propositional formula in ΓP true also makes ϕP true. Notice that ϕP is a tautology if and only if ϕP is a propositional consequence of .

Lemma 2.4.2. If ΓP={γ1P,γ2P,,γnP} is a nonempty finite set of propositional formulas and ϕP is a propositional formula, then ϕP is a propositional consequence of ΓP if and only if

[γ1Pγ2PγnP]ϕP

is a tautology.

Proof. Exercise 3.

Now we extend our definition of propositional consequence to include formulas of first-order logic:

Definition 2.4.3. Suppose that Γ is a finite set of L-formulas and ϕ is an L-formula. We will say that ϕ is a propositional consequence of Γ if ϕP is a propositional consequence of ΓP, where ϕP and ΓP are the results of applying the procedure above uniformly to ϕ and all of the formulas in Γ.

Example 2.4.4. Suppose that L contains two unary relation symbols, P and Q. Let Γ be the set

{xP(x)yQ(y),yQ(y)P(x),¬P(x)(y=z)}.

If we let ϕ be the formula xP(x)¬(y=z), then by applying our procedure uniformly to the elements of Γ and ϕ, we see that.

ΓPis{AB,BC,¬CD}

and ϕP is A¬D, where the fact that we have substituted the same propositional variables for the same formulas in ϕ and the elements of Γ is ensured by our applying the procedure uniformly to all of the formulas in question. At this point it is easy to verify that ϕ is a propositional consequence of Γ.

Finally, our rule of inference:

Definition 2.4.5. If Γ is a finite set of L-formulas, ϕ is an L-formula, and ϕ is a propositional consequence of Γ, then (Γ,ϕ) is a rule of inference of type (PC).

Chaff: All of this formalism just might be hiding what is really going on here. What rule (PC) says is that if you have proved γ1 and γ2 and [(γ1γ2)ϕ]P is a tautology, then you may conclude ϕ. Nothing fancier than that.

Also notice that if ϕ is a formula such that ϕP is a tautology, rule (PC) allows us to assert ϕ in any deduction, using Γ=.

Quantifier Rules

The motivation behind our quantifier rules is very simple. Suppose, without making any particular assumptions about x, that you were able to prove "x is an ambitious aardvark". Then it seems reasonable to claim that you have proved "(x)x is an ambitious aardvark". Dually, if you were able to prove the Riemann Hypothesis from the assumption that "x is a bossy bullfrog", then from the assumption "(x)x is a bossy bullfrog", you should still be able to prove the Riemann Hypothesis.

Definition 2.4.6. Suppose that the variable x is not free in the formula ψ. Then both of the following are rules of inference of type (QR):

({ψϕ},ψ(xϕ))

({ϕψ},(xϕ)ψ).

The "not making any particular assumptions about x" comment is made formal by the requirement that x not be free in ψ.

Chaff: Just to make sure that you are not lost in the brackets of the definition, what we are saying here is that if x is not free in ψ:

  1. From the formula ψϕ, you may deduce ψ(xϕ).
  2. From the formula ϕψ, you may deduce (xϕ)ψ.

Exercises

  1. We claim that the collection Λ of logical axioms is decidable. Outline an algorithm which, given an L-formula θ, outputs "yes" if θ is an element of Λ and outputs "no" if θ is not an element of Λ. You do not have to be too fussy. Notice that you have to be able to decide if a term t is substitutable for a variable x in a formula ϕ. See Exercise 7 in Section 1.8.
  2. Show that the set of rules of inference is decidable. So outline an algorithm that will decide, given a finite set of formulas Γ and a formula θ, whether or not (Γ,θ) is a rule of inference.
  3. Prove Lemma 2.4.2.
  4. Write a deduction of the second quantifier axiom (Q2) without using (Q2) as an axiom.
  5. For each of the following, decide if ϕ is a propositional consequence of Γ and justify your assertion.
    (a) Γ is {(P(x))Q(y),(xP(x))(xR(x)),x¬R(x)}; ϕ is Q(y).
    (b) Γ is {x=yQ(y),Q(y)x+y<z}; ϕ is x+y<z.
    (c) Γ is {P(x,y,x),x<yM(w,p),(¬P(x,y,x))(¬x<y)}; ϕ is ¬M(w,p).
  6. Prove that if θ is not valid, then θP is not a tautology. Deduce that if θP is a tautology, then θ is valid.

This page titled 2.4: Rules of Inference is shared under a CC BY-NC-SA 4.0 license and was authored, remixed, and/or curated by Christopher Leary and Lars Kristiansen (OpenSUNY) via source content that was edited to the style and standards of the LibreTexts platform.

Support Center

How can we help?