:up:

The conclusion still always follows with p=1 and must in a way be "contained" in what one starts with. — Count Timothy von Icarus

I see now.

Everything contained in the conclusion must be contained in the premise; we learn nothing from deduction. — Count Timothy von Icarus

Hence, deduction is informative because it involves communication. — Count Timothy von Icarus

Perhaps mathematics is better thought of in terms of signs and relations instead of identity. — Count Timothy von Icarus

"2+2 has a relation with 4 that is informative."

Something that I can think of is that, for Peano, 4 is exactly S(S(0))+S(S(0)), which 2+2, which is S(S(S(S(0)))). I understand you will then reply that S(S(0))+S(S(0)) and S(S(S(S(0)))) are different things whose identity will be established by a computation.

Now, if I were to play the platonist, I would say that both S(S(0))+S(S(0)) and S(S(S(S(0)))) are symbols that point to the same thing. Just like "2" in Times New Roman and "2" in Arial are two symbols that, to an intelligent mind, reference the same universal. Though you will then reply that I must perform the computation to be able to reference the same universal. In that sense the two are not contradictory.

Were I to play the nominalist, S(S(0))+S(S(0)) and S(S(S(S(0)))) are both symbols that are constructed in relationship to each other (so in that sense your criticism that they are not quite the same is sensible) but that nevertheless are applied the same (in physical theories).

But even, and especially, for the nominalist, I think 2+2=4 can be informative while maintaning an identity. 2+2 and 4 are indeed not the same object, but as soon as you establish 2+2=4, you are giving a hint as to what kind of mathematics you are doing. That is, 2+2=4 doesn't give you all the information you need, as there are different arithmetics where 2+2=4, but 2+2=4 rules out many arithmetics; but that is why we have formulations of those different arithmetics and the person using them needs to know how to use them. Peano arithmetic is the one we use the most in everyday life — doing taxes and splitting a bill. But we use module-60 arithmetic when adding up minutes of time. Within Peano arithmetic, 2+2=4 is the same, so it is indeed not informative within Peano arithmetic, but it is informative when Peano arithmetic is applied in real life: pushing two rocks against two rocks gives you four rocks. Peano arithmetic is applicable to this structure, thus the application gives us information.

The less obvious computations are $\int_{0}^{2}\frac{3x^2}{2}dx$ that gives us 4, but $\int_{0}^{2}\frac{3x^2}{2}dx$ is descriptive exactly of the speed of an accelerating car and knowing that a certain arithmetic also applies to the situation will give us the information of the total traveled distance.

Of course, this might be circular on the application level:

PA applies to a structure.
PA gives information about the structure.
The information we get is assumed in the first premise.

But I know everything you said about computation is still going to apply:

It perhaps depends on how much you embrace pancomputationalism in physics and information theoretic explanations of the other special sciences. If we think number only appears in nature in terms of computation and process then that seems suggestive at the very least. — Count Timothy von Icarus

I don't know anything about either of those theories, so I can't say. But it doesn't feel like this conversation applies to mathematics per se.

His argument is that intuitionist assumptions — Count Timothy von Icarus

Like the denial of LNC?

Oh no! Leontiskos has "inundated" the thread! More posts and words from him than any other poster! I better scold him for that right away! No, actually, unlike his hypocritical self, I don't begrudge anyone from posting as much as they want to post.

Note so that, hopefully, Leontiskos will desist from mischaracterizing my views: In all these posts: I am not claiming that classical logic is the only correct or useful logic. I am not claiming that classical logic accords with the many notions of logic and language in everyday discourse. And I do not claim that classical logic should not be critiqued. (Indeed, such critiques as from constructivism, predicativism, finitism, relevance logic, etc. are rich sources).) But when classical logic is being critiqued, it should not be mischaracterized, misrepresented or misconstrued, so explanations of how classical logic actually operates are productive. And giving explanations of classical logic does not imply advocacy for it or a presumption that it is the only formal logic that should be consulted. I admire the thought that goes into formal logic; I enjoy studying it; I appreciate its role in formalization of mathematics; I appreciate its use in such things as computing; I appreciate that it is the subject of much of philosophy of mathematics and that it generates rich questions in mathematics and philosophy. And, in my own limited way, I have studied other formal logics and have read and appreciated critiques of classical logic. I do not claim that anyone should even care about formal logic, but when people do talk about it, they should get it right, and it is eminently proper to remark when they don't.

