[Skip Navigation] [CSUSB] / [CNS] / [CSE] / [R J Botting] / [ ] / logic_25_Proofs
[Contents] [Source Text] || [Notation] || [Copyright] || [Contact] [Search ]
Wed Nov 14 16:19:21 PST 2012

### Contents

Open Proofs in MATHS

# Introduction

My MATHS notation is designed to make the validation and proof of software a more practical process. It therefore includes a checkable way to derive conclusions from previously established results. It uses a block-structured form of logic called natural deduction augmented by abbreviations and algebraic steps( [ Algebra and Calculations ] ). The goal is a natural but verifiable way to discover and present demonstrations.

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

MATHS combines two systems for proving things: see [ Natural Deduction ] and [ Algebra and Calculations ] below.

# Natural Deduction

In Natural deduction systems there is, at any point a stack of things which are currently taken to be true, plus rules permitting various changes to this stack. First any valid algebraic step can be used to add a new proposition. Second, MATHS has three "Natural" ways of deriving new consequences from assumed or proven truths. We look at the "natural" steps first.

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

A deductive step is documented like this:
` ( evidence ) |- ( label_of_result ): result .`
The evidence can be a reference to any previously assumed axiom, any previously proved result, or to any documented theorem or rule - as long as they are with in the scope of the current statement [ evidence ] below. The scoping of variables and labels is very like that in a structured program, see below: [ 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:
Table
ShownMeaningFormal 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 hereAll 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 thisLabel of statements after last Let

(Close Table)

# Blatant Assertion

One obvious question is where we get the evidence for our deductions. Sometimes these come from definitions. Sometimes they come from previously deduced results. We can also introduce new assumptions, either for the sake of argument (see later) or because they are part of a system of assumptions that the writer is constructing. It is a useful step to expose our assumptions!

The syntax is like this

` 		|- (label): axiom.`
In other words an unproven assertion is taken to be an assumption. Compare the above with the assertion of a conclusion that follows from various reasons:
` 		(reasons) |- (label): conclusion`
Without the assertion sign we just labeled an expression so that we can talk about it informally:
` 		(label): expression.`

# Valid Deductions

## Simple Propositions

Here is a table of valid deductions. P, Q and R are any statements. If you have the statement between the "If" and the "then", then you can deduce the statement after the "then" in one step. The "iff" rules work in both directions. They are also used in [ Algebra and Calculations ] below.

1. |- (and1): If P and Q then P.
2. |- (and2): If P and Q then Q.
3. |- (demorgan1): not(P and Q) iff not P or not Q.
4. |- (and3): If P and Q then (P and Q), -- combines two proven results into one.
5. |- (and4): P and P iff P, idempotent.
6. |- (and5): P and Q iff Q and P, commutative.
7. |- (and6): (P and Q) and R iff P and (Q and R), associative`.

8. |- (or1): If (P or Q) and not P then Q, modus tolens.
9. |- (or2): If (P or Q and not Q then P, modus tolens.
10. |- (or3): P or P iff P, idempotent.
11. |- (or4): (P or Q) iff (Q or P), commutative.
12. |- (or5): (P or Q) or R iff P or (Q or R), associative.
13. |- (demorgan2): not(P or Q) iff not P and not Q.
14. |- (nor1): If not(P or Q) then not P.
15. |- (nor2): If not(P or Q) then not Q.

16. (above)|- (dn1): if not not P then P.
17. (above)|- (dn2): if P then not not P.

18. |- (dist1): P and (Q or R) iff (P and Q) or (P and R).
19. |- (dist2): P or (Q and R) iff (P or Q) and (P or R).

20. |- (abs1): P and(P or Q) iff (P or Q).
21. |- (abs2): P or (P and Q) iff (P and Q).

22. |- (mp): If (P and(if P then Q)) then Q, modus ponens.
23. |- (mtp): If (not Q) and (if P then Q) then not P, modus tolendo ponens.
24. (mp)|- (iftrans): If (if P then Q) and (if Q then R) then (if P then R).

25. |- (nif1): If not(if P then Q) then P.
26. |- (nif2): If not(if P then Q) then not Q.
27. |- (nif3): If not(if P then Q) then P and not Q.
28. (nif1, nif2, nif3)|- (nif4): not(if P then Q) iff P and not Q.

29. |- (iff1): If (P iff Q) then (if P then Q).
30. |- (iff2): If (P iff Q) then (if Q then P).
31. |- (iff3): If ((if Q then P) and (if Q then P)) then (P iff Q).
32. (dn1, dn2, iff3)|- (dn): not not P iff P.
33. |- (iff4): (P iff Q) iff ( ((Q and P) or (not P and not Q))).
34. (iff4)|- (iff5): (P iff Q)iff(Q iff P), commutative.
35. (above)|- (iff6): (P iff (Q iff R) iff ((P iff Q) iff R), associative.
36. (above)|- (ifftrans): If (P iff Q) and (Q iff R) then (P iff R).

37. |- (niff): If not (P iff Q) then ((Q and not P) or (not P and Q)).

38. |- (qn1): not for some x:T(W(x)) iff for all x:T(not W(x)).
39. |- (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 ;

When W or f bind the same set of free variables in P and Q we have:
1. |- (subs): If (P iff Q)then (W(P) iff W(Q))
2. |- (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:

3. Equals can be substituted for equals.
4. |- (euclid): If (e1=e2)then (W(e1) iff W(e2))
5. |- (euclid): If (e1=e2)then (f(e1) = f(e2))

The above can be generalized when we have several equations... see [ Algebra and Calculations ] below.

When a term t is defined to equal e we have:

6. |- (def): W(t) iff W(e)
7. |- (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.

From the above rules you can deduce that '=' is an equivalence relation:

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

These are useful rules that underlie algebra.

## For all and some

Many statements contain quantifiers: for all, for some, for no,... Here are some notes on using them and documenting their use. To see methods for deriving for all and for no see [ Natural Proofs ] below.

The following rules need special documentation to indicate how a previous formula has been modified:
Table
(label) NameFromStepConcludeWhenExplanation

1. |- (eg): Existential Generalization
2. W(e) (eg, x=>e)|- for some x:T(W(x)) e must be an expression of type T See eg_explained

3. |- (ei): Existential Instantiation
4. 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

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

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

(Close Table)

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): for some x(P(x)) implies P(new variable).

When we know that something has a given property then we can give it a temporary name -- that is not in use. This should be a short variable-like identifier that is not bound. It becomes bound for the rest of the surrounding proof/block.

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

9. for some x:Cat(x has four legs) then we can deduce
10. (ei)|-x has four legs since x is free. But we can not be sure that
11. (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 for 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

12. all men are mortal we can deduce
13. 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(x=x).
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:
14. (mp)|-if (P and if P then Q) then Q.
15. (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:

16. (Sqrt): For all Real x, y, if x=sqrt(y) then y=x*x,

So it is valid to derive

17. (s2): 9 = 3*3 from
18. (s1): 3=sqrt(9) by the following steps:
19. |- (s1): 3=sqrt(9).
20. (Sqrt(x=>3, y=>9))|- (s1a): if 3=sqrt(9) then 9=3*3,
21. (s1, s1a, mp)|- (s2): 9=3*3.

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

# Using Rules In Other Documents

If you want to use any of the rules above then it is easy to refer to them. This document has been published on the World Wide Web and has the Universal Resource Locator
` http://www.csci.csusb.edu/dick/maths/logic_25_Proofs.html`
The individual rules have all anchors for links. For example,
` 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`
then you can use "logic" as a reason whenever you want to use any of the rules in this document.

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

I theory you shouldn't have to document all of the rules you use, as shown above, instead something like the following provides enough hints:
Po
1. (s1): 3=sqrt(9),
2. (Sqrt, s1)|- (s2): 9=3*3.

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

1. (a): A.
2. (a)|- (b): B.
We "chain" them together lke this:
Po
1. (a): A.
2. (-1)|- (b): B.
or this:
Po
1. (a): A,
2. (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.

In MATHS a labeled theorem always has a link to a section that can provide more information on how the theorem can be proved... even if the section does not exist (yet?). Thus sections that fill in some details provide for readers who want or need more hints. Meanwhile, people in a hurry or with stronger intuition can ignore these 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.

All assumptions(axioms) should be labeled so that they can be referred to later. Later deductions use these labels so that a reader can reconstruct the process and check it:
`	|- ( 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

In addition to deductive steps we can use nested pieces of documentation to explore the consequences of extra assumptions. Propositions of the form
1. for x:S, if P then Q can be proved by assuming that x:S and P is true and then deducing Q as a result. The format look like this:
Let
1. x:S,
2. (let)|-P.
3. ...
4. ...
5. (...)|-Q.

(Close Let )
In the above P is the hypothesis, Q is the result and the whole would be used to prove:
2. 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

(declare): introduces a temporary declaration (x:S), and then
(assume): makes an assumption (P), and then
(derive): derives a consequence Q.

(Close Let )
The older syntax uses the symbols "Let{" and "}" like this:
` Let { |-(1): x:S, (2): P. (...)|-..., (...)|-(result): Q}.`
` 	.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`
` 	(above)|- for x:S, if P then Q.`

Note. In general, you may introduce many variables and assumptions inside a "Let...". If you do then they must all be listed before the 'then' in the formula that you conclude.

` 	.Let x:S, A, B, C, ...`
` 		...`
` 		(hyp,...)|- (result): Q.`
` 	.Close.Let`
` 	(above) |- for x:A, if a and B and C ... then Q.`

Note. You can, if you wish, include any number of the theorems you prove inside the "Let" after the "then" in the conclusion.

` 	.Let x:S, A, B, C, ...`
` 		...`
` 		(hyp,...)|-  P.`
` 		...`
` 		(hyp,...)|-  Q.`
` 	.Close.Let`
` 	(above) |- for x:A, if A and B and C ... then P and Q.`

# Syntax of Proofs

The general syntax is
3. proof::= (natural | proof_by_case | reducto_ad_absurdum) | |[p:po]( start(p) block #( or block) end(p) ),
4. block::=hypothesis derivation closure,
5. hypothesis::= #(axiom|comment|definition),
6. derivation::=#(derived|comment|definition).
7. closure::=derived.

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.

8. po::= "Po"|"Let"|"Consider"| "Case"|...,
9. start(p)::= directive & ("." p EOLN).
10. end(p)::= directive & (".Close" "." p EOLN).
11. or::= "Or"|"Else"|"But"|....,

# 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

## Natural Proofs

Universal Propositions
` 	 |-(l): for x:T, if P then Q.`
`	...`
` 	. Proof of l`
` 	.Let`
` 		(let)|-(l.1): x:T,`
` 		(let)|-(l.2): P.`
` 		...`
` 		(...)|-Q.`
` 	.Close.Let`

Either-Or Propositions

` 	(...)|-(l): P or Q.`
`	...`
` 	. Proof of l`
` 	.Let`
` 		(let)|-(l.1): not P...	(...)|- Q.`
` 	.Close.Let`
Also see the use of Cases below.

No more than one

` 	|- (l) for 0..1  x:T (W2(x)).`
`	...`
` 	. Proof of l`
` 	.Let`
` 		 (let)|-(l1): x1,x2:T,(l2):W(x1), (l3):W(x2)....`
` 		(...)|- x1=x2.`
` 	.Close.Let`

Uniqueness

` 	|- (l) for one  x:T (W2(x)).`
`	...`
` 	. Proof of l`
` 	(...) |-(l1): for some  x:T (W2(x)).`
` 	(...) |-(l2): for 0..1  x:T (W2(x)).`

The third way to prove a proposition is by assuming the contrary and analyzing it. The aim is to find contradictions in all possible alternatives. This has been called "Reducto ad Absurdum" for the last 2000 years or so. More recently it has been formalized as the method of Semantic tableaux and used in Artificial Intelligence. For more see [ Reducto ad Absurdum ] and [ logic_27_Tableaux.html ] (semantic Tableaux).

Proofs do not always work out the way we want - for example sometimes to prove P, we assume not P but find one or more alternatives being left open, for instance Q. In this case, we can still 'harvest' a weaker proposition than P - P or Q.

Thus in MATHS - at any time in a document - we can open up a hypothetical context, examine the consequences and then draw conclusions as we discard the context. An important guideline, which you may find goes very much against the grain - do not assume your goal, assume the opposite. In short proof consists of playing the devil's advocate, unsuccessfully.

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. (relations)|-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].`

The same structure works between sets and relations to give higher-order logic proofs. For example to prove subset we can establish a chain of subset relations:

` 	.Net`
` 	S1`
` 	(y1)|-`
` 		==> S2`
` 	(y2)|-`
` 		==> S3`
` 	(y3)|-`
` 		==> S4`
` 	(y4)|-`
` 		==> S5`
` 	...`
` 	.Close.Net`
` 	(above)|-(l):  S1 ==> S[n].`

For more on relations see [ logic_40_Relations.html ] and later pages.

Other forms of algebraic reasoning have been developed by mathematicians, see [ Algebra in math_10_Intro ]

## More Algebra

Standard algebra allows us to extend euclid above to add equals to equals and son on. For example, if we have several equations:
1. e1=f1
2. e2=f2
3. ...

We can conclude
16. F(e1,e2,...) = F(f1,f2,...).

Formally the step would be noted as by listing the labels of the equations and the operations applied. For example

` 	(l1,l2,...,F)|-(r): F(e1,e2,...) = F(f1,f2,...).`
(where the equation listed above are labeled l1,l2,...

In practice this starts to turn into reverse polish notation.

This form of reasoning works best when we have a known mathematical algebra like [ maths/math_43_Algebras.html ] and [ maths/math_45_Three_Operators.html ] for example.

Net

[ http://www.futilitycloset.com/2012/09/22/weighty-matters/ ]

1. |-Natural numbers with addition and subtraction.
2. |- (fc1): me+x=170.
3. |- (fc2): wife+x=130.
4. |- (fc3): me+wife+x=292.
5. (fc1, fc2, +, fc3, -)|- (fc4): me+x+wife+x-me-wife-x = 170+130-292.
6. (fc4, algebra)|- (fc5): x = 8.

(End of Net)

## 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 like a high level programming language is to an assembly language. See [ logicthetool.html ] and

Source: 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

17. for all x:T, if R then P means
18. for all x:T(if R then P).

Similarly, for most associative operators,o, the STANDARD MATHS abbreviation:

19. 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:

20. |- (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:

21. |- (Trading): (for all x (if R then P) iff for all x(not R or P))
22. and (for all x (if R then P) iff for all x((R and P) iff R))
23. 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

24. if P then Q by an equivalence
25. 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:

26. 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:
27. 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

28. if P then Q analyze
29. not(if P then Q) or in translation:
30. 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.

31. analysis::= hypothesis derivation closure.
32. hypothesis::= #(axiom|comment|definition),
33. derivation::=#(derived|comment|definition).
34. 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

35. 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`

36. |-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

### Example Classical Theorem

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.

## Tables can Express Proof by Cases

This is a recent (2008) idea which is a Partly Baked Idea (but not much better than Half Baked). Instead of listing each case in turn the cases are tabulated in parallel. Here is the case analysis of [ Proof of constructive_dilemma ] in this format:
37. (cd1)|-
Table
Case PCase Q
(cd2)|-R.(cd3)|-R.

(Close Table)

38. (above)|-R.

39. 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.`

40. |- (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))`

## How do you show this step -- humor

Spiked Math Comics lists some popular symbols [ 413.html ] and proposes an obscene alternative.

## Examples of Reducto Ad Absurdum

### Proof of dn

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

The proofs use the well known Principle of 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

Define a set of numbers by some property:
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

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

# Syntax of Arguments and Informal arguments

12. Rebutted_proof::=proof #rebuttal.
13. rebuttal::=start("But") block end("But"), a rebuttal is often put after a more or less informal argument and should weaken the conclusion of that argument.

A rebuttal can be place inside a rebuttal to rebut it and so support the original argument.

# MATHS proofs considered easier

Formal 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 and (2) selecting the special cases to analyze. These to steps are often 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.

. . . . . . . . . ( end of section Glossary) <<Contents | End>>

Open for business! Please tell me what you think of this page. Clisck the "[Contact]" button at the top of the page or send Email to rbotting at CSUSB in domain edu.

. . . . . . . . . ( end of section Comments and Reviews) <<Contents | End>>

# Glossary

14. argument::=A sequence of steps that go from a set of assumptions to a conclusion.
15. 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 might be described by Net{radius:Positive Real, center:Point, area:=π*radius^2, ...}.

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.