Suspending some of the usual laws of logic

Question

What would the consequences be, if we suspended some of the usual laws of logic so that they were no longer available as tools in proofs?

(a) The Law of Self-Implication

A ⇒ A for any proposition A

This is a consequence of the rule of inference of conditional introduction: because A ⊢ A for any proposition A, the deduction theorem implies that ⊢ A ⇒ A. What forms of logic where conditional introduction of this sort is not allowed, and what features do they have?

(b) The Law of Excluded Middle

A∨¬A for any proposition A

This is mostly used in proofs of things by dilemma, to show that if A ⇒ B and ¬A ⇒ B, then B is true because A∨¬A. Using the rule of inference of disjunctive syllogism (i.e. material implication), this is equivalent to A ⇒ A, because A ⇒ B is equivalent to ¬A∨B. What forms of logic prevent us from having A∨¬A as a theorem for free, for every A?

(c) The Law of Non-contradiction

¬(A&¬A) for any proposition A

This proposition is essentially built into how we approach reductio ad absurdum, and comes close to being the defining property of logical negation. Using de Morgan's Laws, it's equivalent to the Law of the Excluded Middle. What forms of logic prevent us from having ¬(A&¬A) as a theorem for free, for every A?

Answer 1

Well, then we get other logical systems with possibly interesting properties and applications.

1. Giving up (a) is tough, I'm not aware of any logic where this doesn't hold. (But I wouldn't be surprised if there is one.)

2. (b) does not hold in intuitionistic logics and also not in partial logics. Many logicians consider a failure of (b) to be desirable.

3. (c) is given up in paraconsistent logics, e.g. in a logic with with 4 truth values you can interpret the values as {}, {T}, {F}, {T, F} where the latter is the case A & not A is true - dialethists do this to "deal" with semantic paradoxes.

Answer 2

1. A regular logic without identity A=>A is not imaginable because if something isn't itself we can't prove anything. But actually there is a system called Ludics strongly related to the Curry-Howard isomorphism and to Linear Logic which don't use identity and reformulate Logic in a completely new way.

2. A logic where can't prove A / ~A is an Intuitionistic Logic. See for instance the philosophy of Brouwer (Intuitionism and Formalism). It's a logic that can be used to describe computer programs in the "functional paradigm" (See Curry-Howard isomorphism). Moreover, intuitionistic logic can be described with a sequent calculus without right contraction (conclusion).

Another interesting thing : what happens when we forbid/restrict the structural rules (contraction and weakening also called duplication and erasure) ? See Linear Logic, Relevant Logic, Affine Logic...

Answer 3

In category theory, one is not allowed to say that A=A, but that A is similar to A (isomorphic is the technical term). Now each category has three interpretations: as a category, as a type theory/logic, as a geometry. So when interpreted as a logic this shows that your a) has been given up. One cannot assert identity but similitude.

Less technically (or operationally), supposing objects have an unbounded number of attributes - how can we assert identity? We can compare attributes that are accessible to us, but how about those attributes that are not now, or can never be accessible to us in principle? We can then only assert similitude.

EDIT

in the Type Theory entry in the nLab they write:

Therefore it makes sense to demand for any two terms x,y:X of a type X the existence of an identity type Id.X(x,y) which represents the proposition that x is equal to y, hence such that a term p:Id.X(x,y) is a proof of this fact. But this idea necessarily iterates, with the equality of two such proofs in turn being witnessed by a term of a second order identity type, and so on. Reflecting on this shows that the type-theoretic notion of equality resulting this way is not the traditional one, but is the notion of homotopy equivalence or equivalence in an (∞,1)-category. Type theory with such identity types properly implemented is thus called homotopy type theory.