.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: Equals can be substituted for equals. |- (euclid): If (e1=e2)then (W(e1) iff W(e2)) |- (euclid): If (e1=e2)then (f(e1) = f(e2)) The above can be generalized when we have several equations... see .See Algebra and Calculations below. 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 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 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(x=x). (-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: (relations)|- 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 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. .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]. The same structure works between sets and relations to give .Key higher-order logic proofs. For example to prove subset we can establish a chain of subset relations: .As_is .Net .As_is S1 .As_is (y1)|- .As_is ==> S2 .As_is (y2)|- .As_is ==> S3 .As_is (y3)|- .As_is ==> S4 .As_is (y4)|- .As_is ==> S5 .As_is ... .As_is .Close.Net .As_is (above)|-(l): S1 ==> S[n]. For more on .Key relations see .See ./logic_40_Relations.html and later pages. Other forms of algebraic reasoning have been developed by mathematicians, see .See http://www/dick/maths/math_10_Intro.html#Algebra . 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: .List e1=f1 e2=f2 ... .Close.List We can conclude 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 .As_is (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 .See ./maths/math_43_Algebras.html and .See ./maths/math_45_Three_Operators.html for example. Here is an example, follow the link to see what it is about: .Net .See http://www.futilitycloset.com/2012/09/22/weighty-matters/ |- Natural numbers with addition and subtraction. |- (fc1):me+x=170. |- (fc2):wife+x=130. |- (fc3):me+wife+x=292. (fc1, fc2, +, fc3, -)|- (fc4): me+x+wife+x-me-wife-x = 170+130-292. (fc4, algebra)|- (fc5): x = 8. .Close.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 .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 Example Proof by Case For more on these techniques see .See ./logic_27_Tableaux.html (theory). . 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. Here are several examples .See ./tttt.html (tabulated cases. 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. . 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 . How do you show this step -- humor Spiked Math Comics lists some popular symbols .See http://spikedmath.com/413.html and proposes an obscene alternative. .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 in MATHS