you do not know what you mean by 'particular.' — Leontiskos

That is false. And it is said without basis. I know what I mean by the word. I use it in its everyday sense.

No one in this thread has been able to understand what that concept means — Leontiskos

What the concept of 'a particular contradiction' means? 'particular' is used in the everyday sense such as definition 1 at Merriam online.

to talk about a particular contradiction without a sense of a non-particular contradiction does not make sense. — Leontiskos

I don't use 'non-particular'. There are particular contradictions (such as "B & ~B") and there is a definition of 'is a contradiction'.

* A formula is a contradiction if and only if it is the conjunction of a formula and its negation.

* Sometimes 'contradiction' is also used in the sense that a formula is not necessarily a conjunction of a formula and its negation but is a formula that entails a conjunction of a formula and its negation. (For that sense, I usually use 'inconsistent'.)

* With natural deduction, we sometimes refer to a pair of lines such that one is the negation of the other. But notice, that is merely commentary, as the formal deduction does not depend on the use of the term 'contradiction' but only on specifying a rule by reference to there being one line with a formula and another line with its negation.

A contradiction is an assertion of Propositional Logic that is false in all situations; that is, it is false for all possible values of its variables. — Tautologies and Contradictions

That is the semantical side of the coin. 'contradiction' is usually defined syntactically (a formula and its negation) but it does follow that a sentence is a contradiction if and only if it is logically false.

The conclusion of a reductio is like, "This is an apple." — Leontiskos

No, the conclusion of a reductio is of the form "~P" from the assumption "P", or for the non-intuitionistic version, "P" from the assumption "~P".

G be a set of premises and a sentence P is not a member of G. And we want to show that G proves ~P. Then we may use any of the members of G in our argument. But, along with members of G, we also may suppose P to derive a contradiction, thus to show that G proves ~P.
— TonesInDeepFreeze

The fiction in the reductio for the formalist is that there is some formal difference between an assumption or premise and a supposition. I say that there is not. — Leontiskos

Leontiskos can say whatever he likes, but he is terribly confused and uninformed about the subject.

I explained how reductio works in natural deduction, as just quoted by Leontiskos.

And formulation of the rules for natural deduction do not need to mention 'premise', 'assumption' or 'suppostion'. We may mention those words for convenience, but the specification of a natural deduction system does not require such words. Leontiskos would learn what a natural deduction system actually is - not his nutty imagination of what he thinks it is - by just reading a reliable text or article that covers the subject.

There is a difference between P being a member of G and P not being a member of G. That is not a "formalist" fiction.

I'll take time and effort to give even greater detail, though Leontiskos will likely ignore it or mangle it in the dysfunctional, electrically shorting food processor that is his brain when it spews garbage about logic.

One elegant way to formulate sentential natural deduction is with these rules that permit:

Enter P on a line and charge that line to itself.

If P, along with possibly other lines, shows Q, then infer P -> Q and charge it with all lines charged to Q except the line for P.

From P and P -> Q, infer Q and charge it with all lines charged to P and to P -> Q.

If P, along with possibly other lines, shows a formula Q and a formula ~Q, then infer ~P and charge it with all the lines used to show Q and to show ~Q except the line for P.

If ~P, along with possibly other lines, shows a formula Q and a formula ~Q, then infer P and charge it with all lines used to show Q and used to show ~Q, except the line for ~P. [not intuitionistic]

From P and Q, infer P & Q and charge it with all lines charged to P and to Q.

From P & Q, infer P or infer Q and charge it with all lines charged to P & Q.

From P or from Q, infer P v Q and charge it with all lines charged to P.

From P v Q, P -> R and Q -> R, infer R and charge it with all lines charged to P v Q and to P -> R and to Q -> R.

There is no mention of 'premise', 'assumption' or 'supposition'.

Those rules are equivalent with:

{P} |- P

If Gu{P} |- Q, then G |- P -> Q

If G |- P and H |- P -> Q, then GuH |- Q

If Gu{P} |- Q and Gu{P} |- ~Q, then G |- ~P

If Gu{~P} |- Q and Gu{~P} |- ~Q, then G |- P [not intuitionistic]

If G |- P and H |- Q, then GuH |- P & Q

If G |- P & Q, then G |- P and G |- Q

