Talk:Rule of inference

glaring omission

One glaring omission is not to mention derived rules of inference, that some rules of inference can be deduced giving others. An example at least should be given, and mention made that there are some minimal sets of rules of inference that can be used to derive the rest. This may form another article later on.

• I did this (a while ago) Brighterorange 22:03, 25 Apr 2005 (UTC)

I take issue with the following statement: "If the premise set is empty, then the conclusion is said to be a theorem or axiom of the logic." An axiom for sure, but a theorem? Those two are opposites. A theorem requires reasoning and therefore qualifies as having a premise. --69.1.21.106 11:33, 22 January 2007 (UTC)

It is standard to say that theorems of a theory T are derivable from the empty set "with respect to (the axioms of) T". Specifically, the derivation relation is generally relativized to a system, so that if ⊢_T denotes derivability in T, then if A is a theorem of T, it is written ⊢_T P to mean that P is derivable in T from the empty set. If we take derivation in a more abstract form, then usually we write T ⊢ A to mean that A is derivable solely from the theory T, where T may be the axioms of classical logic, and ⊢ some abstract derivation relation. Nortexoid 17:36, 22 January 2007 (UTC)

missing links?

• Shouldn't this article point to Inference engine, somehow ? --Jerome Potts (talk) 14:46, 13 March 2009 (UTC)

Restored lede

I restored the _correct_ definition of rule of inference; until/unless a page reference is provided in the Quine source, I'm not buying that this supports the non-standard characterization of a rule of inference as a 'logical truth'. 67.118.103.210 (talk) 23:05, 15 January 2010 (UTC)

I would also like to be able to consult the reference

