Relationship between Structural Contraction and the Absorption theorem?

Question

Edit: Originally I called the absorption theorem “contraction theorem” which makes everything needlessly wordy and confusing. I will call the left structural contraction rule simply LSC rule, and the “contraction theorem” absorption. I’ve also made the question’s scope a lot smaller (see last paragraphs). I realized that I might have some misunderstandings I need to clear up, particularly with the role that LSC plays in proving absorption in sequent calculus and natural deduction.

---

Left contraction rule (LSC): Given Γ, A, A ⊢ Δ, derive Γ, A ⊢ Δ
Absorption theorem: ⊢ (A → (A → B)) → (A → B)

What is the relationship between the LSC rule in sequent calculus and the absorption theorem?

1. Can there be a logic that don't allow the LSC but retains absorption as a theorem?
2. Can there be a logic that does not have absorption as a theorem but have the LSC rule?

For the first question, suppose we take the ordinary sequent calculus for classical logic and just drop LSC. It seems like absorption wouldn’t be effected by it, as a proof of it does not use LSC (but merely the rules of the conditional). However, as I understood it, dropping LSC corresponds to dropping reiteration rule in natural deduction, but the reiteration rule is needed (alongside ->-Intro and MP) to prove the absorption theorem. Is there a disparity here or am I missing something?

Answer 1

Suppose we have a logic with a derivability relation ⊢ and a conditional → that obeys the deduction theorem for that logic, i.e.

Γ ∪ {A} ⊢ B    if and only if     Γ ⊢ A → B

Where Γ is a set of sentences, which can be thought of as representing background information or side premises.

Then generally speaking, there will be a correspondence between the rules for valid inferences within that logic and the theorems within that logic. Any valid derivation can be converted into sentential form using a conditional; and any conditional can be converted into a derivation. The forward direction relates to the rule of conditional proof: assume A, derive B, then discharge the assumption A to introduce the conditional A → B. The reverse direction relates to the rule of modus ponens: A → B, together with A, derives B.

So, if you want to have a logic and a conditional such that there is a lack of correspondence between the rules of inference and the theorems, you must find a conditional that does not obey the deduction theorem. If a rule of inference holds, but the corresponding conditional sentence is not derivable, then we have an exception in the forward direction, i.e. conditional proof fails. If we have a conditional sentence but the corresponding rule is not valid, then we have an exception in the reverse direction, i.e. modus ponens fails.

In classical logic, the material conditional obeys the deduction theorem, so that is of no use for this purpose. But there are non-classical logics with conditionals that do not obey the deduction theorem, and there are conditionals that can be defined within classical logic that are not material.

(Incidentally, your contraction rule relates to the property of the idempotency of entailment.)

Straightforwardly, there is nothing to stop you devising a logic in which (A → (A → B)) → (A → B) is an axiom, but the rule of contraction does not hold in general. The only issue would be whether such a logic is useful.

In the commonly studied logics that I am familiar with, the contraction rule and the absorption theorem mostly stand or fall together. In the relevance logics R and E, both hold. In linear logic, neither hold. In Adams' probability logic both hold. For Stalnaker's conditional, both hold.

In the modal logic T, □(□(A → □(A → B)) → □(A → B)) is a theorem, but in K it is not. So you might have an example there. There are many trivalent logics in which the deduction theorem does not hold, so there may be examples there too. (See, e.g. "De Finettian Logics of Indicative Conditionals", by Paul Égré, Lorenzo Rossi, Jan Sprenger)

Answer 2

As I understand your question, you want to know what role if any LSC plays in proving the Absorption theorem. The following proof uses the deduction theorem.

Theorem: ⊢ (A → (A → B)) → (A → B)

Proof.

1. ⊢ (A → (A → B)) → (A → B) iff

(A → (A → B)) ⊢ A → B

2. (A → (A → B)) ⊢ A → B iff

(A → (A → B)), A ⊢ B

Modus Ponens gives us A → (A → B)), A ⊢ A → B

3. (A → (A → B)), A ⊢ A → B iff (A → (A → B)), A, A ⊢ B

NOW YOU NEED THE LSC TO GET

4. (A → (A → B)), A ⊢ A → B iff (A → (A → B)), A ⊢ B

Looking back at lines 1-4, we see

5. ⊢ (A → (A → B)) → (A → B) iff (A → (A → B)), A ⊢ B

We readily verify (A → (A → B)), A ⊢ B

with the following demonstration.

1. A→ (A → B)
2. A
3. A → B [1,2; MP]
4. B [2, 3; MP]

Therefore ⊢ (A → (A → B)) → (A → B)

Q.E.D.

So its proof does require the LSC, in classical logic.

So to your first question:

Can there be a logic that don't allow the LSC but retains absorption as a theorem.

To prove Absorption I have shown, you need the LSC rule. So the answer to this question is no.

OP asked

Can there be a logic that does not have absorption as a theorem but have the LSC rule?

There CANNOT be a logic that does not have Absorption as a theorem but has tautology, as the following demonstration shows.

Definition if A then B= not A or B

1. If A then (if A then B).
2. Not A or (not A or B). [1; Df]
3. (Not A or not A) or B. [2; associativity]
4. Not(A and A) or B. [3; DeMorgan]
5. Not A or B. [4; tautology]
6. If A then B. [5; Df]

⊢ (A → (A → B)) → (A → B)

Since a logic has tautology iff it has LSC (proved below), there CANNOT be a logic that does not have Absorption as a theorem but has LSC.

The preceding proofs used a system of natural deduction with the following six underived rules of inference, and three axioms.

Conjunction: A,B; therefore A and B

Simplification 1: A and B; therefore A

Simplification 2: A and B; therefore B

Double Negation 1: A; therefore not(not A)

Double Negation 2: not(not A); therefore A

Conjunctive Syllogism: A, not(A and not B); therefore B.

Axiom of the Corresponding Conditional

If A1,A2,..., An ⊢ B then (if A1 and A2 and... and An then B).

From this, we can prove the following corollary, which is usually considered an aspect of the deduction theorem.

Corollary: If A ⊢ B then ⊢ A → B

Axiom of Analyticity

If A is a theorem of the statement calculus then A is a tautology.

Axiom of Semantical Equivalence

If 'A if and only if B' is a tautology then A=B.

Now you have sufficient information to prove the converse of the axiom of the corresponding conditional. You can then combine them into one theorem.

Theorem: A1,A2,..., An ⊢ B iff (if A1 and A2 and... and An then B).

Using the deduction theorem, which can be proved in this system, we have as a theorem of the sequent calculus:

Γ, A, A ⊢ B iff Γ ⊢ if A then (if A then B).

Using the theorem

If A then (if B then C)=if A and B then C, we have:

Γ, A, A ⊢ B iff Γ ⊢ if (A and A) hen B.

Now go in the reverse direction, to prove:

Γ, A and A ⊢ B iff Γ ⊢ if (A and A) then B.

Now by transitivity of iff you can infer

Γ, A, A ⊢ B iff Γ, A and A ⊢ B

Now one of the theorems of the statement calculus is Tautology : (A and A) = A.

So in the sequent calculus you can go from Γ,A,A to Γ, A and A by the theorem I just proved. Then by taut, you get the LSC; from Γ, A, A ⊢ Σ derive Γ, A ⊢ Σ.

Therefore, a logic has tautology if and only if it has LSC.

In the system of natural deduction I am discussing, you also have necessary and sufficient information to prove the deduction theorem.

Deduction Metatheorem

For n>1

If A1,A2,..., An ⊢ B then A1,A2,..., An-1 ⊢ An → B

On page 242 of 'Symbolic Logic' by Irving M. Copi, he states

Of course there is some connection between them as there is between any two statements such as P ⊢ Q and ⊢ P → Q. Given the latter, the former is easily established. To the sequence of well formed formulas s1, S2,.. SK (where SK is P → Q), which constitutes a demonstration for ⊢ P → Q, we need only add P as SK+1, and derive Q as SK + 2, for it follows from SK and SK + 1 by modus ponens.

Thus I will assume the OP has some familiarity with constructing demonstrations.

Therefore the following statement holds:

If ⊢ P → Q then P ⊢ Q.

If the premises of a valid argument are true then its conclusion must be true. Therefore, we can open the scope of assumption A in the middle of some demonstration. Then proceed validly to some subsequent line B. Thus that portion of the demonstration shows A ⊢ B. Now, from the corollary to the axiom of the corresponding conditional, we can close the scope of the assumption, by writing A → B. The opening and closing of scopes of assumptions allows us to reason naturally, hence the name nattural deduction.

In the sequent calculus, we have repetition A ⊢ A. Therefore by the corollary to the axiom of the corresponding conditional, we have A → A.

Theorem: A ↔ A

1. A → A [previous theorem]
2. A → A [1; repetition]
3. A → A ∧ A → A [1,2; conjunction]
4. A ↔ A [3; Df of iff]

Q.E.D.

Metatheorem: A = A

By the Axiom of Analyticity, if 'A if and only if A' is a theorem of the statement calculus, then it's a tautology. Hence it's a tautology. By the Axiom of Semantical Equivalence, if it's a tautology then A = A. Hence A = A.

Q.E.D.

Thus, Absorption is a theorem of any logic which has repetition, conjunction, DeMorgan's Law for negation of a conjunction, and associativity of disjunction.

Using the system of natural deduction I have presented here, it's trivial to derive repetition.