If G |- P or H |- Q, then GuH |- P v Q

If G |- P v Q, and H |- P -> R and J |- Q -> R, then GuHuJ |- R

There is no mention of 'premise', 'assumption' or 'supposition' nor, for that matter, 'contradiction'.

if from ¬(A → (B ∧ ¬B)) we infer that A implies no contradiction — Lionino

We don't infer that. Suppose A is "P & ~P", then A itself is a contradiction.

If ~(A -> (B & ~B)) is true then A is true. But if A is a contradiction, then ~(A -> (B & ~B)) is not true.

You are misstepping when you take ~(A -> (B & ~B)) to mean "A implies no contradiction" or that ~(A -> (B & ~B)) entails that there is no contradiction that A implies.

Otherwise, try to prove it. Assume:

~(A -> (B & ~B))

Then try to prove:

For every C, if C is a contradiction, then A does not imply C.

What are the assumptions you will use to try to prove it? Are you making a claim about what pertains in ordinary symbolic logic? Or are you making a claim about how statements of such forms are understood in certain everyday contexts? If you are making a claim about what pertains in ordinary symbolic logic, then your attempted proof should not include premises that are not derivable in context of ordinary symbolic logic.

(A¬→(B∧¬B)), if such a thing were proper writing, — Lionino

It is not well formed.

But we could have a notation P-/->Q, but what would it mean if not ~(P -> Q)?

The truth-functionalist is likely to object to me, “But your claims are not verifiable within classical logic!” — Leontiskos

One may instruct as to what does and does not obtain in classical logic without claiming that classical logic is the only credible logic. If the subject is classical logic, then we need to not make false claims about it, no matter what our views about it may be. So, if (made up example) someone said, "in classical logic, RAA is a rule for checking the well-formedness of expressions" then one doesn't have to commit to any particular view of classical logic in order just to point out that that is not what RAA is and not how RAA works.

Now, in this discussion, there has been talk about classical logic qua classical logic. And so it is eminently proper to point out when classical logic is misconstrued or misrepresented. Just as one doesn't have to be an intuitionist or advocate for paraconsistent logic, etc. to point out when intuitionististic logic or paraconsistent logic, etc. is misconstrued or misrepresented. How can that not be eminently reasonable? And it is eminently unreasonable, irrational and anti-intellectual to try to arrogate a presumed dialectic high ground by dissuading people from pointing out how classical logic actually does operate.

My hunch here is that the classical logic system treats everything in this purely relational and context-dependent way and assumes that every non-simple proposition can be cast as a simple 'p' while preserving all of the validity relations. — Leontiskos

That is so blatantly, ridiculously, shamefully wrong. It could be written only by someone who doesn't know jack about the subject. It is the opposite of the truth. Classical sentential logic is based on compositionality and not reducing all arguments to merely atomic formulas. And classical predicate logic extends with quantifiers.

P→Q
∴¬P

The revised textbook would need to add an asterisk: "This is a fallacy*."

" *Except in that case where Q = (b∧¬b)" — Leontiskos

Again, Leontiskos doesn't know jack about this subject.

When we say "It is not the case that P->Q implies ~P" it is understood that that means "It is not the case that for all formulas P and Q, P->Q implies ~P". 'P' and 'Q' are understood to be sentential variables and that in informal discussion, the quantification 'for all' is implicit. Of course we understand that P->Q implies ~P for certain P and Q while it is not the case that for all P and Q, P->Q implies ~P. And Leontiskos's claim about this - "some rules of classical logic to come into conflict" - is patently false.

Anyone who has studied even an introductory text in the subject would understand that. The study of the subject is not responsible for Leontiskos's ignorance about it.

There's more and more and more misconception and ignorance in Leontiskos's posts. One cannot even keep pace with them.

@Leontiskos keeps blindly flailing over the fact that RAA rejects one premise but not the others. That objection is based on not understanding RAA, not understanding exactly what it is.

1 P {1}
2 Q {2}
3 ~(P & Q) {3}
4 P & Q {1,2}
5 ~P {1,2,3}

that is valid. {1,2,3} |= ~P

1 P {1}
2 Q {2}
3 ~(P & Q) {3}
4 P & Q {1,2}
5 ~Q {1,2,3}

that is valid. {1,2,3} |= ~Q

1 P {1}
2 Q {2}
3 ~(P & Q) {3}
4 P & Q {1,2}
5 ~~(P & Q) {1,2,3}

that is valid. {1,2,3} |= ~~(P & Q)

RAA permits only valid inferences. The fact that there are different valid arguments we may choose from does not vitiate that RAA permits only valid inferences.

There's been discussion about modus tollens and RAA vis-a-vis each other.

Contraposition is a one formula version of the rule RAA.

With a natural deduction system with RAA, we can derive contraposition as an axiom.

With an axiom system with contraposition as an axiom, we can derive RAA as a rule.

This is the path that Banno and @TonesInDeepFreeze have chosen:

(a→(b∧¬b)) → ¬a — Leontiskos

I've chosen to correctly report that that is a truth table tautology and a theorem of ordinary symbolic logic. Will Leontiskos's tribunal find me guilty of the crime of being a "truth functionalist" for that?

One is a statement in the meta-language and the other in the object language. They are different levels of statement.
— TonesInDeepFreeze

A direct proof requires no recourse to the meta-language. When the reductio identifies a contradiction it is dipping into the meta-language. That exchange earlier with Tones was about whether the reductio is truth-functional. It turns out that you cannot represent a reductio in the object language. — Leontiskos

That is a confusion of someone who doesn't know jack about the subject.

The formulas of the object language are written in the object language and referred to in the metalanguage. A proof mentions formulas from the object langugae, but the proof is a sequence of formulas (or tree of them, or a sequence of pairs of formulas and sets of line numbers, etc., depending on the system). The sequences are not written in the object language. For example, a sequence as written by:

1 P -> Q {1}
2 P {2}
3 Q {1,2}

mentions the formulas P -> Q, P, and Q, but also 1, 2, 3 and {} that are in the meta-language.

RAA is no different in that respect from such proof forms a modus ponens, conjunction introduction, etc.

↪TonesInDeepFreeze pointed out, a reductio is meant to show the inconsistency of some assumption given a set of premises (i.e. more than 1!). — Leontiskos

I didn't say that. Leontiskos says he hardly reads my posts, but not so hardly to stop him from putting words in my mouth. Leontiskos is a strawmaner extraordinaire.

I didn't say "more than 1". Leontiskos pulled that from thin air.

Indeed, here is an RAA from even the empty set of sentences:

1. P & ~P {1}
2. P {1}
3. ~P {1}
4. ~(P & ~P} { }

Indeed, every logically true sentence is provable from the empty set of sentences, and the negation of every logically false sentence is provable from the empty set of sentences.

And I didn't say "the inconsistency of some assumption given a set of premises" (or if I did, then I typed incorrectly). What I said is that RAA shows that a sentence is inconsistent with the set of premises. There's a world of difference between those.

We have established that "A does not imply a contradiction" is not a good reading of ¬(a→b∧¬b). — Lionino

You're welcome for that. (Not too very bumptious of me.)

TonesInDeepFreeze [has] chosen:

(a→(b∧¬b)) → ¬a — Leontiskos

I haven't "chosen" it except that it is:

a theorem of sentential logic

a tautology

a symbolization, in one formula form, of certain common reasoning

What I have consistently said is that reductio is not valid in the same way that a direct proof is. — Leontiskos

RAA is valid in the same way any other rule is valid:

A rule is valid if and only if application is truth preserving, which is to say that any interpretation in which the premises are true is an interpretation in which the conclusion is true.

how do you prove that you may derive ~ρ from ρ→(φ^~φ)? — Lionino

By showing a derivation:

1. P -> (Q & ~Q) {1}
2. P {2}
3. Q & ~Q {1,2}
4. ~P {1}

RAA is a rule. If it is a primitive rule, then there's no call to prove it. If it is a derived rule from primitive rules, then we prove that any inference with the derived rule can be formulated with the primitive rules only.

A natural deduction system would have RAA as primitive. Ordinarily an axiom system would have RAA as derived.

Or, you might ask "how do we know that a rule is valid"? Well, we prove:

With any application of the rules, any interpretation in which the premises are true is an interpretation in which the conclusion is true.

That is the soundness theorem.

how do you prove that you may derive ~ρ from ρ→(φ^~φ)?
— Lionino

I consider it an open question as to whether this question is answerable. — Leontiskos

I answered it.

When we do a reductio
A, A→¬B∧B ⊢ ¬A is valid

