Introduction

Algebra and Calculations

For an informal introduction with hints, advice, philosophy, and pointers to tools see [ logic_20_Proofs100.html ] and come back here later if knowing the rules might help.

This introduces logic from the point of view of a computer professional using ASCII. For the traditional methods see [ pfnot.html ] and [ bpf.html ]

Two Systems of Proof

Natural Deduction

Algebra and Calculations

Natural Deduction

First, propositions can be deduced directly from what is currently held to be true. In the following table the rules are written as wffs: `if P and R then Q means that P, R|-Q` is a valid step in an demonstration.

Similarly, a rule written like this "P iff Q" validates deductions like this: P|-Q and like this: Q|-P. But most powerful of all they allow the substitution of P for Q in any other formula: W(P) iff W(Q) or expression f(P) = f(Q). However in these two last case we must be sure that that if W(_) or f(_) bind any free variables that are in P then Q must have the same free variables.

Valid Deductive Steps

 ( evidence ) |- ( label_of_result ): result .

evidence

Block Structure

In most documentation (and math texts!) the reasons are likely to be incomplete and so not guaranteed to be valid. People tend to tighten up their reasoning when contradictions force them to[Lakatos]. At the least, people usually omit the labels of the [ Valid Deductions ] tabulated below.

Here are some common abbreviated reasons:
Shown Meaning Formal meaning
(-1) Using the previous result (New Jun 28th 2007)
(-2) Using the previous two results (New Jun 28th 2007)
(above) I'm too lazy to work out which evidence I need here All above assertions at this level.
() I'm too hurried to type above (above)
(given) I've been told that... Axiom
(goal) I'm trying to prove or find this.
(let) For the sake of argument let... Assumption [ Block Structure ]
(hyp) I just assumed this Label of statements after last Let
(RAA) Reducto Ad Absurdum The assumption in the above Let lead to a contradiction.

Shown	Meaning	Formal meaning
(-1)	Using the previous result (New Jun 28th 2007)
(-2)	Using the previous two results (New Jun 28th 2007)
(above)	I'm too lazy to work out which evidence I need here	All above assertions at this level.
()	I'm too hurried to type above	(above)
(given)	I've been told that...	Axiom
(goal)	I'm trying to prove or find this.
(let)	For the sake of argument let...	Assumption [ Block Structure ]
(hyp)	I just assumed this	Label of statements after last Let
(RAA)	Reducto Ad Absurdum	The assumption in the above Let lead to a contradiction.

Blatant Assertion

The syntax is like this

 		|- (label): axiom.

 		(reasons) |- (label): conclusion

 		(label): expression.

Valid Deductions

Simple Propositions

Algebra and Calculations

