For an introduction see
[ logic_20_Proofs100.html ]
which give informal hints and discusses some
philophical ideas associated with proofs and some
tools and automation,
or
[ logic_25_Proofs.html ]
which presents an attempt at a practical yet formal
way of presenting proofs in a machine readable, renderable,
and checkable form.
(ProofBuilder): hamburger helper for budding logicians
[ poster.html ]
Source:
[RentelnDundes05]
(JANUARY 2005 NOTICES OF THE AMS 29)
Net
Works well in a classroom or seminar setting.
Reference is usually to a forthcoming paper of the
author, which is often not as forthcoming as at first.
How could three different government agencies
be wrong?
The author gives only the case n = 2 and suggests
that it contains most of the ideas of the general
proof.
"The reader may easily supply the details."
"The other 253 cases are analogous."
"We'll prove this later in the course."
A more convincing form of proof by example. Combines
well with proof by omission.
"Trivial."
"Convince yourself that this is true!"
Best done with access to at least four alphabets and
special symbols.
An issue or two of a journal devoted to your proof
is useful.
A long plotless sequence of true and/or meaningless
syntactically related statements.
The author cites the negation, converse, or generalization
of a theorem from the literature to support
his claims.
"I saw Karp in the elevator and he said it was probably
NP-complete."
"Eight-dimensional colored cycle stripping is NPcomplete
[Karp, personal communication]."
"To see that infinite-dimensional colored cycle
stripping is decidable, we reduce it to the halting
problem."
The author cites a simple corollary of a theorem
to be found in a privately circulated memoir of the
Slovenian Philological Society, 1883.
A large body of useful consequences all follow
from the proposition in question.
Long and diligent search has not revealed a counterexample.
The negation of the proposition is unimaginable or
meaningless. Popular for proofs of the existence
of God.
In reference A, Theorem 5 is said to follow from
Theorem 3 in reference B, which is shown to follow
from Corollary 6.2 in reference C, which is an
easy consequence of Theorem 5 in reference A.
A method is given to construct the desired proof.
The correctness of the method is proved by any of
these techniques.
It is useful to have some kind of authority relation
to the audience.
Nothing even remotely resembling the cited theorem
appears in the reference given.
Some of the standard but inconvenient definitions
are changed for the statement of the result.
Cloud-shaped drawings frequently help here.
An argument will
convince a reasonable man, but a proof
is needed to convince an unreasonable
one.
(End of Net)
. . . . . . . . . ( end of section Proofs) <<Contents | End>>
Special characters are defined in
[ intro_characters.html ]
that also outlines the syntax of expressions and a document.
Proofs follow a natural deduction style that start with
assumptions ("Let") and continue to a consequence ("Close Let")
and then discard the assumptions and deduce a conclusion. Look
here
[ Block Structure in logic_25_Proofs ]
for more on the structure and rules.
The notation also allows you to create a new network of variables
and constraints. A "Net" has a number of variables (including none) and
a number of properties (including none) that connect variables.
You can give them a name and then reuse them. The schema, formal system,
or an elementary piece of documentation starts with "Net" and finishes "End of Net".
For more, see
[ notn_13_Docn_Syntax.html ]
for these ways of defining and reusing pieces of logic and algebra
in your documents. A quick example: a circle
might be described by
Net{radius:Positive Real, center:Point, area:=π*radius^2, ...}.
For a complete listing of pages in this part of my site by topic see
[ home.html ]
The notation used here is a formal language with syntax
and a semantics described using traditional formal logic
[ logic_0_Intro.html ]
plus sets, functions, relations, and other mathematical extensions.
For a more rigorous description of the standard notations
see
- STANDARD::= See http://www.csci.csusb.edu/dick/maths/math_11_STANDARD.html
- above::reason="I'm too lazy to work out which of the above statements I need here", often the last 3 or 4 statements.
The previous and previous but one statments are shown as (-1) and (-2).
- given::reason="I've been told that...", used to describe a problem.
- given::variable="I'll be given a value or object like this...", used to describe a problem.
- goal::theorem="The result I'm trying to prove right now".
- goal::variable="The value or object I'm trying to find or construct".
- let::reason="For the sake of argument let...", introduces a temporary hypothesis that survives until the end of the surrounding "Let...Close.Let" block or Case.
- hyp::reason="I assumed this in my last Let/Case/Po/...".
- QED::conclusion="Quite Easily Done" or "Quod Erat Demonstrandum", indicates that you have proved what you wanted to prove.
- QEF::conclusion="Quite Easily Faked", -- indicate that you have proved that the object you constructed fitted the goal you were given.
- RAA::conclusion="Reducto Ad Absurdum". This allows you to discard the last
assumption (let) that you introduced.