But A, A→¬B∧B ⊢ A is also valid

So the question is: how do we choose between either? — Lionino

Choose in what sense?

Do you mean whether we should claim A or claim ~A?

I wouldn't claim either. The premises are inconsistent, a fortiori the arguments are not sound. I would claim a conclusion only from an argument that is not only valid but is sound, and especially not from an argument in which the needed premises are inconsistent.

This is the RAA, innit?
(S∧¬P)→(B∧¬B)
S
∴ P — Lionino

No. Here is an RAA:

1. (S & ~P) -> (B & ~B) {1}
2. S {2}
3. ~P {3}
4. B {1,2,3}
5. ~B {1,2,3}
6. ~~P {1,2}

Or if the version of the rule is to go through a conjunction B & ~B instead of B and ~B on separate lines:

1. (S & ~P) -> (B & ~B) {1}
2. S {2}
3. ~P {3}
4. B & ~B {1,2,3}
5. ~~P {1,2}

With the non-intuitionistic form we can have the sentence on the last line be P.

lying is not the same as saying something that is false. — Leontiskos

When someone says a falsehood negligently, especially with the intent to discredit another, that too is a lie. And when someone says a falsehood that they have committed to belief by willful intent, that too is a lie. And when someone has clearly been shown that what they've said is false but continue to say it anyway, that too is a lie and an egregious lie.

And notice that I did not say that Leontiskos lied the first time he made the false claims about me. Rather, I called to his attention that I have said the very opposite of what he claims I've said. But then he continued to make the false claims. At that point I securely said they are lies.

I have been ignoring your posts, and have only read a handful of them. — Leontiskos

But not ignoring them enough to not lie about them.

As Philosophim said:

Not exactly the model of a sage and wise poster. You came on here with a chip on your shoulder to everyone. I gave you a chance to have a good conversation, but I didn't see a change in your attitude.
— Philosophim — Leontiskos

My reply:

Not exactly the model of a sage and wise poster.
— Philosophim

You leave out that I went on to give a proof in two versions. And it is appropriate to ask whether a poster is really serious asking for something that is, as far logic is concerned, as simple as showing that 4 is an even number. If in a thread about number theory someone happened to write "4 is even", and then another said "Prove it", you think that would not be remarkable enough to reply "Are you serious? You don't know how how to prove it?", let alone to then go on to prove it anyway.

You came on here with a chip on your shoulder to everyone.
— Philosophim

Where is here? This thread? I came with no shoulder chip, not to anyone, let alone "everyone". If I permitted myself to do as you do - to posit a false claim about interior states - I would say that you do so from your own umbrage at having been corrected.

And my point stands that I did not insult you, whereupon you insulted me.

I gave you a chance to have a good conversation
— Philosophim

By saying "don't be a troll".

You can converse as you please. I'm not stopping you. And I have read your subsequent posts, even after your insulting "don't be a troll" and have given you even more information and explanation. I have not shut down any conversation. — TonesInDeepFreeze

I don't have time for silly spats and allegations. — Leontiskos

Ah, the time honored tactic of pretending to be above a dispute by perpetuating it. And pointing out that Leontiskos is lying when he says I said the opposite of what I actually said is not silly. Rather it is mighty proper.

If you can't answer simple questions without telling me that I am lying a dozen times then I will just put you back on ignore. — Leontiskos

Time, energy and interest allowing, I answer sincere and coherent questions as best I can.

I answer sincere and coherent questions as best I can. — TonesInDeepFreeze

Then why do I have 13 new replies from you today, 11 of which are in a single thread? You're a spammer and I don't have time for this stupid shit. Get someone else to teach you how a reductio works. Maybe they can also teach you how to interact without spamming. Consider it a rule of life that when you spam people they ignore you. Adios!

Then why do I have 13 new replies from you today, 11 of which are in a single thread? You're a spammer and I don't have time for this stupid shit. Get someone else to teach you how a reductio works. Maybe they can also teach you how to interact without spamming. Adios! — Leontiskos

How predictable of Leontiskos! His hypocrisy is remarkable. Arguably he has posted more than anyone in this thread. A significantly greater number of posts and characters than I have. And he made several posts about my posts and about me during a time when I was not posting in this thread, just as recently made several during a time when he was not posting. He exercised his prerogative that way, and I exercised mine.