|- (and1): If P and Q then P.
|- (and2): If P and Q then Q.
|- (demorgan1): not(P and Q) iff not P or not Q.
|- (and3): If P and Q then (P and Q), -- combines two proven results into one.
|- (and4): P and P iff P, idempotent.
|- (and5): P and Q iff Q and P, commutative.
|- (and6): (P and Q) and R iff P and (Q and R), associative`.
|- (or1): If (P or Q) and not P then Q, modus tolens.
|- (or2): If (P or Q and not Q then P, modus tolens.
|- (or3): P or P iff P, idempotent.
|- (or4): (P or Q) iff (Q or P), commutative.
|- (or5): (P or Q) or R iff P or (Q or R), associative.
|- (demorgan2): not(P or Q) iff not P and not Q.
|- (nor1): If not(P or Q) then not P.
|- (nor2): If not(P or Q) then not Q.
(above)|- (dn1): if not not P then P.
(above)|- (dn2): if P then not not P.
|- (dist1): P and (Q or R) iff (P and Q) or (P and R).
|- (dist2): P or (Q and R) iff (P or Q) and (P or R).
|- (abs1): P and(P or Q) iff (P or Q).
|- (abs2): P or (P and Q) iff (P and Q).
|- (mp): If (P and(if P then Q)) then Q, modus ponens.
|- (mtp): If (not Q) and (if P then Q) then not P, modus tolendo ponens.
(mp)|- (iftrans): If (if P then Q) and (if Q then R) then (if P then R).
|- (nif1): If not(if P then Q) then P.
|- (nif2): If not(if P then Q) then not Q.
|- (nif3): If not(if P then Q) then P and not Q.
(nif1, nif2, nif3)|- (nif4): not(if P then Q) iff P and not Q.
|- (iff1): If (P iff Q) then (if P then Q).
|- (iff2): If (P iff Q) then (if Q then P).
|- (iff3): If ((if Q then P) and (if Q then P)) then (P iff Q).
(dn1, dn2, iff3)|- (dn): not not P iff P.
|- (iff4): (P iff Q) iff ( ((Q and P) or (not P and not Q))).
(iff4)|- (iff5): (P iff Q)iff(Q iff P), commutative.
(above)|- (iff6): (P iff (Q iff R) iff ((P iff Q) iff R), associative.
(above)|- (ifftrans): If (P iff Q) and (Q iff R) then (P iff R).
|- (niff): If not (P iff Q) then ((Q and not P) or (not P and Q)).
|- (qn1): not for some x:T(W(x)) iff for all x:T(not W(x)).
|- (qn2): not for all x:T(W(x)) iff for some x:T(not W(x)).

Note: Some of the above are axioms that are assumed in logic texts and others of them are theorems in these texts. The derivable rules are indicated by listing the reasons before the insertion sign. For practical purposes it does not matter which is which. Readers are invited to fill in the proofs as exercises.

The following rules are very useful ;

|- (subs): If (P iff Q)then (W(P) iff W(Q))
|- (subs): If (P iff Q)then (f(P) = f(Q))
When W or f bind the same set of free variables in e1 and e2 we have:
|- (euclid): If (e1=e1)then (W(e1) iff W(e2))
|- (euclid): If (e1=e1)then (f(e1) = f(e2))
When a term t is defined to equal e we have:
|- (def): W(t) iff W(e)
|- (def): f(t) = f(e)
In practice it is better to list the term as the reason rather than putting "def". It makes it easier to figure out which definition is being used.

(above)|- (eqid): e = e.
(above)|- (eqcomm): (e1 = e2) iff (e2 = e1).
(above)|- (eqtrans): if (e1 = e2) and (e2 = e3) then (e2 = e1).

For all and some

for all

for some

for no

for all

for no

Natural Proofs

The following rules need special documentation to indicate how a previous formula has been modified:
(label) Name From Step Conclude When Explanation
|-(eg): Existential Generalization W(e) (eg, x=>e)|- for some x:T(W(x)) e must be an expression of type T See eg_explained

|- (ei): Existential Instantiation
for some x:T(W(x)) (ei, x=>v)|- v:T, W(v) v must be free variable before, and is now bound. See ei_explained

|- (ud): Unique definition
for one x:T(W(x)) (ud, v=>x)|- W(v) v must be free variable before, and is now bound. See ud_explained

|- (ui): Universal Instantiation
for all x:T(W(x)) (ui, x=>e)|- W(e) e is an expression of type T See ui_explained

(label) Name	From	Step	Conclude	When	Explanation
\|-(eg): Existential Generalization	W(e)	(eg, x=>e)\|-	for some x:T(W(x))	e must be an expression of type T	See eg_explained
\|- (ei): Existential Instantiation	for some x:T(W(x))	(ei, x=>v)\|-	v:T, W(v)	v must be free variable before, and is now bound.	See ei_explained
\|- (ud): Unique definition	for one x:T(W(x))	(ud, v=>x)\|-	W(v)	v must be free variable before, and is now bound.	See ud_explained
\|- (ui): Universal Instantiation	for all x:T(W(x))	(ui, x=>e)\|-	W(e)	e is an expression of type T	See ui_explained

In practice the name (eg,ei,ud,ui) can be omitted. It's good to put them in when doing exercises or when using the rules for the first time with a new audience.

Similarly, in practice, the substitution (...=>...) is often omitted.

Deductions from quantifiers explained

ei_explained

variable-like

Notice that we replace the description of the object by a short variable identifier. BUT only as long as it is not in use. It must not be free in the expression. It must not have been bound in the surounding context. It becomes bound and so is safely distinguishable from other uses of the identifier outside the quantifier.

For example if we know

for some x:Cat(x has four legs) then we can deduce
(ei)|-x has four legs since x is free. But we can not be sure that
(ei, x=>Fluffy)|-Fluffy has four legs even if we know that Fluffy is a cat, since we can not substitute a bound identifier like "Fluffy" for the x in the formula.

(eg_explained): P(expression) implies for some x(P(x)). If we know that something is true about a particular object we can conclude that it is true of some object. This is the inverse of ei.
For example that the Statue of Liberty stands in the United states, then we can conclude that there exists at least one object that fits that property: for some x:Statue(x in USA). From the observation, of a cockroach in the house we can deduce that cockroaches exist in my house.
Notice we introduce and bind a new variable to stand for the expression. We must be careful that it is not already in use (free or bound) inside the property P. If so we can use a different symbol.

(ud_explained): If one x(P(x)) then can define v such that P(v). Unique definition operates very like ei: if there is a single unique x, then there exists an x... and we can invent a new name for it. However, we can deduce another property: any other thing that has the same property is actually equal to the name we used.
Again we must create a new name for the newly defined object. It can not be a identify with a previous meaning.

(ui_explained): If for all x(P(x)) then P(any expression). This is the most powerful, and in a way, challenging deduction rule to use. It give you the power to substitute any expression for the variable -- including constants, variables, free variables, bound variables, etc. From
all men are mortal we can deduce
Socrates is mortal by using ui because we know that Socrates was a man.
The ui rule is also challenging in many cases because you may have to get creative or lucky to hit on just the right substitution to get the result you want. The other challenging thing about universal formula is that you can re-use them many times. In fact there is no limit to how often you have to get creative to prove some results. This explains why some theorems take 400 years to prove.
As in all substitutions, we must be careful when the expression being inserted in P(x) contains any variables that are bound in P(x). These need to be systematically renamed before substituting the expression. For example before putting y in place of x in for all x(for some y(P(x,y))) we must rewrite it as for all x(for some z(P(x,z)) and then derive for some z(P(y,z))
One form of ui relies on the assumption that types are not empty. This is because we can use any free variable as an object of the type. So we can reason.
Let
1. for all x:T ( true ).
2. (-1, eqid)|-for all x:T (x=x ).
3. (-1, ui, x=>v)|-v = v.
4. (-1, eg, x=>v)|-for some x:T(v=v).
5. (-1)|-for some x:T(true).
(Close Let )
(Note -- I found this reasoning in chapter 10 of Principia Mathematica...) This is a good reason for all people who construct types to make sure that they do not create empty universe by having inconsistent assumptions. For ths reason, in the MATHS system, if you define a new type you are expected to provide an example of a set of objects that fit the type.

Use Theorems as Rules
Rules like Modus Ponens ( [ mp ] above) and Universal Instantiation ( [ ui ] above) let us use theorems as deduction rules:
(mp)|-if (P and if P then Q) then Q.
(ui)|-if for all x:T(W(x)) and e ∈ T then W(e).
So we can and will express new rules for particular systems as well formed formula. For example, in the theory of real numbers we have:
(Sqrt): For all Real x, y, if x=sqrt(y) then y=x*x,
So it is valid to derive
(s2): 9 = 3*3 from
(s1): 3=sqrt(9) by the following steps:
|- (s1): 3=sqrt(9).
(Sqrt(x=>3, y=>9))|- (s1a): if 3=sqrt(9) then 9=3*3,
(s1, s1a, mp)|- (s2): 9=3*3.

. . . . . . . . . ( end of section Valid Deductions) <<Contents | End>>

Using Rules In Other Documents

 http://www.csci.csusb.edu/dick/maths/logic_25_Proofs.html

 http://www.csci.csusb.edu/dick/maths/logic_25_Proofs.html#mp

 http://www.csci.csusb.edu/dick/maths/logic_25_Proofs.html#ui

If you prepare your documents using the MATHS notation you can automatically generate WWW pages like this one. By publishing them you add to the results that other people can use. [ notn_4_Re_Use_.html ]

You can also define a short hand identifier for a URL and use that in is place. For example if your document has this definition

 		logic::=http://www.csci.csusb.edu/dick/maths/logic_25_Proofs.html

You should not quote or use formula out of context however. In MATHS formulas that are introduced inside proofs(Lets) and logistic systems(Nets) should not be referred to outside that Let or Net of assumptions and conclusions.

Omitting reasons

(s1): 3=sqrt(9),
(Sqrt, s1)|- (s2): 9=3*3.

In the above the 'mp' step is intuitive for most readers. Further, as rule, rather then writing
Po

(a): A.
(a)|- (b): B.

(a): A.
(-1)|- (b): B.

(a): A,
(above)|- (b): B.

Notice how the period in the long version has become a comma in the short version. It indicates a hidden label or link. A browser or markup program may insert a suitable label.

In practice the degree of explanation needed depends on the sophistication of the audience, the time available to the writer, and the risk of being wrong. It is wise to at least indicate which formal systems contains the rules in use.

Theorems Linked to Proofs

Given a theorem that is documented like this

	(premises)|-(label): wff.

then the proof should be in section

	. Proof of label

In a complete piece of documentation every theorem will have a label l and a possible separate section headed Proof of l. A Hypertext system should make links between the labels and the proofs.

There is a well known method of teaching advanced mathematics that consists of giving the class lists of definitions and theorems without proofs and requiring the class to provide the proofs. This is called the "Moore" method. It seems likely that an effective way to learn a formal system is to fill in all the proofs without reading them first. There is therefore something to be said, in text books, for omitting the proofs.

However most mathematicians have had the disquieting experience of going back to a result they have worked out and been unable to reconstruct how they got there. One concludes that in research one needs to record the steps one takes. How one does this without slowing the process down to a crawl is not known to me, at this time.

In practice, an engineer needs to be able to see the proof when he or she is suspicious that the step is not valid and so the design that depends on it is in risk of failing unexpectedly. Thus in documenting software one needs to provide the most complete proofs but for teaching and learning on needs to omit them.

Steps Linked to Evidence

	|- ( label ): wff

is referred to by the label itself before the assertion sign:

	( evidence ) |- ( new_label ): wff

A hypertext system can provide links between identifiers of other theorems and axioms when they are used as evidence to deduce other results.

Block Structure

for x:S, if P then Q

x:S

x:S,
(let)|-P.
...
...
(...)|-Q.

for all x:S(if P then Q).
This means that we define a new temporary environment and with new variable x and assumption P. The above structure has three parts:
Let
(Close Let )
The older syntax uses the symbols "Let{" and "}" like this:
```
 Let { |-(1): x:S, (2): P. (...)|-..., (...)|-(result): Q}.
