"They probably wouldn't, because the grammar of ordinary language does not follow the rules of propositional logic.

In propositional logic, the following is a valid argument:

P → ¬P
∴ ¬P"

Exactly. And if someone wouldn't make such an inference, I am suggesting that that is a logical mistake of some sort, which is a way of saying the argument is not valid.

There's no logical mistake? It's just the case that "if ... then ..." in ordinary English doesn't mean what "→" means in propositional logic.

Can you explain how those meanings diverge?

"I disagree with regards to ordinary language" I'm not quite getting it, what is the disagreement you have concerning ordinary language? You think someone would make an inference from A->not-A to therefore not-A in ordinary language?

A → B means B or not A

If I punch you then you will cry does not mean you will cry or I won't punch you.

I think you mean to say that the one implies the other through logical equivalence. That is different than saying that the expressions mean different things.

In fact, I would say A->B does not "mean" B or not-A.

you will cry or I won't punch you — Michael

This uses the inclusive OR which is also not so standard in English.

Is it worth pointing out, again, that "P→~P" is not a contradiction? If P→~P is true, then P is false.

If that's been said once, it's been said a thousand times... which is not once.

What is going on here is not a pedantic mismatch between English and some esoteric academic exercise. Rather, there are ambiguities in the English use of "If... then...", "...or..." and various other terms that we must settle in order to examine the structure of our utterances in detail.

What is going on here is not a pedantic mismatch between English and some esoteric academic exercise. Rather, there are ambiguities in the English use of "If... then...", "...or..." and various other terms that we must settle in order to examine the structure of our utterances in detail. — Banno

I consider the logical conditional a performative, as exists in an algorithmic way.

Consider, "If X = 4, then Y = 7." That is , if we set X at 4 then Y is set at 7. We could not program if we could not make such statements. If P then Q results in the occurence of Q when P is the case necessarily. I consider this an analytic operation and consistent with computer logic in programming (as far as I know about programming).

I consider the linguistic conditional not an indication of what is or what will be, but a hypothetical counterfactual that does not indicate, but hypothosizes. Because it does not indicate, we don't speak in the indicative mood, but in the subjunctive, as in what we wish, hope, or hypothesize about.

As in: "If I were President, I would lower taxes." This is not represented as P -> T. That would overstate the meaning of my speculative statement. Note the "were," not "was." This is a counterfactual (it hypothethesizes an antecedent that did not occur), not a logical conditional.

"If I was President, I lowered taxes" makes more sense as a formal conditional.

If I was President, I lowered taxes
I was President
ergo I lowered taxes

But not:

If I were President, I would lower taxes
I were President
ergo I would lower taxes

What does it mean that I were President versus I was President? I think the meaning is critical in changing from the formal indicative conditional to the non-formal linguistic subjunctive conditional.

My thoughts at least.

↪NotAristotle
Is it worth pointing out, again, that "P→~P" is not a contradiction? If P→~P is true, then P is false.

If that's been said once, it's been said a thousand times... which is not once. — Banno

I know Banno; I am not disagreeing with the formal validity of that argument.

there are ambiguities in the English use of "If... then...", "...or..." and various other terms that we must settle in order to examine the structure of our utterances in detail. — Banno

I don't disagree with that either. But the argument A → ~A ∴ ~A clearly does not translate into natural language very well (I don't think there is any way to translate it in a way that renders the translation sensible and "logical"). And yet, the argument is valid formally speaking.

Michael suggested that the argument is not sound in ordinary language. I think he may be right. However, even arguments that are not sound can still be valid such that we can understand how the speaker reached their conclusion (though we may point out to them that such-and-such premise is not true). For example, if someone argued:

1. P
2. P→Q
Therefore, Q.

We might correct them, "well, actually ~Q." "Your reasoning is spot on and logical, it just happens to be that ~P, so while your reasoning is valid, the argument you presented is unsound."

On the other hand, "If it is raining, then it is not raining, therefore it is not raining" sounds like an unwarranted leap that is not logical when we consider it in an informal way. The problem isn't just that the initial premise is unsound (within an informal context); the problem is that the argument just doesn't make sense and is not logical, so soundness aside, that is why I call it "not valid" informally.

We might correct them, "well, actually ~Q." "Your reasoning is spot on and logical, it just happens to be that ~P, so while your reasoning is valid, the argument you presented is unsound." — NotAristotle

Yes, there is a difference between an unsound argument that arises from an incorrect fact as opposed to one that arises from a contradiction.

- If I go to the store, I will buy milk, I went to the store, so I bought milk. That's true, unless I forgot to buy milk.

- If I go to the store, I will not have gone to the store, I went to the store, so I didn't go to the store. That statement is never true regardless of what I do. The reason it's never true is because "If I go to the store, I will not have gone to the store" is logically equivalent to "I did not go to the store."

I don't see any reason to introduce modality. It just adds to the confusion.

SO you want to introduce a new form of validity, that depends not on the explicit structure of the argument but on your intuition. Ok.

"I disagree with regards to ordinary language" I'm not quite getting it, what is the disagreement you have concerning ordinary language? You think someone would make an inference from A->not-A to therefore not-A in ordinary language? — NotAristotle

The formal meaning of negation in intuitionistic logic refers to the syntactical inconsistency of the negated sign, rather than to a purported semantic counterexample denoted by the negated sign. Classical logic inherits the same meaning of negation from intuitionistic logic, except for infinitary propositions that appeal to the Law of Excluded Middle, which have no scientific or commonsensical application. So we should stick to discussing negation in intuitionistic logic, before proceeding to other formal logics such as affine linear logic, whose concept of negation is closer to ordinary use. In such cases (A --> Not A) --> Not A is not derivable, corresponding to the fact that Not A obtains the same semantic status of A.

But can we elucidate the meaning of (A --> Not A) --> Not A in the systems for which it is valid, by appealing to the mutually exclusive states of the weather? Suppose that a weather forecaster said "It is raining in Hampshire therefore it is not raining in Hampshire". Jokes about the english weather aside, wouldn't you assume that they were talking about anything apart from the weather in Hampshire? in which case your abstaining from assigning a meaning to their words would resonate with the formal meaning of negation in intuitionistic and classical logic.

As for formalities,

(A --> ~A) --> ~A is little more than the obvious identity relation ~A --> ~A, due to the fact that ~A is definitionally equal to A --> f , where f denotes absurdity. So we at least have

(A --> f) --> ~A

But the only means of obtaining f from A is via the principle of explosion (A And ~A) --> f. And so it is sufficient that A implies ~A.

(A --> ~A) --> ~A

And since the converse direction is immediately true, we could in fact define the negation of A to be the fixed point of the expression X => (A --> X) that Haskell programmers call a Reader Monad.

~A = A --> ~A
~A = (A --> (A --> (A --> ..... ) ))

which serves to highlight the meaning of Negation As Failure (NAF); A proof of ~A amounts to a finite proof that the right hand side doesn't converge, which represents an infinite failure to prove A by random search. But if we haven't managed to prove either A or ~A using our available time and resources, then we are at liberty to declare ~A by decree and reason accordingly, in which case ~A serves to nullify any hypothesized A by turning it into ~A, so as to ensure consistency with our failure to decide the issue, at least for the time being...