A poster is not wrong for catching up to several posts in a thread all at once. How in the world would it be unreasonable for a poster to exercise the prerogative to post and to reply to posts after, for whatever reason, not having posted in a thread during several days?

No one has to confine themselves to Leontiskos's own posting times to reply to him so as to refrain from catching up at some later time.

/

And as to teaching how reductio works, I posted an exact specification how it works, in two formulations. Leontiskos could read that post, or better yet, get an introductory textbook that uses natural deduction, because sure as shootin' he ain't got a clue now, as I showed.

Question: How does reductio work?

Answer: There are two related inference rules:

(1) If P, along with possibly other lines, shows a formula Q and a formula ~Q, then infer ~P and charge it with all the lines used to show Q and to show ~Q except the line for P.

(2) If ~P, along with possibly other lines, shows a formula Q and a formula ~Q, then infer P and charge it with all lines used to show Q and used to show ~Q, except the line for ~P. [not intuitionistic]

Those rules are equivalent with:

(1) If Gu{P} |- Q and Gu{P} |- ~Q, then G |- ~P

(2) If Gu{~P} |- Q and Gu{~P} |- ~Q, then G |- P [not intuitionistic]

You're welcome for that. (Not too very bumptious of me.) — TonesInDeepFreeze

The post you quoted there was before you joined these threads. So there is no connection to you. "We" there simply means "I" — not bumptious of me, the greatly humble person I am.

1. (S & ~P) -> (B & ~B) {1}
2. S {2}
3. ~P {3}
4. B & ~B {1,2,3}
5. ~~P {1,2} — TonesInDeepFreeze

Ok, that is the derivation. The source I quoted at least is correct when abriding it. The RAA however is not how it was being presented in this thread by others before, which is what I was trying to confirm.

With the non-intuitionistic form we can have the sentence on the last line be P. — TonesInDeepFreeze

We are all speaking non-intuitionistically here, which is standard at least in amateur circles.

(1) If Gu{P} |- Q and Gu{P} |- ~Q, then G |- ~P — TonesInDeepFreeze

The bulk of the debate here between Banno and Leontiskos (and me interjecting sometimes) is why say G |- ~P instead ~P |- G.
The debate gets to the point on this post https://thephilosophyforum.com/discussion/comment/918628 by me
then to this https://thephilosophyforum.com/discussion/comment/918657 by Leontiskos
then this https://thephilosophyforum.com/discussion/comment/918724 by me
then he replied with this https://thephilosophyforum.com/discussion/comment/919282 and this post right under https://thephilosophyforum.com/discussion/comment/919292
I did not further reply

I ask that you check those before replying on this specific point, as I don't want to go in circles or pointlessly extend the thread.

I see now. — Lionino

@Count Timothy von Icarus
I still would like some final thoughts on this post specifically.

Thanks for that. I don't mean to belabor this thread, but speaking naturally, I would say this.

A contradiction for logic is like a fork in the road. It forces us to choose one way or another, for we cannot choose both. A reductio ad absurdum is the combination of this fork along with a concrete choice in favor of one side of the fork. "Here is a fork/contradiction in the road, and we will choose this side." The <choice> or <uncharacteristic act of will> is what <separates a direct proof from an indirect proof>.

In a formal sense a reductio in no way determines that we must take one side of the fork rather than the other. Yet the reason a reductio is not usually controversial is because there usually is a set of axioms that both interlocutors are committed to, and a quality reductio will place those axioms in one side of the scale, thus persuading such interlocutors to choose the side of the fork that favors the axioms. I maintain—as I said at the outset—that a reductio involves a <background of plausibility> in order to adjudicate between the two sides of the fork. If there is no background rationale for adjudicating in favor of one side of the fork rather than the other, then the reductio will have no rational force <as a choice between (ρ→~μ) ∨ (μ→~ρ) >.

Do (A implies B) and (A implies notB) contradict each other? — flannel jesus

So what do you think now?

1. (S & ~P) -> (B & ~B) {1}
2. S {2}
3. ~P {3}
4. B & ~B {1,2,3}
5. ~~P {1,2}
— TonesInDeepFreeze

Ok, that is the derivation. The source I quoted at least is correct when abriding it. The RAA however is not how it was being presented in this thread by others before, which is what I was trying to confirm. — Lionino

You asked:

