12/21/06
Becoming familiar with common inference patterns and being able to use them via replacement rules. This helps with assessing ordinary everyday reasoning such as that found in the law, in newspapers, in advertisements, etc.
First, a little background... Introductory logic is often taught using one of two different styles of sets of inference rules. There are systems using 'Introlim' rules, where every connective has an introduction rule and an elimination rule, and all rules work on the main connective of a formula. And, alternatively, there are eclectic collections of rules of inference, often refined out of traditional forms, which seem more suited to everyday reasoning and brief formal proofs (you will see these in several standard introductory textbooks such as Copi or Hausman).
Both these styles of inference rules are somewhat at stress with ordinary reasoning. Take, for example, De Morgan's 'laws' ∼(F.G)≡∼F∨∼G. De Morgan came up with these 150 odd years ago as an encapsulation of one standard 'rule of thought'. Even folk that know little of logic use this kind of reasoning all the time, and they use it not merely on the main connective of a formula but also within the body of the formula itself. Imagine yourself at a health club and someone says
'If you are going to stick to your diet you can't have both cake and ice cream'
and the friend replies
'You mean if I am going to stick to my diet I'm either going to have to give up cake or ice cream'
Here is the inference pattern
D⊃ ∼(C.I) ∴ D⊃(∼C∨∼I)
And it is a valid inference. But if you prove this inference within our system, it can take a fair amount of work.
In the real world, the health club exerciser would merely, consciously or unconsciously, look at the red subformula and make the substitution to blue via De Morgan's law.
D⊃ ∼(C.I) ∴ D⊃(∼C∨∼I)
In part what we are trying to do in the course is to help students to reason correctly and to appraise the reasoning of others (in life, in law, on television, in advertisements, in other academic fields etc.). We can make a gesture toward the latter end by permitting De Morgan, and other common types of inference patterns via what is known as 'replacement' or 'rewrite' rules.
The program has in it an additional menu item called Rewrite Rules (under the Advanced Menu) and it lists the following named patterns.
The way these are used is that a line in a proof is selected, say one with D⊃ ∼(C.I) on it, and Rewrite Rules are selected from the menu. Then a particular rewrite rules is selected (eg De Morgan) and a subformula. The program will then display what the rewrite looks like. And, if it is acceptable, it can be added to the proof. The interface looks like this:
What is mentioned in the rewrite rules are patterns. And the symbol '::' means that occurrences of the pattern on the left can be rewritten to the pattern on the right, and the pattern on the right can be rewritten to the pattern on the left. Then, of course, the symbol ':-' means that the pattern on the left can be rewritten to that on the right (but not from right to left). In the De Morgan illustration in the image, the rule is being used from right to left on a subformula of the original formula (exactly as in the Health Club).
There are a number of well-known theorems which express equivalences between formulas. Experienced logicians know these off by heart. You have already derived many of them. Be sure you can derive the rest. Feel free to use rewrite rules on these.
Absorption1) (F∨(F.G))≡F
2) ∴ (F.(F∨G))≡F
3) ∴ (F⊃(F⊃G))≡(F⊃G)
Association
4) ∴ F∨(G∨H)≡(F∨G)∨H
5) ∴ F.(G.H)≡(F.G).H
Proofs
Commutation
6) ∴ F∨G≡G∨F
7) ∴ F.G≡G.F
8) ∴ (F≡G)≡(G≡F)
9) ∴ F⊃(G⊃H)≡G⊃(F⊃H)
10) ∴(F⊃G)≡(∼G⊃∼F)
Proofs
11) ∴ ∼(F.G)≡∼F∨∼G
12) ∴ ∼(F∨G)≡∼F.∼G
13) ∴ F.(G∨H)≡(F.G)∨(F.H)
14) ∴ F∨(G.H)≡(F∨G).(F∨H)
15) ∴ F≡∼∼F
Proofs
16) ∴ (F≡G)≡(F⊃G).(G⊃F)
17) ∴ (F≡G)≡(F.G)∨(∼F.∼G)
18) ∴ F∨∼F
19) ∴ (F⊃(G⊃H))≡((F.G)⊃H)
20) ∴ (F.F)≡F
21) ∴ (F∨F)≡F
Proofs
22) ∴ F⊃G≡∼F∨G
23) ∴ (F⊃G)≡∼(F.∼G)
24) ∴ (F∨G)≡(∼F⊃G)
25) ∴ (F.G)≡∼(F⊃∼G)
26) ∴ (F≡G)≡ ((F⊃G) . (G⊃F))
Proofs
27) F⊃G,G⊃H∴F⊃H
28) ∴ F⊃G≡∼G⊃∼F
Proofs