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(
.See 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
.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
.See http://www.math.csusb.edu/notes/proofs/pfnot/pfnot.html
and
.See http://www.math.csusb.edu/notes/proofs/bpf/bpf.html

. Two Systems of Proof
MATHS combines two systems for proving things: see
.See Natural Deduction
and 
.See 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:
.As_is ( 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
.See evidence
below.  The scoping of variables and labels is very like that in a
structured program, see below: 
.See 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 
.See Valid Deductions
tabulated below.

Here are some common abbreviated reasons:
.Table Shown	Meaning	Formal meaning
.Row (-1)	Using the previous result (New Jun 28th 2007)
.Row (-2)	Using the previous two results (New Jun 28th 2007)
.Row (above)	I'm too lazy to work out which evidence I need here	All above assertions at this level.
.Row ()	I'm too hurried to type `above`	(above)
.Row (given)	I've been told that...	Axiom
.Row (goal)	I'm trying to prove or find this.
.Row (let)	For the sake of argument let...	Assumption
.See Block Structure
.Row (hyp)	I just assumed this	Label of statements after last `Let`
.Row (RAA)	Reducto Ad Absurdum	The assumption in the above `Let` lead to a contradiction.
.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
.As_is 		|- (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:
.As_is 		(reasons) |- (label): conclusion
Without the assertion sign we just labeled an expression so that we
can talk about it informally:
.As_is 		(label): expression.


.Open 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
.See Algebra and Calculations
below.
.Box
	|- (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.

        ()|- (dn1): if not not P then P.
        ()|- (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.
	()|- (iff6): (P iff (Q iff R) iff ((P iff Q) iff R), associative.
	()|-(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)).
.Close.Box

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 ;
.Box
When `W` or `f` bind the same set of free variables in `P` and `Q` we have:
 |- (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.
.Close.Box
From the above rules you can deduce that '=' is an equivalence relation:
.Box
	(above)|- (eqid): e = e.
	(above)|- (eqcomm): (e1 = e2) iff (e2 = e1).
	(above)|- (eqtrans): if (e1 = e2) and (e2 = e3) then (e2 = e1).
.Close.Box
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
.See Natural Proofs
below.

The following rules need special documentation to indicate how a previous formula has been modified:
.Table (label) Name	From	Step	Conclude	When	Explanation
.Row |- (eg): Existential Generalization
.Item W(e)
.Item (eg, x=>e)|-
.Item for some x:T(W(x))  
.Item `e` must be an expression of type `T`
.Item See $eg_explained
.Row
|- (ei): Existential Instantiation
.Item for some x:T(W(x))
.Item (ei, x=>v)|-
.Item v:T, W(v) 
.Item `v` must be free variable before, and is now bound.
.Item See $ei_explained
.Row
|- (ud): Unique definition
.Item for one x:T(W(x))
.Item (ud, v=>x)|-
.Item W(v)	
.Item `v` must be free variable before, and is now bound.
.Item See $ud_explained
.Row
|- (ui): Universal Instantiation
.Item for all x:T(W(x))
.Item (ui, x=>e)|-
.Item W(e)
.Item `e` is an expression of type `T`
.Item 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
	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 for all x:T ( true ).
	(-1, eqid) |- for all x:T (x=x ).
	(-1, ui, x=>v) |- v = v.
	(-1, eg, x=>v) |- for some x:T(v=v).
	(-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 (
.See mp
above) and Universal Instantiation (
.See 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 \in 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.

.Close Valid Deductions
. 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
.As_is http://www.csci.csusb.edu/dick/maths/logic_25_Proofs.html
The individual rules have all anchors for links.  For example,
.As_is http://www.csci.csusb.edu/dick/maths/logic_25_Proofs.html#mp
.As_is 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.
.See http://www.csci.csusb.edu/dick/maths/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
.As_is 		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
	(s1):	3=sqrt(9),
	(Sqrt, s1)|-(s2): 9=3*3.
.Close.Po

In the above the 'mp' step is intuitive for most readers. Further, as rule,
rather then writing
.Po
	(a): A.
	(a)|-(b): B.
.Close.Po
We "chain" them together lke this:
.Po
	(a): A.
	(-1)|-(b): B.
.Close.Po
or this:
.Po
	(a): A,
	()|-(b): B.
.Close.Po

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
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
.As_is	(premises)|-(label): wff.

then the proof should be in section	
.As_is	. 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
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:
.As_is	|- ( label ): wff

is referred to by the label itself before the assertion sign:
.As_is	( 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
	`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 x:S, 
	(let)|- P.
	...
	...
	(...)|-Q.
.Close.Let
In the above `P` is the hypothesis, `Q` is the result and the whole
would be used to prove:
	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:
.As_is Let { |-(1): x:S, (2): P. (...)|-..., (...)|-(result): Q}.
The newer form uses directives:
.As_is 	.Let
.As_is 		(1): x:S,
.As_is 		(let)|-(2): P.
.As_is 		...
.As_is 		(1,2,...)|- (result): Q.
.As_is 	.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:
.As_is 	.Let x:S, 
.As_is 		(let)|- P.
.As_is 		...
.As_is 		(hyp,...)|- (result): Q.
.As_is 	.Close.Let
.As_is 	(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.
.As_is 	.Let x:S, A, B, C, ...
.As_is 		...
.As_is 		(hyp,...)|- (result): Q.
.As_is 	.Close.Let
.As_is 	(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.
.As_is 	.Let x:S, A, B, C, ...
.As_is 		...
.As_is 		(hyp,...)|-  P.
.As_is 		...
.As_is 		(hyp,...)|-  Q.
.As_is 	.Close.Let
.As_is 	(above) |- for x:A, if A and B and C ... then P and Q.

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

po::= "Po"|"Let"|"Consider"| "Case"|...,
start(p) ::= directive & ("." p EOLN).
end(p) ::= directive & (".Close" "." p EOLN).
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.
 
.Open Valid Forms of Proof
. Natural Proofs
.Box
Universal Propositions
.As_is 	 |-(l): for x:T, if P then Q.	
.As_is	...
.As_is 	. Proof of l
.As_is 	.Let
.As_is 		(let)|-(l.1): x:T, 
.As_is 		(let)|-(l.2): P.	
.As_is 		...
.As_is 		(...)|-Q. 
.As_is 	.Close.Let

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

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

Uniqueness
.As_is 	|- (l) for one  x:T (W2(x)).
.As_is	...
.As_is 	. Proof of l
.As_is 	(...) |-(l1): for some  x:T (W2(x)).
.As_is 	(...) |-(l2): for 0..1  x:T (W2(x)).
.Close.Box

 
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
.See Reducto ad Absurdum
and
.See ./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.

assertion::=  $axiom | $conjecture | $derived
derived::=  $theorem |  $deduction,
label::="(" $identifier "):",
reference::=$identifier.
ref_to::$label ->$reference = the[r:$reference]( "(" r "):" = (_) ).
axiom::=  $label  $wff,
conjecture::='??{' $documentation "}??",
 
deduction::=$line_break_line & ($white_space "(" $evidence ")" $conclusion $eoln).
evidence::= $List($re_used($reference | $defined_term | $comment )).
.See http://www/dick/maths/notn_4_Re_Use_.html#re_used

conclusion::="|-" O($label)  $derived_wff. 
algebraic_step::=$expression  #( EOLN $evidence "|-" EOLN  $relation $expression),  
This echoes the Gries and Schnieder layout, see
.See Algebra and Calculations
below.

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
.See http://www.cs.cornell.edu/Info/People/gries/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:
|-   if e1 R1 e2 R2 e3...R[n-1] e[n] then  e1 ;R e[n].

	Note:  ";R" is short for "R1; R2; ... R[n-1]"
A suitable syntax is
.As_is 	.Net
.As_is 		 e1
.As_is 	(y1)|-
.As_is 		R1 e2
.As_is 	(y2)|- 
.As_is 		R2 e3
.As_is 	(y2)|-
.As_is 		R3 e4
.As_is 	...
.As_is 	.Close.Net
Or in rendered format:
()|-(Dummy):  e1 ;(R) e[n].
. Proof of Dummy
.Net
	 e1
(y1)|-
	 R1 e2
(y2)|- 
	R2 e3
(y2)|-
	R3 e4
	...
.Close.Net
 
In the above the `y`s 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`.
.As_is 	.Net
.As_is 		e1
.As_is 	(y1)|-
.As_is 		= e2
.As_is 	(y2)|-
.As_is 		= e3
.As_is 	(y3)|-
.As_is 		= e4
.As_is 	(y4)|-
.As_is 		= e5
.As_is 	...
.As_is 	.Close.Net
.As_is 	(above)|-(l):  e1 = e[n].
The following is for chains of 'if-and-only-if' steps:
.As_is 	.Net
.As_is 	e1
.As_is 	(y1)|-
.As_is 		iff e2
.As_is 	(y2)|-
.As_is 		iff e3
.As_is 	(y3)|-
.As_is 		iff e4
.As_is 	(y4)|-
.As_is 		iff e5
.As_is 	...
.As_is 	.Close.Net
.As_is 	(above)|-(l):  e1 iff e[n].

Other forms of algebraic reasoning have been developed by mathematicians, see
.See http://www/dick/maths/math_10_Intro.html#Algebra
. 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 
.See http://www.cs.cornell.edu/Info/People/gries/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
	for all x:T, if R then P 
means
	for all x:T(if R then P).

.See http://www/dick/maths/logic_10_PC_LPC.html#Definitions of Quantifiers

Similarly, for most associative operators,o, the STANDARD MATHS abbreviation:
	o[x:{a}](P(x)) = P(a)

.See http://www/dick/maths/math_11_STANDARD.html#SERIAL_AND_PARALLEL
is the Gries/Schneider `one point law`.  Here are some other versions
that can be useful in proving things:
	|- (one_point_laws): all following
.List
	o[x:{a}](P(x)) = P(a).
	for all x:{a}(P(x)) iff P(a).
	for some x:{a}(P(x)) iff P(a).
	for some x(x=a and P(x)) iff P(a).
	for all x(x=a and P(x)) iff P(a).
.Close.List

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:
 |- (Trading):	(for all x (if R then P) iff for all x(not R  or  P))
	and	(for all x (if R then P) iff for all x((R and P) iff R))
	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
	if P then Q
by an equivalence
	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
	(let)|- (hyp): P and Q.
	(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:
Translate_to_Boolean_algebra::=following
.Net
	P and Q = P*Q.
	P or Q = P+Q.
	not P = -P.
	
	(if P then Q) = - P+ Q.
	not(if P then Q) = P*(-Q).

	(P iff Q) = (- P * - Q) + (P * Q).
	not(P iff Q) = ((-P)*Q) + (P*(-Q)).
.Close.Net Translate_to_Boolean_algebra
See the Rules of Boolean algebra:
BOOLE::=http://www/dick/maths/math_41_Two_Operators.html#BOOLEAN_ALGEBRA
and an example:
.See http://www/dick/cs556/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
	if P then Q
analyze
	not(if P then Q)
or in translation:
	P*(-Q).

For example to show that `if then` is transitive($iftrans):
. Proof of iftrans
.Net
 (if P then Q) and (if Q then R) and not (if P then R)
(Translate_to_Boolean_algebra)|-
 = (-P+Q)*(-Q+R)*P*(-R) 
(BOOLE)|-
 = (-P+Q)*(-Q*-R)+R*(-R))*P 
 = (-P+Q)*(-Q*-R)+0)*P 
 = (-P+Q)*(-Q*-R)))*P 
 = (-P+Q)*P*(-Q*-R))) 
 = (-P*P+Q*P)*(-Q*-R) 
 = (0+Q*P)*(-Q*-R) 
 = (Q*P)*(-Q*-R) 
 = Q*P*(-Q)*(-R) 
 = Q*(-Q)*P*(-R) 
 = 0.
.Close.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.

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

analytical::= ".Case" $block #(".Else" $block) ".Close.Case".
.Box
	(or): 
.As_is		P or Q. 
.As_is		.Case
.As_is 			|-P. ... 
.As_is 		(...)|-R. 
.As_is		.Else 
.As_is 			|-Q. ... 
.As_is 		(...)|-R
.As_is 		.Close.Case
.As_is		(above)|- R
(See
.See [HuthRyan00]
page 19 and 11)
	(if): 
.As_is		if P then Q. 
.As_is		.Case
.As_is 			|-not P. ... 
.As_is 		|-Q. 
.As_is		.Else 
.As_is 			|-Q. ... 
.As_is 		|-R
.As_is 		.Close.Case
.As_is		|- R
	(neg): 
.As_is		not(P iff Q). 
.As_is		.Case
.As_is			|-P,not Q. ... 
.As_is 		|-R. 
.As_is		.Else 
.As_is			|- Q,not P. ... 
.As_is 		|-R,   
.As_is 		.Close.Case
.As_is		|- R
.Close.Box
|- analysis=reason"." ".Case" L(#(axiom | comment | definition) #(derived | comment | definition) derived, ".Else" ) ".Close.Case".

Semantic tableaux
.See ./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.

.Open Example Proof by Case
. Example Classical Theorem
(below)|-(constructive_dilemma): if ((P or Q) and (if P then R) and (if Q then R)) then R
. Proof of constructive_dilemma
.Let 
	|-(cd1): P or Q,   
	|-(cd2): if P then R,  
	|-(cd3): if Q then R.
(cd1)|-
.Case
	|-(cd5.1): P.
 (cd5.1, cd2, mp) |- R

.Else
	|-(cd5.2): Q.
 (cd5.2, cd3, mp) |- R 
.Close.Case
 (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:

.Image dilemma.gif Graphical analysis of dilemma

.Close
For more on these techniques see
.See ./logic_27_Tableaux.html
below.

It is also possible and sometimes shorter to use
.See 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
.See Proof of constructive_dilemma
in this format:
(cd1)|-
.Table Case P	Case Q
.Row (cd2)|-R.	(cd3)|-R.
.Close.Table
()|-R.
. Reducto ad Absurdum
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
.As_is	( label1, label2)|-false.
	|- (absurd): if P and not P then false.

Here are the standard forms
.Box
	(rabs1): 
.As_is		.Let
.As_is 			|-P, not Q.
.As_is 			 ... derive any absurdity
.As_is 		.Close.Let
.As_is 			(above)|- if P then Q.
	(rabs2): 
.As_is		.Let
.As_is			|-not P, not Q.
.As_is 			 ... derive any absurdity
.As_is 		.Close.Let
.As_is		(above)|- P or Q.
	(rabs3): 
.As_is		.Let
.As_is			 |-not P.
.As_is 			 ... derive any absurdity
.As_is 		.Close.Let
.As_is 			(above)|- not P

	(rabs4): 
.As_is		.Let
.As_is			x:T, |-not W(x).
.As_is 			 ... derive any absurdity
.As_is 		.Close.Let
.As_is 		(above)|- for all x:T(W(x)).
	(rabs5): 
.As_is		.Let
.As_is			for all x:T(not W(x)).
.As_is 			 ... derive any absurdity
.As_is 		.Close.Let
.As_is 		(above)|-for some x:T(W(x))
.Close.Box

.Open Examples of Reducto Ad Absurdum
. Proof of dn
        not not P iff P.

First prove 
	()|-(dn1):if not not P then P.
.Let
	not not P, not P
.Close.Let

Next prove 
	()|-(dn2): if P then not not P.
.Let
	P, not not not P,

	Use previous result with (not not P)!
	(dn1)|- not P.
.Close.Let
Now assemble 'dn':
	(dn1, dn2, iff3)|- not not P iff P.

. A Proof of an odd result
(below)|-(exrab): if for some x, all y (x R y) then for all y, some x( x R y)
. Proof of exrab
.Let
	|-(np1): for some x, all y (x R y),
	|-(np2): not for all y, some x( x R y).

  (np1,ei,x=>a)|-(np3): for all y (a R y),     
   (np2, qn2, qn2)|-(np4): for some y, all x(not x R y),
 (np4, ei, y=>b)|-(np5): for all x (not x R b),
 (np3, u1, y=>b)|-(np6): a R b,
 (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 x.
.Let |-(hyp): not for some y(if F(y) then F(x)),
   (qn1)|- for all y(not(if F(y) then F(x))),
   (ui, y=>x, nif4)|-F(x) and not F(x),
   $RAA.
.Close.Let
	(above)|- for some y(if F(y) then F(x)).
.Close.Let

.Close Examples of Reducto Ad Absurdum
. 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.
.See http://www/dick/maths/home.html
 
.Open Example of Useful Template -- Mathematical Induction
The proofs use the well known Principle of Mathematical Induction:
induction::=http://www/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:
	P::@Nat={ n. ...}.
	...

Prove that 1 has the property:
	()|-(basis): 1 in P.

Prove that if a number has the property then so has the next number.
	()|-(step): for all k:P ( k+1 in P).
	...

	(basis,step,induction)|- P = Nat.
.Close.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
serial::=http://www.csci.csusb.edu/dick/maths/notn_12_Expressions.html#Serial Operators
and
numbers::=http://www/dick/maths/math_42_Numbers.html

 (serial, numbers, induction)|-(triangle): for all n:Nat, +(1..n)=n*(n+1)/2.

. Proof of triangle
.Let
    F::Nat->@ = fun[n:Nat](+(1..n)=n*(n+1)/2)).
    P::@Nat={n:Nat || F(n) }.

    +(1..1) = +(1)
	(def)|-
		= 1
	(-1)|-
		= 1*(2)/2
	(-1)|-
		= 1*(1+1)/2.
   (-1) |- F(1),
   (-1) |-(basis): 1 in P.                     

.Let
	(1): k:Nat,
	(2): k in P. 
   +(1..(k+1))
	(1, serial)|-
		= +(1..k) + (k+1)
	(2)|-
		= k*(k+1)/2+k+1
	(algebra)|-
		= (k+1)*(k+2)/2
	(algebra)|-
		= (k+1)*((k+1)+1)/2.
	|-(QED): k+1 in P
.Close.Let
    (above)|-(step): for all k:P(k+1 in P).
  (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`.. .

.Close Example of Useful Template: Mathematical Induction

. Links to other useful Templates
.Hole
 
.Close Valid Forms of Proof
. Syntax of Arguments and Informal arguments
Rebutted_proof::=$proof #$rebuttal.
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
.See ./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.

.Open Glossary
above::reason="I'm too lazy to work out which of the above statements I need here", often the last 2 or three statements.
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...",
.See Block Structure
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 fitte the goal you were given.
RAA::conclusion="Reducto Ad Absurdum".
.Close Glossary
.Open Comments and Reviews
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`.
.Close Comments and Reviews
. 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.
.Close Proofs and Demonstrations