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



      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)

          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


          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


  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.