Misplaced Pages

Well-formed formula: Difference between revisions

Article snapshot taken from Wikipedia with creative commons attribution-sharealike license. Give it a read and then ask your questions in the chat. We can research this topic together.
Browse history interactively← Previous editNext edit →Content deleted Content addedVisualWikitext
Revision as of 00:42, 10 April 2007 editLaymanal (talk | contribs)4 edits Some generalization is added with respect to the pronounciation of "WFF" and the definition of "proof".← Previous edit Revision as of 00:56, 10 April 2007 edit undoCBM (talk | contribs)Extended confirmed users, File movers, Pending changes reviewers, Rollbackers55,390 edits Remove unenclcylopedic, signed comments from article. Undid revision 121565082 by Laymanal (talk)Next edit →
Line 1: Line 1:
{{dablink|For the ] government policy, see ].}} {{dablink|For the ] government policy, see ].}}


In ], '''WFF''' (pronounced "wiff") is an abbreviation for '''well-formed formula'''. Given a ], a WFF is any string that is generated by that grammar. In ], '''WFF''' (pronounced "wiff") is an abbreviation for '''well-formed formula'''. Given a ], a WFF is any string that is generated by that grammar.

However, some logicians (Frederic B. Fitch, Alan R Anderson, and Nuel D. Belnap, Jr.) and lawyer-logician Layman E. Allen pronounce it "woof" (as in "wood").

For example, in ] the sequence of symbols <math>((\alpha\rightarrow\beta)\rightarrow(\neg\beta\rightarrow\neg\alpha))</math> is a WFF because it is grammatically correct. The sequence of symbols <math>((\alpha\rightarrow\beta)\rightarrow(\beta\beta))\alpha))</math> is not a WFF, because it does not conform to the grammar of propositional calculus.


In formal logic, ]s are sequences of WFFs with certain properties, and the final WFF in the sequence is what is proven. In formal logic, ]s are sequences of WFFs with certain properties, and the final WFF in the sequence is what is proven.


==Examples==
In some formalizations of formal logic proofs are sequences of WFFs with certain properties, and the final WFF in the sequence is what is proven. However, in the powerful Frederic B. Fitch sub-proof formalizations of formal logic, proofs are sequences of items, where items are sequences of sub-proofs or WFFs, and the last item in the sequence is a WFF of what is proven. (See Frederic B. Fitch, SYMBOLIC LOGIC - AN INTRODUCTION, Ronald Press, New York, 1952, and Layman E. Allen, WFF 'N PROOF: The Game of Modern Logic, Ann Arbor, Michigan, 1968).
For example, in ] the sequence of symbols
] 00:42, 10 April 2007 (UTC)laymanal


:<math>((\alpha\rightarrow\beta)\rightarrow(\neg\beta\rightarrow\neg\alpha))</math>
⚫ ==Trivia==


is a WFF because it is grammatically correct. The sequence of symbols
⚫ ''WFF'' is the basis for an esoteric pun used in the name of a product: "WFF 'n Proof: The Game of Modern Logic," by Layman Allen, a professor at the ]. The board game is designed to teach the principles of symbolic logic to children (in ]), and its name is a pun on '']'', a nonsense word used as a ] at ] made popular in ''The Whiffenpoof Song''.


:<math>((\alpha\rightarrow\beta)\rightarrow(\beta\beta))\alpha))</math>
The above Trivia is fairly accurate, but only fairly so. But even trivia deserves a respectable correspondence to reality, even if involves only trivia about trivia. First, the trade-marked name of the game is "WFF 'N PROOF", all upper-case. Second, "WFF" alone was never the sole basis of the pun; its basis was the pair of names of two series of games about logic. Besides being the standard abbreviation in logic for "well-formed formula", "WFF" was the name adopted for a series of games dealing with the concept of "WFFhood" (or should that be "WFFship", or even "WFFness"?) that were created during the period when WFF 'N PROOF itself was evolving. There was an accompanying series of games created about the same time called the "PROOF" games that dealt with the concept of proof. I remember well what I believe to be the first utterance ever on planet earth of the term "WFF 'N PROOF". It occurred on a warm, sun-shiny afternoon in the Spring of 1960 on the back-yard lawn of a graduate law student named, "Charles Padden" when the two of us were at Yale Law School. Charles had just popped a can of cold beer for my benefit, and handed it to me with the question, "So, how are the games coming along?" My response was, "Well, the WFF and PROOF games are ... Oh, shit! we've given them the wrong names. They should be combined and called "WFF 'N PROOF".


