often written as follows: The two terms on the left, P → Q and P, are called premises (by convention linked by a comma), the symbol ⊢ means "yields" (in the sense of logical deduction), and the term on the right is called the conclusion: P → Q, P ⊢ Q For the modus ponens to succeed, both premises P → Q and P must be true. Because, as demonstrated above the premise P → Q is a tautology, "truth" is always the case no matter how x, y and z are valued, but "truth" is only the case for P in those circumstances when P evaluates as "true" (e.g. rows OR OR OR : x'y'z' + x'y'z + x'yz' + xyz' = x'y' + yz'). P → Q , P ⊢ Q i.e.: ( ~(y & z) & (x → y) ) → ( ~ (x & z) ) , ( ~(y & z) & (x → y) ) ⊢ ( ~ (x & z) ) i.e.: IF "No Ys are Zs" and "All Xs are Ys" THEN "No Xs are Zs", "No Ys are Zs" and "All Xs are Ys" ⊢ "No Xs are Zs" One is now free to "detach" the conclusion "No Xs are Zs", perhaps to use it in a subsequent deduction (or as a topic of conversation). The use of tautological implication means that other possible deductions exist besides "No Xs are Zs"; the criterion for a successful deduction is that the 1s under the sub-major connective on the right include all the 1s under the sub-major connective on the left (the major connective being the implication that results in the tautology). For example, in the truth table, on the right side of the implication (→, the major connective symbol) the bold-face column under the sub-major connective symbol " ~ " has all the same 1s that appear in the bold-faced column under the left-side sub-major connective & (rows , , and ), plus two more (rows and ). Gallery See also Rainbow box Spider diagram – an extension of Euler diagrams adding existence to contour intersections. Venn diagram Notes References Further reading By date of publishing: Sir William Hamilton 1860 Lectures on Metaphysics and Logic edited by Henry Longueville Mansel and John Veitch, William Blackwood and Sons, Edinburgh and London. W. Stanley Jevons 1880 Elementary Lessons in Logic: Deductive and Inductive. With Copious