```
The newer form uses directives:
```
 	.Let
```
```
 		(1): x:S,
```
```
 		(let)|-(2): P.
```
```
 		...
```
```
 		(1,2,...)|- (result): Q.
```
```
 	.Close.Let
```
Notice that using "(let)" makes it easier to see where we shift from the hypothesis to the derivation of results.
A shorter form:
```
 	.Let x:S,
```
```
 		(let)|- P.
```
```
 		...
```
```
 		(hyp,...)|- (result): Q.
```
```
 	.Close.Let
```
Syntax of Proofs
The general syntax is
proof::= (natural | proof_by_case | reducto_ad_absurdum) | |[p:po]( start(p) block #( or block) end(p) ),
block::=hypothesis derivation closure,
hypothesis::= #(axiom|comment|definition),
derivation::=#(derived|comment|definition).
closure::=derived.
po::= "Po"|"Let"|"Consider"| "Case"|...,
start(p)::= directive & ("." p EOLN).
end(p)::= directive & (".Close" "." p EOLN).
or::= "Or"|"Else"|"But"|....,
A case or block must be closed when any proposition is derived which is the negation of a proposition previously derived in the current case, or any case that contains the current case.

Semantics of a Block
After the end of the Block the declarations and assumptions are discarded and the whole proposition is derived in their place. The declarations and assumptions work exactly like the declarations in a block structured language (say C) - each demonstration adds a collection of declarations, assumptions and consequences on to a stack - all of which are deleted at the end of the demonstration, producing the desired conclusion in their place.

Valid Forms of Proof
1. assertion::= axiom | conjecture | derived
2. derived::= theorem | deduction,
3. label::="(" identifier "):",
4. reference::=identifier.
5. ref_to::label ->reference = the[r:reference]( "(" r "):" = (_) ).
6. axiom::= label wff,
7. conjecture::='??{' documentation "}??",
8. deduction::=line_break_line & (white_space "(" evidence ")" conclusion eoln).
9. evidence::= List(re_used(reference | defined_term | comment )). [ re_used in notn_4_Re_Use_ ]
10. conclusion::="|-" O(label) derived_wff.
11. algebraic_step::=expression #( EOLN evidence "|-" EOLN relation expression), This echoes the Gries and Schnieder layout, see [ Algebra and Calculations ] below.
12. theorem::= "( evidence")""|-" label wff, If the above label was L then the|-would be made into an anchor in a hypertext system that refers to a name "Proof of " L.
  Normally all proofs are gathered at the end of the piece of documentation in which the theorems are asserted.
  
  Algebra and Calculations
  David Gries is a strong proponent of reasoning by using equations, see [ logicthetool.html ] and in particular exploiting the algebraic properties if iff rather than the logical properties of if_then_(ifftrans, iff5, and iff6 above).
  MATHS combines natural deduction and algebra. An algebraic step uses an inference like the following:
13. |-if e1 R1 e2 R2 e3...R[n-1] e[n] then e1 ;R e[n].
14. Note: ";R" is short for "R1; R2; ... R[n-1]" A suitable syntax is
```
 	.Net
