# Suspending some of the usual laws of logic

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?

``````¬(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?

• Is the formalisation of (b) correct or would it need an exclusive "or"? – Lukas Mar 27 '13 at 21:44
• @Lukas: using a strong disjunction is equivalent to asserting (b) and (c) simultaneously. Because of the useful duality between "inclusive or" (weak disjunction) and "and" (conjunction), people tend to strongly favour writing logical statements and axioms using weak disjunction. It's quite a good practise to do so, and here in particular it highlights two separate properties of negation in classical logic. – Niel de Beaudrap Mar 28 '13 at 11:19
• I have revised the question in an attempt to improve the content. If anyone would like to suggest further improvements to make this question better suited for this site, please submit an edit. – Niel de Beaudrap Mar 28 '13 at 14:48
• @NieldeBeaudrap I changed "law of identity" to "law of self-implication" since the former name seems pretty inapt and invites confusion with the "law of self-identity" (aka reflexivity of identity). – Dennis Mar 29 '13 at 4:41

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.

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...

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.

• However, in a category, one does have maps from A to itself. The statement `A ⇒ A` would be most naturally rendered by the existence of the identity morphism on A, which is guaranteed by the category axioms. Your answer seems to be addressing the notion of "individuality" rather than `A ⇒ A`. – Niel de Beaudrap Mar 27 '13 at 16:22
• deBeaudrap: Fair enough; but although it's called the identity morphism, it isn't asserting identity in the usual sense but only that it is isomorphic to itself. There is in fact a generalisation of category theory where the identity axiom is dropped - called semicategories. Perhaps I should revise my answer in relation to this notion instead. I'm not sure what you mean by individuality. – Mozibur Ullah Mar 27 '13 at 16:40
• It is the isomorphism (or in fact, just 'morphism') which I'm addressing here. It seems fairly clear to me that the OP is not addressing identity per se, but implication. Semicategories do seem to be the pertinent idea there. – Niel de Beaudrap Mar 27 '13 at 16:42
• @deBeadrap: You're right about the OPs question. After calling a) the law of identity - he says underneath A implies A. I think, however both sides of this are salient. – Mozibur Ullah Mar 27 '13 at 16:52