"PROOF BY CONTRADICTION" SCD
This is also known by the Latin label, "reductio ad absurdum" (reducing to an absurdity), and by another Latin label, "tertium non datur" (no third way, beyond true and false), and by the English label, "nonconstructive proof".

A proof of a thesis under these labels is invoked whenever the thesis cannot be proved constructively by deriving what it is supposed to prove.

  1. The nonconstructive proof assumes negation of the thesis to be proven;
  2. then sees if this logically leads to a contradiction;
  3. if so, then, by arguing that contradiction of the contradiction of a thesis is equivalent to the thesis (double negation is positive, just as double clicking of light switch restores the state), the claim is made that the thesis has been proven.
An immediate difficulty arises which, to my knowledge, is totally ignored in the literature. What does "negation" mean? Ignoring this question is one case of "Proof by Contradiction" SCD. (Another case is described near the end of this file.)

In my library, I've a little memoir that discusses many different interpretations. Two primary ones are especially relevant here:

  1. negation by exception;
  2. negation by exclusion.
The following setup will allow for both.
I declare the homology (which is implicit in the literature): factor lattice: statement logic :: analytic geometry : synthetic geometry. (Factor lattice does for statement logic what analytic does for synthetic geometry, namely, provides coordinates for statements).

We can consider negation by exception by the familiar model from arithmetic of facor theory.

In factor language, "proof by contradicction" (double negation) means that a number is equivalent to the complement of its complement.

In the factor lattice on 48 = 16 x 3 = 24 x 3:

  1. let the "thesis" be coordinated by 2. Its complement in the factor lattice on 48 is 3.
  2. But the complement of 3 in the factor lattice on 48 is 16, NOT 2!
The difficulty is that 2 is UNCOMPLEMENTED in the factor lattice on 48.

Arguably, outside of logomath, we might be able to claim that a given thesis is true , but it does not follow from this that the thesis is the whole truth -- in factor lattice language, we can claim that 2 is in the factor lattice on 48, but it does not follow from this that 2 is the highest power (degree) of 2 in the factor lattice on 48.

The above result would follow also from coordinating our thesis with the factors 4, 8.

On the other hand, to claim that you should not use a known factor as a coordinate is to admit that some statements are beyond formalization.

But what about negation by exclusion? That also can be represented by a factor lattice. For, by symmetry, every lattice has an associated "anti-lattice" in which joins and meets are interchanged.

In this case:

  1. the first complement of 2 is in the anti-lattice coordinated as -2;
  2. then another complementation returns to the original lattice, coordinating not with 2 but with 16.
  3. So, either way, the lattice coordination disagrees with the standard interpretation in the logic used in mathematical literature.
The great Dutch mathematician, L. E. J. Brouwer (1881-1966), rejected this type of proof. Among various objections, Brouwer asked, "If a criminal, in committing a crime, succeeds in destroying the only evidence which can be used to convict him, must I then conclude he is not guilty of the crime. No! I want a third possibility: not proven."

In fact, Scottish jurisprudence has long has this third type of proof. There's an old movie, directed by the great David Lean ("Lawrence of Arabia", "Dr. Zhivago", "Bridge Over the River Kwi", etc.), which has the title, "Madeleine", about a famous murder case in the 19th century. A young heiress, Madeleine Smith, was tried for poisoning her lover because she discovered he was only a fortune-hunter. The Crown proved Madelein bought arsenic but could not prove she put it in the chocolate which poisoned him. So the Scottish jury, instead of finding her innocent, returned a victory of "Not proven", which hung over her the rest of her life.

Such a verdict could have been given in the famous Lockerbie bombing case of 1988, when a Pan American liner with 270 people was blown up by a bomb in the luggage. This type of finding was also advocated by Sen. Arlen Spector (PA) in the 1999 impeachment trial of President Clinton.

Lawyers for American mob figures have been able to get their clients declared innocent by forcing a trial to be rushed forward before enough evidence could be collected. The "Not proven" verdict would allow the person be be retried if evidence appears, because "double jeapardy" is involved only after a verdict of "Innocent".

I've an online fable about this type of proof: fable.htm.

In effect, the lattice reasoning above says "Complement of complement of 2 is not proven".

Elsewhere I argue that only mathematics by constructive proof is "First Class Mathematics"; that math by nonconstructive proof is "Second Class Mathematics". So the second case of SCD is to pretend that "Second Class Mathematics" is "First Class Mathematics".