Philosophy of Logic, [[Willard Van Orman Quine|W.V.O. Quine

with a page number, to see what Quine actually says. However, it seems somewhat odd to say that a rule of "inference" is a "law of logic" when a rule of inference might say

From the string "♥♥" infer the string "♣♣♣"

That is a perfectly good rule of inference, and might even be valid depending on the semantics assigned, but it is unlikely to be a law of logic. The point is that Quine is speaking in some context, and I can't assess the statement here without looking up what that context is. — Carl (CBM · talk) 16:08, 21 January 2010 (UTC)

This is ridiculous. If you don't understand this then you shouldn't be editing anything in the field of logic at all. First of all the statement stands alone without any context needed from Quine to make anything clear. If you were sufficiently familiar with the various ways in which people use and study rules of inference, then there wouldn't be a question about it. For instance....yes one could say "From the string '♥♥' infer the string '♣♣♣' " However invariably when this is done appropriately what is meant is that one can derive '♣♣♣' from '♥♥' not "infer" it. To say that you are inferring when you are deriving needs to be made explicit in the rules. Second of all, when you are saying that you can validly infer '♣♣♣' from '♥♥' what you are saying is that there is some logical truth which justifies this move. Your believe that your formulation is "the correct" one and mine is not is based on your limited experience. Defining a rule of inference as a function belongs in the last paragraph of the lede. It is not the most generally applicable way to start a discussion about a rule of inference. This is also a classic case of "mathematosis." If that statement is removed again, I will report a vandalism. At some point in the future I may add the page number, but not before you have a chance to read the whole chapter on "logical truth" yourself.Furthermore you don't seem to know what "non-standard" means. You need it. Be well and loosen your grip there Emil. Pontiff Greg Bard (talk) 18:12, 21 January 2010 (UTC)

Revert

Was your revert of the rule of inference article based on your evaluation of the content or the process? I presume you read what you reverted. Is it your belief that its not the case that "Every valid rule of inference is put forward as a logical truth and every logical truth can serve as a valid rule of inference" as supported by the leading expert on the subject? I am quite puzzled by this behavior.Pontiff Greg Bard (talk) 19:55, 21 January 2010 (UTC)

As you are well aware, the place to discuss the content of an article is on that article's talk page. Algebraist 19:59, 21 January 2010 (UTC)

I thought I might engage you civilly about your actions on your talk page. So why don't you go ahead and explain here please.Pontiff Greg Bard (talk) 21:04, 21 January 2010 (UTC)

I reverted your edit because I was unable to make any sense of it, and it seems that several other people have had similar problems, which you have yet to resolve. I was also unable to find any reference to rules of inference in the relevant chapter of Quine's work (admittedly via the imperfect medium of Google Books). Where precisely should we be looking? Algebraist 21:10, 21 January 2010 (UTC)

"I was unable to make any sense of it": In such a case, the proper reaction is to ask for an explanation and reword the article, rather than presuming that it is confusing because it is wrong. It would be helpful if you explained exactly what you find confusing about the statement. Paradoctor (talk) 22:57, 21 January 2010 (UTC)

take a look at this Pontiff Greg Bard (talk) 22:03, 21 January 2010 (UTC)

As the statement is under dispute, quoting the relevant passage(s) would be helpful here. Paradoctor (talk) 22:57, 21 January 2010 (UTC)

Well, the book has the literal text that Gregbard added, but with "principle of inference" instead of "rule of inference". But the context of the quote there is important. Ayer is not talking about rules of inference in general; he is talking about Principia Mathematica (the book was apparently first published in 1936). So what Ayers is actually saying is that in Principia, every rule of inference is a logical truth and vice versa. And that's reasonable enough; I think most people today think that the deduction rules of first-order logic are "logical truths".

However, the Ayers quote is not referring to arbitrary formal systems, as the first paragraph of the lede of this article does. Not only would the idea of an arbitrary formal system would have been quite novel when the book was written, but Ayers actually says on the same page

"And the system of Russell and Whitehead itself is probably only one of many possible logics, each of which is composed of tautologies as interesting to the logician as the arbitrarily selected Aristotelean "laws of thought".

The fact that Ayers says "probably" shows the age of the reference. But the main point here is that Ayers does not claim that the tautologies of all those other (possible) logics are also "laws of logic".

It would be worth pointing out somewhere on the article the relationship between valid implications and admissible rules. But the location of the text currently is misleading because Ayers is not referring to arbitrary formal systems. Moreover, there are formal systems in which propositions such as "x = y" are valid, but "x = y" is certainly not a law of logic. — Carl (CBM · talk) 23:46, 21 January 2010 (UTC)

Carl, as I pointed out on your talk page... even non-classical logics do not set out to be nonsense. They set out to be valid systems of logic which are different than the standard, classical etcetera.What you are failing to realize is that when you give the example of a formal system in which 'x = y' is valid, but 'x = y' is 'certainly not a law of logic' it is only within the standard, classical logic we all reason in normally that it is 'certainly not a law of logic'. The system you describe in which "x=y" is valid is telling us that according to it "x=y" is a logical truth. Even the system with only squares and triangles communicates logical truths in the same way. It's just a different way of expressing it. Pontiff Greg Bard (talk) 00:12, 22 January 2010 (UTC)

But when people use the phrase "law of logic" they are not referring to random non-standard formal systems. What they mean by "law" is something that is holds in the real world. I have also seen people use "Law of Logic" for something that is true by virtue of its form alone - and "x = y" is not true by virtue of form alone even if it is a valid inference rule. However, I have never seen a text that uses terms like "law of logic" while simultaneously considering arbitrary formal systems that are not just predicate logic and its usual semantics. — Carl (CBM · talk) 03:16, 22 January 2010 (UTC)

For another example, Quine writes in "Philosophy of logic" p. 15 [1] that the law of the excluded middle is a law of logic. But the law of the excluded middle is not a valid inference rule in intuitionistic predicate calculus. — Carl (CBM · talk) 03:16, 22 January 2010 (UTC)

Carl, please let me point out that people throw around the term "law of logic" not very carefully at times. When you say "...'x = y' is not true by virtue of form alone even if it is a valid inference rule." you are again slipping back into our everyday real world logic while talking about a separate system in which "x=y" is a valid logical schema. Within that system YES "x=y" is true by virtue of form alone. In intuitionistic predicate calculus, (a non-classical logic) the so-called "law of the excluded middle" is not a "law of logic" at all. That's why it's not a valid rule of inference. People only call it "the law of the excluded middle" with respect to classical/traditional logic. Again, the goal of a non-classical logic is set forth a different way to derive (what that say are) logical truths. It is not about a difference in what is logical and extra-logical. It is a change in the very set of logical truths. I'm sorry Carl, but the truth remains without counterexample. Every valid rule of inference is put forward as a logical truth and every logical truth can serve as a rule of inference. Do I need to construct some out of squares and triangles so as to demonstrate? Pontiff Greg Bard (talk) 04:13, 22 January 2010 (UTC)

"By form alone" means "syntactically", and "x = y" is never valid because of its syntax. The only way to make it valid in a variant of first order logic is to change the semantics. But the sentence will still not be true by form alone there. — Carl (CBM · talk) 04:21, 22 January 2010 (UTC)

The formal language FLX=Y:

Alphabet: {'x', '=', 'y'}

Formation rule: {"Any string of one or more 'x's followed by an '=' followed by a string of one or more 'y's is a valid formula of FLX=Y."}

At this point it should be clear that YES, "x=y" is valid because of its syntax, syntax that is, that I assigned. There is nothing special or inherent to the universe that says that the syntax of language requires "x=y" to not be valid.Greg Bard (talk) 23:14, 22 January 2010 (UTC)

You have missed my point, but when I tried to edit the text I realized there are more fundamental problems, which I explain in the next section. — Carl (CBM · talk) 23:27, 22 January 2010 (UTC)

I haven't addressed those issues below yet. You think I have missed the point, and I also think I have missed a point I am making. I have just presented a counterexample to your claim, and as it stands you have not presented any valid counterexample to my claim. I will address the below issues below. I think we can actually achieve some mutually satisfactory formulation if we work together. The concept of a rule of inference is intimately tied to the concept of logical truth, so some account of it should be made. Stay cool Carl. Greg Bard (talk) 23:40, 22 January 2010 (UTC)

removed again

Actually, when I went to edit the sentence to clarify things, I realized it is worse than I thought. Now:

1. A logical truth of a formal system, according to our article, is a formula in the formal language of the formal system.
2. A rule of inference is not a formula. It is a transformation rule.

So when the sentence says,

"Every valid rule of inference is put forward as a logical truth and every logical truth can serve as a valid rule of inference."

this is bizarre. A formula cannot "serve" as a rule of inference. It's possible to decode what Ayers means, but (1) the sentence I removed doesn't do so and (2) what he means only applies to a certain class of formal systems.

What Ayers seems to mean is that, for systems that satisfy the deduction theorem, the rule of inference $A\vdash B$ corresponds to the valid formula $A\to B$. However, there are systems which do not satisfy the deduction theorem, and in such a system it seems that rules of inference do not correspond to valid formulas. This does not make Ayers wrong; he is only talking about Principia Mathematica, and most likely that system does satisfy the deduction theorem. — Carl (CBM · talk) 04:34, 22 January 2010 (UTC)

Indeed. And what's worse, the sentence is even more bizarre if we for the sake of argument allow the concept of logical truth to apply to metastatements about the logic more general than its valid formulas. Let me give an example. Let's suppose that the logic we are talking about is the intuitionistic logic, and consider these two statements:

1. If $A\land B$ is valid, then A is valid.
2. If $A\lor B$ is valid, then A is valid or B is valid.

Both are true principles of this logic. The first one expresses the rule $A\land B/A$, whereas the second one cannot be expressed by any set of rules (in the usual, single-conclusion sense used in this article). However, there is no sensible way of defining "logical truth" which would make the first one logically true, and the second one not, other than artificially declaring that a logical truth must have the syntactic form of an inference rule, in which case the sentence becomes a pointless tautology. — Emil J. 11:21, 22 January 2010 (UTC)

That's a nice example. This is exactly why we need to pay attention to things such as: (1) what exact definition is a particular author using for "logical truth" and (2) what context are they speaking in when we quote them? Taking single sentences from different books will just lead us to contradictions. — Carl (CBM · talk) 12:20, 22 January 2010 (UTC)

Why exactly do you believe that a rule of inference is not a formula? It is a formula of some metalanguage. Both rules of inference and formulas are concepts. What form they take when we inscribe or utter them is irrelevant to the issue. We are perfectly well able to say that a formula can "serve" as a rule of inference. I find the belief to the contrary to be very strange?! You find it bizarre? This is to say that you do not understand that a logical truth can serve as a rule of inference? Really?

← Moved from inside my comment above. — Carl (CBM · talk) 00:06, 23 January 2010 (UTC)

It is not clear AT ALL that what Ayers means only applies to a certain class of formal systems. That would be highly uncharacteristic given the task that philosophical logicians set out to do (i.e. identify the most general truths, remove presuppositions, etcetera). I am very cognizant of the fact that different authors may use terminology specific to their own literature. There still is no reason to believe that Ayers intends anything other than the most general statement (i.e. the face value of the statement in question), furthermore I have seen no evidence of anything resembling a counterexample. If there are clarifications to be made, I would like to know about it, and come to a formulation. However I haven't seen any justification for rejecting this well supported statement. Greg Bard (talk) 00:02, 23 January 2010 (UTC)

What Ayers is saying is not that an inference rule is a valid statement of some metalanguage; he is saying that each valid inference rule corresponds to a valid formula of the original object language. I was going to clarify how this correspondence would go, at which point I realized that it does not always happen. However, it you want to think of logical truths in the metalanguage, EmilJ's example shows a logial truth in the metalanguage that does not correspond to any rule of inference. — Carl (CBM · talk) 00:06, 23 January 2010 (UTC)

Logical truth

"In classical orthodox logic, every valid rule of inference is put forward as a logical truth and every logical truth can serve as a valid rule of inference."

Folks, this statement is supported by a reliable source. There is no reason to believe that Ayer intended anything other than the prima facie meaning of it. Furthermore, all the "flying by the seat of the pants" being done by people who insist, insist, insist, that they know there is a problem, but cannot articulate what it is in a way which can address the problem. Even furthermore, it appears to me, that the people who think they know what they are doing have demonstrated at least some confusion to me. Carl, I thought we had reached a consensus between at least us two before Greathouse intervened appealing to your concern (and without articulating his own concern, but rather substituting your conclusion for his own which I consider to be political quite franky). Greathouse, if you can show me that you understand the concerns being addressed, then I apologize, however it appears to be another raw political move otherwise. Isn't it great having numbers? You don't even have to think for yourself. Please offer an alternative formulation which will satisfy you. If you can't or won't, I'm going to feel as though its not good faith collaboration anymore.

Carl, you are concerned about different authors having different definitions. This tells me directly that you do not understand (with much respect). Carl, a set theorist has a different definition of logical truth than a model theorist, than someone using propositional logic, than someone using predicate logic. The whole point is that what all of these people are doing is coming up with their own formulation or account of logical truth. The set theorist defines it in terms of sets, the model theorist defines it in terms of models, etcetera. Think about it. If this wasn't the case, then why would anyone ever care what mathematicians think in the first place. They have to be logical and they have to be attempting to express truths. Otherwise they are all artists. (and we know mathematicians aren't artists because editing Wikipedia is an art).

Your "counterexample" involving a metalanguage is irrelevant because we aren't talking about the metalanguage in its capacity as a "classical logic" (if indeed it is a classical logic in a particular case --like I said it doesn't matter) and therefore not a counterexample to classical orthodox logic. We are talking about an object language, and we are perfectly well able to say for sure that