This is the RAA, innit?
(S∧¬P)→(B∧¬B)
S
∴ P — Lionino

So I answered correctly that it is not. And I showed an actual RAA.

Yours is a valid inference, but it is not formulated as RAA.

With the non-intuitionistic form we can have the sentence on the last line be P.
— TonesInDeepFreeze

We are all speaking non-intuitionistically here, which is standard at least in amateur circles. — Lionino

I mention it because the proof itself ends with ~~P. To get P requires additional steps that are not intuitionistic. And I mention, as added information, that they are not intuitionisitc because that is interesting and good to know. I wouldn't always belabor the point, but in this context it is stark that there are two forms: classical and intuitionistic, and in the natural deduction system I presented, we need both to achieve all the classical inferences.

And sometimes people do speak on behalf of intuitionism in this forum, as well as there are likely readers of threads that don't post in them.

(1) If Gu{P} |- Q and Gu{P} |- ~Q, then G |- ~P
— TonesInDeepFreeze

The bulk of the debate here between Banno and Leontiskos (and me interjecting sometimes) is why say G |- ~P instead ~P |- G. — Lionino

Whatever the bulk the debate is about, I presented an exact formulation of the rule a a reference for whomever might want to know exactly what the rule is. And as part of my explanations why certain objections to the rule are off-base.

We don't say: If Gu{P} |- Q and Gu{P} |- ~Q, then ~P |- G.

We don't say that because |- is meant to be equivalent with |=.
And it is not the case that for all G and P, we have:
If Gu{P} |= Q and Gu{P} |= ~Q, then ~P |= G

Formulating a rule: "If Gu{P} |- Q and Gu{P} |- ~Q, then ~P |- G" would be stupid. And, believe it or not, logicians try not to offer stupidities that would thwart the very intent of presenting a formulation.

You're welcome for that. (Not too very bumptious of me.)
— TonesInDeepFreeze

The post you quoted there was before you joined these threads. So there is no connection to you. "We" there simply means "I" — not bumptious of me, the greatly humble person I am. — Lionino

Ugh.

From the post I quoted:

We have established that "A does not imply a contradiction" is not a good reading of ¬(a→b∧¬b). — Lionino

That was from 13 days ago. I entered the thread 19 days ago.

So, "The post you quoted there was before you joined these threads" is false. And my remark "You're welcome for that" is apposite in the timeline:

From 14 days ago, though my comments about the point went further back, a detailed, informative post:

Do you think it is correct to translate this as: when it is not true that A implies a contradiction, we know A is true?
— Lionino

Tones replied that that is not true for all contradictions but for some interpretations.
— Lionino

That's not what I said.

If I recall correctly, you said that "A -> (B & ~B)"* may be translated as "A implies a contradiction". (*Or it might have been a related formula; not crucial since my point pertains to all such examples.)

That is not the case as follows:

(1) The sentence has a sub-sentence that is a contradiction, but the sentence itself does not mention the notion of 'contradiction'.

(2) To say "a contradiction" is to implicitly quantify: "There exists a contradiction such that A implies it". And that quantifies over sentences. If we unpack, we get: "There exists a sentence Q such that Q is a contradiction and A implies it".

A translation of "A -> (B & ~B)" is:

If A, then both B and it is not the case that B.

and not

"A implies a contradiction".

(3) "B & ~B" is a particular contradiction, not just "a contradiction". Even though all contradictions are equivalent, a translation should not throw away the particular sentences that happened to be mentioned.

(4) If we have that A implies B & ~B, then of course, we correctly say "A implies a contradiction". But that is a statement about A, not part of a translation.

"If A implies B & ~B, then A implies a contradiction" is true, but it is a statement about the sentences, not a translation of them. — TonesInDeepFreeze

After that post, you finally understood the point (I had explained it previously) as you wrote:

"If A implies B & ~B, then A implies a contradiction" is true, but it is a statement about the sentences, not a translation of them.
— TonesInDeepFreeze

Yes, granted. I used the word "translation" wrong in basically all of my posts. I meant "is a true statement about..." instead. — Lionino

So, celebrating that information had been understood, I replied:

Thank you for recognizing my point. — TonesInDeepFreeze

Later you wrote:

We have established that "A does not imply a contradiction" is not a good reading of ¬(a→b∧¬b). — Lionino

Then I said, "You're welcome for that". And you are.

Regarding axioms in proofs:

I'll call both of the two forms below 'RAA' (though different writers label them in different ways):

(1) If Gu{P} |- Q and Gu{P} |- ~Q, then G |- ~P

(2) If Gu{~P} |- Q and Gu{~P} |- ~Q, then G |- P [not intuitionistic]

In a natural deduction proof, any formula can be entered on a line and charged with that line number. It is not required that the formula be a member of a given axiom set. But some lines can be "discharged" so that even though the line was used, it is no longer counted on as being required for the inference. That is the essence of natural deduction. For example, an RAA:

(1) P -> (Q & ~ Q) {1}
(2) P {2}
(3) Q & ~Q {1,2}
(4) ~P {1}

Line (2) was discharged at line (4).

{1} in line (4) is the set of formulas that are charged to the conclusion ~P. So, proving ~P in this case depends only on line (1) and not on line (2). Line (2) was discharged.

And it is well understood that this also is correct:

(1) P -> (Q & ~ Q) {1}
(2) P {2}
(3) Q & ~Q {1,2}
(4) ~(P -> (Q & ~ Q)) {2}

Line (1) was discharged at line (4).

{2} in line (4) is the set of formulas that are charged to the conclusion ~P. So, proving ~P in this case depends only on line (2) and not on line (1). Line (1) was discharged.

If we want only inferences from a given set of axioms, then each member of the set of formulas that are charged to the conclusion of an argument must be a member of that set of axioms. But the discharged formulas do not have to be members of that set of axioms.

Of course, having (1) as an axiom and (2) as not is different from having (2) as an axiom and (1) as not. Of course, it is optional which we choose to work with.

And of course, one is free to choose which axioms to work with, or to add to add premises of interest. But the discharged lines are not counted in the "bottom line". And yes, of course, the choices of axioms or added premises are subject to whatever criteria we wish to subject them to. That we have that option is not a fault in RAA. It's not a matter of a fault in RAA but rather it's the obvious fact that we are free to choose whichever axioms or premises we want to choose.

Ugh. — TonesInDeepFreeze

You got it wrong. I know what I meant with my posts. "We" there refers to me, I was not talking about anyone else. The specific post you quoted did not help sort out the issue, specifically the nitpick on "translation", which is why I had to make a whole new thread for that topic specifically. In fact in my thread you corrected yourself about something midway through the discussion:

I'm dumping this: — TonesInDeepFreeze

But feel free to take credit for whatever you want in your mind, it doesn't bother me.

We don't say: If Gu{P} |- Q and Gu{P} |- ~Q, then ~P |- G. — TonesInDeepFreeze

I made a mistake. I meant to say:

"The bulk of the debate here between Banno and Leontiskos (and me interjecting sometimes) is why say G |- ~P instead of P |- ~G."

That is something that Banno expresses here:

Indeed, the "problem" is not with reduction, but with and-elimination. And-elimination has this form
ρ^μ ⊢ρ, or ρ^μ ⊢μ. We can choose which inference to use, but both are quite valid.

We can write RAA as inferring an and-sentence, a conjunct:

ρ,μ ⊢φ^~φ⊢ (ρ→~μ) ^ (μ→~ρ)

(ρ^μ) →φ^~φ⊢ (ρ→~μ) ^ (μ→~ρ)
(fixed error)

...and see that the choice is not in the reductio but in choosing between the conjuncts. — Banno

It has happened before in the history of science where we had to reject G when finding out that Gu{P} is contradictory, because P was so evidently true.

In a formal sense a reductio in no way determines that we must take one side of the fork rather than the other. Yet the reason a reductio is not usually controversial is because there usually is a set of axioms that both interlocutors are committed to, and a quality reductio will place those axioms in one side of the scale, thus persuading such interlocutors to choose the side of the fork that favors the axioms. I maintain—as I said at the outset—that a reductio involves a <background of plausibility> in order to adjudicate between the two sides of the fork. If there is no background rationale for adjudicating in favor of one side of the fork rather than the other, then the reductio will have no rational force <as a choice between (ρ→~μ) ∨ (μ→~ρ) >. — Leontiskos

Ok. That is much clearer than your other posts. I suppose I agree with what is conveyed. However, the RAA has formally either rho or mu as a premise, so no choice between the conjunct is needed within the RAA, the RAA is logical.