Talk:Propositional calculus

From Wikipedia, the free encyclopedia

WikiProject Mathematics
Mathematics Portal
This article is within the scope of WikiProject Mathematics, which collaborates on articles related to mathematics.
Mathematics rating: B Class Top Priority  Field: Foundations, logic, and set theory

Contents

[edit] Pre-2005 discussions

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

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

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

From the article:

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

Well, which is it?

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

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

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

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

Symbolic logic have these info. -- looxix 01:43 Mar 21, 2003 (UTC)
  • Delete logical calculus to rename propositional calculus to it. Thanks
    • I've repointed the redirect, probaly better than deleting a valid title jimfbleak
    • Taku: do you realise it was originally at logical calculus until looxix moved it? There's a brief naming discussion on the talk page you should probably contribute to, rather than making a unilateral decision to move. -- Tim Starling 15:51 18 May 2003 (UTC)
Actually, I am not so sure the difference between propositional calculus and logical calculus (yeah, and I am working on logic articles now, what an arrogant), so I leave this for other folks. -- Taku 16:28 18 May 2003 (UTC)

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

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

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

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

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

Norm Megill nm at alum.mit.edu

Hello, Norm -- I'm a big fan of metamath! It seems to me that this is not a content problem, but a rendering problem. Do you know what versions of IE this has problems with, eg 5.0, 5.5, 6.0?
One solution: We use two ways of doing math here -- in-line Unicode, and TeX. For IE readers, we could if we wanted, render the characters that IE does not support to GIFs/PNGs, and force full rendering of TeX math to images for users of that browser. But this will screw up our caching system, which tries to serve the same page for all browsers to users who are not logged in.
Another solution: We could post-process cached pages to do this, at the cost of extra compute when being visited by IE. (Which is, unfortunately, the most common browser...)
I'm not sure what the correct answer is... -- The Anome 17:38 9 Jun 2003 (UTC)
By the way, thanks Norm, for releasing those bitmaps into the public domain. The Anome 17:42 9 Jun 2003 (UTC)
One possible solution would be to use the corresponding TeX markup for these sections. Except in the most basic cases, these are automatically converted to PNG (depending on user preferences - which can be configured to always use PNG). Using TeX markup for inline stuff (in the middle of a sentence) is generally undesirable, since it creates spacing issues, but sometimes a clever rephrasing of the article can get the TeX markup into its own line to avoid this problem. (Doh, someone else beat me to it! :) -- Wapcaplet 17:41 9 Jun 2003 (UTC)
(Though, I just remembered, some versions of MSIE, 4.0 and some versions of 5.x if I recall correctly, do not support PNG... erg.) -- Wapcaplet 17:48 9 Jun 2003 (UTC)
When the GIF patent runs out we could always serve GIFs after then, but... yecch. (It's this month in the US, next year elsewhere, so I have read). The Anome 17:49 9 Jun 2003 (UTC)

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

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

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

Norm Megill nm at alum.mit.edu

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

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

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

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

Well, those wouldn't be considered basic rules. They can be derived through reductio and disjunction elimination, though... Evercat 00:44 18 Jun 2003 (UTC)
Still, one thing I was wondering was whether the move [ A v B, -A, therefore B ] wasn't considered a basic rule? When I was taught logic it was recognised as a 2nd type of disjunction elimination. But it's not given on that page. Evercat 00:49 18 Jun 2003 (UTC)
The problem is just that the choice of basic and derived rules is really quite arbitrary, especially in such a simple logic. The article as t stood said, "This is the propositional calculus," "These are the rules of derivation," which is wildly misleading. Any rule in only as basic as some textbook writer chooses to make it. (You can get a sound, complete propositional calculus whose only basic rule is modus ponens. And so forth.)
Incidentally, though, the difference between two forms of "disjunction elimination" raises issues of concern to Intuitionism. But this is not an intuitionistic calculus.

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

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

[edit] Move proposal

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

  1. I think it is the most common name, by quite a margin;
  2. It means the article need not, as it does not, deal with rival propositional logics, such as intuitionistic logic and quantum logic. As it stands, the article fails to do justice to its name.
Since the article outlines both a natural deduction system and Hilbert type axiomatic system under the names of Calculus and Alternative Calculus respectively, it should be clear that there is more than one type of calculus for propositional logic. Second, the article, up to and including the section Grammar, is not about 'classical logic specifically, as a distinction between intuitionistic and classical logic would only be made by giving their respective axiomatizations (or rules for a sequent calculus or semantic tableaux). Hence I feel the most appropriate title of the article is simply Propositional logic. (And under the calculus sections, make explicit mention that they are for classical systems.) Nortexoid 13:07, 21 Mar 2005 (UTC)

Some other issues need addressing:

  • Currently propositional logic is a redirect to propositional calculus, without any suggestion that the two terms are not synonyms. This, as I understand the terms logic and calculus, is misleading: a logic is a certain kind of consequence relation, and a calculus is an effective method for understanding (in particular) a logic. In particular, the natural deduction calculus is called the natural deduction system, obscuring the fact that the current article is presnting a particular calculus as if it were the propositional calculus. This is not OK.
But as I've said above, since it gives an alternative calculus (Hilbert style), that is not the case. Nortexoid 00:47, 22 Mar 2005 (UTC)
  • Instead, we need a more refined taxonomy, dealing with the above issue, and also with
    1. classical logic (currently, a redirect to logic, which is OK, but not ideal);
    2. classical propositional logic is blank (please don't start this page: if the move goes ahead it will just need to be deleted).
    3. Naming alternative calculi of propositional logic, eg. Hilbert's calculus, sequent calculus, tableau calculus. Also should make clear that the given natural deduction calculus is just one of a rather large varierty of such frameworks.

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

[edit] 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)

[edit] 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)

