What logical systems categorize A->~A as a contradiction.?

Question

In the basic propositional logic I learned in school A->~A is not a contradiction because it is not false when ~A is true. What logical systems would hold this statement to always be false?

Answer 1

By request of virmaior, here are my comments unified as an answer — It seems likely to me that such a logic might not exist, or might be too limited.

A possible obstacle.    Consider the classic proof by contradiction of the fact that the square-root of 2 is irrational. Let

R ≡ [a,b ∈ ℕ] & [a/b = sqrt(2)] & [gcd(a,b)=1]

which is to say that a/b is a reduced ratio of integers which is equal to the square root of 2. The way that the usual proof-by-contradition of the irrationality of sqrt(2) goes is to demonstrate that a=2c and b=2d for integers c and d, which is to say that 2 divides both a and b. Thus gcd(a,b) ≠ 1, which implies ~R. That is, we prove that

R ⇒ ~R

from which we infer that ~R. The punchline of the proof is that ~R holds no matter what a and b are, so that sqrt(2) is irrational; but the way we prove it is by showing that R ⇒ ~R, and in any case the latter is a theorem — so it can only be a contradiction if the logical system is inconsistent.

Now, mathematics is usually done with classical logic, in which conditionals A ⇒ B can be vacuously satisfied (that is, A ⇒ B will be true if A happens to be false). A logic in which A ⇒ ~A is false whenever ~A is true, must not use material implication — that is, it must be that A ⇒ B is not equivalent to ~A v B. But it must do more than just this: it must, among other things, make it impossible to derive the above proof of R ⇒ ~R for the specific case of the proposition R above relating to the square root of 2. I suspect that this might be difficult to achieve.

We may consider alternative proofs for the square root of 2: for instance, it is possible to show intuitionistically that the only even numbers which have rational square roots are those which are multiples of 4, from which we can then infer that the square root of 2 is irrational without using the above argument. So we can prove that the square root of 2 is irrational without relying on R ⇒ ~R being true. But this of course doesn't imply that R ⇒ ~R is not true; we can still derive that particular proposition intuitionistically.

Any logic in which ~A implies that ~(A ⇒ ~A) must somehow prevent this specific mathematical argument from being formulated, which may mean that it is too limited a logic to be able to perform much in the way of mathematics. That might make it a logic of limited interest.

How to begin looking.    In order to consider logics in which A ⇒ ~A can be false when ~A is true, there are some things at minimum which you must look for: it must be a logic in which

1. is non-weakening: we cannot infer B ⇒ ~A for all B, from ~A; and
2. is non-explosive: we cannot infer A ⇒ B for all B, from ~A.

Classical logic obviously isn't such a logic, because implication is material implication; and common forms of intuitionistic logic don't work either, because the weakening inference which we want to avoid is usually valid (e.g. as a logical axiom at the link above).

A possible starting point for such a search would be relevance logic, which at least is non-explosive and non-weaking: implications must actually allow one to derive the conclusion from the premise by reasoning with non-logical constants. It appears that paraconsistent logic (which is related to intuitionistic logic by a duality relation) may also provide an avenue for research, albeit one in which the notion of "falsehood" is quite profoundly problematised. But in any case, even while considering logical systems which are neither "weakening" or "explosive" in the sense above, you must somehow overcome two obstacles:

• The system must not allow you to prove R ⇒ ~R above, for particular cases R such as that related to the quare root of 2 above. (This means that an approach with relevance logic, for example, will have to be a more limited variety in which the above proof does not carry through.)

• If you really mean that you want for A ⇒ ~A to be false when ~A is true, you will have to specify what precisely you mean by 'falsehood'. In relevance logic, 'truth' amounts to 'provability': so for instance A v ~A is only 'true' if we have a separate proof for A or a separate proof for ~A. Do you take falsehood of A ⇒ ~A to be a meta-logical impossibility of obtaining a proof? Or do you take it to mean that you can prove ~(A ⇒ ~A)? Either way you may find yourself presented with a challenge.

Answer 2

@Addems answer is right, it is just not clear.

In any logic with the ordinary definitions of implies, not and or:

'A implies not A' iff 'not A or not A' iff 'not A'

So no extension of ordinary logic is going to find this a contradiction. Even weakenings of modern logic that keep the definition of A implies B meaning A or not B still make this a theorem.

So only systems with a less mechanical definition of 'implies' like hard-core constructivism could ever possibly find 'A implies not A' to be a theorem. The only useful ones of those are always weaker than standard logic, so they will not add theorems. So no useful or normal theory of logic will have this as a theorem.

'A implies not A' is not a contradiction in and of itself. When it is proved, it establishes that A is false. This is the basis of all uses of reductio-ad-absurdum. You assume A to be true and show that it contradicts itself, and that proves A false.

If the proof itself were a contradiction, you could no longer do this.

Answer 3

I know of none, and that's probably for good reason--I doubt there is a good argument for considering it a contradiction, given that the sentence A --> B should have truth conditions distinct from the truth conditions of those for A and B. It is a new sentence that shouldn't imply A itself or B, or else the "conditional" nature of the expression would be pretty thoroughly violated. Therefore A --> ~A should not necessarily imply that A and ~A are both true, and so it probably shouldn't imply a contradiction.

But note that I do not mean to suggest that First Order Logic is in any sense the "correct" logic, and like most philosophers I recognize the failure of the material conditional to express the same content as is contained in most "if-then" English constructions. But I do suggest that, of the failures of First Order Logic, the fact that the sentence A --> ~A is not considered a contradiction isn't one of them.

Answer 4

Perhaps a good way to start would be to think about what kind of considerations might lead one to say that A→¬A should be read as contradictory.

Here's a possibility: Suppose we want an implication sign that reads more as a Logical Consequence operator, such that if we get to the point where we affirm that A→¬A this represents a premise on the left affirming its negation, and therefore ought to itself be seen as reason to discharge A as an assumption.

At a first pass, we might pose your question as trying to add an an "implication connective" → to a Natural Deduction system with the traditional rules for negation, conjunction etc., which features the following elimination rule:

A → ¬A
______   (→ elim1)
⊥

as well as, presumably, the Modus Ponens rule

A → B      A
______________   (→ elim2)
B

and the traditional implication introduction

[A]
.
.
B
_____  (→ int)
A → B

It's unproblematic that such a system can in fact be constructed using Natural Deduction technology to be a logic that properly extends Intutionistic propositional logic. The question is, what additional power does this kind of implication connective give us that we didn't have before? Might it be possible to derive some unusual consequences (such as a collapse into inconsistency)? I'll have a think about that and edit this answer if I can come up with anything.

Answer 5

One possibility is Model Theory, the modern context for mathematical logic, where you have rules of inference, a language, models, and interpretations.

Here your language will be propositional logic, the rule of inference will be modus ponens, and the model will be just the smallest Boolean algebra {T, F}.

Now, all (well-formed) formulae are designated as theorems or non-theorems.

Then it should be possible to show that A ->~A is not a theorem.

Another way to look at this is to think of propositional implication as Aristotelian consequence; then we notice that this statement is not a valid law of reasoning.