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 ]
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.
( 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
Shown | Meaning | Formal meaning |
---|---|---|
(-1) | Using the previous result (New Jun 28th 2007) | |
(-2) | Using the previous two results (New Jun 28th 2007) | |
(above) | I'm too lazy to work out which evidence I need here | All above assertions at this level. |
() | I'm too hurried to type above | (above) |
(given) | I've been told that... | Axiom |
(goal) | I'm trying to prove or find this. | |
(let) | For the sake of argument let... | Assumption [ Block Structure ] |
(hyp) | I just assumed this | Label of statements after last Let |
(RAA) | Reducto Ad Absurdum | The assumption in the above Let lead to a contradiction. |
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): conclusionWithout the assertion sign we just labeled an expression so that we can talk about it informally:
(label): expression.
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 e1 and e2 we have:
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:
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.
The following rules need special documentation to indicate how a previous formula has been modified:
Table
(label) Name | From | Step | Conclude | When | Explanation |
---|---|---|---|---|---|
| W(e) | (eg, x=>e)|- | for some x:T(W(x)) | e must be an expression of type T | See eg_explained |
| 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 |
| for one x:T(W(x)) | (ud, v=>x)|- | W(v) | v must be free variable before, and is now bound. | See ud_explained |
| for all x:T(W(x)) | (ui, x=>e)|- | W(e) | e is an expression of type T | See ui_explained |
In practice the name (eg,ei,ud,ui) can be omitted. It's good to put them in when doing exercises or when using the rules for the first time with a new audience.
Similarly, in practice, the substitution (...=>...) is often omitted.
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
(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
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
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:
So it is valid to derive
. . . . . . . . . ( end of section Valid Deductions) <<Contents | End>>
http://www.csci.csusb.edu/dick/maths/logic_25_Proofs.htmlThe 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.htmlthen 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.
In the above the 'mp' step is intuitive for most readers. Further, as rule,
rather then writing
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.
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.
|- ( 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.
This means that we define a new temporary environment
and with new variable x and assumption P.
The above structure has three parts:
Let
Let { |-(1): x:S, (2): P. (...)|-..., (...)|-(result): Q}.The newer form uses directives:
.Let
(1): x:S,
(let)|-(2): P.
...
(1,2,...)|- (result): Q.
.Close.LetNotice 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.
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.
|-(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.LetAlso 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.
Normally all proofs are gathered at the end of the piece of documentation in which the theorems are asserted.
MATHS combines natural deduction and algebra. An algebraic step uses an inference like the following:
.Net
e1
(y1)|-
R1 e2
(y2)|-
R2 e3
(y2)|-
R3 e4
...
.Close.NetOr in rendered format:
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 ]
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.
Here is an example, follow the link to see what it is about:
Net
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
[ Definitions of Quantifiers in logic_10_PC_LPC ]
Similarly, for most associative operators,o, the STANDARD MATHS abbreviation:
[ 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:
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:
The above are useful because they can be used to replace an implication like
The following translation rules are helpful:
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
For example to show that if then is transitive(iftrans):
It can be combined with rules from semantic tableaux that handle quantifiers.
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.
P or Q.
.Case
|-P. ...
(...)|-R.
.Else
|-Q. ...
(...)|-R
.Close.Case
(above)|- R(See [HuthRyan00] page 19 and 11)
if P then Q.
.Case
|-not P. ...
|-Q.
.Else
|-Q. ...
|-R
.Close.Case
|- R
not(P iff Q).
.Case
|-P,not Q. ...
|-R.
.Else
|- Q,not P. ...
|-R,
.Close.Case
|- R
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.
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:
. . . . . . . . . ( end of section Example Proof by Case) <<Contents | End>> For more on these techniques see [ logic_27_Tableaux.html ] (theory).
Case P | Case Q |
---|---|
(cd2)|-R. | (cd3)|-R. |
Here are several examples [ tttt.html ] (tabulated cases.
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.
( label1, label2)|-false.
Here are the standard forms
.Let
|-P, not Q.
... derive any absurdity
.Close.Let
(above)|- if P then Q.
.Let
|-not P, not Q.
... derive any absurdity
.Close.Let
(above)|- P or Q.
.Let
|-not P.
... derive any absurdity
.Close.Let
(above)|- not P
.Let
x:T, |-not W(x).
... derive any absurdity
.Close.Let
(above)|- for all x:T(W(x)).
.Let
for all x:T(not W(x)).
... derive any absurdity
.Close.Let
(above)|-for some x:T(W(x))
First prove
Next prove
. . . . . . . . . ( end of section Examples of Reducto Ad Absurdum) <<Contents | End>>
The key to mathematical induction is a pattern like this:
Net
Prove that 1 has the property:
Prove that if a number has the property then so has the next number.
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
Let
. . . . . . . . . ( end of section Example of Useful Template: Mathematical Induction) <<Contents | End>>
. . . . . . . . . ( end of section Valid Forms of Proof) <<Contents | End>>
A rebuttal can be place inside a rebuttal to rebut it and so support the original argument.
. . . . . . . . . ( end of section Glossary) <<Contents | End>>
. . . . . . . . . ( end of section Comments and Reviews) <<Contents | End>>
. . . . . . . . . ( end of section Proofs in MATHS) <<Contents | End>>
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 ]
For a more rigorous description of the standard notations see