"In (any given particular object language we are studying which is a) classical orthodox logic, every valid rule of inference is put forward as a logical truth and every logical truth can serve as a valid rule of inference." However, we sure don't say all the time that we are talking about an object language because it's part of the definition of an object language that it's the thing we are talking about.

So can someone other than myself formulate satisfactorily the relationship between a logical truth and a rule of inference? If you think it's not important, then I would respectfully say you don't know what you are talking about. If this aspect remains out, for long I will certainly be reinserting it again with the understanding that everyone has had every opportunity to formulate things for them-self.Greg Bard (talk) 22:04, 14 February 2010 (UTC)

Greg, I'm not surprised that you attack me and fail to WP:AGF. I'm thick-skinned, though, so no hard feelings. The only alternative formulation that would satisfy me, at the moment, is nothing -- the present state of the article. Perhaps you will convince me that there is need for such an addition, but you have not so far.

I find the counterexamples suggested sufficient, though I was convinced by my own counterexamples which came to mind quite readily. I would suggest that you do not understand the points raised, and it's certain that you lack consensus.

The best reason for not including this line is that it's not true. While (a certain interpretation of) it holds in PM, it fails in many -- even most -- modern system of classical logic. At best the comment would have a place in a subsection of that article; at worst, nowhere. The idea that an 80-year-old comment on a quite-outdated logical system should go in the lede of an article like this is risible. And even in PM, the statement is not literally true (since a transformation is a different type from a wff), though it can be salvaged:

In the classical orthodox logic of Principia Mathematica, every valid rule of inference is equivalent to a class of logical truths and every logical truth can be transformed into a valid rule of inference.

But even this specific and convoluted form fails to inform the reader of what a rule of inference is, and as such is inappropriate for the lede.

CRGreathouse (t | c) 23:55, 14 February 2010 (UTC)

I appreciate your thick skin, and I have appreciated you Greathouse for a long time (I think I have told you at least once before that I like your work on elective systems). I do not appreciate being characterized as attacking, much less your "not being surprised." I can't refrain from stating for the record that I am, in fact, AGF otherwise I wouldn't be soliciting your input sincerely. Your statement of negative expectations, however is a failure of AGF, and I think that is regrettable, because I do otherwise respect your contributions. I too will try not to harbor hard feelings against you. Let's work together on a formulation shall we? Respectfully, your statement that the "only alternative formulation that would satisfy me, at the moment, is nothing" is not good faith collaboration. If you are just supporting people you find credible, rather than actually understand the issue yourself, then that is basically a political action and not a situation that I can redress reasonably with you, now is it? Up until now you hadn't offered any evidence of understanding why anyone is reverting this fundamental aspect from the article.

Now that you have give me something which can be used constructively... Principia Mathematica is not classical/traditional/othodox logic. I am talking about what regular people used to reason (you know --the audience of the article), most of which hasn't changed since Aristotle. I am a little bit taken aback by the non-recognition of logical truth as appropriate and important to elucidate in the lede. To me it is very much a case that if you don't understand that logical truth is fundamental to the concept of a rule of inference then you really do not understand what a rule of inference is, much less a valid rule of inference. I do greatly appreciate your reformulation. Thank you for that. I would reformulate to: "In classical orthodox logic every valid rule of inference is equivalent to a particular set of logical truths and every logical truth can be transformed into a valid rule of inference." Be well and stay cool Ghouse.Greg Bard (talk) 00:56, 15 February 2010 (UTC)

Respectfully, your statement that the "only alternative formulation that would satisfy me, at the moment, is nothing" is not good faith collaboration.

I'mn sorry you feel that way. It is extremely common in Wikipedia that the best thing to do with a statement is to remove it. Sometimes articles have been improved by removing a statement I have written, and I fully support such removals. I think this is another such case.

If you are just supporting people you find credible, rather than actually understand the issue yourself

You have accused me of doing this, and I have no idea why. I read the original source and drew my own conclusions. I don't know any of the other editors involved.

Now that you have give me something which can be used constructively... Principia Mathematica is not classical/traditional/othodox logic. I am talking about what regular people used to reason (you know --the audience of the article), most of which hasn't changed since Aristotle.

Ah. In that case, the problem is that your information is unsourced, since Ayer was speaking only of the PM. If you will find a source backing this statement outside PM I will reconsider my viewpoint. I am bothered less by the fact that your statement is unsourced than other editors might be, but I am extremely concerned about its loose formulation. I would be happier putting in a more precise statement, or failing that putting in an informal statement with a reference providing formalisms.

CRGreathouse (t | c) 01:12, 15 February 2010 (UTC)

Although Ayer refers to PM in previous pages, there is no reason to believe he means anything other than a general statement which is the prima facie reading. Whereas yours (and the others) reading actually consists in "reading in" meaning which he does not necessarily intend. I would certainly favor the solution you propose (i.e. some informal statement concerning the connection between a rule of inference and a logical truth.) The way I see it, I have provided a reliable source with an apparently canonical account. At some point all the "flying by the seat of the pants" by self-appointed experts needs to be replaced by some reliable source to the contrary, otherwise its all just POV. Be well, Greg Bard (talk) 02:04, 15 February 2010 (UTC)

A couple points: (1) I have not edited this article since Jan. 23, so I am not sure why the top post in this section is addressed to me.

(2) Regarding the Ayer reference: Gregbard said above, "Although Ayer refers to PM in previous pages,...". Ayer actually refers to PM in the same paragraph from which the material under discussion is sourced. That's why I'm confident Ayers was talking about PM in the quoted material. Moreover, the fact that Ayer is discussing PM in the first place is indicative of the age of the source: it's from 1936. I don't think that there was any well-developed semantics for any non-classical logic at that time.

As I said in a previous section, I tried to edit the material to make it more clear (back in January) but I stopped when I realized it was impossible. The main problem with the reformulated version is that I have no idea what "orthodox logic" is.

I think that this would be better handled in a section on soundness of inference rules. Really, the thing that the material under discussion is getting at is somewhat circular: "logical truth" and "valid" both come down to "true in every model". — Carl (CBM · talk) 04:13, 15 February 2010 (UTC)

Looks like it's long past time for a User Conduct RFC 71.139.28.90 (talk) 05:17, 15 February 2010 (UTC)

May I respectfully suggest that everybody WP:CALM down a little instead? You're all experienced and valuable contributors, and it pains me watching you slide slowly towards the inner circles of hell like this. Paradoctor (talk) 10:54, 15 February 2010 (UTC)

Paradoctor, IP -- I have no dispute with Greg, we're just discussing content. I think we've both backed off our most annoying claims of the other (sorry there, Greg!) so things are looking better and better, IMO. Although perhaps a wider perspective would be useful -- per'aps we should invite the relevant WikiProjects to have their interested members comment here?

CRGreathouse (t | c) 13:44, 15 February 2010 (UTC)

I suspect that Hans is harassing me anonymously, as he has been known to use opportunities like this to attack me. Greathouse and I are collaborating wonderfully as far as I am concerned. My problem at the time was confirming that I wasn't dealing with non-political/non-ideological activity and he satisfied that by actually discussing the content. I apologized in advance for asking him to. This anonymous harassment by 71.139.28.90, however is completely unconnected to any content issue and is the type of political behavior that I was concerned about.

I propose to include a more broad and general statement that we can all live with such as:

"The concept of a rule of inference is very closely connected to the concept of logical truth. Usually when a logical system is constructed, it is constructed so that every rule of inference is equivalent to a logical truth and every logical truth of the system can be transformed into a rule of inference consistent with the others."

Now I am cognizant of the point Carl made about circularity, and it is an interesting observation about the nature of logical truth and r.o.i. however unless we get a very good formulation, it may be too abstract an aspect to get into in detail in the lede. Yes Carl, they both amount to being true in every model, and Quine talks about expressing logical truth in terms of models also. However, models appeal to the concept of "truth" by definition, and so therefore we do not get away from defining logical truth in terms without "truth". We are able to define logical truth (as well as truth) in terms of satisfaction, however that does not avoid circularity either. What does avoid the circularity is defining it in terms of derivability which does not appeal to truth... and that is also why it is important to understand that a theorem should primarily be understood as derived, and not neccessarily as "truth".Greg Bard (talk) 16:59, 15 February 2010 (UTC)

Greg, would you give me an example of what you're suggesting? That is, for some reasonable system, the conversion of a rule of inference to a logical truth and the conversion of a different logical truth to a rule of inference?

In classical propositional logic, what rule of inference is equivalent to the logical truth (((((φ → ψ) → (¬ χ → ¬ θ)) → χ) → τ) → ((τ → φ) → (θ → φ))) (Merideth's axiom)?

In sequent calculus, what logical truth is equivalent to (WR)?

This may help me better understand your position.

CRGreathouse (t | c) 15:12, 16 February 2010 (UTC)

It seemed to me that the claim was really just a restatement of the deduction theorem, for systems that support it. The Ayer reference was written in 1936, so it is unlikely that it would have considered the sequent calculus, which was very new at the time. — Carl (CBM · talk) 15:32, 16 February 2010 (UTC)

The logical truth (((((φ → ψ) → (¬χ → ¬θ)) → χ) → τ) → ((τ → φ) → (θ → φ))) is equivalent to the rule / (((((φ → ψ) → (¬χ → ¬θ)) → χ) → τ) → ((τ → φ) → (θ → φ))) with 0 premises, and the same strategy obviously works for any valid formula. The opposite direction (how to make logical truths out of general rules) is the problem, and indeed relies on the deduction theorem as Carl says.—Emil J. 15:44, 16 February 2010 (UTC)

Carl, if I haven't thanked you for your patience recently...my goodness thank you for always being the mature adult genius in the room. To answer your question...

If a classical propositional logic has

"(((((φ → ψ) → (¬ χ → ¬ θ)) → χ) → τ) → ((τ → φ) → (θ → φ)))"

as a theorem then it also may have

"If you have '((((φ → ψ) → (¬ χ → ¬ θ)) → χ) → τ )' written on a line of a proof, then you can write '((τ → φ) → (θ → φ))' on a line by itself in the proof." as a rule of inference.

This is to say that that '((τ → φ) → (θ → φ))' is the name of a theorem of the system.

It still seems to me that the formulation beginning "In classical logic..." is perfectly adequate to the task here. If you are talking about systems where the deduction theorem doesn't apply, you are no long talking about anything classical or orthodox. "Orthodox" wasn't intended as the title of some logic Carl, it's just an adjective. We should adequately account for "orthodox" logic before we get buried under a heap of convoluted, contrived, constructions, and exceptions that the vast vast vast majority of readers do not care the least bit about. Greg Bard (talk) 19:32, 16 February 2010 (UTC)

I don't see how that rule generalizes at all, Greg. You just replaced an implication with a turnstile. But what about truths without top-level implication? Carl (below) brings up the example of ω-logic, but what about simple things like $\neg a\vee \neg \neg a$ and $\neg a\vee a$?

And supposing that we can find some way to represent all of these, it's not clear (to me) that this is interesting enough to warrant mention in the article, let alone crucial enough to discuss in the lede.

CRGreathouse (t | c) 23:06, 16 February 2010 (UTC)

I just cut (among other things) this from the lede:

Axiom schemata can also be viewed as rules of inference with zero premises.

It strikes me that this is EmilJ's take on the truth => rule direction: that an axiom can become the rule "Given nothing, you can conclude {truth}.". This certainly shows one way of understanding (one direction of) Ayer's statement. But it seems as uninteresting to say "Given A, we can use ' ⊢ A' as a rule" as to say "Given A, we can use 'A ⊢ ' as a rule". Both are valid, and neither says anything deep about rules of inference.

CRGreathouse (t | c) 23:20, 16 February 2010 (UTC)

Greathouse, with respect, there are several important issues you have brought into sharp relief. Unfortunately, not all of them are about the content but rather your approach. If you do not see as a direct result of your education and experience that logical truth is fundamental to this topic (and many other topics in logic as well I should say!) then you have a different experience and education than I do --not a superior one. "In philosophical logic" (a phrase used almost exclusively by mathematicians) logical truth is the fundamental concept and everything in logic can been seen as some account of logical truth. So, the question becomes, do you see "philosophical logic" as an equal stakeholder to mathematical logic. If you do, well then you can just take my word as representing the appropriate content from with "philosophical logic" and the content takes its place alongside the mathematical content with "no hard feelings." On the other hand if you feel that all of this is an intrusion, well then I can't really reason with you towards seeing what is and is not appropriate. I would have to address the disposition, and not the content (hypothetically speaking of course. I'm sure you want to be a respectful interdisciplinary contributor right?).

