What is the difference between negation-eliminiation ¬E and contradiction-introduction ⊥I?

Question

I don't understand the difference between the rules negation elimination and contradiction introduction. I am using the Open Logic Project's natural deduction proof checker proof checker. The rules on the website include:

Rule ¬E

m| ¬A
n| A
 | ⊥     ¬E m, n

and

Rule ⊥I


m| A
n| ¬A
 | ⊥     ⊥I m, n

What's the difference? Is it just the order of A and ¬A?

Answer 1

At the top of the page it says

The specific system used here is the one found in forall x: Calgary. [...] However, the system also supports the rules used in the forall x: Cambridge remix.

That is, this proof checker supports the union of two slightly different sets of inference rules, and that results in some duplication. At least one rule appears identically under two names:

m| ⊥
 | A     X m


m| ⊥
 | A     ⊥E m

¬E and ⊥I are effectively identical as well. You can replace ¬E 12,34 by ⊥I 34,12 without making any other change to the proof.

If you're taking a class or following a textbook, you should use their rules, which won't have any duplicates, and will hopefully be a subset of those supported by this proof checker.

Answer 2

Propositional logic has a structure that is captured by the mathematical concept of a Boolean algebra. A Boolean algebra has multiple equivalent definitions. A standard one is a set of well-formed formulae; three operations "not", "and", and "or"; and two distinguished types of propositions, "contradiction" and "tautology"; subject to the following rules:

For all well-formed formulae A, B, and C, in some contextual universe of discourse:

Commutativity

• A and B is true if and only if B and A is true.
• A or B is true if and only if B or A is true.

Example: "I am sad and it is raining" has identical truth conditions to "It is raining and I am sad". The former is true if and only if the latter is true. This means they are logically equivalent, which in logic is taken to express that they have the same meaning.

Associativity

• A, and B and C is true if and only if A and B, and C is true.
• A, or B or C is true if and only if A or B, or C is true.

Example: "I will go to China, and I will visit the Great Wall and Tiananmen Square" is only true if "I will go to China and visit the Great Wall, and I will go to China and visit Tiananmen Square" is true; and "I will go to China and visit the Great Wall, and I will go to China and visit Tiananmen Square" is only true if "I will go to China and visit the Great Wall and Tiananmen Square" is true. To see this, try claiming that one is true while the other is not.

Identity

• A and a tautology is true if and only if A is true.
• A or a contradiction is true if and only if A is true.

Example: "I have a Lamborghini, and tall people are tall", is true only if "I have a Lamborghini" is true; and "I have a Lamborghini" is true, only if "I have a Lamborghini, and tall people are tall" is true.

Complement

• A or a tautology is true if and only if a tautology is true.
  • Hint: a tautology is always true, so "A or a tautology" is always true, even if A is not true.
• A and a contradiction is true if and only if a contradiction is true
  • Hint: a contradiction is always false, so "A and a contradiction" is always false, even if A is true.

Example: "I went to the party at 8pm and I practice drums 25 hours a day" is true if and only if "I practice drums 25 hours a day" is true (which it isn't).

Distributivity

• A, or B and C is true if and only if A or B, and A or C is true.
• A, and B or C is true if and only if A and B, or A and C is true.

Example: "She ate her lunch, or she threw it away and lied about eating it" is true if and only if "She ate her lunch or she threw it away", and "She ate her lunch or lied about eating it" are true.

From the above, you can observe that commutativity is a property of propositional logic, so if A and not A form a contradiction, then by commutativity it follows that not A and A form a contradiction.

What's the difference? Is it just the order of A and ¬A?

Yes; those rules are identical if you use commutativity.