[Skip Navigation] [CSUSB] / [CNS] / [CSE] / [R J Botting] / [ ] / logic_2_Proofs
[Contents] [Source Text] || [Notation] || [Copyright] || [Contact] [Search ]
Fri May 6 09:40:55 PDT 2011

# Proofs

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.

## Tools for Proofs

(ProofBuilder): hamburger helper for budding logicians [ poster.html ]

## Proofs that are not proofs

Source: [RentelnDundes05] (JANUARY 2005 NOTICES OF THE AMS 29)
Net

### Proof by vigorous handwaving

Works well in a classroom or seminar setting.

### Proof by forward reference

Reference is usually to a forthcoming paper of the author, which is often not as forthcoming as at first.

### Proof by funding

How could three different government agencies be wrong?

### Proof by example

The author gives only the case n = 2 and suggests that it contains most of the ideas of the general proof.

### Proof by omission

"The reader may easily supply the details."

"The other 253 cases are analogous."

### Proof by deferral

"We'll prove this later in the course."

### Proof by picture

A more convincing form of proof by example. Combines well with proof by omission.

### Proof by intimidation

"Trivial."

### Proof by seduction

"Convince yourself that this is true!"

### Proof by cumbersome notation

Best done with access to at least four alphabets and special symbols.

### Proof by exhaustion

An issue or two of a journal devoted to your proof is useful.

### Proof by obfuscation

A long plotless sequence of true and/or meaningless syntactically related statements.

### Proof by wishful citation

The author cites the negation, converse, or generalization of a theorem from the literature to support his claims.

### Proof by eminent authority

"I saw Karp in the elevator and he said it was probably NP-complete."

### Proof by personal communication

"Eight-dimensional colored cycle stripping is NPcomplete [Karp, personal communication]."

### Proof by reduction to the wrong problem

"To see that infinite-dimensional colored cycle stripping is decidable, we reduce it to the halting problem."

### Proof by reference to inaccessible literature

The author cites a simple corollary of a theorem to be found in a privately circulated memoir of the Slovenian Philological Society, 1883.

### Proof by importance

A large body of useful consequences all follow from the proposition in question.

### Proof by accumulated evidence

Long and diligent search has not revealed a counterexample.

### Proof by cosmology

The negation of the proposition is unimaginable or meaningless. Popular for proofs of the existence of God.

### Proof by mutual reference

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.

### Proof by metaproof

A method is given to construct the desired proof. The correctness of the method is proved by any of these techniques.

### Proof by vehement assertion

It is useful to have some kind of authority relation to the audience.

### Proof by ghost reference

Nothing even remotely resembling the cited theorem appears in the reference given.

### Proof by semantic shift

Some of the standard but inconvenient definitions are changed for the statement of the result.

### Proof by appeal to intuition

Cloud-shaped drawings frequently help here.

### What is the difference between an argument and a proof?

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

# Notes on MATHS Notation

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 ]

# Notes on the Underlying Logic of MATHS

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

1. STANDARD::= See http://www.csci.csusb.edu/dick/maths/math_11_STANDARD.html

# Glossary

2. 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).
3. given::reason="I've been told that...", used to describe a problem.
4. given::variable="I'll be given a value or object like this...", used to describe a problem.
5. goal::theorem="The result I'm trying to prove right now".
6. goal::variable="The value or object I'm trying to find or construct".
7. 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.
8. hyp::reason="I assumed this in my last Let/Case/Po/...".
9. QED::conclusion="Quite Easily Done" or "Quod Erat Demonstrandum", indicates that you have proved what you wanted to prove.
10. QEF::conclusion="Quite Easily Faked", -- indicate that you have proved that the object you constructed fitted the goal you were given.
11. RAA::conclusion="Reducto Ad Absurdum". This allows you to discard the last assumption (let) that you introduced.