As for my example.... you asked for an equivalent, and I provided it. I could have written it out long-hand as:

"If you have a '(' followed by another '(' followed by another '(' followed by another '(' followed by a 'φ' followed by a '→' ... written on a line of a proof, then you can write '(' followed by another '(' followed by a 'τ' ... on a line by itself in the proof." as a rule of inference.

And as for your last observation consistent with EmilJ example... I understand that it appears not to be a deep or useful observation to you. However, the fact that logical truth amounts to nothing more than the grammar of the language, and that grammar of a language determines logical truth is actually quite a deep observation about logical truth. What is "deep" is that there is nothing magically embedded into the fabric of the universe that says that X is a logical truth, but rather it depends on the rules of language. Whereas, the general impression of the average person is probably the opposite, that a "logical truth" is very solidly part of the universe etcetera.Greg Bard (talk) 23:50, 16 February 2010 (UTC)

Greg Bard, you have put words into my mouth! I have never claimed that logical truth is unimportant to this article, but rather that the concept of replacing a statement A with the transformation rule ' ⊢ A' is unimportant (to this article, at least).

And you still have not explained

1. How to express truths not containing the symbol '→' as rules of inference

2. Why being able to do this matters enough to include it in this article

3. Why this transformation is so central to the article Rules of inference as to be included in its lede

I am personally curious about the first -- it may help me understand the others. But frankly the others are more germane here.

CRGreathouse (t | c) 00:13, 17 February 2010 (UTC)

Okay I am not intending to put words in your mouth, and it seems you are saying the exact same thing that I am saying that you are saying again. Secondly, you are putting words in my mouth if you are saying that I am saying either (2) or (3). Those are questions that you guys are asking --not me.

In answer to your first question, you have to remember that both "logical truths" and "rules of inference" are ideas, not physical objects. When you write down either you are creating a token instance of a concept. The string of characters you use are the name of the concept. Both the rule of inference and the logical truth which is equivalent to it are literally equivalent. It is only the token instances that are in need of transformation. The matter of fact in the world that corresponds to tertium non datur (i.e. the idea that a statement is either true or false) is an idea. One name of that idea is "(pV~p)", another name of that idea is "If you have "p" on a line of a proof by itself, than you are prohibited from writing "~p" on a line by itself," and another name is "tertium non datur." I don't know why you would think things aren't going well as your edit summary suggests. I also do not see the problem with the latest formulation "...closely connected..." etcetera. As for why its important, I have already provided several reasons which are more than sufficient. At some point it has to become a matter of responsibility over one's own reflectiveness. Greg Bard (talk) 02:10, 17 February 2010 (UTC)

I'm certainly not saying that you're saying (2) or (3). I've asked you to speak to those points but I don't believe you have.

I'm vaguely insulted that you think that I don't understand that truths and rules are ideas, or that the strings representing them are names. I don't think you intended insult, but I also have trouble imagining you imagining me not understanding those concepts.

You write

Both the rule of inference and the logical truth which is equivalent to it are literally equivalent.

but this is not true, at least in your formulation. See for example [2]. You also write

One name of that idea is "(pV~p)", another name of that idea is "If you have "p" on a line of a proof by itself, than you are prohibited from writing "~p" on a line by itself," and another name is "tertium non datur."

and this is also wrong. Tertium non datur says that at least one of p and not-p must be true; it does not forbid both from being true. (That's the Law of Noncontradiction.) This is a baffling sort of mistake to me -- the distinction is important in a wide arrays of logics I would have assumed you to be familiar with (e.g. the paraconsistent logics). You also write

As for why its important, I have already provided several reasons which are more than sufficient. At some point it has to become a matter of responsibility over one's own reflectiveness.

I do take responsibility for my own reflectiveness. But that doesn't mean I will come to the same conclusions you have!

CRGreathouse (t | c) 02:30, 17 February 2010 (UTC)

Yeah, I only used tertium non datur as an example with no "-->." It was not the right application of that concept, but the principle remains the same. I do not intend to insult. I absolutely DO have a hard time imagining that you do not understand these things... and yet you have deleted the material without reformulating it so as to satisfy yourself...as if you do not understand that you can't have an article about rules of inference without explaining the relationship to logical truth. You guys have come up with a bunch of irrelevant counterexamples (If the formulation is "In classical logic, ...." and you provide no counterexample within classical logic then the "counterexample" is not a counterexample, it's irrelevant) I seem to me that my points have been ignored. I'm sorry GHouse, but I am at a loss, and not for lack of trying. If you can tell me exactly what your problem is with the latest formulation (just calling it contentious doesn't really help at all does it?!) then maybe I can respond. It doesn't seem to me that any problem with it has been identified at all. As I stated before, if your reason is basically that you "just don't see the need" then that is a matter requiring more education on the matter, and I do not intend to insult.

Could you acknowledge for me that you do see philosophy and mathematics as equal stakeholders in this article, because I am inclined to believe this to be the origin of the problems. Greg Bard (talk) 03:42, 17 February 2010 (UTC)

I have explained by position ad naseum (and I imagine you feel the same). None of your changes have addressed my fundamental issues: the point is not well-defined, not correct in its straightforward interpretation, not notable, and not central enough to the topic at hand to be in the lede. (Logical truth *may* just possibly be germane, Logical truth probably isn't, and the logical truth <=> rule of inference transformation is almost surely not.) I have gone over each of these in a good amount of detail -- you're not doing yourself credit by denying that.

As I stated before, if your reason is basically that you "just don't see the need" then that is a matter requiring more education on the matter, and I do not intend to insult.

You do insult. By saying this you assume that I have not considered or do not understand the matter at hand, and that's an insult not just to my education but to the effort I have put into discussing the matter with you. This is a pattern I have noticed with your comments on Talk, in many places beside here: you claim that others are not knowledgeable about the topic at hand. Was the article discussed Solution of the Poincaré conjecture (which I have edited without a strong understanding of the underlying topic) I would simply acknowledge my lack of knowledge; but here I am well familiar with the topic and its surrounding issues.

But I will answer your question here:

Could you acknowledge for me that you do see philosophy and mathematics as equal stakeholders in this article

First, I find the question unusual: as mathematics is merely a (large and important) branch of philosophy, philosophy is always a stakeholder in math articles. In the particular case of this article I have been thinking of it as primarily a philosophy article (though I acknowledge the role of math in it). So I suppose the answer is no: I do not consider the two as equal stakeholders in this article, I feel that it is probably more philosophy than math. Of course if you'd like I could go through the article and get a better feel for all the various parts and how it fits together and give a more thorough answer, but I don't think that's what you wanted.

CRGreathouse (t | c) 03:58, 17 February 2010 (UTC)

That's interesting; I see this article as primarily about symbolic logic and computer science, not particularly about philosophical logic. — Carl (CBM · talk) 04:31, 17 February 2010 (UTC)

I would call computer science a bit far afield myself. No one ever sees anything as philosophical Carl. Some things are not (like "sandwiches"). However there are many topics within mathematics, and almost every topic within mathematical logic is a least in part "about" "philosophical" logic.-GB

I sincerely apologize Greathouse. I don't want to insult you or anyone else. However, I still do hold a sincere belief that if you don't see the relationship of logical truth to rules of inference as a fundamental, defining characteristic, and most generally applicable aspect, then you are missing something important --long carefully considered discussion notwithstanding. If I were a professor and the essay question was about rules of inference, you wouldn't get the question right unless you explained that the idea is to manifest a logical truth.

I don't think philosophy is a stakeholder in every math article (any more than every other subject) however, in logic, philosophy is a stakeholder. Incidentally, the debate about whether or not something is important this way is a bit subjective unless we are going to look at what academics say about it. Please take a look at Quine, "Philosophy of Logic." No one can dispute that he was one of, if not the expert on the subject. I too acknowledge that I have only a B.A. in philosophy, that I am learning too, but that I have a sufficient understanding of things to understand what is and is not notable within a philosophical context. There should be no surprise to see logical truth covered in this article AT ALL, this is also true for the logical connectives, tautology, rules of inference and several other articles. Yet the connection to logical truth has been removed form several of these articles. There is no way that I should be struggling with this issue.Greg Bard (talk) 05:06, 17 February 2010 (UTC)

The question was subjective (and my response was subjective and off-the-cuff), but you asked so I answered. :)

Please take a look at Quine, "Philosophy of Logic."

I've already read it.

CRGreathouse (t | c) 06:12, 17 February 2010 (UTC)

Deduction theorem

Re Gregbard: there are plenty of systems of classical logic in which the deduction theorem fails. That is, there are systems T with sentences A and B, all in classical logic, so that

1. T + A deduces B, and
2. T does not deduce A→B

Such system can even be found in which the language is the language of arithmetic in all finite types, all the inference rules of T are finitary, all the inference rules of T are true in the standard model, and T consists of a theory in first-order logic with a single additional (finitary, classically true) rule of inference. In such a system, (1) corresponds to a rule of inference, but there is no corresponding valid formula because of (2). — Carl (CBM · talk) 04:12, 17 February 2010 (UTC)

If that is a classical logic under a standard interpretation then you have provided a counterexample and I am astonished and puzzled to learn that. However, I have already moved on to a more general formulation which also has been rejected and no reasons have been forthcoming.

"The concept of a rule of inference is very closely connected to the concept of logical truth. Usually when a logical system is constructed, it is constructed so that every rule of inference is equivalent to a logical truth and every logical truth of the system can be transformed into a rule of inference consistent with the others."

It seems to me that this avoids the problem altogether and adequately covers the connection to logical truth.Greg Bard (talk) 05:06, 17 February 2010 (UTC)

This version, if true, is still sufficiently mealymouthed that I don't see any value to including it. And I still have concerns about the translation of truths to rules. My example above was intentional: if you consider $p\vee \neg p$ and

If you have "p" on a line of a proof by itself, than you are prohibited from writing "~p" on a line by itself

to be the same (for the purpose of converting rules of inference and logical truths), then how will you properly distinguish $\neg a\vee \neg \neg a$ and $\neg a\vee a$? And what about the rewriting systems you are so fond of using as examples, where it's not clear that any such translation is possible?

Really, Greg, this has gone on long enough. The statement wasn't a big deal in Ayer's day, and the developments in logic since that time have rendered it quite obsolete. In fact I would hazard to guess that, other than for weak systems, Goedel's theorem will cause real problems with any such bold mixings of language and metalanguage.

CRGreathouse (t | c) 06:12, 17 February 2010 (UTC)

Um yeah, it's gone on long enough, overthought and hypercritical past the point of uselessness. I will interpret the whole "if true, still mealymouthed" statement as meaning you no longer have any substantive objection.Greg Bard (talk) 06:20, 17 February 2010 (UTC)

"Mealymouthed" means that the statement no longer makes any testable claim, because it relies on "Usually" rather than a universal quantifier. And don't be ridiculous -- every other person commenting here has objected to your insertions. Everyone has substantive objections, and we've all brought them up.

CRGreathouse (t | c) 06:35, 17 February 2010 (UTC)

ω rule

I was thinking about this earlier, and I think nobody here has mentioned the ω rule as another example of a rule of inference that is not expressible as a formula. The ω rule is an infinitary inference rule used to study first-order arithmetic, which says that if P(x) is a formula of Peano arithmetic and you can assert (individually) P(1), P(2), P(3), ..., so that you have separate assertions of P(n) for each standard natural number n, then you can deduce ∀x P(x) from this infinite collection of assertions.

The ω rule is interesting here because it is a logical truth, but it isn't sound for classical first-order semantics. It isn't sound because its conclusion can fail in non-standard models even when all of its hypotheses hold, and so it does not preserve truth in arbitrary models of Peano arithmetic.

But the ω rule is a logical truth in the sense that (disquotationally) the truth of ∀x P(x) follows logically from the (disquotational) truth of P(k) for every natural number k; this is just the T-schema for the universal quantifier. This is the sense of "logical truth" that Ayer is talking about: not just "truth in every first-order model" but Logical Truth in the philosophical sense. The ω rule is that sort of Logical Truth, but it cannot possibly be represented as a formula in PA, because formulas of PA are finite. — Carl (CBM · talk) 17:48, 16 February 2010 (UTC)

Carl, this doesn't speak to classical standard logic does it? Be well. Greg Bard (talk) 03:42, 17 February 2010 (UTC)

Yes, ω logic is a classical logic, rather than an intuitionistic one. It is not the same as first-order logic, but that's a separate matter. The thing I'm pointing out is that the ω rule is a Logical Truth, in the philosophical sense, but it does not correspond to any logically valid formula in the language of arithmetic. — Carl (CBM · talk) 03:56, 17 February 2010 (UTC)

There's a axiom schema in L_ω1ω which corresponds to that rule. I don't really want to side with the Bard, but he may have a point. — Arthur Rubin (talk) 09:07, 17 February 2010 (UTC)

There is some point: that in a system that supports the deduction theorem, a rule of inference $A\vdash B$ in which A and B are formulas corresponds to a valid formula $A\to B$. However, the claim that is being added to the article is that "every logical truth corresponds to a rule of inference and every rule of inference corresponds to a logical truth".

If one reads "logical truth" there to mean "valid formula" then the claim fails:

1. For theories that don't support the deduction theorem
2. For deduction rules where A is not a sentence (e.g. the ω rule considered in the language of PA)

If one reads "logical truth" in the philosophical sense, meaning any logically valid statement, perhaps in the metatheory, then the claim still fails:

1. The ω rule is a logical truth in the philosophical sense, but it's not sound for ordinary first-order semantics, so it can't be taken as a rule of inference without modifying those semantics
2. The disjunction and witness properties from intuitionistic logic are logical truths in that setting (it is logically true that if you prove A ∨ B then you can either prove A or you can prove B; in fact a syntactic analysis of the proof of A ∨ B will show which of these is provable). But there is no way of stating this as a rule of inference in the ordinary sense, because the conclusion depends not just on the last line of the proof ("A"' ∨ B) but on the entire proof above it.

I tried to edit the article to clarify the text, which is what led me to realize that the real thing that Gregbard is getting at is simply the deduction theorem. However, I don't see why we should present the deduction theorem in first paragraph of the lede, or cast it as a statement about "logical truth". — Carl (CBM · talk) 12:16, 17 February 2010 (UTC)

Maybe we're going about this wrong, and what we need is to mention the deduction (meta)theorem? CRGreathouse (t | c) 15:38, 17 February 2010 (UTC)

Dense lead

The lead is supposed to be the most reader-friendly introduction to the topic (I often even add a picture that summarizes the lead). That having been said, I find the lead for this page far too dense. It needs a plain English summary. The currently detailed overview would fit nicely in an "Overview" section.-Tesseract2 (talk) 16:59, 15 October 2010 (UTC)

I tried to help. ᛭ LokiClock (talk) 04:14, 3 September 2011 (UTC)

The Rule: A, B Hence A->B

I recall from one of Irving Copi's logic books that there is a pattern of deduction that goes:----

A

B

---

A->B

Copi introduced this rule before quantifiers were discussed. I don't see this rule in the Wikipedia's rules of inference. Is it among them? Should it be listed?

(I'm not making a claim that this is a valid abbrevation of a rule, but I think it suggests a common form of everyday argument, which is: assume A, show B follows, conclude "if A then B". As I recall, Copi took pains to point out it that this form of argument is not modus ponens.)

Tashiro (talk) 15:33, 1 October 2012 (UTC)

WP:GOCE copy edit

I have performed a copy edit of this article under the auspices of the Guild of Copy Editors. If I changed the meaning of a sentence in a way that makes it inaccurate, feel free to change it.

I have removed a number of "clarification needed" and similar tags. Given the text I started with, I have made the article as clear as I could. As with many articles, this one cannot be made entirely clear to a layperson with no background in logic or other related subjects. I think the goal should be to make the article as clear and accurate as possible to someone with a basic understanding of the terms used in it. – Jonesey95 (talk) 00:35, 30 January 2014 (UTC)

Peano Axioms and Provability

In the section on "Axiom schemas and axioms" it mentions that certain statements are provable under the Peano axioms, but the Peano axioms page, when I follow the link, has nothing about provability.

It would be nice if this example was removed or better explained.

I'm fairly new to Wikipedia, so if this is not the best way to bring up things like this, please let me know. — Preceding unsigned comment added by Jadiker (talk • contribs) 09:37, 19 November 2017 (UTC)