Talk:Propositional calculus
From Academic Kids
There is something misleading in calling a propositional calculus an axiomatic system and then presenting rules for predicate calculi that don't have axioms. Most or all of the rules here are for natural deduction systems. Either an alternative, axiomatic approach should be canvassed (and the issue of independence of axioms, etc., be discussed), or else it should be clearly stipulated that "axiomatic system" can apply to systems with an empty axiom-set. (A perverse but, I suppose, allowable usage.)
From the article:
- Disjunction Elimination: From wffs of the form ( φ ∧ <-SHOULDN'T THIS BE ∨?? ψ ), ( φ → χ ), and ( ψ → χ ), we may infer χ.
Well, which is it?
- It's or, as you already corrected (I got an edit conflict). If it were AND, we would only need either the second or the third wff to derive Chi. Jeronimo
Since this article is only about propositional logic and doesn't say anything about first-order logic or anything else along those lines, shouldn't it be titled "propositional logic"? Michael Hardy 01:08 Mar 21, 2003 (UTC)
It would probably be better if more information on the other calculi was added. -- Derek Ross
- Symbolic logic have these info. -- looxix 01:43 Mar 21, 2003 (UTC)
- Delete logical calculus to rename propositional calculus to it. Thanks
- I've repointed the redirect, probaly better than deleting a valid title jimfbleak
- Taku: do you realise it was originally at logical calculus until looxix moved it? There's a brief naming discussion on the talk page you should probably contribute to, rather than making a unilateral decision to move. -- Tim Starling 15:51 18 May 2003 (UTC)
- Actually, I am not so sure the difference between propositional calculus and logical calculus (yeah, and I am working on logic articles now, what an arrogant), so I leave this for other folks. -- Taku 16:28 18 May 2003 (UTC)
I am currently referencing this page on my site ( http://us.metamath.org/ ) but have some mixed feelings about it, since some of the symbols do not render in Internet Explorer. While I personally use Mozilla, perhaps 85% of my visitors use IE. For a while I avoided links to Wikipedia for this reason, but the content has gotten quite good and now I prefer it.
While I don't wish to impose any editorial decisions on the part of the author(s), are there guidelines on Wikipedia w.r.t. the use of math symbols? Should the users of IE be given consideration?
The Unicode symbols that don't render in IE on the 'Propositional calculus' page are '∧' and '∨'. The others seem to render OK.
On the 'First-order predicate calculus' page 3 additional symbols don't render in IE: '∀', '∃', and '∈'.
One possibility is to use GIFs for these five symbols, until Microsoft fixes IE. One source of them are the GIFs on my page http://us.metamath.org/symbols/symbols.html .
Norm Megill nm at alum.mit.edu
- Hello, Norm -- I'm a big fan of metamath! It seems to me that this is not a content problem, but a rendering problem. Do you know what versions of IE this has problems with, eg 5.0, 5.5, 6.0?
- One solution: We use two ways of doing math here -- in-line Unicode, and TeX. For IE readers, we could if we wanted, render the characters that IE does not support to GIFs/PNGs, and force full rendering of TeX math to images for users of that browser. But this will screw up our caching system, which tries to serve the same page for all browsers to users who are not logged in.
- Another solution: We could post-process cached pages to do this, at the cost of extra compute when being visited by IE. (Which is, unfortunately, the most common browser...)
- I'm not sure what the correct answer is... -- The Anome 17:38 9 Jun 2003 (UTC)
- By the way, thanks Norm, for releasing those bitmaps into the public domain. The Anome 17:42 9 Jun 2003 (UTC)
- One possible solution would be to use the corresponding TeX markup for these sections. Except in the most basic cases, these are automatically converted to PNG (depending on user preferences - which can be configured to always use PNG). Using TeX markup for inline stuff (in the middle of a sentence) is generally undesirable, since it creates spacing issues, but sometimes a clever rephrasing of the article can get the TeX markup into its own line to avoid this problem. (Doh, someone else beat me to it! :) -- Wapcaplet 17:41 9 Jun 2003 (UTC)
- (Though, I just remembered, some versions of MSIE, 4.0 and some versions of 5.x if I recall correctly, do not support PNG... erg.) -- Wapcaplet 17:48 9 Jun 2003 (UTC)
The IE version I have is 6.0.2600. But the real problem is Microsoft's WGL4 Unicode font which (per their own spec) simply omits these 5 symbols (among others). Even though there have always been slots for them in the Unicode standard, Microsoft inexplicably did not bother bringing them over from WGL4's lowly predecessor, the Symbol font. Apparently they didn't consider them to be of any use. (Let me refrain from any remarks about "math literacy"...) This messed up my own plans to convert the Metamath site to Unicode a couple of years ago.
About the GIFs on my site: Even though my symbol bitmaps were originally created with the GIMP, any that are on public display were purposely reprocessed into GIFs by a Unisys-licensed product in order to make them (presumably) legal. I have been tempted to convert them to PNG but don't know how well older browsers handle transparency (if, as you indicate above, they handle PNGs at all), which is important for my site. In any case the bitmaps are the same regardless of how they are encoded, and I suppose anyone could re-encode them into their preferred format.
Of course I don't know the best solution for Wikipedia but just wanted to make sure there is an awareness of the issue. In the meantime on my site I am recommending Mozilla to read Wikipedia. Thanks for your responses.
Norm Megill nm at alum.mit.edu
Shouldn't this be in there somewhere, or can it be already worked out from the article somehow?
From wffs of the form ¬ ( φ ∨ ψ ) we may infer ( ¬ φ ∧ ¬ ψ ).
From wffs of the form ¬ ( φ ∧ ψ ) we may infer ( ¬ φ ∨ ¬ ψ ).
كسيپ Cyp 00:37 18 Jun 2003 (UTC)
- Well, those wouldn't be considered basic rules. They can be derived through reductio and disjunction elimination, though... Evercat 00:44 18 Jun 2003 (UTC)
- Still, one thing I was wondering was whether the move [ A v B, -A, therefore B ] wasn't considered a basic rule? When I was taught logic it was recognised as a 2nd type of disjunction elimination. But it's not given on that page. Evercat 00:49 18 Jun 2003 (UTC)
- The problem is just that the choice of basic and derived rules is really quite arbitrary, especially in such a simple logic. The article as t stood said, "This is the propositional calculus," "These are the rules of derivation," which is wildly misleading. Any rule in only as basic as some textbook writer chooses to make it. (You can get a sound, complete propositional calculus whose only basic rule is modus ponens. And so forth.)
- Incidentally, though, the difference between two forms of "disjunction elimination" raises issues of concern to Intuitionism. But this is not an intuitionistic calculus.
Shouldn't we try to clearly state the difference between syntax, semantics and proof rules? CSTAR 23:29, 18 May 2004 (UTC)
'Letters of the alphabet are wffs.' The problem with this is that there are only 26 letters of the alphabet, and really we need an infinite supply of letters, e.g. x, x', x, x', etc. As you can always put another ' on, we never run out.--Publunch 11:21, 6 Nov 2004 (UTC)
| Contents |
Move proposal
I propose moving this article to Classical propositional logic, because:
- I think it is the most common name, by quite a margin;
- It means the article need not, as it does not, deal with rival propositional logics, such as intuitionistic logic and quantum logic. As it stands, the article fails to do justice to its name.
- Since the article outlines both a natural deduction system and Hilbert type axiomatic system under the names of Calculus and Alternative Calculus respectively, it should be clear that there is more than one type of calculus for propositional logic. Second, the article, up to and including the section Grammar, is not about 'classical logic specifically, as a distinction between intuitionistic and classical logic would only be made by giving their respective axiomatizations (or rules for a sequent calculus or semantic tableaux). Hence I feel the most appropriate title of the article is simply Propositional logic. (And under the calculus sections, make explicit mention that they are for classical systems.) Nortexoid 13:07, 21 Mar 2005 (UTC)
Some other issues need addressing:
- Currently propositional logic is a redirect to propositional calculus, without any suggestion that the two terms are not synonyms. This, as I understand the terms logic and calculus, is misleading: a logic is a certain kind of consequence relation, and a calculus is an effective method for understanding (in particular) a logic. In particular, the natural deduction calculus is called the natural deduction system, obscuring the fact that the current article is presnting a particular calculus as if it were the propositional calculus. This is not OK.
- But as I've said above, since it gives an alternative calculus (Hilbert style), that is not the case. Nortexoid 00:47, 22 Mar 2005 (UTC)
- Instead, we need a more refined taxonomy, dealing with the above issue, and also with
- classical logic (currently, a redirect to logic, which is OK, but not ideal);
- classical propositional logic is blank (please don't start this page: if the move goes ahead it will just need to be deleted).
- Naming alternative calculi of propositional logic, eg. Hilbert's calculus, sequent calculus, tableau calculus. Also should make clear that the given natural deduction calculus is just one of a rather large varierty of such frameworks.
Comment? ---- Charles Stewart 22:11, 13 Nov 2004 (UTC)
Formatting
It's inconsistent. Some is in Unicode, some is in ASCI, and the rest is in TeX. Unicode should be used, if at all, only inline with text (i.e. not on lines by itself, e.g. for derivations/axiom lists). Nortexoid 04:03, 18 Mar 2005 (UTC)
- I'd say that TeX is to be preferred whenever it is appropriate, since the WP software allows users to govern whether it is typeset or transformed into Unicode. I don't care enough to make a start with making the logic articles more consistent in this respect; it's on my very-far-from-urgent list. Much more urgent, I think, is the move I proposed above: do you have the first comment? ---- Charles Stewart 09:59, 18 Mar 2005 (UTC)
- See Wikipedia talk:WikiProject Mathematics/Archive4(TeX) for a very long and very detailed discussion on the subject. If anybody has more questions, just ask them at Wikipedia talk:WikiProject Mathematics (that's the headquarters of Math on Wikipedia). Oleg Alexandrov 10:15, 18 Mar 2005 (UTC)
- Ok, interesting pro/con discussion for use of TeX, but there is at least one non-aesthetic reason for using unicode -- it is cut/paste-able. One aesthetic reason for using it inline with text is that the font style and size is consistent with the text. Nortexoid 13:12, 21 Mar 2005 (UTC)
- Sorry for the late reply, I missed this for some reason. What I should have said above, is, as you noticed, the issue of TeX vs. html. As far as Unicode is concerned, I agree that one better not use it. Oleg Alexandrov 18:42, 20 Apr 2005 (UTC)
Types/Styles of propositional calculus?
This is coming from someone who knew little of propositional calculus and is using Wikipedia as an introduction. I have run into something that caused my a deal of confusion. All of the off-site references about propositional calculus, including MetaMath and two freely available PDF books on the subject, refer to a three-axiom system of prepositional calculus as if it were the 'standard' way of defining the axioms. I understand that there are many ways to write the axioms which are functionally identical, but it would perhaps be helpful to give names to the more common versions. In particular, the one MetaMath uses contains these three axioms:
- φ → (χ → φ)
- (φ → (χ → ψ)) → ((φ → χ) → (φ → ψ))
- ( ( ¬ χ ) → ( ¬ φ ) ) → ( ( ( ¬ χ ) → φ ) → χ )
These correspond to THEN-1, THEN-2, and some unspecified axiom from the article. This confused me for a good long time.
Kutulu 20:35, 3 Jun 2005 (UTC)
Why metamath is not a good link for this article
In general, I don't think we should treat tools for logicians as regular references, but instead we should have them as links from specialised articles. Different editors might reasonably disagree on this, but I find in is more in keeping with the tone of being an encyclopedia and not a web directory. In any case, metamath is a tool that, while it can handle propositional logic as a special case, is designed to be used with predicate logic and has no special support for propositional logic. I don't see any case for having it as a link from this article. --- Charles Stewart 17:05, 6 Jun 2005 (UTC)
- I'm not sure what you mean by having "no special support" for propositional logic. In particular, their interactive "Metamath Solitaire" tool uses only a three-axiom system for propositional logic as the default set of axioms -- you need to explicitly select the additional axiom sets for predicate logic, ZFC set theory, etc as additional axioms. Given that it's just an external link, and that it is related to propositional logic, I don't see how it's harmful to have the link there. It includes a good introduction to propositional logic as the base for higher set theory, and helps demonstrate how the various forms of logical calculus (if that's the right term) as built up from each other. Though, it's just a link so I'm not going to argue any more than this :) Kutulu 15:50, 8 Jun 2005 (UTC)
- Propositional logic has good properties that predicate logic does not, which are exploited by tools for propositional logic, like decidability, completeness wrt. truth tables. The point is that any tool for predicate logic, such as most of the 27 links in this directory (http://dmoz.org/Science/Math/Logic_and_Foundations/Software/) are useful as tools for propositional logic: should we include them all on this basis? Maybe adding these kinds of directory resources would be good for users of wikipedia, but it is a step away from being an encyclopedia, and if we have them at all, which I think might be a violation of the "not a directory" part of WP:NOT, I would certainly prefer to have them in a separate page than on this page. --- Charles Stewart 17:45, 8 Jun 2005 (UTC)
Case for a move, revisited
Kutulu's confusion above (in Types/Styles of propositional calculus?) makes the case I was arguing before: we should make and respect the distinction that blah-logic is about the consequence relation whilst blah-calculus is about sets of inference rules that characterise the logic (perhaps among many other logics). A few months back, predicate logic was moved to first-order logic: while the grounds for the move were not exactly those I'm arguing here, I think it strengthens the case for a move.
My revised suggestion for a move is simply to move to propositional logic, and add a section to the article discussing non-classical propositional logics, thus obviating the need for "classical" in the title of the article. Thoughts? --- Charles Stewart 20:17, 6 Jun 2005 (UTC)