```
```
 		 e1
```
```
 	(y1)|-
```
```
 		R1 e2
```
```
 	(y2)|-
```
```
 		R2 e3
```
```
 	(y2)|-
```
```
 		R3 e4
```
```
 	...
```
```
 	.Close.Net
```
  Or in rendered format:
15. (above)|- (Dummy): e1 ;(R) e[n].
  Proof of Dummy
  
  Net
  1. e1
  2. (y1)|-
  3. R1 e2
  4. (y2)|-
  5. R2 e3
  6. (y2)|-
  7. R3 e4
  8. ...
  (End of Net)
  In the above the ys are explanations of why the step is valid - typically a list of references to theorems and axioms.
  Two forms are particularly useful. First when all the relations are equalities, and secondly when they are all iff.
```
 	.Net
```
```
 		e1
```
```
 	(y1)|-
```
```
 		= e2
```
```
 	(y2)|-
```
```
 		= e3
```
```
 	(y3)|-
```
```
 		= e4
```
```
 	(y4)|-
```
```
 		= e5
```
```
 	...
```
```
 	.Close.Net
```
```
 	(above)|-(l):  e1 = e[n].
```
  The following is for chains of 'if-and-only-if' steps:
```
 	.Net
```
```
 	e1
```
```
 	(y1)|-
```
```
 		iff e2
```
```
 	(y2)|-
```
```
 		iff e3
```
```
 	(y3)|-
```
```
 		iff e4
```
```
 	(y4)|-
```
```
 		iff e5
```
```
 	...
```
```
 	.Close.Net
```
```
 	(above)|-(l):  e1 iff e[n].
```
  Other forms of algebraic reasoning have been developed by mathematicians, see [ Algebra in math_10_Intro ]
  The Gries/Schnieder Laws
  David Gries has argued that using chains of 'iff' and '=' steps is the best way to prove things. His arguments are convincing. However the price is the learning of more rules than the logician's ideal set of independent axioms. It turns out that the rules are often definitions or theorems in the logician's systems (a good example is Kalish and Montague's text). In other words the Gries/Schneider system is to symbolic logic rather like a high level programming language is to an assembly language. See [ logicthetool.html ] and
  Gries & Schneider 93, David Gries & Fred B Schneider, A Logical Approach to Discrete Math, Springer Verlag Texts and Monographs in Computer Science 1993, ISBN 3-540-94115-0(NY)
  Some these laws in Gries & Schneider were already a part of MATHS as notational conveniences and definitions. For example, the trading axiom in the Gries/Schneider system is equivalent to the MATHS definition that
16. for all x:T, if R then P means
17. for all x:T(if R then P).
  [ Definitions of Quantifiers in logic_10_PC_LPC ]
  Similarly, for most associative operators,o, the STANDARD MATHS abbreviation:
18. o[x:{a}](P(x)) = P(a)
  [ SERIAL_AND_PARALLEL in math_11_STANDARD ] is the Gries/Schneider one point law. Here are some other versions that can be useful in proving things:
19. |- (one_point_laws): all following
  1. o[x:{a}](P(x)) = P(a).
  2. for all x:{a}(P(x)) iff P(a).
  3. for some x:{a}(P(x)) iff P(a).
  4. for some x(x=a and P(x)) iff P(a).
  5. for all x(x=a and P(x)) iff P(a).
  It is likely that using these laws will often lead to proofs that are simpler because they use few large steps rather than many small steps here are some transcriptions of some of these rule into MATHS:
20. |- (Trading): (for all x (if R then P) iff for all x(not R or P))
21. and (for all x (if R then P) iff for all x((R and P) iff R))
22. and (for all x (if R then P) iff for all x((R or P) iff P)).
  The above are useful because they can be used to replace an implication like
23. if P then Q by an equivalence
24. P and Q iff P and then prove the equivalence rather than the implication. For example, to prove if P and Q then P is true, use the trading rules to get ((P and Q) and P iff P and Q). Now (P and Q) and P is the same as (P and P) and Q or P and Q by the laws of Boolean Algebra. In the Natural deduction form:
  Let
  1. (let)|- (hyp): P and Q.
  2. (hyp, and1, mp)|- (conclusion): P.
  (Close Let )
  
  Boolean Algebra
  George Boole's Rules of Thought are a very neat way to sort out a argument. The technique is to reduce everything to the three operators: and, or, not. Then use the laws of Boolean algebra to simplify the possibilities.
  The following translation rules are helpful:
25. Translate_to_Boolean_algebra::=following
  Net
  1. P and Q = P*Q.
  2. P or Q = P+Q.
  3. not P = -P.
  4. (if P then Q) = - P+ Q.
  5. not(if P then Q) = P*(-Q).
  6. (P iff Q) = (- P * - Q) + (P * Q).
  7. not(P iff Q) = ((-P)*Q) + (P*(-Q)).
  (End of Net Translate_to_Boolean_algebra)
  See the Rules of Boolean algebra:
26. BOOLE::= See http://cse.csusb.edu/dick/maths/math_41_Two_Operators.html#BOOLEAN_ALGEBRA and an example: [ lunch.html ]
  It is often better to prove the universal truth of some formula by proving that the negative is false. For example rather than working with
27. if P then Q analyze
28. not(if P then Q) or in translation:
29. P*(-Q).
  For example to show that if then is transitive(iftrans):
  Proof of iftrans
  
  Net
  1. (if P then Q) and (if Q then R) and not (if P then R)
  2. (Translate_to_Boolean_algebra)|-
  3. = (-P+Q)*(-Q+R)*P*(-R)
  4. (BOOLE)|-
  5. = (-P+Q)*(-Q*-R)+R*(-R))*P
  6. = (-P+Q)*(-Q*-R)+0)*P
  7. = (-P+Q)*(-Q*-R)))*P
  8. = (-P+Q)*P*(-Q*-R)))
  9. = (-P*P+Q*P)*(-Q*-R)
  10. = (0+Q*P)*(-Q*-R)
  11. = (Q*P)*(-Q*-R)
  12. = Q*P*(-Q)*(-R)
  13. = Q*(-Q)*P*(-R)
  14. = 0.
  (End of Net)
  Boolean Algebra is seductively easy on simple formula.
  It can be combined with rules from semantic tableaux that handle quantifiers.
  Trying Ideas Out
  For many years mathematicians have tended to use the words 'Let' and 'Consider' to introduce ideas for examination. MATHS also encourages creative (or lateral) thinking. At any time an idea can can be documented and experimented with - as long as it is in an enclosed context. Edward de Bono's work (debono) suggests there is need for a new word that frees the mind to examine the ideas without pre-judging them. He suggested "Po". "Po" invites the reader (or listener) to suspend judgment of an idea for a time. It means that the idea is thought about without evaluating it as true or false. Significantly the string "po" is found in "hypothesis", "suppose", "posit", "proposition" which indicates something of the way it is intended to work. It is also part of "poetry" - indicating that an idea can be thought about for aesthetic as well as pragmatic reasons. In MATHS the word 'Po' is followed by a set of (braced) documentation which includes the assumptions and derives the consequences. After the end of the demonstration a conclusion can be drawn from the complete process. Edward de Bono (debono) had no intent for "Po" to be part of a formal language, but when I tried it out Po worked better than any other keyword.
30. analysis::= hypothesis derivation closure.
31. hypothesis::= #(axiom|comment|definition),
32. derivation::=#(derived|comment|definition).
33. closure::=derived.
  A case or proof must be closed when any proposition is derived which is the negation of a proposition previously derived in the current case, or any case that contains the current case.
  
  Proof by Cases
34. analytical::= ".Case" block #(".Else" block) ".Close.Case".
  1. (or):
```
		P or Q.
```
```
		.Case
```
```
 			|-P. ...
```
```
 		(...)|-R.
```
```
		.Else
```
```
 			|-Q. ...
```
```
 		(...)|-R
```
```
 		.Close.Case
```
```
		(above)|- R
```
    (See [HuthRyan00] page 19 and 11)
  2. (if):
```
		if P then Q.
```
```
		.Case
```
```
 			|-not P. ...
```
```
 		|-Q.
```
```
		.Else
```
```
 			|-Q. ...
```
```
 		|-R
```
```
 		.Close.Case
```
```
		|- R
```
  3. (neg):
```
		not(P iff Q).
```
```
		.Case
```
```
			|-P,not Q. ...
```
```
 		|-R.
```
```
		.Else
```
```
			|- Q,not P. ...
```
```
 		|-R,
```
```
 		.Close.Case
```
```
		|- R
```
35. |-analysis=reason"." ".Case" L(#(axiom | comment | definition) #(derived | comment | definition) derived, ".Else" ) ".Close.Case".
  Semantic tableaux [ logic_27_Tableaux.html ] are a way of organizing and semi-automating these proofs.
  A small extension: Each case establishes a result that can be used in later cases. After ".Case P....|-Q .Else" you can use if P then Q in later cases.
  
  Example Proof by Case
  1. (below)|- (constructive_dilemma): if ((P or Q) and (if P then R) and (if Q then R)) then R
    Proof of constructive_dilemma
    
    Let
    1. |- (cd1): P or Q,
    2. |- (cd2): if P then R,
    3. |- (cd3): if Q then R.
    4. (cd1)|-
      Case
      1. |- (cd5.1): P.
      2. (cd5.1, cd2, mp)|-R
      (End of Case)
      Case
      1. |- (cd5.2): Q.
      2. (cd5.2, cd3, mp)|-R
      (Close Case )
    5. (cd1, or)|-R,
    (Close Let )
    
    Proofs by case are often easier to find and document using graphics. There is every reason to have software to convert a presentation like the above into a diagram like the following:
  For more on these techniques see [ logic_27_Tableaux.html ] below.
  It is also possible and sometimes shorter to use [ Boolean Algebra ] to sort out a complex collection of cases. Electronic engineers have developed useful diagrams to help this.
  
  Reducto ad Absurdum
36. reducto_ad_absurdum::= ".Let" hypothesis derivation closure ".Close.Let". Here the closure is deducing two results that are complementary - one negates the other. You can document them like this
```
	( label1, label2)|-false.
```
37. |- (absurd): if P and not P then false.
  Here are the standard forms
  1. (rabs1):
```
		.Let
```
```
 			|-P, not Q.
```
```
 			 ... derive any absurdity
```
```
 		.Close.Let
```
```
 			(above)|- if P then Q.
```
  2. (rabs2):
```
		.Let
```
```
			|-not P, not Q.
