Talk:Propositional formula

From Wikipedia, the free encyclopedia

WikiProject Mathematics
This article is within the scope of WikiProject Mathematics, which collaborates on articles related to mathematics.
Mathematics rating: Start Class Mid Priority  Field: Foundations, logic, and set theory
Please update this rating as the article progresses, or if the rating is inaccurate. Please also add comments to suggest improvements to the article.

[edit] Expansion

This article was woefully short, so I am going to work on expanding it. I don't want to repeat all of propositional logic here, but we should be able to give a brief overview of the properties of formulas, mention truth assignments, etc. It will take a few days, and the rough draft I have needs a lot of wikilinks to be added. — Carl (CBM · talk) 00:49, 23 October 2007 (UTC)


The development has become too unwieldy so I've moved it to User:Wvbailey/Propositional formula: visitors are welcome! Bill Wvbailey 14:11, 29 October 2007 (UTC)

---

I'm not sure what this means: "The use of symbols { T, F } is discouraged in mathematics because of the possibility of confusion with "Truth" and "Falsity",..." The symbols T and F are usually used in mathematics, since truth and falsity is exactly what they are supposed to represent.
One issue that the content above brings to mind is that this article is just about propositional formulas. It isn't meant to be about all of propositional logic. We can have a few sentences that link to other important concepts, like valuations. Here is a rough list of the things that I think should be included in this article:
  • Basic inductive definition of propositional formulas in the language with negation and the four binary operators \land, \lor, \to, \leftrightarrow. This is the system most often used in math texts. Not present in current version.
  • Discussion of how the definition would be extende3d to cover other connectives. Link to Logical connectives
  • Discussion on parsing and unique readability
  • Very brief summary style discussion of valuations, just enough to give background for the rest of the article. Link to tautology.
  • Discussion of normal forms
— Carl (CBM · talk) 15:31, 25 October 2007 (UTC)

---

We had a conflict edit, so there is a lot more here now. I basically agree with what you've written. I will cut the "brainstorm" to reduce the clutter. I am evolving in the direction you are proposing. I am suffering from some confusions and frustrations: in particular I don't like Enderton's 2002 treatment. I find Kleene's 1952 far better. It seems we should be able to construct a very simple induction-like method of how to construct the formulas. Even Kleene's is too complex because he's constructing an arithmetic+logic system. Kleene has some three little lemmas about parenthesis pairing and nesting etc.

RE {T, F}. Problem is, folks other than mathematicians use propositional formulas. I advise anyone doing so (i.e. creating propositional formulas and then evaluating them) to stay away from T and F. If they are doing rhetoric, then the T & F need to come into play. Kleene also agrees, at least with regards to "metamathematical consistency proofs for the calculus" (1952:125). My practical/engineering experience with {T, F} has been very, very poor. In practice, many folks use "reverse logic" and make a mess of T & F. Also, you cannot "compute" with it using what I would call true Boolean logic, i.e. the logic of Boole: ~a = (1-a), a & B = a * b, a V b = (1 - (1-a)*(1-b)), etc.
RE synthesis versus analysis: both aspects need development
RE parsing, normal forms etc. I agree. A lot needs to be said about such things as ((A & B) & C) = (A & B & C)
RE the "algebra" versus the "valuation": my understanding here is the "algebra" is the substitution rules that I have been trying to "axiomatize" with the inductive definitions, plus the reduction-rules such as De Morgan etc. Plus the notions of "distributive law" and "associative law" etc. .
RE: NOT, OR, AND: I recommend we use NOT, OR, AND and define IMPLY, XOR in terms of these others. My thought was to put in the big table as a summary of the definitions of the operators, and be done with it.

WvbaileyBill

The most common presentation of propositional logic use the classical connectives \land, \lor, \to, \leftrightarrow, \lnot. I think sticking with that convention is fine. In any case the article will discuss how other connectives, that take arbitrary finite numbers of formulas, can be added.
There are quotes above that use the word term. Nowadays that word is usually reserved for certain expression in first order logic; there are no more terms in propositional logic. Everything is a formula. — Carl (CBM · talk) 03:35, 26 October 2007 (UTC)

RE: "term". I wouldn't have a problem with just using "formula" excepting engineers and computer scientists use the notion "term" for a conjunction of variables, i.e. (p & ~q & r) is a "term". In particular minterms are used in the notion of disjunctive normal form. There is a never-ending set of definitions in engineering such as literal for variable or its inverse, prime implicants etc. It's an alternate universe to mathematics. So perhaps I can define "formula" inductively and then define "term" as an alternate usage for (a & b) or (a & b & ... & z). There's also an alterm used in conjunctive normal form e.g. (a V b V ...V z). Bill Wvbailey 18:06, 26 October 2007 (UTC)

We can certainly say that term is used in certain fields. But in any case it isn't necessary to define terms in order to merely define formulas. — Carl (CBM · talk) 10:29, 28 October 2007 (UTC)

I agree. I changed above what I had written before. Bill —Preceding unsigned comment added by Wvbailey (talkcontribs) 15:03, 28 October 2007 (UTC)