![]() | This page is an archive of past discussions. Do not edit the contents of this page. If you wish to start a new discussion or revive an old one, please do so on the current talk page. |
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:
Well, which is it?
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
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
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)
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)
I propose moving this article to Classical propositional logic, because:
Some other issues need addressing:
Comment? Charles Stewart 22:11, 13 Nov 2004 (UTC)
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)
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)
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)
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)
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:
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:
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:
I can do all of them, if you, Wikipedians, agree.
Eric 07:05, 11 October 2005 (UTC)
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)
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)
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)
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)
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)
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)
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)
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)
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)
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)
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)
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)
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)
If we are going to go back to axioms and away from natural deduction, I would like to make a suggestion. Use just "→" and "" as primative connectives. All the others can be defined in terms of them. And the axiom schemas might be:
—The preceding unsigned comment was added by JRSpriggs ( talk • contribs) .
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)
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 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 .
Can you beat that? JRSpriggs 02:36, 1 July 2006 (UTC)
JA: Big 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! 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)
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)
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)
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)
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)
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, S0, S1, …, Sn. Let a0, a1, …, an 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)
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:
JA: Proper or popular. It always seems to come to that. Jon Awbrey 03:42, 11 August 2006 (UTC)
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)
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:
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)
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)
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)
What exactly does this mean and is it both true and important?--Philogo 20:44, 10 November 2008 (UTC)
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)
(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)
Is there any special name to this rule? Albmont ( talk) 20:55, 12 March 2009 (UTC)
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)
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)
What about quantum logic?-- 79.111.146.149 ( talk) 19:57, 20 October 2009 (UTC)
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)
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)
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)
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)
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)
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)
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)
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'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)
i was linked to this article:
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)
---
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*).
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:
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:
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)
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 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)
Admittedly I do have a double-interest in adding these resources, but I do not think there is a *conflict* of interest. -TH.
"...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)
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, ." ? 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)
Describing a logic involves a notion of "consequence" at 3 levels:
I'm not aware of any author using the notation 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 .
The difference between and a bar becomes necessary in the "conditional introduction" rule. It should be precisely meaning that if there is a derivation of from and from some other formulas in using an arbitrary number of inference rules, then we can infer from the formulas in .
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 notation can be hidden/avoided by using instead dots as in
A |
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 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 , , ... 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 and , infer , i.e. . 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)
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.
![]() | This page is an archive of past discussions. Do not edit the contents of this page. If you wish to start a new discussion or revive an old one, please do so on the current talk page. |
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:
Well, which is it?
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
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
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)
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)
I propose moving this article to Classical propositional logic, because:
Some other issues need addressing:
Comment? Charles Stewart 22:11, 13 Nov 2004 (UTC)
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)
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)
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)
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)
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:
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:
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:
I can do all of them, if you, Wikipedians, agree.
Eric 07:05, 11 October 2005 (UTC)
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)
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)
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)
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)
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)
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)
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)
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)
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)
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)
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)
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)
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)
If we are going to go back to axioms and away from natural deduction, I would like to make a suggestion. Use just "→" and "" as primative connectives. All the others can be defined in terms of them. And the axiom schemas might be:
—The preceding unsigned comment was added by JRSpriggs ( talk • contribs) .
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)
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 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 .
Can you beat that? JRSpriggs 02:36, 1 July 2006 (UTC)
JA: Big 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! 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)
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)
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)
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)
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)
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, S0, S1, …, Sn. Let a0, a1, …, an 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)
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:
JA: Proper or popular. It always seems to come to that. Jon Awbrey 03:42, 11 August 2006 (UTC)
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)
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:
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)
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)
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)
What exactly does this mean and is it both true and important?--Philogo 20:44, 10 November 2008 (UTC)
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)
(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)
Is there any special name to this rule? Albmont ( talk) 20:55, 12 March 2009 (UTC)
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)
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)
What about quantum logic?-- 79.111.146.149 ( talk) 19:57, 20 October 2009 (UTC)
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)
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)
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)
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)
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)
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)
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)
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'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)
i was linked to this article:
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)
---
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*).
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:
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:
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)
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 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)
Admittedly I do have a double-interest in adding these resources, but I do not think there is a *conflict* of interest. -TH.
"...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)
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, ." ? 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)
Describing a logic involves a notion of "consequence" at 3 levels:
I'm not aware of any author using the notation 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 .
The difference between and a bar becomes necessary in the "conditional introduction" rule. It should be precisely meaning that if there is a derivation of from and from some other formulas in using an arbitrary number of inference rules, then we can infer from the formulas in .
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 notation can be hidden/avoided by using instead dots as in
A |
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 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 , , ... 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 and , infer , i.e. . 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)
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.