```
```
 			 ... derive any absurdity
```
```
 		.Close.Let
```
```
		(above)|- P or Q.
```
  3. (rabs3):
```
		.Let
```
```
			 |-not P.
```
```
 			 ... derive any absurdity
```
```
 		.Close.Let
```
```
 			(above)|- not P
```
  4. (rabs4):
```
		.Let
```
```
			x:T, |-not W(x).
```
```
 			 ... derive any absurdity
```
```
 		.Close.Let
```
```
 		(above)|- for all x:T(W(x)).
```
  5. (rabs5):
```
		.Let
```
```
			for all x:T(not W(x)).
```
```
 			 ... derive any absurdity
```
```
 		.Close.Let
```
```
 		(above)|-for some x:T(W(x))
```
  Examples of Reducto Ad Absurdum
  1. not not P iff P.
    First prove
  2. (above)|- (dn1): if not not P then P.
    Let
    1. not not P, not P
    (Close Let )
    
    Next prove
  3. (above)|- (dn2): if P then not not P.
    Let
    1. P, not not not P,
    2. Use previous result with (not not P)!
    3. (dn1)|-not P.
    (Close Let )
    Now assemble 'dn':
  4. (dn1, dn2, iff3)|-not not P iff P.
    
    A Proof of an odd result
  5. (below)|- (exrab): if for some x, all y (x R y) then for all y, some x( x R y)
    Proof of exrab
    
    Let
    1. |- (np1): for some x, all y (x R y),
    2. |- (np2): not for all y, some x( x R y).
    3. (np1, ei, x=>a)|- (np3): for all y (a R y),
    4. (np2, qn2, qn2)|- (np4): for some y, all x(not x R y),
    5. (np4, ei, y=>b)|- (np5): for all x (not x R b),
    6. (np3, u1, y=>b)|- (np6): a R b,
    7. (np5, ui, x=>a)|- (np7): not a R b,
    (Close Let )
    
    Example Proof of for all x, some y(if F(y) then F(x))
    
    Let
    1. x.
      Let
      1. |-(hyp): not for some y(if F(y) then F(x)),
      2. (qn1)|-for all y(not(if F(y) then F(x))),
      3. (ui, y=>x, nif4)|-F(x) and not F(x),
      4. RAA.
      (Close Let )
    2. (above)|-for some y(if F(y) then F(x)).
    (Close Let )
  . . . . . . . . . ( end of section Examples of Reducto Ad Absurdum) <<Contents | End>>
  Proof Templates
  Any proof or demonstration is a just special piece of documentation. MATHS naming/cross-reference rules apply, so a pattern of proof can by given a name and then be used in many places. Indeed modern mathematics forms a "rattlebag" of interesting and more or less useful templates. [ home.html ]
  
  Example of Useful Template -- Mathematical Induction
  1. induction::= See http://cse.csusb.edu/dick/maths/math_42_Numbers.html#INDUCTION.
    The key to mathematical induction is a pattern like this:
    Net
    1. P::@Nat={ n. ...}.
    2. ...
      Prove that 1 has the property:
    3. (above)|- (basis): 1 in P.
      Prove that if a number has the property then so has the next number.
    4. (above)|- (step): for all k:P ( k+1 in P).
    5. ...
    6. (basis, step, induction)|-P = Nat.
    (End of Net)
    A classic example uses the mathematical induction template from the theory of numbers. The example shows that the sum of the natural numbers from 1 to n ( +(1..n)) is equal to n*(n+1)/2 for all n>0. The axioms for +(a..b) are in
  2. serial::= See http://www.csci.csusb.edu/dick/maths/notn_12_Expressions.html#Serial Operators and
  3. numbers::= See http://cse.csusb.edu/dick/maths/math_42_Numbers.html
  4. (serial, numbers, induction)|- (triangle): for all n:Nat, +(1..n)=n*(n+1)/2.
    
    Proof of triangle
    
    Let
    1. F::Nat->@ = fun[n:Nat](+(1..n)=n*(n+1)/2)).
    2. P::@Nat={n:Nat || F(n) }.
    3. +(1..1) = +(1)
    4. (def)|-
    5. = 1
    6. (-1)|-
    7. = 1*(2)/2
    8. (-1)|-
    9. = 1*(1+1)/2.
    10. (-1)|-F(1),
    11. (-1)|- (basis): 1 in P.
      
      Let
      1. (1): k:Nat,
      2. (2): k in P.
      3. +(1..(k+1))
      4. (1, serial)|-
      5. = +(1..k) + (k+1)
      6. (2)|-
      7. = k*(k+1)/2+k+1
      8. (algebra)|-
      9. = (k+1)*(k+2)/2
      10. (algebra)|-
      11. = (k+1)*((k+1)+1)/2.
      12. |- (QED): k+1 in P
      (Close Let )
    12. (above)|- (step): for all k:P(k+1 in P).
    13. (basis, step, induction)|-for all n:Nat, P(n).
    (Close Let )
    
    Exercise -- Generalize Induction
    Induction above shows a way to prove a property true for any Natural number. The natural numbers are 1,2,3,4.... or 1.. . Develop similar templates and prove them for properties that hold for 0.., 2.., or for any n0: n0.. .
  . . . . . . . . . ( end of section Example of Useful Template: Mathematical Induction) <<Contents | End>>
  
  Links to other useful Templates
  [click here if you can fill this hole]
. . . . . . . . . ( end of section Valid Forms of Proof) <<Contents | End>>

Note
MATHS proofs tend to be almost mechanical (especially those that use [ logic_27_Tableaux.html ] )except for (1) choosing an expression to substitute for universally quantified variables (2) selecting the special cases to analyze. This can be quite difficult. Much theoretical work has been done in the field of Artificial Intelligence to make this as automatic as possible. It has been shown that in any interesting logic there can not exist an algorithm that will prove all true statements.

Glossary
1. above::reason="I'm too lazy to work out which of the above statements I need here", often the last 2 or three statements.
2. given::reason="I've been told that...", used to describe a problem.
3. given::variable="I'll be given a value or object like this...", used to describe a problem.
4. goal::theorem="The result I'm trying to prove right now".
5. goal::variable="The value or object I'm trying to find or construct".
6. let::reason="For the sake of argument let...", [ Block Structure ]
7. hyp::reason="I assumed this in my last Let/Case/Po/...".
8. QED::conclusion="Quite Easily Done" or "Quod Erat Demonstrandum", indicates that you have proved what you wanted to prove.
9. QEF::conclusion="Quite Easily Faked", -- indicate that you have proved that the object you constructed fitte the goal you were given.
10. RAA::conclusion="Reducto Ad Absurdum".
. . . . . . . . . ( end of section Glossary) <<Contents | End>>
Comments and Reviews
. . . . . . . . . ( end of section Comments and Reviews) <<Contents | End>>
Glossary
argument::=A sequence of steps that go from a set of assumptions to a conclusion.
valid::=Something that can not produce a false conclusion from true givens. There are valid arguments, valid proofs, and valid steps.

. . . . . . . . . ( end of section Proofs and Demonstrations) <<Contents | End>>

Notes on MATHS Notation

Special characters are defined in [ intro_characters.html ] that also outlines the syntax of expressions and a document.

Proofs follow a natural deduction style that start with assumptions ("Let") and continue to a consequence ("Close Let") and then discard the assumptions and deduce a conclusion. Look here [ Block Structure in logic_25_Proofs ] for more on the structure and rules.

The notation also allows you to create a new network of variables and constraints. A "Net" has a number of variables (including none) and a number of properties (including none) that connect variables. You can give them a name and then reuse them. The schema, formal system, or an elementary piece of documentation starts with "Net" and finishes "End of Net". For more, see [ notn_13_Docn_Syntax.html ] for these ways of defining and reusing pieces of logic and algebra in your documents. A quick example: a circle = Net{radius:Positive Real, center:Point}.

For a complete listing of pages in this part of my site by topic see [ home.html ]

Notes on the Underlying Logic of MATHS

The notation used here is a formal language with syntax and a semantics described using traditional formal logic [ logic_0_Intro.html ] plus sets, functions, relations, and other mathematical extensions.

For a more rigorous description of the standard notations see

STANDARD::= See http://www.csci.csusb.edu/dick/maths/math_11_STANDARD.html

Glossary

above::reason="I'm too lazy to work out which of the above statements I need here", often the last 3 or 4 statements. The previous and previous but one statments are shown as (-1) and (-2).

given::reason="I've been told that...", used to describe a problem.

given::variable="I'll be given a value or object like this...", used to describe a problem.

goal::theorem="The result I'm trying to prove right now".

goal::variable="The value or object I'm trying to find or construct".

let::reason="For the sake of argument let...", introduces a temporary hypothesis that survives until the end of the surrounding "Let...Close.Let" block or Case.

hyp::reason="I assumed this in my last Let/Case/Po/...".

QED::conclusion="Quite Easily Done" or "Quod Erat Demonstrandum", indicates that you have proved what you wanted to prove.

QEF::conclusion="Quite Easily Faked", -- indicate that you have proved that the object you constructed fitted the goal you were given.

RAA::conclusion="Reducto Ad Absurdum". This allows you to discard the last assumption (let) that you introduced.

Contents

Introduction

Simple Propositions

For all and some

Natural Proofs

Proof of Dummy

Example Classical Theorem

Proof of constructive_dilemma

Proof of dn

Proof of exrab

Example Proof of for all x, some y(if F(y) then F(x))

Glossary