ΑΒΓΔ.XYZ

If a set of assumed proofs have as a consequence (the sign is often dropped) then anything follows.

(One)

ΔΔα(Weak-R)\dfrac{\Delta \vdash \bot } {\Delta \vdash \alpha} \textsf{(Weak-R)}

Similarly, if from the assumption that is refuted we can conclude the statement that can never be refuted () then we can deduce any other statement from . (remember is the initial object in a co-Heyting algebra).

(Two)

ΔΔα(Weak-R)\dfrac{\Delta \dashv \top } {\Delta \dashv \alpha} \textsf{(Weak-R)}

Similarly the following rule shows that one must interpret the left side disjunctively.

(Three)

ΔβΔ,αβ(Weak-L)\dfrac{\Delta \dashv \beta} {\Delta, \alpha \dashv \beta} \textsf{(Weak-L)}

For if from a hypothetised refuted Δ one can refute 𝛽, then adding an arbitrary 𝛼 to Δ will not affect the refutation. This addition must be harmless. It explains also why the rule is called a weakening.

Notes:

With great respect, Henry Story, Born 29th July 1967 - died 5th Sptember 2023


From Mathematics StackExchange, Henry Story, April 2020:

Examples of co-implication (a.k.a co-exponential)