Learn how to write proofs...
- Innovative proof-checking software makes
it easy to learn how
- Free, full-version, PC-based
downloadable program (2.5 MB)
- Last
updated 2009-03-25
Contents
1. Testimonials
2. Features
3. Sample Proofs
5. To the Educator:
Why teach formal logic and set theory?
Testimonials
"[DC Proof] is well conceived, carefully planned and remarkable in its pedagogy and content."
─Brendan Kelly Ph.D., Ed.D., Emeritus Professor of Mathematics and Mathematics
Education, OISE/University of Toronto, Canada
"What impressed me most about
[DC Proof] is that it seems to focus
on ensuring that logic is stripped to its bare essentials, and these
simplest concepts are taught very thoroughly indeed, with full cross
referencing between practice and theory."
─Stephen Simmons, Clinical Director, National Health Service, UK
"[DC Proof] is a better tool for learning about proofs in the way that mathematicians usually do them."
─Norman Megill,
creator of
Metamath,
Lexington MA, USA
"I find [DC Proof] much easier to use
than other theorem provers... I found COQ et al to be quite heavy to
integrate. DC Proof on the other hand has a more natural language associated
with it."
─Tom
Hubbard, Lead Software Systems Engineer, Bedford MA, USA
Features
- Convenient pull-down menus of the rules and
axioms of logic enable you to construct formal arguments and
proofs line by line
- Color-coded variables
(in predicate logic) indicate at a glance what kind of generalizations can be made, and when
conclusions may be drawn
- Able to view proofs at various levels of detail,
hiding or revealing details as required
─ absolutely
indispensible for writing longer proofs!
- User comments and meaningful
variable names (of unlimited length) that facilitate both the reading and
writing of proofs
- Interactive tutorial that introduces you to
the standard methods of proof (view
table of contents and excerpt):
- Direct proof
- Indirect proof, or proof by contradiction
- Proof by contrapositive
- Proof by cases
- Proof by induction
- Manipulation of universal and existential
quantifiers
- A simplified set theory (functions, subsets,
power sets, Cartesian products, etc.)
- Use of formal definitions (in elementary number theory)
- Direct proof
Sample Proofs
Samples of proofs in the easy-to-read DC Proof format:
- Sun, cloud and rain (propositional logic)
- Dolphins, mammals and fish
(predicate logic)
- The composition of
functions (set theory)
- Resolution of Bertrand Russell's The Barber Paradox (predicate logic)
System Requirements
DC Proof is a PC-based program that requires the following software to run:
- PC users require Windows 95 or later
- Mac OS X or Linux users require a Windows
emulator or the equivalent. Recommended are:
-
Wine 1.0.1
- Free download
- Limited tech support
- No need to install Windows
-
CodeWeavers
Crossover
- 30 day free trial, reasonably priced
- Makes using Wine 1.0.1 easier
- Tech support included
- No need to install Windows
-
Wine 1.0.1
- All users require MS Internet Explorer, Version 4 or later
- DC Proof uses components of IE
- IE must be installed on your computer
- IE need not be your default browser,
and need not be running or active at any time
- Free download of latest version of IE available from Microsoft
- DC Proof uses components of IE
To the Educator: Why teach formal logic and set theory?
First, the rules and axioms of formal logic and set theory are common to all branches of mathematics. While it may be impractical to present most proofs formally, these rules and axioms must be understood by every mathematician. Every geometer, for example, must understand the law of the contrapositive. And every number theorist must understand De Morgan's Law, and so on.
Studies have also shown that proof-writing skills learned in one branch of mathematics such as geometry may not be easily transferred to other branches such as abstract algebra and real analysis. See for example, F. A. Ersoz, "Proof in different mathematical domains," Proceedings of the ICMI Study 19 Conference, 2009, Volume 1. Here, Ersoz suggests (p. 163) that the many informal "axioms" of Euclidean geometry, as usually taught, are based largely on personal intuition and imagination. This can blur the boundary between the formal and informal, and lead to confusion as to what constitutes a legitimate proof in other domains (branches) of mathematics. He also suggests (p. 164) that introductory geometry courses seldom present many of the methods of proof used in more abstract courses─methods like proofs by induction, contrapositive or contradiction.
When first introducing the various methods of proof, it would also make sense to use illustrations from the simplest possible domains; that is, from systems with a minimum number of rules and axioms. And the simplest such domain is, of course, formal logic and set theory.
An approach based, initially at least, on formal logic and set theory may then be the best way to teach the methods of proof that can be applied widely in every branch of mathematics.
