 | This article needs additional citations for verification .(April 2017) |
WFF 'N PROOF is a game of modern logic, developed to teach principles of symbolic logic. It was developed by Layman E. Allen in 1962 [1] [2] a former professor of Yale Law School and the University of Michigan.
As marketed in the 1960s WFF 'N PROOF was a series of 20 games of increasing complexity, varying with the logical rules and methods available.
All players must be able to recognize a "well-formed formula" (WFF in Łukasiewicz notation), to assemble dice values into valid statements (WFFs) and to apply the rules of logical inference so as to complete a proof. [1] Games are played by two or more people. The first player to roll the cubes sets a WFF as a Goal. Each player then tries to construct (with whatever is available) a complete logical proof of the goal. The Solution to the goal is the Premises which they started their proof with, and the Rules they used to get to the Goal.
Players take turns moving to the Essentials, Permitted Premises, or Permitted Rules sections of the mat. Any cube moved to Essentials must be used in any Solution, and must be an essential part of that solution; any cube value in Permitted Premises may be used as part of a premise; any cube value in Permitted Rules may be used as part of a Rule. Thus the players themselves shape the Solution, forcing one another to create new Solutions in response to moves.
At any point a player may challenge the last mover, if they feel the last mover has made a mistake. There are three types of Challenges. A-Flub means that the Challenger can make a Solution using the cubes in Required and Permitted and one more cube from Resources. P-Flub, or Challenge Impossible means the player believes the Mover cannot make a Solution using the cubes in Required, Permitted, and Resources. C-A-Flub means that the Challenger believes that the Mover, or some previous mover, missed an A-Flub. After a challenge, at least one player must show a correct Solution on paper.
The scoring goes like this:
The player who wins the challenge scores 10 points.
The loser of the challenge scores 6.
If there is a third player, he must side with or against the Challenger and scores points depending upon that decision.
The name is a play on Whiffenpoofs, an a cappella singing group established at Yale University in 1909. [3]
Disjunction introduction or addition is a rule of inference of propositional logic and almost every other deduction system. The rule makes it possible to introduce disjunctions to logical proofs. It is the inference that if P is true, then P or Q must be true.
First-order logic—also called predicate logic, predicate calculus, quantificational logic—is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantified variables over non-logical objects, and allows the use of sentences that contain variables, so that rather than propositions such as "Socrates is a man", one can have expressions in the form "there exists x such that x is Socrates and x is a man", where "there exists" is a quantifier, while x is a variable. This distinguishes it from propositional logic, which does not use quantifiers or relations; in this sense, propositional logic is the foundation of first-order logic.
The propositional calculus is a branch of logic. It is also called propositional logic, statement logic, sentential calculus, sentential logic, or sometimes zeroth-order logic. It deals with propositions and relations between propositions, including the construction of arguments based on them. Compound propositions are formed by connecting propositions by logical connectives representing the truth functions of conjunction, disjunction, implication, biconditional, and negation. Some sources include other connectives, as in the table below.
In propositional logic, modus ponens, also known as modus ponendo ponens, implication elimination, or affirming the antecedent, is a deductive argument form and rule of inference. It can be summarized as "P implies Q.P is true. Therefore, Q must also be true."
In logic and deductive reasoning, an argument is sound if it is both valid in form and has no false premises. Soundness has a related meaning in mathematical logic, wherein a formal system of logic is sound if and only if every well-formed formula that can be proven in the system is logically valid with respect to the logical semantics of the system.
In logic and proof theory, natural deduction is a kind of proof calculus in which logical reasoning is expressed by inference rules closely related to the "natural" way of reasoning. This contrasts with Hilbert-style systems, which instead use axioms as much as possible to express the logical laws of deductive reasoning.
Deductive reasoning is the process of drawing valid inferences. An inference is valid if its conclusion follows logically from its premises, meaning that it is impossible for the premises to be true and the conclusion to be false.
"What the Tortoise Said to Achilles", written by Lewis Carroll in 1895 for the philosophical journal Mind, is a brief allegorical dialogue on the foundations of logic. The title alludes to one of Zeno's paradoxes of motion, in which Achilles could never overtake the tortoise in a race. In Carroll's dialogue, the tortoise challenges Achilles to use the force of logic to make him accept the conclusion of a simple deductive argument. Ultimately, Achilles fails, because the clever tortoise leads him into an infinite regression.
In philosophy of logic and logic, a rule of inference, inference rule or transformation rule is a logical form consisting of a function which takes premises, analyzes their syntax, and returns a conclusion.
A formal system is an abstract structure and formalization of an axiomatic system used for inferring theorems from axioms by a set of inference rules.
In mathematical logic, propositional logic and predicate logic, a well-formed formula, abbreviated WFF or wff, often simply formula, is a finite sequence of symbols from a given alphabet that is part of a formal language.
Computability logic (CoL) is a research program and mathematical framework for redeveloping logic as a systematic formal theory of computability, as opposed to classical logic, which is a formal theory of truth. It was introduced and so named by Giorgi Japaridze in 2003.
Academic Games is a competition in the U.S. in which players win by out-thinking each other in mathematics, language arts, and social studies. Formal tournaments are organized by local leagues, and on a national level by the Academic Games Leagues of America (AGLOA). Member leagues in eight states hold a national tournament every year, in which players in four divisions compete in eight different games covering math, English, and history. Some turn-based games require a kit consisting of a board and playing cubes, while other games have a central reader announcing questions or clues and each player answering individually.
In logic and analytic philosophy, an atomic sentence is a type of declarative sentence which is either true or false and which cannot be broken down into other simpler sentences. For example, "The dog ran" is an atomic sentence in natural language, whereas "The dog ran and the cat hid" is a molecular sentence in natural language.
In mathematics and computer science, a recursive definition, or inductive definition, is used to define the elements in a set in terms of other elements in the set. Some examples of recursively-definable objects include factorials, natural numbers, Fibonacci numbers, and the Cantor ternary set.
Metamath is a formal language and an associated computer program for archiving and verifying mathematical proofs. Several databases of proved theorems have been developed using Metamath covering standard results in logic, set theory, number theory, algebra, topology and analysis, among others.
An argument is a series of sentences, statements, or propositions some of which are called premises and one is the conclusion. The purpose of an argument is to give reasons for one's conclusion via justification, explanation, and/or persuasion.
Suppes–Lemmon notation is a natural deductive logic notation system developed by E.J. Lemmon. Derived from Suppes' method, it represents natural deduction proofs as sequences of justified steps. Both methods use inference rules derived from Gentzen's 1934/1935 natural deduction system, in which proofs were presented in tree-diagram form rather than in the tabular form of Suppes and Lemmon. Although the tree-diagram layout has advantages for philosophical and educational purposes, the tabular layout is much more convenient for practical applications.
Logical consequence is a fundamental concept in logic which describes the relationship between statements that hold true when one statement logically follows from one or more statements. A valid logical argument is one in which the conclusion is entailed by the premises, because the conclusion is the consequence of the premises. The philosophical analysis of logical consequence involves the questions: In what sense does a conclusion follow from its premises? and What does it mean for a conclusion to be a consequence of premises? All of philosophical logic is meant to provide accounts of the nature of logical consequence and the nature of logical truth.
Logic is the study of correct reasoning. It includes both formal and informal logic. Formal logic is the study of deductively valid inferences or logical truths. It examines how conclusions follow from premises due to the structure of arguments alone, independent of their topic and content. Informal logic is associated with informal fallacies, critical thinking, and argumentation theory. Informal logic examines arguments expressed in natural language while formal logic uses formal language. When used as a countable noun, the term "a logic" refers to a logical formal system that articulates a proof system. Logic plays a central role in many fields, such as philosophy, mathematics, computer science, and linguistics.