Talk:Propositional calculus/Archive 1

Archive 1

Archive 2

Pre-2005 discussions

To someone without a background in mathematical logic, the first paragraph is incomprehensible. Atomic formulas, for example, are not defined and do not have a link.

The first paragraph also attempts a rigorous mathematical statement of what the subject is. There is no informal description following it. Articles such as First Order Logic (FOL) reference this article as a major reference. If the casual user is trying to work out what, say, what this statement means: 'Prolog is based on FOL'. They might quickly loose interest as they are left no clearer. This is an article with the same title, which makes perfect sense to my question: Propositional Calculus Is there any of this simplicity which could be used to assist the novice in Wikipedia?

There is something misleading in calling a propositional calculus an axiomatic system and then presenting rules for predicate calculi that don't have axioms. Most or all of the rules here are for natural deduction systems. Either an alternative, axiomatic approach should be canvassed (and the issue of independence of axioms, etc., be discussed), or else it should be clearly stipulated that "axiomatic system" can apply to systems with an empty axiom-set. (A perverse but, I suppose, allowable usage.)

From the article:

Disjunction Elimination: From wffs of the form ( φ ∧ <-SHOULDN'T THIS BE ∨?? ψ ), ( φ → χ ), and ( ψ → χ ), we may infer χ.

Well, which is it?

It's or, as you already corrected (I got an edit conflict). If it were AND, we would only need either the second or the third wff to derive Chi. Jeronimo

I changed the Disjunction Elimination, Disjunction Introduction and Biconditional Elimination to read 'from the wffs' because only taking all the premisses formulas into account, may the conclusion be made (and not, as is suggested without 'the', that from any of the presmisses formulas the consequent may be deduced) -- [Ogilvie]

Since this article is only about propositional logic and doesn't say anything about first-order logic or anything else along those lines, shouldn't it be titled "propositional logic"? Michael Hardy 01:08 Mar 21, 2003 (UTC)

It would probably be better if more information on the other calculi was added. -- Derek Ross

Symbolic logic have these info. -- looxix 01:43 Mar 21, 2003 (UTC)

• Delete logical calculus to rename propositional calculus to it. Thanks
  • I've repointed the redirect, probaly better than deleting a valid title jimfbleak
  • Taku: do you realise it was originally at logical calculus until looxix moved it? There's a brief naming discussion on the talk page you should probably contribute to, rather than making a unilateral decision to move. -- Tim Starling 15:51 18 May 2003 (UTC)

Actually, I am not so sure the difference between propositional calculus and logical calculus (yeah, and I am working on logic articles now, what an arrogant), so I leave this for other folks. -- Taku 16:28 18 May 2003 (UTC)

I am currently referencing this page on my site ( http://us.metamath.org/ ) but have some mixed feelings about it, since some of the symbols do not render in Internet Explorer. While I personally use Mozilla, perhaps 85% of my visitors use IE. For a while I avoided links to Wikipedia for this reason, but the content has gotten quite good and now I prefer it.

While I don't wish to impose any editorial decisions on the part of the author(s), are there guidelines on Wikipedia w.r.t. the use of math symbols? Should the users of IE be given consideration?

The Unicode symbols that don't render in IE on the 'Propositional calculus' page are '∧' and '∨'. The others seem to render OK.

On the 'First-order predicate calculus' page 3 additional symbols don't render in IE: '∀', '∃', and '∈'.

One possibility is to use GIFs for these five symbols, until Microsoft fixes IE. One source of them are the GIFs on my page http://us.metamath.org/symbols/symbols.html .

Norm Megill nm at alum.mit.edu

Hello, Norm -- I'm a big fan of metamath! It seems to me that this is not a content problem, but a rendering problem. Do you know what versions of IE this has problems with, eg 5.0, 5.5, 6.0?

One solution: We use two ways of doing math here -- in-line Unicode, and TeX. For IE readers, we could if we wanted, render the characters that IE does not support to GIFs/PNGs, and force full rendering of TeX math to images for users of that browser. But this will screw up our caching system, which tries to serve the same page for all browsers to users who are not logged in.

Another solution: We could post-process cached pages to do this, at the cost of extra compute when being visited by IE. (Which is, unfortunately, the most common browser...)

I'm not sure what the correct answer is... -- The Anome 17:38 9 Jun 2003 (UTC)

By the way, thanks Norm, for releasing those bitmaps into the public domain. The Anome 17:42 9 Jun 2003 (UTC)

One possible solution would be to use the corresponding TeX markup for these sections. Except in the most basic cases, these are automatically converted to PNG (depending on user preferences - which can be configured to always use PNG). Using TeX markup for inline stuff (in the middle of a sentence) is generally undesirable, since it creates spacing issues, but sometimes a clever rephrasing of the article can get the TeX markup into its own line to avoid this problem. (Doh, someone else beat me to it! :) -- Wapcaplet 17:41 9 Jun 2003 (UTC)

(Though, I just remembered, some versions of MSIE, 4.0 and some versions of 5.x if I recall correctly, do not support PNG... erg.) -- Wapcaplet 17:48 9 Jun 2003 (UTC)

When the GIF patent runs out we could always serve GIFs after then, but... yecch. (It's this month in the US, next year elsewhere, so I have read). The Anome 17:49 9 Jun 2003 (UTC)

The IE version I have is 6.0.2600. But the real problem is Microsoft's WGL4 Unicode font which (per their own spec) simply omits these 5 symbols (among others). Even though there have always been slots for them in the Unicode standard, Microsoft inexplicably did not bother bringing them over from WGL4's lowly predecessor, the Symbol font. Apparently they didn't consider them to be of any use. (Let me refrain from any remarks about "math literacy"...) This messed up my own plans to convert the Metamath site to Unicode a couple of years ago.

About the GIFs on my site: Even though my symbol bitmaps were originally created with the GIMP, any that are on public display were purposely reprocessed into GIFs by a Unisys-licensed product in order to make them (presumably) legal. I have been tempted to convert them to PNG but don't know how well older browsers handle transparency (if, as you indicate above, they handle PNGs at all), which is important for my site. In any case the bitmaps are the same regardless of how they are encoded, and I suppose anyone could re-encode them into their preferred format.

Of course I don't know the best solution for Wikipedia but just wanted to make sure there is an awareness of the issue. In the meantime on my site I am recommending Mozilla to read Wikipedia. Thanks for your responses.

Norm Megill nm at alum.mit.edu

Shouldn't this be in there somewhere, or can it be already worked out from the article somehow?

From wffs of the form ¬ ( φ ∨ ψ ) we may infer ( ¬ φ ∧ ¬ ψ ).

From wffs of the form ¬ ( φ ∧ ψ ) we may infer ( ¬ φ ∨ ¬ ψ ).

كسيپ Cyp 00:37 18 Jun 2003 (UTC)

Well, those wouldn't be considered basic rules. They can be derived through reductio and disjunction elimination, though... Evercat 00:44 18 Jun 2003 (UTC)

Still, one thing I was wondering was whether the move [ A v B, -A, therefore B ] wasn't considered a basic rule? When I was taught logic it was recognised as a 2nd type of disjunction elimination. But it's not given on that page. Evercat 00:49 18 Jun 2003 (UTC)

The problem is just that the choice of basic and derived rules is really quite arbitrary, especially in such a simple logic. The article as t stood said, "This is the propositional calculus," "These are the rules of derivation," which is wildly misleading. Any rule in only as basic as some textbook writer chooses to make it. (You can get a sound, complete propositional calculus whose only basic rule is modus ponens. And so forth.)

Incidentally, though, the difference between two forms of "disjunction elimination" raises issues of concern to Intuitionism. But this is not an intuitionistic calculus.

Shouldn't we try to clearly state the difference between syntax, semantics and proof rules? CSTAR 23:29, 18 May 2004 (UTC)

'Letters of the alphabet are wffs.' The problem with this is that there are only 26 letters of the alphabet, and really we need an infinite supply of letters, e.g. x, x', x, x', etc. As you can always put another ' on, we never run out.--Publunch 11:21, 6 Nov 2004 (UTC)

Move proposal

I propose moving this article to Classical propositional logic, because:

1. I think it is the most common name, by quite a margin;
2. It means the article need not, as it does not, deal with rival propositional logics, such as intuitionistic logic and quantum logic. As it stands, the article fails to do justice to its name.

Since the article outlines both a natural deduction system and Hilbert type axiomatic system under the names of Calculus and Alternative Calculus respectively, it should be clear that there is more than one type of calculus for propositional logic. Second, the article, up to and including the section Grammar, is not about 'classical logic specifically, as a distinction between intuitionistic and classical logic would only be made by giving their respective axiomatizations (or rules for a sequent calculus or semantic tableaux). Hence I feel the most appropriate title of the article is simply Propositional logic. (And under the calculus sections, make explicit mention that they are for classical systems.) Nortexoid 13:07, 21 Mar 2005 (UTC)

Some other issues need addressing:

• Currently propositional logic is a redirect to propositional calculus, without any suggestion that the two terms are not synonyms. This, as I understand the terms logic and calculus, is misleading: a logic is a certain kind of consequence relation, and a calculus is an effective method for understanding (in particular) a logic. In particular, the natural deduction calculus is called the natural deduction system, obscuring the fact that the current article is presnting a particular calculus as if it were the propositional calculus. This is not OK.

But as I've said above, since it gives an alternative calculus (Hilbert style), that is not the case. Nortexoid 00:47, 22 Mar 2005 (UTC)

• Instead, we need a more refined taxonomy, dealing with the above issue, and also with
  1. classical logic (currently, a redirect to logic, which is OK, but not ideal);
  2. classical propositional logic is blank (please don't start this page: if the move goes ahead it will just need to be deleted).
  3. Naming alternative calculi of propositional logic, eg. Hilbert's calculus, sequent calculus, tableau calculus. Also should make clear that the given natural deduction calculus is just one of a rather large varierty of such frameworks.

Comment? Charles Stewart 22:11, 13 Nov 2004 (UTC)

Formatting

It's inconsistent. Some is in Unicode, some is in ASCI, and the rest is in TeX. Unicode should be used, if at all, only inline with text (i.e. not on lines by itself, e.g. for derivations/axiom lists). Nortexoid 04:03, 18 Mar 2005 (UTC)

I'd say that TeX is to be preferred whenever it is appropriate, since the WP software allows users to govern whether it is typeset or transformed into Unicode. I don't care enough to make a start with making the logic articles more consistent in this respect; it's on my very-far-from-urgent list. Much more urgent, I think, is the move I proposed above: do you have the first comment? ---- Charles Stewart 09:59, 18 Mar 2005 (UTC)

See Wikipedia talk:WikiProject Mathematics/Archive4(TeX) for a very long and very detailed discussion on the subject. If anybody has more questions, just ask them at Wikipedia talk:WikiProject Mathematics (that's the headquarters of Math on Wikipedia). Oleg Alexandrov 10:15, 18 Mar 2005 (UTC)

Ok, interesting pro/con discussion for use of TeX, but there is at least one non-aesthetic reason for using unicode -- it is cut/paste-able. One aesthetic reason for using it inline with text is that the font style and size is consistent with the text. Nortexoid 13:12, 21 Mar 2005 (UTC)

Sorry for the late reply, I missed this for some reason. What I should have said above, is, as you noticed, the issue of TeX vs. html. As far as Unicode is concerned, I agree that one better not use it. Oleg Alexandrov 18:42, 20 Apr 2005 (UTC)

Types/Styles of propositional calculus?

This is coming from someone who knew little of propositional calculus and is using Wikipedia as an introduction. I have run into something that caused my a deal of confusion. All of the off-site references about propositional calculus, including MetaMath and two freely available PDF books on the subject, refer to a three-axiom system of prepositional calculus as if it were the 'standard' way of defining the axioms. I understand that there are many ways to write the axioms which are functionally identical, but it would perhaps be helpful to give names to the more common versions. In particular, the one MetaMath uses contains these three axioms:

• φ → (χ → φ)
• (φ → (χ → ψ)) → ((φ → χ) → (φ → ψ))
• ( ( ¬ χ ) → ( ¬ φ ) ) → ( ( ( ¬ χ ) → φ ) → χ )

These correspond to THEN-1, THEN-2, and some unspecified axiom from the article. This confused me for a good long time.

Kutulu 20:35, 3 Jun 2005 (UTC)

Why metamath is not a good link for this article

In general, I don't think we should treat tools for logicians as regular references, but instead we should have them as links from specialised articles. Different editors might reasonably disagree on this, but I find in is more in keeping with the tone of being an encyclopedia and not a web directory. In any case, metamath is a tool that, while it can handle propositional logic as a special case, is designed to be used with predicate logic and has no special support for propositional logic. I don't see any case for having it as a link from this article. --- Charles Stewart 17:05, 6 Jun 2005 (UTC)

I'm not sure what you mean by having "no special support" for propositional logic. In particular, their interactive "Metamath Solitaire" tool uses only a three-axiom system for propositional logic as the default set of axioms -- you need to explicitly select the additional axiom sets for predicate logic, ZFC set theory, etc as additional axioms. Given that it's just an external link, and that it is related to propositional logic, I don't see how it's harmful to have the link there. It includes a good introduction to propositional logic as the base for higher set theory, and helps demonstrate how the various forms of logical calculus (if that's the right term) as built up from each other. Though, it's just a link so I'm not going to argue any more than this :) Kutulu 15:50, 8 Jun 2005 (UTC)

Propositional logic has good properties that predicate logic does not, which are exploited by tools for propositional logic, like decidability, completeness wrt. truth tables. The point is that any tool for predicate logic, such as most of the 27 links in this directory are useful as tools for propositional logic: should we include them all on this basis? Maybe adding these kinds of directory resources would be good for users of wikipedia, but it is a step away from being an encyclopedia, and if we have them at all, which I think might be a violation of the "not a directory" part of WP:NOT, I would certainly prefer to have them in a separate page than on this page. --- Charles Stewart 17:45, 8 Jun 2005 (UTC)

Case for a move, revisited

Kutulu's confusion above (in Types/Styles of propositional calculus?) makes the case I was arguing before: we should make and respect the distinction that blah-logic is about the consequence relation whilst blah-calculus is about sets of inference rules that characterise the logic (perhaps among many other logics). A few months back, predicate logic was moved to first-order logic: while the grounds for the move were not exactly those I'm arguing here, I think it strengthens the case for a move.

My revised suggestion for a move is simply to move to propositional logic, and add a section to the article discussing non-classical propositional logics, thus obviating the need for "classical" in the title of the article. Thoughts? --- Charles Stewart 20:17, 6 Jun 2005 (UTC)

Turnstile, ⊢, doesn't show up properly in IE

I have redone the 'propositional logic' table that I had put a .PNG picture of in this page a few months ago, but this time in Wiki format. Now, every body can edit it. However, there are two problems here:

1. The turnstile symbol, ⊢, doesn't show up properly in IE; it's ok in Firefox though.
2. Some lines, prior to the table, should be merged to the table or else we will have same ideas presented in two different formats; some sort of redundancy.

There is a more serious concern about the paragraph describing the inference rules. Biconditional introduction and Biconditional elimination are not primitive rules of L, they are definitions (abbreviations). They are not even theorems like Modus Tollendo Tollens (MTT). In addition, the Rule of Assumption is not included. The nine primitive rules of system L are:

1. The Rule of Assumption (A)
2. Modus Ponendo Ponens (MPP)
3. The Rule of Double Negation (DN)
4. The Rule of Conditional Proof (CP)
5. The Rule of ∧-introduction (∧I)
6. The Rule of ∧-elimination (∧E)
7. The Rule of ∨-introduction (∨I)
8. The Rule of ∨-elimination (∨E)
9. Reductio Ad Absurdum (RAA)

Theorems can be derived from these nine rules.

Example:

p → q, ¬q ⊢ ¬p [Modus Tollendo Tollens (MTT)]
Assumption number	Line number	Formula (wff)	Lines in-use and Justification
1	(1)	(p → q)	A
2	(2)	¬q	A
3	(3)	p	A (for RAA)
1,3	(4)	q	1,3,MPP
1,2,3	(5)	q ∧ ¬q	2,4,∧I
1,2	(6)	¬p	3,5,RAA
Q.E.D

Therefore, I suggest a thorough revision of 'Inference rules' paragraph, unles if its author has intended an uncommon logical system.

The 'Propositional calculus' article also needs more details on the following issues:

• The language of the system
• A definition of a proof
• The description of the rules of L in a way that the assumption column in a proof can be calculated by every one.

I can do all of them, if you, Wikipedians, agree.

Eric 07:05, 11 October 2005 (UTC)

Whoops! Can't have a sound or complete system without a semantics!

Something is wrong with this article. The system has no semantics (the truth tables). So its an uninterpreted language. Systems like this cannot be either sound or complete. Those terms have no meaning for logics that have no semantics. The two proof sketchs both refer to a semantics, so somebody better put one in. Right now those references and the proofs are incoherent. --GeePriest 05:43, 12 June 2006 (UTC)

JA: This remark betrays a misconception about how mathematics works. The mathematical objects, things that we may refer to under many assorted names, but briefly and conveniently in this context as propositions, are already there and quite familiar to us in many different guises long before we get around to cooking up, or cocking up, as the case may be, a really fine and dandy fully-blooded and fully-fledged formal calculus for reckoning more effectively and efficiently with them. In mathematics as in existentialism, then, semantics precedes syntactics. Jon Awbrey 19:56, 16 June 2006 (UTC)

Mathematicians may find that they can use PL without a detailed semantics, using certain assumptions, however, any Logic needs an exhaustive semantics in order to that it be possible to express propositions within it. And this is an article on Logic not Mathematics. Wireless99 15:08, 29 August 2007 (UTC)

The semantics are discussed in Soundness and completeness of the rules. The entire article needs work, though. — Carl (CBM · talk) 15:45, 29 August 2007 (UTC)

So they are. Was reading Jon Awbrey's contributions and getting a little fed up with him, should probably have held back a little and read everything else before writing something - apologies. Would like to see truth tables included at some point though. Wireless99 17:16, 29 August 2007 (UTC)

Move to Propositional Logic? And back Again

JA: I don't remember seeing a proper move request, notice of proposed move, discussion, vote and so on, for the change from "propositional calculus" to "propositional logic". There is a POV reflected in the latter title, one that I happen to prefer, but there is still a distinction between "a" propositional calculus, one of many particular syntactic systems, and "the" propositional logic, the invariant mathematical object that all of those calculi are logicallly equivalent languages for representing. Thus it is still important to distinguish the syntax from the semantics, as the latter level takes a lot more work to develop properly. Jon Awbrey 13:08, 9 May 2006 (UTC)

JA: This article was improperly moved from Propositional calculus to Propositional logic without any prior discussion last month. The new contributor that did this proceeded to add much useful and correct material, and so I let it pass without objection. One of the things that I feared might happen has now happened. Namely, the article is now being mushed to pieces by philosophy buffs who display every freshperson misconception about the mathematical subject matter that I have ever seen in all my born years. Thus, I will now undo the improper name change that was committed last month. Jon Awbrey 19:20, 16 June 2006 (UTC)

Material on hold. Three axioms

JA: The material on "Three axioms" appears to have been inserted at random. Can the contributor explain why it was put where it was? Jon Awbrey 21:35, 16 June 2006 (UTC)

Three axioms

Out of the three connectives for conjunction, disjunction, and implication (∧, ∨, and →), one can be taken as primitive and the other two can be defined in terms of it and negation (¬) (and indeed all four can be defined in terms of a sole sufficient operator). The biconditional can of course be defined in terms of conjunction and implication.

A simple axiom system discovered by Jan Łukasiewicz takes implication and negation as primitive, and is as follows:

• φ → (χ → φ)
• (φ → (χ → ψ)) → ((φ → χ) → (φ → ψ))
• (¬φ → ¬χ) → (χ → φ)

The inference rule is modus ponens, as above. Then a ∨ b is defined as ¬a → b, a ∧ b is defined as ¬(a → ¬b), and a ↔ b is defined as (a → b)∧(b → a), that is, ¬((a → b) → ¬(b → a)). With these definitions in hand, it is possible to derive the previous axioms in the new system. Conversely, the first two axioms are the same as in the previous system, and the new third axiom can be derived in the previous system. Thus the two systems are equivalent.

That was me. This axiomatization is quite common. Perhaps the most common. I inserted it because I referred to it in another article I'd been reworking, and figured I ought to write something about it. As to whether it ought to go in a different section, I had an eye to start reworking this article as well, which is a bit of a mess, so I wasn't going to worry about it. But I am happy to leave it out until your dispute with the other editor is settled. 72.137.20.109 15:22, 17 June 2006 (UTC)

JA: No problem in principle with the idea of comparing different axiom systems, I'm just not sure that this introductory article can bear the weight of another level of sophistication, as it seems to be carrying all the tensions that it can master just doing what it does at present. So maybe it's material for a different level of article that follows up on this first invitation to the realm. Before we can start to consider variant axiom systems, even just for classical propositional logic, it is necessary to introduce the difference between model-theoretic and proof-theoretic ways of looking at the subject matter, and even that may be too much for an introductory article to bear. Not sure yet. Jon Awbrey 12:56, 18 June 2006 (UTC)

Absolutely. The next step was going to be to demystify the subject, and then split the article up. But as I say I shall wait for the dust to settle. 192.75.48.150 14:57, 19 June 2006 (UTC)

JA: The sad thing is that I actually prefer the term Prop Log, as it comes in handy for referring either to the level of broadly equivalent structure that all peculiar Prop Calcs have in common, or else to the normative rules of inference that are optimized for reasoning about the abstract objects that we all know and love as propositions. So I was caught unawares by the sort of abuse that the term logic invites. Oh well, like you say, let's wait for the rain. Jon Awbrey 15:08, 19 June 2006 (UTC)

Attempted POV Fork

JA: To the anonymous user who keeps trying to create a separate article for Propositional Logic. You cannot do that. The redirect from Propositional Logic to Propositional Calculus is ancient. There was an improper name change that was made last month and that has created too much confusion, and so it has been reversed to its original condition. This article has been worked up by multiple experts who know what they are talking about, and you cannot just go off and create a new subject out of your own imaginings. So knock it off. There is no assertion that Prop Calc and Prop Log are two separate subjects, as that would not be in accord with established usage. It is only that the term Propositional Logic appears to be confusing some readers into trying to hijack this article out of the category of Mathematical logic. Jon Awbrey 05:04, 17 June 2006 (UTC)

JA: I have made an informal request for an administrator to help out with this issue. Jon Awbrey 05:20, 17 June 2006 (UTC)

I have to revert the rename done by Jon because it had annihilated the article's history. If you want to do a move, do it properly (this may require administrator intervention). -lethe ^{talk +} 07:19, 17 June 2006 (UTC)

Right now, there are several redirects. Before I fix them, I want to establish what title this article is going to have. The original move was carried out properly. There is a discussion above, and it was taken to WP:RM. So please, if you want to revert it, try to also do it properly. -lethe ^{talk +} 07:27, 17 June 2006 (UTC)

JA: I have asked Oleg to help sort this out. Jon Awbrey 07:34, 17 June 2006 (UTC) [Intemperate remarks deleted] Jon Awbrey 13:06, 18 June 2006 (UTC)

Yeah, I know you asked Oleg, I saw it on his talk page, and that's why I'm here. I know you'd probably prefer Oleg to me, but I'm an admin too, so maybe I can help you. So, there were two discussion sections about the move in this talk page above, and it was brought up at WP:RM, where it was then enacted by an admin. OK, but perhaps the tags were never placed on the article, so it wasn't completely proper. -lethe ^{talk +} 07:38, 17 June 2006 (UTC)

JA: I followed the instructions given on the move page and the other advice that I was given about preserving histories when doing a move blocked by a previous redir history. Unless Nightstallion destroyed the history on the previous move, then it should all still be here, one place or the other, and people have repeatedly told me that's all the matters. Jon Awbrey 07:40, 17 June 2006 (UTC)

The page had no history before I reverted. -lethe ^{talk +} 07:43, 17 June 2006 (UTC)

Alright, I just moved the article back to Propositional calculus, using the move function and deleting the redirect page with history. -lethe ^{talk +} 07:44, 17 June 2006 (UTC)

JA: The above discussions are obsolete business from 2004 and mid 2005, most of them were discussing a variety of different contemplated splits and name changes, and none of thems ever became formal proposals. Jon Awbrey 07:47, 17 June 2006 (UTC)

Well they were cited at WP:RM. If no serious objections are raised, then that's good enough. But anyway, I have reverted the move properly, in a history preserving way. Are you satisfied now? If there are people who still want the move (Charles Stewart?), let them come back and initiate a new process. -lethe ^{talk +} 07:49, 17 June 2006 (UTC)

I posted a note at Wikipedia talk:WikiProject Mathematics. I put this page on my watchlist, and if arguments show up I'll try to get involved. Oleg Alexandrov (talk) 07:53, 17 June 2006 (UTC)

JA: That's not what the instructions at WP:RM say, which I always follow if I guess it will be controversial. Of course, we all guess wrong at times. People don't watch, well I don't watch WP:RM unless I have an active proposal there, they watch their content pages. I guess I'll have to start. Jon Awbrey 07:56, 17 June 2006 (UTC)

I certainly don't watch WP:RM. In fact, a comment made on the request made by Arthur Rubin made it look like perhaps he had wanted to say something about the move, but I may be reading too much into his comment. -lethe ^{talk +} 08:04, 17 June 2006 (UTC)

JA: It may help you to know that there is most likely some other funny business afoot here. Visit Talk:Charles Peirce of you want the whole sad tale in progress. Need sleep, to hell with the clown ... Jon Awbrey 08:26, 17 June 2006 (UTC)

Toward less slippery stepping stones to logic

JA: It looks like it will take the rest of the week just to clean up the article to the point where we can see what we have accumulated over the years. As a fan of CSP's and GSB's ways of doing this, with just 4 axioms plus rules of replacement and substitution, I'm not especially thrilled with the horrendously inelegant so-called "natural deduction system", so I'm thinking about going back to Chang & Keisler, Ebbinghaus–Flum–Thomas, Van Dalen, and other books I remember liking from school daze, for the ways that they do this. And the 3 axiom system has much to recommend it for the aptness of its comparison to Intuitionistic Prop Calc, Combinatory Logic, and so on. Jon Awbrey 14:24, 21 June 2006 (UTC)

JA: The parameter Α can be finite as we are not trying to define a universal structure yet, and there is a pressure to keep this article introductory, so let's not worry about the non-finite case for now. Jon Awbrey 05:42, 26 June 2006 (UTC)

In that case, perhaps it would be better not to mention the number of propositional variables at all rather than give a perhaps misleading impression. In any case, only finitely many letters or digits would be used. It is just a question of whether people can make arbitrarily long variable names, if they need to do so. But I would rather not suggest that it is necessary to create a new logic just because you need more variables for a particular application. JRSpriggs 09:00, 27 June 2006 (UTC)

JA: That seemed to make sense to me — but then I'm still between my 1st and 2nd cup of coffee — and so I went back and subbed "collection" for the affected mentions of "finite set". But now that I look at it, that's a bit off, and the reason is that we are talking about a calculus, that is, a formal system for calculation, and calculations are finite-basis thingies. Yes, I know some people like to define formal languages with infinite alphabets and infinitely long words, but I personally take that to be one of those spurious sorts of generalizations for generalization's sake that lose the spirit of the initial idea. What next? Infinitely long proofs? No doubt it's been thunk of already. But we all know this game, the countable number of variables will still have to be indexed on some system of numeration that is finite-based, etc., etc. — so all in all I don't see the point of going down that road in this stepping-stone type article. Jon Awbrey 12:50, 27 June 2006 (UTC)

JA: The strategy of making the argument set an explicit parameter is a fairly standard tactic in these sorts of situations. It does not mean that we have a different "logic" for each venn diagram, because we save the word "logic" for a higher purpose, but we do have a different calculus on each set of parameters, and each one of these is a well-controlled finite-basis categorical object. Once we get our feet on the ground with a small number of such objects, we can begin to think about the necessary morphisms, extensions, limits, universal constructions, and so on. But that is a tale for another day, not of necessity to be told in this article. Dunno yet. Jon Awbrey 13:06, 27 June 2006 (UTC)

Simpler logic

If we are going to go back to axioms and away from natural deduction, I would like to make a suggestion. Use just "→" and "$\bot$" as primative connectives. All the others can be defined in terms of them. And the axiom schemas might be:

• P→(Q→P)
• (P→(Q→R))→((P→Q)→(P→R))
• ((P→Q)→P)→P
• $\bot$→P
• from P and P→Q infer Q

—The preceding unsigned comment was added by JRSpriggs (talk • contribs) .

I already added the Łukasiewicz version to the article. I myself prefer having a constant, as you have, rather than a unary operator, as he has. In fact, I would leave out Peirce's law and ex-falso, and use double negation instead $((P\to \bot )\to \bot )\to P$, leaving only three axioms. But these are less common. 192.75.48.150 17:16, 26 June 2006 (UTC)

JA: Appreciate having another hand on deck. The article is currently in some kind of metamorphosis. There has been a history of dispute about several issues, the name to use and the proper level to cast it at, just to name a couple, and I think that the sense of the interested parties is still up in the air. Without trying to address any substantive issues, I started a routine first pass at copyediting last week, just ironing out inconsistencies in notation and minor errors, and have gotten only about a third of the way through, so that work will continue this week.

JA: I like the idea of presenting several axiom systems and comparing their differential features, but it's a question how much of that we can do and still maintain the article as a "gateway to logic", "key to the realm", or whatever. I will try to hurry along with the copyedit process so that it will be easier to compare the different approaches. Jon Awbrey 13:16, 26 June 2006 (UTC)

As for me, I'm not impatient. I'd say there's no hurry. 192.75.48.150 17:16, 26 June 2006 (UTC)

JA: P.S. I personally like the lattice symbols, but my sense is that many readers will find them strange and off-putting, and I'm trying to avoid that wherever it can be done without falsifying the subject. Jon Awbrey 13:20, 26 June 2006 (UTC)

JA: I tried moving the various systems around just to see how it would look, but I'm not sure that I got all the pieces sorted to the right places, so it would probably be a good idea if others check and see. Jon Awbrey 05:30, 30 June 2006 (UTC)

It could just be my lack of familiarity with Łukasiewicz's version of logic, but I think that the version I mentioned is easier to use which is more important than the number of axioms. To show this, I will use $\lnot A\equiv (A\rightarrow \bot )$ and derive his third axiom from my version. I challenge you to derive Peirce's law as easily from Łukasiewicz's system. I will use the deduction theorem and I suggest that you do as well and that you might want to define $\bot \equiv \lnot (A\rightarrow (B\rightarrow A))$.

• • $\lnot A\rightarrow \lnot B$ 1. hypothesis
    • $B\!$ 2. hypothesis
      • $A\rightarrow \bot$ 3. hypothesis
      • $\lnot A$ 4. definition of not
      • $\lnot B$ 5. modus ponens 4,1
      • $B\rightarrow \bot$ 6. definition of not
      • $\bot$ 7. modus ponens 2,6
      • $\bot \rightarrow A$ 8. ex-falso
      • $A\!$ 9. modus ponens 7,8
    • $(A\rightarrow \bot )\rightarrow A$ 10. deduction from 3 to 9
    • $((A\rightarrow \bot )\rightarrow A)\rightarrow A$ 11. Peirce's law
    • $A\!$ 12. modus ponens 10,11
  • $B\rightarrow A\!$ 13. deduction from 2 to 12
• $(\lnot A\rightarrow \lnot B)\rightarrow (B\rightarrow A)$ 14. deduction from 1 to 13 QED

Can you beat that? JRSpriggs 02:36, 1 July 2006 (UTC)

JA: Big $!\uparrow$ Holiday, so will be intermittent at best, but in the spirit of starting the fireworks early I will just say this. I like doing comparative axiomatics because of my interest in the relation between classical logic and combinatory logic, but ... when it comes to pure classical propositional logic there is no finer or simpler than the CSP–GSB graphical set up. See Logical graphs, where there is my favorite proof of Peirce's law. When it comes right down to it, as far as Prop Calc goes, it's a positive disservice to the student to reach them anything else first, as many of them never recover from the sheer glop of the traditional textbook turg-idiocies. And dat's da truth! $\star \star \star$ Jon Awbrey 03:34, 1 July 2006 (UTC)

JA: For ease of reference, here is the statement and proof of Peirce's law in logical graphs.

Theorem

o-----------------------------------------------------------o | Peirce's Law` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` | o-----------------------------------------------------------o | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` | | ` ` ` ` p o---o q ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` | | ` ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` | | ` ` ` ` ` o---o p ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` | | ` ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` | | ` ` ` ` ` o---o p ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` | | ` ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` | | ` ` ` ` ` O ` ` ` ` ` ` ` ` = ` ` ` ` ` ` ` ` ` O ` ` ` ` | | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` | o-----------------------------------------------------------o | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` | | ` ` `(((p (q)) (p)) (p))) ` = ` ` ` ` ` ` ` ` ` ` ` ` ` ` | | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` | o-----------------------------------------------------------o

Proof

o-----------------------------------------------------------o | Peirce's Law. `Proof` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` | o-----------------------------------------------------------o | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` | | ` ` ` ` p o---o q ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` | | ` ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` | | ` ` ` ` ` o---o p ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` | | ` ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` | | ` ` ` ` ` o---o p ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` | | ` ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` | | ` ` ` ` ` O ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` | | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` | o==================================< Collect >==============o | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` | | ` ` ` ` ` o---o q ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` | | ` ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` | | ` ` ` ` ` o---o ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` | | ` ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` | | ` ` ` ` p o---o p ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` | | ` ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` | | ` ` ` ` ` O ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` | | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` | o==================================< Recess >===============o | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` | | ` ` ` ` ` o---o ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` | | ` ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` | | ` ` ` ` p o---o p ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` | | ` ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` | | ` ` ` ` ` O ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` | | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` | o==================================< Refold >===============o | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` | | ` ` ` ` p o---o p ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` | | ` ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` | | ` ` ` ` ` O ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` | | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` | o==================================< Delete >===============o | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` | | ` ` ` ` ` o---o ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` | | ` ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` | | ` ` ` ` ` O ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` | | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` | o==================================< Refold >===============o | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` | | ` ` ` ` ` O ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` | | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` | o==================================< QED >==================o

JA: So, how do you like dem axials? Jon Awbrey 15:15, 1 July 2006 (UTC)

I am not familiar with those logical graphs and I doubt that they would be a very practical way for us to teach logic to the readers of this encyclopedia. My point was not to have a contest of who can display the most erudition to the other. My point was to determine which system of logic we should teach. I think that it should be the one which gives the most powerful results for the least effort. That is why I said "I challenge you (User:192.75.48.150) to derive Peirce's law as easily from Łukasiewicz's system.". I wanted to see whether his system is more or less powerful than the one I was advocating. Comparing how easily we can derive each other's axioms seems like a fair test to me. JRSpriggs 09:11, 2 July 2006 (UTC)

JA: The criterion of efficiency in a propositional calculus that you pose as "the one which gives the most powerful results for the least effort" is the very thing that I am interested in here. But I am much less interested in arguing over which of two evils in the way of efficiency and facility is the lesser, so I will bow out of any bout that is pre-fixed that way. Jon Awbrey 14:24, 2 July 2006 (UTC)

I take it that you think that neither of the two systems mentioned is the most efficient. What do you think IS the most efficient way to do propositional logic? And why do you think that? JRSpriggs 05:11, 3 July 2006 (UTC)

To justify my claim about completeness in Peirce's law and to create a model for what I think we should do here in "propositional calculus", I created Implicational propositional calculus. You might want to check it out. JRSpriggs 09:09, 3 July 2006 (UTC)

Erm? Well, any of these axiomatizations illustrates the interdefinability of operators. I chose the one I did because I think it is simple, it is attributable to someone notable, and it seems to be commonly cited. As such, I believe it deserves mention. Maybe not right in this article, but somewhere. I did not choose it because it is my favourite axiomatization -- I believe I've already stated that it is not. I also did not choose it for its instructional value. To teach propositional logic, I think we ought to use the natural deduction system with redundant rules, as it is already given on this page. This "minimal" system, whatever we choose, is not our primary tool of explanation. I certainly did not choose it because it is most "efficient" -- for that, you can't beat the system which uses all propositional tautologies as axioms. This seems to be even more commonly cited, and it is fair: they are decidable.

Incidentally, I say your natural deduction proof is cheating. These are Hilbert-style axiomatizations. (And by using natural deducton, you've also illustrated my point about instructional value.) -Dan 192.75.48.150 20:52, 4 July 2006 (UTC)

Taking all tautologies as axioms is not most efficient because testing whether a proposition is a tautology is not easy. OK, I do prefer a hybrid system which uses "hypothesis", "reiteration", "deduction", and "modus ponens" as rules of inference au natural; and also uses Peirce's law and ex-falso as axioms. Still, I think that whatever systems we describe should be explicitly proven in the article to be sound and complete, not just hand waving. JRSpriggs 07:37, 5 July 2006 (UTC)

To Dan: You said "I say your natural deduction proof is cheating.". I do not consider it to be cheating because I showed at deduction theorem how such a proof can be converted automatically to a truly axiomatic proof. If I had a compiler available, I would write a program to do the conversion. JRSpriggs 06:01, 12 July 2006 (UTC)

Well now, I never doubted you could convert correct natural deduction proofs into correct axiomatic proofs. Correctness was never the issue, was it? All axiomatizations we've discussed are correct, aren't they? Can you convert efficient natural deduction proofs into efficient axiomatic proofs? What is considered efficient, anyway? As for me, I've stated my motivation: simple, attributable, commonly cited -- and not my personal preference. 192.75.48.150 14:50, 12 July 2006 (UTC)

What is the Object of a Calculus?

JA: Whether Wikipedia will serve any educational purpose is one of those things that I have of late become far less hopeful about, but setting that aside for the moment, here are some of the things that I have spent 40 or 50 very odd years thinking about in this connection. To speak of the efficiency of a calculus, propositional or otherwise, is to presuppose a pragma, an object, a purpose for it. People who presuppose different ends for these rolling stones are likely to be found talking past each other until the end of days. So a critical reflection on efficiency demands that we cease our pre-supposing and begin, as if for the very first time, to drag the array of suppositions out into the light. Perhaps this effort will provide us with a bit of useful exercise while await the imminent end of days. Jon Awbrey 12:56, 5 July 2006 (UTC)

I think that Dan had a point (albeit expressed in a backwards way) when he mentioned tautologies. The purpose of propositional logic is to discover which wffs are tautologies. George Boole used simple algebra (or arithmetic with variables) to do this. And the purpose of discovering the tautologies is to allow us to check the correctness of our informal reasoning when we are not sure whether we have enough reason to reach a conclusion or not. We translate our premises into wffs P1,...,Pn and our desired conclusion into wff C and then ask whether (P1 & P2 & ... & Pn) → C is a tautology or not. Sometimes, I can do this by looking for a valuation which makes it false. If I reach a contradiction in that process, then I know that it is a tautology. If I discover such a valuation, then it is not a tautology. Propositional logic should be a more formalizable and communicable way of doing that. JRSpriggs 06:02, 6 July 2006 (UTC)

However unfortunately, many people have nonclassical ways of reasoning which they have formalized into nonclassical propositional logics. With the possible exceptions of intuitionist logic and modal logic, I think that these are useless. JRSpriggs 06:05, 6 July 2006 (UTC)

JA: Yes, tautology-finding, theorem-proofing, or validity-testing are typical answers. The nice thing about Prop Calc is its completeness, which means that I can take the model-theoretic road and you can take the proof-theoretic road and we'll both get to Loch Theorem — the lake of all truism, I reckon — sooner or later. This is so striking that Chang & Keisler, who use tautology and consistency for the syntactic notions and use validity and satisfiability for the semantic notions, always used to throw me for a loop by calling truth tables a syntactic method (!). Their rationale for saying this appears to be the finitary nature of truth table testing, lending itself to a purely clerical or mechanical decision procedure. Jon Awbrey 12:46, 6 July 2006 (UTC)

I think that a valuation (function from the propositional variables to {falsity, truth}) is the analogue of a model. A valuation which makes a complex proposition true is the analogue of a model which satisfies a formula of predicate logic. So a tautology is the analogue of a formula which is satisfied by all models. These should be the theorems of propositional and predicate logic respectively. JRSpriggs 05:37, 7 July 2006 (UTC)

JA: Right, I always used to consider truth tables as model-theoretic thingies, with the coordinate sequences that are variously called assignments, interpretations, or valuations being the rather reduced analogues of what are called models in FOL. But then I ran into what Chang & Keisler (1973 — at $275+ I'm still saving my ¢'s for the new edition) say here:

At first glance, it seems that we have to examine uncountably many different infinite models A in order to find out whether a sentence φ is valid. This is because validity is a semantical notion, defined in terms of models. However, as the reader surely knows, there is a simple and uniform test by which we can find out in only finitely many steps whether or not a given sentence φ is valid.

This decision procedure for validity is based on a syntactical notion, the notion of a tautology. Let φ be a sentence such that all the sentence symbols which occur in φ are among the n + 1 symbols, S₀, S₁, …, S_n. Let a₀, a₁, …, a_n be a sequence made up of the two letters t, f. We shall call such a sequence an assignment. ... (Chang & Keisler 1973, 7–8).

JA: More later. Jon Awbrey 15:06, 7 July 2006 (UTC)

"Premise" or "Premiss"?

To Jon Awbrey: You just reverted someone for correcting the spelling of "premiss" to "premise". You said that "premiss" is correct in Logic. I checked via Google -- "premiss" is unknown. I checked my large dictionary (Webster's Encyclopedic Unabridged Dictionary of the English Language) -- "premiss" is not there. I checked the indices of my logic books -- most did not mention either version, but two used "premise" only, and just ONE used "premiss", to wit, Mendelson. I think you should revert yourself. JRSpriggs 02:19, 11 August 2006 (UTC)

JA: Premiss is the correct spelling when talking about a logical premiss. People who read the classics know this. People who do not, do not. I will get you a reference later. I promise. Jon Awbrey 03:02, 11 August 2006 (UTC)

JA: I have a more definitive reference in mind, but in the meantime you might consult the Century Dictionary, which at least mentions the fact that premiss is more proper even if premise is more common:

• Century Dictionary

JA: Proper or popular. It always seems to come to that. Jon Awbrey 03:42, 11 August 2006 (UTC)

Well, *someone* has reverted it back to premiss - probably one of Jon Awbrey's accounts. In any case, check Premise (argument) and you'll see it says premiss is the British spelling, but premise is perfectly acceptable. Also try going to Google and typing in define:premise in the search box, and you'll see that this is correct usage. In other words, both spellings are acceptable, like color/colour, but we should stick to just one for the article. There should be no reverting between the two though (think of Wikipedia edit wars with BC/AD and BCE/CE). FranksValli 19:11, 3 February 2007 (UTC)

The most popular is 'premise'. Church 1956 in his famous text uses 'premiss' to distinguish it from the various different uses of 'premise'. Both, however, are correct. Nortexoid 01:31, 5 February 2007 (UTC)

Categorical Inquisitive

JA: I can't recall for sure on this particular article, but it seems like Oleg, or whoever manages the categories, has already trimmed most of these to where he wants them. Please correct if I'm wrong about that. Jon Awbrey 03:24, 12 August 2006 (UTC)

Enormous Article

As noted in the article's banner, this article is enormous. I've seen a lot of treatments of the "propositional calculus" both from an engineering point of view and from the logician's point of view. Even the text-books aren't as cluttered (bloated) as this is.

There seems to be two treatments, and I believe the article could be split along these two lines:

• 1 -- Truth table method: Define the 16 possible two-value relations R(a, b) with truth tables, show how the "laws" (theorems) come about via the tables and be done with it.
• 2 -- Axiomatic method: (axioms of symbol-manipulation). Define a clever, easy-to use set of axioms and derive everything from those. Unfortunately there seem to be no agreement on how to do this. I've seen easy axiomatic systems that quickly define and use the tautologies (e.g. Suppes 1957:204) and then there are the ugly, hard-to-learn ones that start with and use implication (ick: PM).

Simplify, simplify: Engineers and the elementary college text I used (way back when) just introduced the truth-table definitions and went from there. The engineers learned the "laws" (tautological theorems in particular like De Morgan's laws) in context of formula-reduction. Ditto for the truth-table method. The only laws of any real importance are the two distributive laws (OR over AND and AND over OR), association and commutatition plus: De Morgan's law, the one that really matters i.e.: A V B = ~(~A & ~B) and A & B = ~(~A V ~B). The rest can be found from the truth-tables (e.g. idempotency, identity, etc etc).

I hope this will start some dialog. Bill Wvbailey (talk) 20:07, 7 December 2007 (UTC)

Disputed -- Logical graphs

I stuck a "disputed" tag on the section titled "Logical graphs" -- it seems to be filled mostly with feel-good nonsense, and worse, it links to the article Logical graphs, which is a major turn-off -- cryptically opaque, on the verge of non-sense. I raised the issue as needing expert attention at Wikipedia talk:WikiProject Mathematics#Logical graphs. Pending resolution of the discussion there, I am sorely tempted to suggest an AfD for this section of this article. linas (talk) 05:26, 25 January 2008 (UTC)

On not being too hairy

JA: Propositional logic is one of the main stepping stones to logic for beginners, and this article is already making a mountain out of a molehill as far as that goes. I am guessing that some of the hurdles can be mowed down in time. So I'm amenable to replacing Greek with lowercase Roman — tutorially speaking it's best in first encounters to save uppercase Roman for sets — but we definitely don't need to muddy the waters with talk of metavariables, as that concept is otiose in the case of prop log anyway. Jon Awbrey 18:32, 1 June 2006 (UTC)

I agree that this is article is useless as it is. It is too technical to be understood by anyone who does not already know what propositional logic is all about. And those who do will have no reason to read it. --GeePriest 05:46, 12 June 2006 (UTC)

I agree that this article would be too difficult to understand for anyone who doesn't know this stuff beforehand. For example, IMHO the proof of the completeness theorem is completely useless as it is now. It introduces too many new concepts. I read the proof in the Mendelson's "Introduction to Mathematical Logic". It seems much simpler there. What do you think about it? I think it is much better for a beginner. Stefan.vatev (talk) 22:11, 31 October 2008 (UTC)

What I am talking about is described in this section Another outline for a completeness proof. I think it should be better explained and the other proof should be removed. Stefan.vatev (talk) 22:15, 31 October 2008 (UTC)

In logic and philosophy, propositional calculus is often intended to symbolize rational deduction.

What exactly does this mean and is it both true and important?--Philogo 20:44, 10 November 2008 (UTC)

Consistent language in the large table

Looking at the first entry, the ⊢ is transcribed as "therefore", but in later entries (eg Transposition) the ⊢ is transcribed as "is equivalent to". I know that both the symbols and the text are correct, but is it not confusing to use the same symbol and call it different things in the text in both places? Perhaps either replacing it with "therefore" in all the places it's currently "is equiv. to", or using a different symbol to note the bidirectionalness of the later entries. 87.194.127.65 (talk) 20:35, 26 February 2009 (UTC)

In the context of deductive proof, the symbol ⊢ indicates the notion of "implies" or "yields" in the usage of Microsoft Word, Kleene (1952: 87) and Enderton (2002: 111). For example (cf Kleene p. 87)where the D are "assumption formulas":

D₁,D₂,D₃,...D_n ⊢ E

Microsoft Word defines ∴ as "therefore" -- the symbol that I remember from high school. At least in two-valued logic, the symbol for “equivalence” is =, or it can be the biconditional ↔ . Enderton (2001) uses the double-turnstile ⊨ as "tautologically implies" or "is a tautology" (cf p. 23, but he changes the usage after p. 88 (!) ):

Thus (p & (p → q)) → q, and p & (p → q)) ⊨ q evaluate to a tautology (i.e. the 2nd sign → and the sign ⊨ evaluate to to a tautology in a 2-valued truth table) whereas

(p & (p → q)) = q, and (p & (p → q)) ↔ q do not(thus the signs = and ↔ do not evaluate to a tautology in a truth table).

But, in (p & (p → q)) = (p & q), and (p & (p → q)) ↔ (p & q) the signs = and ↔ do evaluate to a tautology.

(I hope I got the above correct . . .). Confused yet? As there are shades of meaning, the article should define its symbols at the outset and stick with them. The trick will be to get the "shades of meaning" correct. Bill Wvbailey (talk) 23:33, 26 February 2009 (UTC)

Please look at this Wikipedia:WikiProject Logic/Standards for notation. We should aim for consistent notation across all articles, not merely within an article.--Philogo (talk) 00:57, 13 March 2009 (UTC)

Make sure you have sources. Bill Wvbailey (talk) 21:34, 13 March 2009 (UTC)

Hi Bill. The article is maintained by Wikipedia:WikiProject Logic and has been stable (after little initial contention) for some time. It is the project's standard and recomendation for stnadard form of notation across Wickapedia. Youe will see alrternative notations reasonmable well documented. We are aiming for consistency across articles so that the poor reader does not have to learn new notatons when going from article to article. We cannot make people adopt the recommended notations but it would help. Personally I miss '~' and '(x)' and '&' but that's neither here nor there! If you have comments or suggestion go to the article's talk page. Cheers.--Philogo (talk) 14:37, 16 March 2009 (UTC)

if p is false, then p implies q

Is there any special name to this rule? $\neg p\vdash (p\to q)\,$ Albmont (talk) 20:55, 12 March 2009 (UTC)

• Article Vacuous truth seems to discuss this logical rule. And please stop replying to yourself! Albmont (talk) 21:03, 12 March 2009 (UTC)

Folks find this counter-intuitive because they cannot help reading into if-then more than material implication. The equivalent, not-p entails (not-p or q) does not appear counterintuitive although it says the same. Ditto-wise not-p entails not(not-p & q). If it gets your dander up then there is an article somewhere on the so-called paradoxes of material implication.--Philogo (talk) 01:06, 13 March 2009 (UTC)

Ok, but I wanted to use it as a piece in a demonstration. Something like this: I was trying to prove that "p implies q", and then I broke up "p" into several cases. In one case, "p" was false, so it's "vacuously true" that "p implies q". In another case, "p" would imply something else, then "q". Hence, the need for a name. Albmont (talk) 19:14, 13 March 2009 (UTC)

_{BTW, I think you mean not-p entails not(p & not-q). :-) Feel free to fix the typo...} Albmont (talk) 19:17, 13 March 2009 (UTC)

Tautologies are sometimes called "vacuous", but I'm cautious and don't use that term. As noted by Philogo, (p --> q) is identically (~p V q) so ~p --> (p --> q) is identically ~p --> (~p V q). Let u = ~p. Then we have u --> (u V q). This is the "addition" formulation in the article's table. It is also *1.3 in Principia Mathematica, i.e. the 3rd most primitive of the "primitive propositions" (cf p. 94-96 in the 1962 edition of Principia Mathematica to *56). PM states that "The principle will be referred to as "Add"." (p. 96) [In the formal sense as PM constructs its argument we also need 1.4: (p V q) --> (q V p).] In this particular case the implication is stronger than plain-vanilla implication, it is tautalogical implication as well (i.e. in the truth table all 4 signs under the sign "-->" are T). Philogo is correct: the student must treat this stuff mechanically; it has nothing whatever to do with intuitive notions once the signs are defined by truth tables. Often when I'm evaluating truth tables I use Excel. Bill Wvbailey (talk) 21:32, 13 March 2009 (UTC)

Albmont wanted to use it in a demonstration (proof) of the conclusion P->q with ~p as the only premiss; I don't think we have helped! He will have been given a list of rules he can cite (or perhaps axioms he can use). He would have to tell us what they are! --Philogo (talk) 14:20, 30 March 2009 (UTC)

"p does not imply q" means what?

What are the truth table values for "p -/-> q" ? Is it the same as "p --> ~q" ?

And I see that mathworld[1] says that the converse of "p --> q" is "q --> p". Is the obverse of "p --> q" simply "~q --> ~p" ? --Michael C. Price ^talk 02:34, 28 March 2009 (UTC)

For the first question, no. Here's the long of it. This is far easier to see with Karnaugh maps but I'd have to draw them up and upload .jpg drawings; this might be faster.

Let's assume that "p -/-> q" =_{defined as} ~(p --> q). We then work forward from the following equivalence #1 and definition #3:

#1: (A & B) = ~(~A V ~B)

#1.1: ~(A & B) = (~A V ~B)

#3: (A -->B) =_def (~A V B)

#j: ~(p --> q) = ~(~p V q) = ~(~(~p) & ~q)) = (p & ~q) by #3 then by #1, or use axiom ~(~A) = A

#k: But (p --> ~q) =_def (~p V ~q) = ~(p & q) by #3 then by #1.1. This doesn't quite get us there . . .

We need more axioms: Given that "always true T" =_def 1 =_def (A V ~A), and axiom A & 1 = A:

#4: ~p = ~p & 1 = ~p & (q V ~q) = (~p & q) V (~p & ~q) by the distribution of AND over OR

#5: ~q = (~q & 1) = ~q & (p V ~p) = (~q & p) V (~q & ~p)by the distribution of AND over OR

We see now that if we substitute #4 and #5 into #k:

#m: (p --> ~q) =_def (~p V ~q) = [(~p & q) V (~p & ~q)] V [(~q & p) V (~q & ~p)]

We need two more axioms: (A & B) = (B & A), and (A V A) = A . Now we can combine the common terms (~p & ~q) in #m. We are left with 3 terms for (p --> ~q) i.e.

#n: (p --> ~q) = [(~p & q) V (~p & ~q) V (p & ~q)]

Both #j and #n are reduced to the OR of their their so-called "minterms" (i.e. they're in disjunctive normal form), and we see that they are not the same.

As is always the case, someone should check my work. BillWvbailey (talk)

Okay, thanks for that. I wasn't sure what the definition of p -/-> q was, but if it is ~(p --> q) then you are correct. Any thoughts on the obverse? --Michael C. Price ^talk 04:35, 28 March 2009 (UTC)

My ancient college text agrees that q --> p is the converse of p --> q. It says that ~q --> ~p is the contrapositive of p --> q. This book (Kemeney et. al Finite Mathematical Structures) does not have the word "obverse" in its index. Nor does Tarski 1946/1941.

Kemeney et. al: yes to converse, no to obverse, yes to contrapositive

Tarski 1946/1941: converse sentence(indirectly but the same), no obverse, "contrapositive sentence"

Robbin 1969: neither converse nor obverse nor contrapositive.

Hamilton 1978: neither converse nor obverse nor contrapositive.

Stolyar 1970: neither converse nor obverse nor contrapositive.

Enderton 2001, 1972: neither converse nor obverse but yes to contraposition def on page 27 same as Kemeney

Suppes 1957: converse of a relation, no obverse, no contrapositive per se.

Rosenbloom 1950: converse of a relation, no obverse, no contrapositive.

Bender and Williamson 2005: yes to converse, no obverse, yes to contrapositive

Goodstein 1966/1963: neither converse nor obverse nor contrapositive

Reichenbach 1947: converse domain, converse of a function, no obverse, no contrapositive

Goodstein: converse of a relation, no obverse, no contraposition

My dictionary defines obverse as: a propostion inferred immediately from another by denying the opposite of that which the given propostion affirms < the obverse of "all A is B" is "no A is not B".

Thus it would appear that "obverse" is a pretty rare usage. Bill Wvbailey (talk) 14:57, 28 March 2009 (UTC)

Yes, I was going from the dictionary definition. The definition of transposition looks the same as contrapositive. Is that right? Are they synonyms? --Michael C. Price ^talk 16:42, 28 March 2009 (UTC)

I've never encountered the word relative to logic. It would seem to be more likely synonymous with "converse", but I looked up the definition and one one hand one definition is like "converse" but there is another form of usage that "changes the sign" when one moves a term from one side of an equation to the other, so in a way it would be similar to the contrapositive -- it keeps the equivalence of the original intact. Indeed, Tarski's index lists "Transposition, see: Law of contraposition". Neither Kemeny nor Reichenbach list it in their indices. Bill Wvbailey (talk) 15:44, 29 March 2009 (UTC)

For 'obverse and 'obversion' see [2] or http://www-rohan.sdsu.edu/faculty/rfreeman/CHAPTER9.pdfor just google 'syllogism obverse'--Philogo (talk) 13:54, 30 March 2009 (UTC)

Some background?

It would be great if this article contained some background on propositional calculus -- when and where did it originate? What were some of its triumphs and roadblocks? etc. As it is, the article dives deep rather quickly, which is slightly terrifying for those of us who are not well-versed in the subject. --Ori.livneh (talk) 14:14, 9 July 2009 (UTC)

Quantum logic

What about quantum logic?--79.111.146.149 (talk) 19:57, 20 October 2009 (UTC)

What about quantum logic? It doesn't seem to fit here. — Arthur Rubin (talk) 20:00, 20 October 2009 (UTC)

Wrong rendering of mathematics

The main document does not look properly rendered, so can someone with a lot of time clean this up properly so it looks like the logic statements in the talk section. —Preceding unsigned comment added by Veganfanatic (talk • contribs) 02:28, 17 November 2009 (UTC)

This is an example: We sometimes distinguish between propositional constants, propositional variables, and schemata. Propositional constants represent some particular proposition, while propositional variables range over the set of all atomic propositions. Schema, however, range over all propositions. It is common to represent propositional constants by $ A $, $ B $, and $ C $, propositional variables by $ P $, $ Q $, and $ R $, and schematic letters are often Greek letters, most often $ \varphi \,\! $, $ \psi $, and $ \chi $. —Preceding unsigned comment added by Veganfanatic (talk • contribs) 02:31, 17 November 2009 (UTC)

You have set up your preferences, so that it shows this way. Go to Special:Preferences, click Appearance and you will see, tha you have "Leave it as TeX (for text browsers)" under Math. You can change this, the default is "HTML if very simple or else PNG". Svick (talk) 02:48, 17 November 2009 (UTC)

Models

I beginning at logic so forgive me for asking stupid questions. When we define what a formal system is, we are talking in the metalanguage, so the definition is like a theory. Are things like propositional logic and first order logic models of our meta theory of formal system? It's confusing because set theories like ZF are theories in first logic and they exhibit models; i.e. a model of a model. Money is tight (talk) 14:43, 5 January 2010 (UTC)

These are different senses of the word "model". For example, ZFC "models" set theory in the same way that Newtonian mechanics "models" the behavior of falling apples. On the other hand, a "model" of a first-order theory (also called a structure) is a specific technical concept. For additional general questions, you should ask at the Mathematics reference desk, where there are more people available to give answers. — Carl (CBM · talk) 16:12, 5 January 2010 (UTC)

Ok I think I got the word model confused. Everyone has an intuitive notion of examples of a definition, so I think first order theories are just examples of our definition of formal systems, whereas model refers to the technical concept. Money is tight (talk) 19:00, 18 January 2010 (UTC)

Basic and derived argument forms descriptions

In the section on "Example 2: Natural deduction system" the description part of the rules is sometimes misleading. E.g. distribution of conjunction over disjunction says that the "turnstile" meta-statement states an equivalence between the formulas flanking the turnstile. That's strictly false. Either make the meta-statement an equivalence (by using left and right turnstiles back-to-back) or rephrase the descriptions to be unidirectional implications. Nortexoid (talk) 10:21, 6 October 2009 (UTC)

In the same section, the article conflates reductio ad absurdem with negation introduction. This is wrong - negation introduction is intuitionistically valid while reductio ad absurdem is not. Negacthulhu (talk) 9:20, 4 July 2010 (UTC)

I tried to fix Negacthulhu (talk · contribs)'s complaint. Is that OK?

The other is now in a separate section "Basic and Derived Argument Forms". I am not sure that there is really a problem there. JRSpriggs (talk) 19:07, 4 July 2010 (UTC)

"Reductio ad absurdum" may refer to either of two rules:

1. From $p\vdash \bot \,,$ infer $\neg p\,;$ or
2. from $\neg p\vdash \bot \,,$ infer $p\,.$

The first is intuitionistically valid and amounts to negation introduction. The second combines that with double negation elimination, becoming intuitionistically invalid. JRSpriggs (talk) 19:40, 4 July 2010 (UTC)

Decidability

I guess one should state that this logic is decidable (not like predicative logic), thanks to truth table.

I just really doesn't know where to put it

--Arthur MILCHIOR (talk) 03:51, 10 May 2010 (UTC)

I assume that you are taking "decidable" to mean that the set of logical theorems is recursive, not merely recursively enumerable.

The decidability of propositional logic can be deduced from its completeness (and, as you say, the decidability of truth tables). So perhaps the section on completeness is an appropriate place to mention it.

By the way, classical first-order predicate logic is also decidable and complete. See Gödel's completeness theorem.

The incompleteness of any consistent recursively-enumerable extension of arithmetic is relative to one particular standard model of the natural numbers. While the completeness of classical first-order predicate logic is relative to the class of all models (including non-standard models). JRSpriggs (talk) 06:20, 10 May 2010 (UTC)

Actually, the incompleteness is not related to the standard model, at least as I see it. But I could be wrong. — Arthur Rubin (talk) 07:45, 10 May 2010 (UTC)

To Arthur: If one defines "completeness" as a formalist might as $\forall \phi (\operatorname {Provable} (\phi )\lor \operatorname {Provable} (\lnot \phi ))\,,$ then it does not depend on models. But that would be giving a different meaning to "completeness" than was used in the other cases of propositional and predicate logic, i.e. if a sentence is true in all appropriate models, then it is provable. I think that one can use that same meaning (as I was trying to do) by restricting attention to just the standard model of arithmetic in the case of the incompleteness theorems. JRSpriggs (talk) 15:17, 10 May 2010 (UTC)

Re JRSpriggs: Higher up, I think you said "decidable and complete" when you meant to say "semidecidable and complete".

Re Arthur, the claim that the Goedel sentence is independent of PA does not (directly) refer to models, but the claim that it is "true" has to refer to some model, because truth is only defined relative to a model. Of course the model intended is the standard model. — Carl (CBM · talk) 15:30, 10 May 2010 (UTC)

To CBM: Thanks for catching my mistake. Mathematics is constantly reminding me just how stupid and fallible I am. I should not have relied upon my memory, but checked.

Our article on first-order logic says "Unlike propositional logic, first-order logic is undecidable (although semidecidable), provided that the language has at least one predicate of arity at least 2 (other than equality). This means that there is no decision procedure that determines whether arbitrary formulas are logically valid. This result was established independently by Alonzo Church and Alan Turing in 1936 and 1937, respectively, giving a negative answer to the Entscheidungsproblem posed by David Hilbert in 1928. Their proofs demonstrate a connection between the unsolvability of the decision problem for first-order logic and the unsolvability of the halting problem.".

Now that I think about it, if predicate logic were decidable, then one could write a truth predicate for Von Neumann–Bernays–Gödel set theory contrary to Tarski's undefinability theorem. JRSpriggs (talk) 16:43, 10 May 2010 (UTC)

"Basic concepts"

The whole "Basic concepts" section is confusing, rambling, inconsistent with the rest of the article and seems to consist mostly of half-baked definitions of concepts that have their own page. And there isn't a single source! It's badly in need of a rewrite, I think. _R_ (talk) 04:14, 30 October 2010 (UTC)

Undefined operator comes from nowhere and messes up this newbie!

Hey folks. You define one carat, and not the other, then WHAM drop a carrot bomb on us. I was doing truth tables to see if I agreed that the a<->b equated to (a->b)/\(b->a) because that seemed wak, but I didn't even realize the karat had been inverted. And then I just sort of guessed that inverted carat must be exclusive or? Is that true? Someone please fix this! Dr.queso (talk) 03:56, 18 August 2010 (UTC)

The symbol $\land \,$ means "and". The equivalence $a\leftrightarrow b\,$ is indeed the same as the conjunction of implications $(a\rightarrow b)\land (b\rightarrow a)\,.$ JRSpriggs (talk) 14:54, 18 August 2010 (UTC)

The symbol that looks like an A without the horizontal center-bar represents logical AND (easy to remember, /\ similar to /-\, similar to set-theory's "intersection" ⋂) and the inverted symbol \/ is logical OR (the ⋁ comes from a German word and is similar in shape to set-theory's "union" ⋃). There are as many symbols for EXCLUSIVE-OR as there are authors, but the common one, in engineering at least, is a + inside a circle ⊕ -- this is because the exclusive-OR operator behaves as a binary "half-adder" (i.e. a ⊕ b = "a + b without carry") -- you need an additional AND to derive the carry in the case a=1 ⋀ b=1). Be very afraid when reading texts older than about 1960 -- the symbolism is all over the place. BTW the symbols can be gotten from the Microsoft's Arial Unicode MS font via the "Insert Symbol" function available in Word or Excel. Bill Wvbailey (talk) 15:07, 18 August 2010 (UTC)

the "v" comes from the latin "vel", which just means "or" nonexclusively... 69.24.112.147 (talk) 10:34, 5 May 2011 (UTC)

History of Propositional logic

My textbook says it was first developed systematically by Aristotle. I don't like to credit Aristotle with anything good, so I double-checked here. The information is missing altogether. —Preceding unsigned comment added by 72.187.199.192 (talk) 15:38, 6 January 2011 (UTC)

What Aristotle improved was Syllogism, not the kind of mathematical logic described here. JRSpriggs (talk) 21:31, 6 January 2011 (UTC)

Which text book was that, and can you quote?— Philogos (talk) 20:42, 21 April 2011 (UTC)

Aristotle was the first person to systematically explain syllogistic logic, and it was the predominant model used until the late 19th century. Aristotle's logic text is the "Prior Analytics" 69.24.112.147 (talk) 10:39, 5 May 2011 (UTC)

Aristotle is pretty much universally regarded as the founder of logic. However, his logic was mostly syllogistic. The earliest seeds of propositional calculus are, i believe, found in Chrysippus Xenfreak (talk) 21:10, 1 January 2012 (UTC)

Wishing there was more information about the history and development of propositional calculus

I was interested in this topic, found by following other links, and was disappointed to find no information regarding the "history" of propositional calculus. I am left not knowing if these concepts were developed in the 20th century, or in the 19th century (or earlier). Who "invented" it? When was it invented? Why was it invented (what problems does it solve)? What limitations does it have? What impact did it have on other branches of math? What was missing or refined after it's first invention? Are there alternate symbols or systems representing the same ideas? These are all items that I think would be relevant in an encyclopedia, even more than several sections which (to me) would be better served in a math text book on the topic. I'm not suggesting what is there is removed. Anybody out there familiar with this topic capable of adding this content? — Preceding unsigned comment added by 76.9.200.130 (talk) 18:55, 22 July 2011 (UTC)

I have not studied the history, but I have learned a little bit about it along the way. The Laws of Thought by George Boole applies arithmetic (simple algebra on real numbers) to develop the basis of classical propositional logic and Boolean algebra (which are pretty much two different ways of looking at the same thing). Aristotle improved syllogisms, a progenitor of predicate logic of which propositional logic is a simplification (by removing quantifiers over objects). Also see Charles Babbage and the development of computers, a closely related subject. JRSpriggs (talk) 05:48, 23 July 2011 (UTC)

Also see History of logic.

There are very many versions of logic. I suggest you use the templates and categories listed at the bottom of the article to search for them. JRSpriggs (talk) 05:56, 23 July 2011 (UTC)

History section

I've planted the seeds for a history section. I have a bit more to add to it though. If i recall correctly, the stoic propositional calculus was lost and then 'rediscovered' (independently?) by Peter Abelard. I'll have to take a look at my medieval philosophy text before i make this claim though. Ideally, i'd also like to bring in DeMorgan, Boole, Wittgenstein (for truth tables), and maybe pierce. I'd like to end it by introducing Frege's calculus and how it combines propositonal and term based statements. (since i introduced aristotle in the beginning.) — Preceding unsigned comment added by Xenfreak (talk • contribs) 21:41, 1 January 2012 (UTC)

A must-read in this context is Emil Post's 1921 Theory of Elementary Propositions in van Heijenoort 1967:264ff in particular section 2 "Truth table development⁶" with footnote 6 "Truth values, truth functions" on page 267. Whether or not you give Wittgenstein (Tractatus) or Post credit for the modern notion of "truth tables", Post traces the notion back to Jevons and Venn via Lewis 1918. He also mentions Boole and Schroeder. But contemporary symbolic logic relies on the symbolic-logic path from Dedekind, Peano, Frege to Russell 1903 (in particular). Then truth tables, then Veitch and finally Karnaugh's mapping and simplfication methods together with de Morgan's theorems. A destinction between algebraic and symbolic logic is important. They both have their roles to play. Bill Wvbailey (talk) 03:49, 2 January 2012 (UTC)

If you'd like, you can say that truth tables were hinted at by those philosophers, although they were developed by Wittgenstein. I'm not sure how far i'd be willing to go, but feel free to add anything you think is relevant. But remember that we're trying to limit the scope to propositional logic, so i doubt i'd include anyone like godel, cantor, Russell, or anyone else unless they made substantial contributions to symbolic logic. I only wanted to introduce frege to sort of imply 'this is where propositional calculus ends, and where first-order begins.' But again, feel free to add anything you feel is relevant. Xenfreak (talk) 00:18, 5 January 2012 (UTC)

RE Wittgenstein and Post: W didn't "develop" truth tables beyond their meager presentation in Tractatus, in fact as I recall he became an architect for his sister, for a while, then abandoned philosophical logic altogether. To quote from the wikipedia biography: "In his lifetime he published just one book review, one article, a children's dictionary, and the 75-page Tractatus Logico-Philosophicus (1921)." Post, on the other hand, made significant contributions after his PhD paper (the one reprinted in van Heijenoort); he was the mentor and teacher of e.g. Martin Davis, and he contributed to mathematical logic until the 1950's.

However, the truth of the matter will be found in in the bibliographies of the important papers. Here's a start:

Bibligraphy: I have cc's of the original papers of Karnaugh, Veitch, and Shannon and the book of Couturat 1914. Not a one of their footnotes or bibliographic references directly include either Post or Wittgenstein. Here are their references, working backwards:

Maurice Karnaugh 1953, The Map Method for Synthesis of Combinatorial Logic Circuits, A.I.E.E, [I had to pay for this puppy]:

1. The Design of Switching Circuits (book), William Keister, a. E. Ritchie, S. H. Washburn, D. van Nostrand Compnay, New York, N.Y. 1951, chap. 5.

2. Synthesis of Electronic Computing and Control Circuits (book), Staff of the Harvard Computation Laboratory. Harvard University Press, Cambridge, Mass, 1951, chap 5.

3. A Chart Method for Simplifying Truth Functions, E. W. Veitch. Proceedings, Association for Computing Machinery, Pittsburgh, Pa., May 2, 3, 1952.

E. W. Veitch 1952, A Chart Method for Simplifying Truth Functions, Proceedings of the 1952 ACM Annual Conference/Annual Metting, ACM, NY:

Footnote 1: C.E. Shannon, A symbolic Analysis of Relay and Switching Circuits, Trans. A.I. E. E. vol. 57 (1938), pp. 713-723.

Footnote 2: Harvard Computation Laboratory staff, Synthesis of Electronc Computing and Control Circuits, Harvard University Press, 1951

Footnote 3: W. V. Quine [1952] The Problem of Simplifying Truth Function, unpublished paper to appear in the american Mathematical Monthly.

Claude E. Shannon 1938, A Symbolic Analysis of Relay and Switching Circuits, Transactions American Institute of Electrical Engineers, vol 57, 1938, Washington D.C. Reprinted in Claude Elwood Shannon, Collected Papers, IEEE Press, New York:

1. "A complete bibliography of the literature of symbolic logic is given in the Journal of Symbolic Logic, volume 1, number 4, December 1936. Those elementary parts of the theory that are useful in connection with relay circuits are wll treated in the two following references."

2. The Algebra of Logic, Louis Couturat. The Open Court Publishing Company.

3. Universal Algebra, A. N. Whitehead. Cambridge at the University Press, volume I, book III, chapters I and II, pages 35-42.

4. E. V. Huntington, Transactions of the American Mathematical Society, volume 35, 1933, pages 274-304. The postulates refered to are the fourth set, given on page 280.

Edward V. Huntington 1933, New Sets of Independent Postulates for the algrebra of Logic, with Special Reference to Whitehead and Russell's Principia Mathematica, http://www.ams.org/journals/tran/1933-035-01/S0002-9947-1933-1501684-X/S0002-9947-1933-1501684-X.pdf.

This comes with a huge bibliography on the first two pages of the document, the following are the names of the authors (with repeats, in the order of presentatation):

Schröder, A. N. Whitehead, E. V. Huntington, Schröder, A. Del Re, Sheffer, B. A. Bernstein, L. L. Dines, B. A. Bernstein, B. A. Bernstein, J. G. P. Nicod, N. Wiener, C. I. Lewis, H. M. Sheffer, A. N. Whitehead and B. Russell, Principia, H. M. Sheffer, Paul Bernays, B. A. Bernstein, D. Hilbert and W. Ackermann, Alfred Tarski, Kurt Gödel, Kurt Gödel, J. Lukasiewicz and A. Tarski, J. Lukasiewicz, A. B. A. Bernstein, Jörgen Jjárgensen, E. V. Huntington, P. Henle, B. A. Bernstein, C. I. Lewis and C. H. Langford.

B. A. Bernstein 1929 Whitehead and Russell's Theory of Deduction as a Mathematical Science http://www.ams.org/journals/bull/1931-37-06/S0002-9904-1931-05191-0/S0002-9904-1931-05191-0.pdf

Bernstein converts what he calls the "theory" of PM to his notion of a mathematical "science" in the way that he converted the "theory of deduction" in Boolean (algebraic logic) to a mathematical science that consists of a system (K, ', +) [he intentionally orrows the signs ' and + from Boolean logic: (K, ~, V) would be the symbols of PM]. The system consists of an undefined class K of elements p, q, r . . . , a unary operation symbolized by ' on the K-elements and a binary operation on the K-elements p, q. There is the "supposition" of a unique element that he calls it "1" (aka "truth" cf p. 487). There is another symbol " = " which he asserts "is not [part of the theory], and so is free from the criticsm expressed in the preceding section" (p. 487, on p. 484 he discusses this notion). From this system of symbols he then derives the 8 postulates that correspond to the postulates found in PM, the first of which is a symbolic version of modus ponens. He believes he has clearly separated the ideas inside the theory and the ideas that are outside it (i.e. " = "). With regards to this notion of "ideas and propositions thare are outside [the theory]" he cites two of his papers in a footnote on page 484. These are the only two cites in the paper excepting PM 2nd edition.

E. J. McCluskey 1965 Introduction to the Theory of Switching circuits, McGraw-Hill Book Company, LCCCN: 65-17394.

Chap 3 (Switching Algebra) references 15 publications including:

1. Shannon 1938

Chap 4 (Simplification of Switching Functions) references 16 publications including these:

1. Veitch 1952

2. Karnaugh 1953

3. Quine, W. V.: The Problem of Simplifying Truth Functions, Am. Math. Monthly, vol. 59 no. 8, pp. 521-531, October 1952

Interestingly, Shannon's treatment is mostly Boolean, with a smattering of symbolic logic. In fact the postulates on page 471 are given as Boolean algebra e.g. 1.a 0*0=0, 1.b. 1+1=1, [etc]. He goes on to discuss Analogue with the Calculus of Propositions (page 474) where he states: "E. V. Huntington⁴ gives the following set of postulates for symbolic logic [etc]". De Morgan's theorems appear in a mixed Boolean-Symbolic form (page 474) e.g. he uses X+Y, XY, and X' (logical NOT). Shannon is using the symbolism of Couturat 1914 i.e. the X+Y, XY, X'.

Couturat 1914 can be downloaded from www.books.google.com. With regards to the influence on Couturat who influenced Shannon who influenced Veitch who influenced Karnaugh, here's a quote re the history of symbolic logic, from Couturat (but who influenced Quine? of the Quine-McClusky method) -- the whole preface is quite useful, actually:

"LEIBNIZ thus formed projects of both what he called a characteristica universalis, aud what he called a calculus rationator; it is not hard to see that these projects are interconnected, since a perfect universal characteristic would comprise, it seems, a logical calculus. LEIBNIZ did not publish the incomplete results which he had obtained, and consequently his ideas had no continuators, with the exception of LAMBERT and some others, up to the time when BOOLE, DE MORGAN, SCHRODER, MacCoLL, and others rediscovered his theorems. But when the investigations of the principles of mathematics became the chief task of logical symbolism, the aspect of symbolic logic as a calculus ceased to be of such importance, as we see in the work of FREGE and RUSSELL. FREGE'S symbolism, though far better for logical analysis than BOOLE'S or the more modern PEANO'S, for instance, is far inferior to PEANo's symbolism in which the merits of internationality and power of expressing mathematical theorems are very satisfactorily attained- in practical convenience. RUSSELL, especially in his later works, has used the ideas of FREGE, many of which he discovered subsequently to, but independently of, FREGE, and modified the symbolism of PEANO as little as possible. Still, the complications thus introduced take away that simple character which seems necessary to a calculus, and which BOOLE and others reached by passing over certain distinctions which a subtler logic has shown us must ultimately be made." (Couturat 1914: Preface pages VI-VII)

There are others in the footnotes e.g. 1 Cf. A. N. WHITEHEAD, A Treatise on Universal Algebra with Applications, Cambridge, 1898; Venn, Peirce, Ladd-Franklin, etc etc.

BillWvbailey (talk) 03:10, 6 January 2012 (UTC)

If you go to the wikipedia article for truth table you'll see that the very last sentence is " Ludwig Wittgenstein is often credited with [truth table's] invention in the Tractatus Logico-Philosophicus" which is cited. I didn't intend for this to be a big debate. I don't think Wittgenstein's contributions to symboic logic were that great compared to his predecessors or contemporaries. However, as someone who's uses truth tables, and who's wondered who invented them, i think it's worthy to include wittgenstein in the history, as minute as his contribution may be. — Preceding unsigned comment added by Xenfreak (talk • contribs) 02:03, 6 January 2012 (UTC)

I agree it seems a minor quibble, but I'm not going to accept a rumor. Just because wikipedia states it is not a cause for celebration. I may have to edit that page to set the record straight: here are the facts -- Post's PhD thesis was finished in 1920 and published in 1921 (cf van Heijenoort), Tractatus appeared in 1921 and was translated in the English language in 1922 by Ogden and Ramsey (cf Monk 2005). The apparent (as-yet-to-be verified) truth is that the development was independent and simultaneous. I'm not convinced either were the first, per the quote from Post. And I've seen the tables somewhere in the late 1800's Venn or Jevons or somewhere (I'll search). Plus the now-huge bibliography above mentions neither. And really until further notice the point is moot -- I haven't been able to convince myself that either had influence on the development of symbolic logic in the 20th C. The only citation of either that I know of, tenuous as it is, is via the bibliography in the 2nd edition of Principia Mathematica where Russell cites Wittgenstein (his erstwhile student and bugbear). But this is in the context of the axiom of reducibility, not "truth tables". I know little about Tarski and Quine, so connections may be there. My advice to both of us is to leave W and Post out of the article until we know more. It appears that far more influential is de Morgan and Couturat + Huntington via Shannon; for example, in a table on page 475 he equates the 'Interpration in relay circuits' to 'Interpretation of the Calculus of Propositions'. Bill Wvbailey (talk) 03:10, 6 January 2012 (UTC)

sorry, i just saw this comment. I'll edit wittgenstein out (for now.) But to keep him out, you'll have to convince me: why doesn't the reference in the truth-tables article that wittgenstein being considered the father of truth-tables suffice? Xenfreak (talk) 03:40, 6 January 2012 (UTC)

Here's why I discourage us from crediting either until we understand better. I just found three references: (1) Hans Reichenbach 1947 Elements of Symbolic Logic, Dover Publications, Inc. NY, ISBN:0-486-24004-5, (2) Alfred Tarski 1946/1961 Introduction to Logic and to the Methodology of Deductive Sciences, Dover Publications Inc, NY, ISBN: 0-486-28462-X (pbk.), and Kleene 1952 (see full citation below). The first two ultimately attribute the notion of truth functions (tables?) to Peirce; Kleene attributing 2-value tables to Post 1921. The first two authors are trivializing "truth tables", considering them to be just manifestations of "truth functions":

(1) From Reichenbach:

"[footnote 1] ¹Truth tables were used by L. Wittgenstein, Tractatus Logic-Philosophicus, Harcourt, Brace, New York, 1922, p. 93, and by E. L. Post, Amer. Journal of Math., XLIII, 1921, p. 163. Materially, the definition of propostional operations in terms of truth and falsehood was used earlier, for instance in B. Russell and A. N. Whitehead, Principia Mathematical, Vol. I., 1910, p. 6-8. Furthermore, C. S. Peirce employed this definition; cf footnote on p. 30." (page 27 in Reichenbach 1947)

(2) From Tarski:

"Chapter 13. Symbolism of sentential calculus; truth functions and truth tables

"There exists a certain and simple and general method, called METHOD OF TRUTH TABLES OR MATRICES, which enabls us, in any particular case, to recognize whether a given sentence from the domain of the sentential caluclus us true, and whether, therefore it can be counted among the laws of this calculus.⁵" [footnote 5: "This method originitates with PEIRCE (who has already been cited at an earlier occasion; cf. footnote 2 on p. 14." (but this reference only mentions that CH. S. PEIRCe (1839-1914) was 'an outstanding American logician and philospher"). (page 38, both text and footnote; capitals in the original).

(3) Kleene 1952 Introduction to Meta-Mathematics, North-Holland Publishing Company, Amsterdam NY, ISBN 0-7204-2103-9, credits Lukasiewicz 1920 for 3-variable tables, and Post 1921 for two variable tables (cf p. 140). Post 1921 (same as the above) is referenced by Kleene on page 531; Wittgenstein is not to be found in the extensive references. BillWvbailey (talk) 04:41, 6 January 2012 (UTC)

i was linked to this article:

http://frege.brown.edu/heck/pdf/unpublished/TruthInFrege.pdf

In it it says

"Frege has sometimes been credited with the discovery of truth-tables (Kneale and Kneale, 1962, pp. 420, 531; Wittgenstein, 1979b, pp. 135ff), and something akin to truth-tables is indeed present in Frege’s early work."

This are sources from Wittgenstein and Kneale, who we include. It says this at the bottom of page 9, Sentential Connectives as Truth Functions. Later in the page, however, the section concludes:

"That said, so far as we know, nowhere in his later writings does Frege give the sort of 'tabular' account that Wittgenstein and the Kneales mention, so there is no real basis for attributing the discovery of truth-tables to Frege. 13" (emphasis in original text.)

And in the footnote on the bottom of page 10, it says:

"Moreover, Frege never considers truth-tables for arbitary formulae, but only for the simplest cases, and there is no indication that he realized, as both Wittgenstein and Post (1921) did, that truth-tables can be used to determine the validity of an arbitrary propositional formula. As is now widely recognized, then, it is Wittgenstein and Post who deserve the real credit for the discovery of truth-tables."

So perhaps, the best thing to say would be to say that the seeds of truth tables were in Frege's work, but the actual tables themselves were developed by Wittgenstein and Post. Xenfreak (talk) 05:23, 6 January 2012 (UTC)

EDIT

i was also linked to this article

http://digitalcommons.mcmaster.ca/cgi/viewcontent.cgi?article=1219&context=russelljournal

It mentions Russell's use of truth-tables which predates Post and Wittgenstein. I think it would be best to mention all four people (russell and frege in the "pre-truth-tables" and Post and Wittgenstein for their tabular development with the quote that the article concludes with

"It is far from clear that anyone person should be given the title of "inventor" of truth-tables"

This is how i'll develop the article for now. If any further information arises, let me know, and i'll alter the history section accordingly. (and you're free, and more than welcome, to do so yourself if you'd like. Xenfreak (talk) 06:15, 6 January 2012 (UTC)

I put all the considerations for truth tables, and their controversy in the section. I cited all the major claims. What i didn't do, however, was copy the citations from the PDF i used as he (Shosky) cited them. I just ended up using the PDF itself (i.e. instead of citing Anscombe, Quine, etc. I just cited the PDF.) This is fine for me, but if anyone in particular is feeling very persnickety about citing my claims in this way, let me know. It won't take more than a moment to copy over the actual citations. Xenfreak (talk) 07:05, 6 January 2012 (UTC)

---

What you wrote looks quite good and it addresses the problem well. This content should also should go into the article Truth tables perhaps in more detail, e.g. the cites I found + yours. Since you started I'll let you finish and then do I'll some editing and make additions. Your sources are interesting, to say the least.

Distinguish "truth table" versus truth functions: Authors seem to be mixing "truth table" with an "algebra of switching"; see McCluskey reference above and below. What I do think you/me should do is be sure to clearly separate out the graphical expedient of a "truth table" for evaluation of truth functions, as opposed to the notion of truth function itself (as it developed historically), i.e. a propositional function that evaluates to {truth, falsity} (this being Russell's usage in PM, that he cites to Frege).

Boolean Algebra of classes versus a logic of truth-functions: Boole developed a theory of classes as opposed to [who? Venn in his 1881 Symbolic Logic? Peirce? Frege? Russell 1903? Russell-Whitehead PM? All?] developing symbolic (bivalent) logic, i.e. with truth and falsity. For Boole: "Let the symbols 1 and 0 be respectively used to denote the Universe [of discourse] and Nothing" (p. 89) and "If then we construct an Algebra in which the only particular symbols of number shall be 0 and 1 and in which every general symbol as x, y etc. shall be understood to admit only of the above special determination . . ." (p. 91*).

• From his On the Foundations of the Mathematical Theory of Logic' to be found in Grattan-Gunness and Gerard Bornet (ed.) 1997 George Boole: Selected Manuscripts on Logic and its Philosophy, Birkhauser Verlag, , Basel Switzerland, ISBN 3-7643-5456-9.

The more I read about this the more important this particular distinction seems, although without a look at e.g. Quine and the problem of mixing "truth" and "falsity" into a symbol-system, I need to get cc's of Peirce.

Confusion of conceptual notions, cf Huntington's 1931 basis set of axioms for both "Boolean Algebra of classes" and "Symbolic Logic of truth functions": This confusion of systems (logic of class membership versus logic of truth-functions) needs to be woven into the article in some detail and developed, because it is from the Boolean notation via Couturat [to Shannon to Veitch to Karnaugh that we now have what we engineers were taught how to manipulate truth tables, and why many of us learned with the Boolean notation, not the symbolic-logic notion. From Shannon via Huntington we got the mixing of the two theories. Here's Huntington:

"Three sets of independent postulates for the algebra of logic, or Boolean algebra, were published by the present writer in 1904. . . . In the meantime, the primitive propositions of Section A of the Principia Mathematica (1910) were expressed in terms of a class called the class of "elementary propositions," a binary operation called "disjunction," and a unary operation called "negation" ; and Bernstein has recently shown (June, 1931) how these primitive propositions can be expressed in abstract mathematical form in terms of (K, +, '). Since the relation between the theory of the Principia and the theory of Boolean algebra has been the subject of some discussion, it becomes a matter of interest to construct a set of independent postulates for Boolean algebra explicitly in terms of (K, +,'), for comparison with the Principia." (Huntington 1931:274ff).

So it looks like Bernstein is very important here. [Note added 17 January 2012: Yes, this is a signficant paper. But I can't find the formation rules, i.e. the syntactic rules. These seem tacit. See more at the references listed above. Wvbailey (talk) 20:22, 17 January 2012 (UTC)]

A confusion of notations: No wonder students get confused and mix the two up. The notations have been used interchangeably, the algebraic xy, x+y, bar-x or x' appears in symbolic truth-functional logic and so does , x & y, x V y, ~x which is clearly symbolic. From what I can see the path from Couturat to the engineers via Shannon to Veitch to Karnaugh is to blame for this: all the notations in these 4 are Boolean in nature. All my engineering texts are in algebraic notation, Notably my E. J. McCluskey 1965. McCluskey was a student of Quine; reference [1] is to you guessed it -- Shannon 1938:

"This algebra will here be called switching algebra. It is identical with a Boolean algebra and was originally applied to switcing circuits [1] by reinterpreting Boolean algebra in terms of switching circuits rather than by developing a switching albebra directly, as will be done here." (p. 66)

When and how did the separation of symbolisms occur? Where did usage of &, V, ~ (or bent-bar) come from? The symbolic notations { V, &, ➙ } is used by Kleene 1952, Reichenbach 1947, and Tarski 1941. The V is used by Herbrand 1930 Investigations in proof theory: the properties of true propositions uses {V, ~ }, Skolem 1928 On Mathematical Logic uses the Boolean set. Goedel 1930 The Completeness of the Functional Calculus uses { V, overbar for negation, &, ➙ }, Goedel 1931 uses { V, ~, ⊃ for implication , & }. So something happened in about 1928-1930 (a need to separate the algebraic +, - and * from the logical?) that led to a clear distinction between "Boolean Algebra of classes" and "Symbolic logic of (bivalent) truth-functions".

Wvbailey (talk) 18:20, 6 January 2012 (UTC)Bill

Sorry for my delay. Unfortunately, i expect to be very busy starting as soon as tomorrow, and probably will lack the time to make these edits. Feel more than free to add in anything you fee is relevent. If i can find some time later today, i'll do the same

Best

-xenfreak — Preceding unsigned comment added by Xenfreak (talk • contribs) 16:16, 8 January 2012 (UTC)

On the Interpretation of the Propositional Calculus

An IP has been adding On the Interpretation of the Propositional Calculus to the external links. It (appears to be) an award-winning Ph.D. thesis (which would not normally be adequate for a reference, although possibly for an external link to point to references), but even if it were a good resource, it isn't a good resource for this article. It might belong in semantics of the propositional calculus (if it existed), or possibly in one of the other articles in the semantics clade. The connection to this article is weak. — Arthur Rubin (talk) 15:25, 21 April 2011 (UTC)

I am the user who has been adding the article mentioned above. (Full disclosure: it is not an award-winning PhD thesis but an award-winning Honours thesis, submitted at the University of Sydney. It won the John Anderson Prize for Best Thesis in Philosophy, and caused me to be awarded a University Medal.)

I appreciate the civilized manner in which Arthur Rubin has made his dispute. I concede that if there were an article for the semantics of the propositional calculus, my link would be best placed there. Since there is not, however, I maintain that my link is well-placed here, and indeed better placed here than on any of the pages existing under the umbrella 'semantics'.

It is not as though the interpretation of the calculus is some out-of-the-way topic only obliquely connected to the topic of the propositional calculus. The interpretation of the calculus is a natural thing for someone to wonder about when they look at this particular Wikipedia article, and this Wikipedia article is also a natural place to go for someone who is wondering about this already.— Preceding unsigned comment added by 123.243.36.225 (talk • contribs) 09:21, April 24, 2011

Hmmm. As not being an expert in the philosophy of the propositional calculus, I decline comment as to the value of the article. It doesn't seem valuable as to modern usage in and relating to mathematical logic, which this article is mostly about. I still think it fits better in Formal semantics (logic) than in propositional calculus. I'm not really sure it's helpful there, either, because of the comparisons between meaning (not formal semantics) of natural-language expressions which are or resemble statements in the propositional calculus.

Because of the relatively low-level (an honours thesis is less "reliable" than a Ph.D. thesis, in general), it couldn't be used as a reference in Wikipedia unless it is referenced favourably in peer-reviewed literature. It may meet WP:EL guidelines, but

Also, per WP:COI, you really shouldn't be adding pointers to your own material. I've asked (in WT:MATH) whether it's proper for me to reference my parents' books and papers in relevant subjects in set theory and mathematical logic, and consensus seems to be it was OK, as they and I are recognized experts in (at least some subfields) of set theory, but I did have to ask.

— Arthur Rubin (talk) 15:56, 24 April 2011 (UTC)

I would argue that the propositional calculus, in addition to being of technological and purely mathematical interest, is also of interest from a philosophical point of view. For a great many students of introductory logic in philosophy departments, this aspect is important. Insofar as this is true, my article is relevant. —Preceding unsigned comment added by 123.243.36.225 (talk) 10:00, 26 April 2011 (UTC)

123.243.36.225 (talk) has made similar edit in articles Philosophy of logic and Philosophy of language : seemingly self-publicity by a student, TG Haze. — Philogos (talk) 23:57, 28 April 2011 (UTC)

Admittedly I do have a double-interest in adding these resources, but I do not think there is a *conflict* of interest. -TH.

Have you read Wikipedia:External links and Wikipedia:Identifying reliable sources? Would it not be more dignified to have your work published in a peer-reviewed academic journal before providing a link to it in these articles? — Philogos (talk) 03:12, 30 April 2011 (UTC)

"...if there were an article for the semantics of the propositional calculus, my link would be best placed there. Since there is not, however, I maintain that my link is well-placed here, and indeed better placed here than on any of the pages existing under the umbrella 'semantics'." There's no requirement for your paper to be a reference anywhere on Wikipedia. If it is needed to reference something asserted in the article, then use it. If it doesn't, then it has absolutely no place. 203.27.72.5 (talk) 03:52, 19 June 2012 (UTC)

Excess implication sign

Is there an error in the last item "Conditional proof (conditional introduction)" there seem to be one too many implies symbols. In other words, shouldn't it say:

"That is, $(p\vdash q)\vdash (p\to q)$." ? This seems to translate what is written in words above.

[If not, then some further explanation is required here.] — Preceding unsigned comment added by 144.32.100.153 (talk) 15:08, 23 January 2014 (UTC)

To 144.32.100.153: Thank you for pointing that out. I have fixed it. JRSpriggs (talk) 16:25, 23 January 2014 (UTC)

Confusion between the "infer that" symbol of the logic ($\vdash$) and the notation for inference rules

Describing a logic involves a notion of "consequence" at 3 levels:

• at the level of formulas, implication aka material implication aka material conditional, etc., depending on the social context of the author, written $A\rightarrow B$ in the current article, reflects that formula $A$ can be derived from formula $B$; such an implication is part of the language of formula of a logic
• at the level of judgements, a sequent $\Gamma \vdash p$ expresses that formula p is derivable from the set of formulas $\Gamma$ (this is sometimes written $\Gamma \rightarrow p$ when implication is itself written differently, e.g. $p\supset q$ as in Buss' article in the Handbook of proof theory); this is also referred to as syntactic logical implication in article logical implication; such a sequent expresses a property of a logic that we express in the meta-language in which we are talking about a logic;
• at the level of derivations, inference rules, conventionally written under the form ${\frac {\Gamma _{1}\vdash A_{1}\qquad \Gamma _{n}\vdash A_{n}}{\Gamma \vdash B}}$ are the basic components of a derivation of a judgement; this is part of the language of derivations of a logic.

I'm not aware of any author using the notation $\vdash$ for inference rules. The Wikipedia articles inference rules and natural deduction themselves both use a bar for inference rules. It should be the same in Section Natural deduction system where a bar should be used instead of $\vdash$.

The difference between $\vdash$ and a bar becomes necessary in the "conditional introduction" rule. It should be ${\frac {\Gamma \cup \{A\}\vdash B}{\Gamma \vdash A\rightarrow B}}$ precisely meaning that if there is a derivation of $B$ from $A$ and from some other formulas in $\Gamma$ using an arbitrary number of inference rules, then we can infer $A\rightarrow B$ from the formulas in $\Gamma$.

The distinction between the three levels above is known from 1935 when Gentzen designed sequent calculus. It is necessary for formulating sequent calculus. When formulating natural deduction, the $\vdash$ notation can be hidden/avoided by using instead dots as in

A

$\vdots$

B

and this is what Gentzen did, followed by Prawitz in his 1965's proof-theoretical study of natural deduction. Nowadays, however, as shown in the current version of the article natural deduction, the sequent notation is used for expressing derivability in natural deduction.

In Hilbert-style systems, the use of a horizontal bar for modus ponens is conventional (and indeed, this is what is done in the modus ponens article). However, the use of a $\vdash$ is not common, even if it is implicitly present, as e.g. in the formulation of the deduction theorem (the current version of the article deduction theorem actually uses it, which is indeed the correct way to state it).

That would be very nice if someone can work on this so that this key article becomes better! Hugo Herbelin (talk) 13:21, 25 March 2014 (UTC) (edited 14:20, 25 March 2014 (UTC)).

An add-on: I overlooked that the notations $p$, $q$, ... are for atoms and that inference rules are currently stated on formulas made of a connective combining atoms. They should apply instead on arbitrary formulas. E.g. conjunction introduction should be From $\Gamma \vdash A$ and $\Gamma \vdash B$, infer $\Gamma \vdash (A\land B)$, i.e. ${\frac {\Gamma \vdash A\qquad \Gamma \vdash B}{\Gamma \vdash A\land B}}$. Hugo Herbelin (talk) 14:20, 25 March 2014 (UTC)

"Our propositional calculus has ten inference rules. " Whose propositional calculus? In the method of assumptions, the number of inference rules can equal the number of theorems, while the lowest number of rules is 7, and it seems like most of the reputable textbooks present systems where there are 7 rules, though sometimes the sets of rules have different elements, if I remember well. — Preceding unsigned comment added by Pernambuco1 (talk • contribs) 16:19, 1 May 2014 (UTC)

Change Page Name OR Opening Sentence

I think that either the page name or the opening sentence should be changed. The page name is "Propositional Calculus" which is slightly at odds with the opening line which reads "Propositional logic...". I know that they're the same thing but a reader new to the topic might not. It certainly looks a little odd in a Google search automatic summary.

I haven't touched the article text/title as I don't know whether this was a deliberate decision.

Thanks for pointing this out. Yes, the opening sentence should reflect the article title. I've updated the lead. --Mark viking (talk) 11:19, 13 January 2015 (UTC)