[edit] Why metamath is not a good link for this article

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

I'm not sure what you mean by having "no special support" for propositional logic. In particular, their interactive "Metamath Solitaire" tool uses only a three-axiom system for propositional logic as the default set of axioms -- you need to explicitly select the additional axiom sets for predicate logic, ZFC set theory, etc as additional axioms. Given that it's just an external link, and that it is related to propositional logic, I don't see how it's harmful to have the link there. It includes a good introduction to propositional logic as the base for higher set theory, and helps demonstrate how the various forms of logical calculus (if that's the right term) as built up from each other. Though, it's just a link so I'm not going to argue any more than this :) Kutulu 15:50, 8 Jun 2005 (UTC)
Propositional logic has good properties that predicate logic does not, which are exploited by tools for propositional logic, like decidability, completeness wrt. truth tables. The point is that any tool for predicate logic, such as most of the 27 links in this directory are useful as tools for propositional logic: should we include them all on this basis? Maybe adding these kinds of directory resources would be good for users of wikipedia, but it is a step away from being an encyclopedia, and if we have them at all, which I think might be a violation of the "not a directory" part of WP:NOT, I would certainly prefer to have them in a separate page than on this page. --- Charles Stewart 17:45, 8 Jun 2005 (UTC)

[edit] 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)

[edit] Turnstile, ⊢, doesn't show up properly in IE

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

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

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

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

Theorems can be derived from these nine rules.

Example:

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

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

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

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

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

Eric 07:05, 11 October 2005 (UTC)

[edit] On not being too hairy

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

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

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

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

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

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

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

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

[edit] Move to Propositional Logic? And back Again

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

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

[edit] Material on hold. Three axioms

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

Three axioms

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

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

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

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

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

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

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

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

[edit] Attempted POV Fork

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

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

I have to revert the rename done by Jon because it had annihilated the article's history. If you want to do a move, do it properly (this may require administrator intervention). -lethe talk + 07:19, 17 June 2006 (UTC)
Right now, there are several redirects. Before I fix them, I want to establish what title this article is going to have. The original move was carried out properly. There is a discussion above, and it was taken to WP:RM. So please, if you want to revert it, try to also do it properly. -lethe talk + 07:27, 17 June 2006 (UTC)

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

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

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

The page had no history before I reverted. -lethe talk + 07:43, 17 June 2006 (UTC)
Alright, I just moved the article back to Propositional calculus, using the move function and deleting the redirect page with history. -lethe talk + 07:44, 17 June 2006 (UTC)

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

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

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

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

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

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

[edit] Toward less slippery stepping stones to logic

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

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

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

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

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

[edit] Simpler logic

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Theorem

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

Proof

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

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

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

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

I take it that you think that neither of the two systems mentioned is the most efficient. What do you think IS the most efficient way to do propositional logic? And why do you think that? JRSpriggs 05:11, 3 July 2006 (UTC)
To justify my claim about completeness in Peirce's law and to create a model for what I think we should do here in "propositional calculus", I created Implicational propositional calculus. You might want to check it out. JRSpriggs 09:09, 3 July 2006 (UTC)
Erm? Well, any of these axiomatizations illustrates the interdefinability of operators. I chose the one I did because I think it is simple, it is attributable to someone notable, and it seems to be commonly cited. As such, I believe it deserves mention. Maybe not right in this article, but somewhere. I did not choose it because it is my favourite axiomatization -- I believe I've already stated that it is not. I also did not choose it for its instructional value. To teach propositional logic, I think we ought to use the natural deduction system with redundant rules, as it is already given on this page. This "minimal" system, whatever we choose, is not our primary tool of explanation. I certainly did not choose it because it is most "efficient" -- for that, you can't beat the system which uses all propositional tautologies as axioms. This seems to be even more commonly cited, and it is fair: they are decidable.
Incidentally, I say your natural deduction proof is cheating. These are Hilbert-style axiomatizations. (And by using natural deducton, you've also illustrated my point about instructional value.) -Dan 192.75.48.150 20:52, 4 July 2006 (UTC)
Taking all tautologies as axioms is not most efficient because testing whether a proposition is a tautology is not easy. OK, I do prefer a hybrid system which uses "hypothesis", "reiteration", "deduction", and "modus ponens" as rules of inference au natural; and also uses Peirce's law and ex-falso as axioms. Still, I think that whatever systems we describe should be explicitly proven in the article to be sound and complete, not just hand waving. JRSpriggs 07:37, 5 July 2006 (UTC)

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

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

[edit] What is the Object of a Calculus?

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

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

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

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

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

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

This decision procedure for validity is based on a syntactical notion, the notion of a tautology. Let φ be a sentence such that all the sentence symbols which occur in φ are among the n + 1 symbols, 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)

[edit] "Premise" or "Premiss"?

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

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

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

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

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

[edit] Categorical Inquisitive

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

[edit] Enormous Article

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

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

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

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

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

[edit] Disputed -- Logical graphs

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