Derived Rule: A ⊢ A

1. A
2. Not(not A) [1; double negation 1]
3. A [2; double negation 2]

Conjunction is an underived rule of inference.

It's trivial to prove Double Negation, using double negation 1, and double negation 2.

Double Negation DN: A = not (not A)

Q.E.D.

Now we can prove DeMorgan's Law for negation of a conjunction.

Theorem: Not(A and B) = not A or not B

1. Not A or not B = not(not(not A) and not(not B)) [Df of or,]
2. Not A or not B = not(A and B) [1; DN]

Q.E.D.

Thus, Absorption is provable in the system of natural deduction presented here.

Now I will make a bold statement. There is only one analytic and complete system of natural deduction, and that's the system I've presented here. I call it the statement calculus, others call it the propositional calculus, still others call it the sentential calculus.

Thus, there are no alternative logics for the OP to consider that are simultaneously analytic and complete. Complete in the sense that all tautologies are theorems of the system. Analytic in the sense that only tautologies are theorems of the system.

Our system is inconsistent if there is a derivable statement A, such that A and not A. By equivalence of the contrapositive, if for any derivable statement A, not (A and not A) then our system is consistent.

Axiom I: If 'A iff B: is a theorem of the statement calculus then A = B.

Definition: A or B = not(A and not B)

Definition: If A then B = not A or B

Definition: A iff B = (if A then B) and (if B then A)

Let A,B be arbitrary statements.

Derived Rule 1 R: A ⊢ A.

Already derived.

Theorem 1: If A then A

Already proved.

Q.E.D.

Theorem 2: not(not(not A and not A)

1. If A then A [Thm1]
2. not A or A [1; Df of if]
3. not(not(not A) and not A) [2; Df of or]

Q.E.D.

Theorem 3 If A then not(not A)

1. A ⊢ not(not A) [DN1]
2. If A then not(not A) [1; DT corollary]

Q.E.D.

Theorem 4 If not(not A) then A

1. not(not A) ⊢ A [DN2]
2. If not(not A) then A [1; DT corollary]

Q.E.D.

Theorem 5: A iff not(not A)

1. If A then not(not A) [Thm3]
2. If not ( not A) then A
3. If A then not(not A) and if not(not A) then A [1,2; conjunction]
4. A iff not(not A) [3; Df of iff]

Q.E.D.

Metatheorem Double Negation DN: A = not(not A)

By axiom I, if A iff not(not A) is a theorem of the statement calculus then A = not(not A). Hence, A = not(not A).

Q.E.D.

Theorem 6: not(A and not A)

1. not(not(not A) and not A) [Thm2]
2. Not(A and not A) [1; DN, substitution]

Q.E.D.

Since A is an arbitrary statement, we have proved for any statement A, not(A and not A).

Our system is consistent if for any derivable statement A, not(A and not A).

Let A be a statement that denotes a proposition whose truth value varies in time. For example A could be "I am hungry". The statement calculus applies to all propositions, temporal or not. A proposition is that which is true or false, and is not part of any language. A statement, on the other hand, is always part of a language, and denotes a proposition.

Definition: An argument is valid if and only if given it's premises are true, then it's conclusion must be true.

There are only 6 underived rules of inference. If each of them is valid, then we can never infer a false conclusion from true premises.

We define the logical operator NOT, as follows:

A not A not(not A)

0 1 0

1 0 1

From the truth functional definition of NOT we have that the argument A; therefore not(not A) is valid, and the argument not(not A); therefore A is valid.

Symbolically, this means

1. A ⊢ not(not A)
2. Not(not A) ⊢ A

We define the logical operator AND, as follows:

A B A and B

0 0 0

0 1 0

1 0 0

1 1 1

From the truth functional definition of AND, we have

1. A, B ⊢ A and B
2. A and B ⊢ A
3. A and B ⊢ B

Now consider the following truth table.

A B not B (A and not B) not(A and not B)

0 0 1 0 1

0 1 0 0 1

1 0 1 1 0

1 1 0 0 1

Consider the argument conjunctive syllogism.

A, not(A and not B); therefore B

There is only one row in which the premises are true, state row 4, and in that row the conclusion B is true. Therefore if the premises of conjunctive syllogism are true, then the conclusion must be true. Hence conjunctive syllogism is a valid argument.

Thus, using 2-valued logic, i.e. binary logic, conjunction, simplification 1, simplification 2, double negation 1, and double negation 2, and conjunctive syllogism, are all valid arguments.

A contradiction denotes a proposition that is false at any moment in time, as the following table shows.

A not A (A and not A)

0 1 0

1 0 0

Therefore, it is impossible to derive a contradiction from true premises, using the six underived rules of inference. Therefore, this system is consistent.