is not a WFF, because it does not conform to the grammar of propositional calculus.
That was the birth of the name of the first series of 24 games that dealt with 13 ideas: the concepts of WFF, PROOF, and 11 rule-of-inference schemas that formulate the basis of standard two-valued propositional logic in Jan Lukasciewicz notation using the powerful subordinate-proof technique of Frederic B. Fitch. So, clearly, it was the full name "WFF 'N PROOF" that was the intended pun with respect to the famous Yale singing group, the Whiffenpoofs. However, the names did lead to some confusion during the period when we both had mail-boxes at the Yale Station postal facility. The Whiffenpoofs and WFF 'N PROOF somewhat frequently received each other's mail. I, who am tone deaf, remember well one delightful invitation to come and sing in Denver. - Layman Allen


⚫ ==Trivia==
] 00:42, 10 April 2007 (UTC)laymanal
⚫ ''WFF'' is the basis for an esoteric pun used in the name of a game product: "WFF 'N PROOF: The Game of Modern Logic," by Layman Allen<ref></ref>, developed while he was at ] (he was later a professor at the ]). The suite of games is designed to teach the principles of symbolic logic to children (in ])<ref>More technically, ] using the ].</ref>. Its name is an accepted pun on '']'', a nonsense word used as a ] at ] made popular in ''The Whiffenpoof Song'' and ].


==Notes==
18:32, 9 April 2007 (UTC)18:32, 9 April 2007 (UTC)18:32, 9 April 2007 (UTC)18:32, 9 April 2007 (UTC)18:32, 9 April 2007 (UTC)18:32, 9 April 2007 (UTC)~~
<references/>


==See also== ==See also==

*] *]


==External links== ==External links==
⚫ * - includes a short ] quiz.
⚫ *


*[http://www.cs.odu.edu/~toida/nerzic/content/logic/pred_logic/construction/wff_intro.html
⚫ Well-Formed Formula for First Order Predicate Logic] - includes a short ] quiz.

⚫ *
] ]


] ]

] ]

] ]

] ]

Revision as of 00:56, 10 April 2007

For the New Zealand government policy, see Working for Families.

In logic, WFF (pronounced "wiff") is an abbreviation for well-formed formula. Given a formal grammar, a WFF is any string that is generated by that grammar.

In formal logic, proofs are sequences of WFFs with certain properties, and the final WFF in the sequence is what is proven.

Examples

For example, in propositional logic the sequence of symbols

( ( α → β ) → ( ¬ β → ¬ α ) ) {\displaystyle ((\alpha \rightarrow \beta )\rightarrow (\neg \beta \rightarrow \neg \alpha ))}

is a WFF because it is grammatically correct. The sequence of symbols

( ( α → β ) → ( β β ) ) α ) ) {\displaystyle ((\alpha \rightarrow \beta )\rightarrow (\beta \beta ))\alpha ))}

is not a WFF, because it does not conform to the grammar of propositional calculus.

Trivia

WFF is the basis for an esoteric pun used in the name of a game product: "WFF 'N PROOF: The Game of Modern Logic," by Layman Allen, developed while he was at Yale Law School (he was later a professor at the University of Michigan). The suite of games is designed to teach the principles of symbolic logic to children (in Polish notation). Its name is an accepted pun on whiffenpoof, a nonsense word used as a cheer at Yale University made popular in The Whiffenpoof Song and The Whiffenpoofs.

Notes

  2. More technically, propositional logic using the Fitch-style calculus.

See also

External links

Category: