#1. For tautologies within the "Propositional Calculus" with expressions like Q -> (P->Q) that use only logical connectives like & v ~ ->, but no quantifiers like All or Every, you can just generate and check all formulas in any convenient order, such as shortest first. You can also handle a limited set of arithmetic, with formulas like 2+2=4 or even "3X=5 has no integer solutions". If you advance to logical systems that include unsolvable questions, your (only?) move is to enumerate proofs and apply a proof checker. This is unsatisfactory since a long proof can have a short conclusion, and there's no way to bound the size of the proof. And there's no guarantee that any given proposition will ever be settled. The Busy Beaver problem for 5-state Turing Machines has been open for two decades, and still has a couple of dozen open cases, where the halting problem is unsettled. #2. IIRC, for Propositional Calculus, there's some finite percentage of Tautologies, strictly greater than 0 and less than 1. Rich ________________________________________ From: math-fun [math-fun-bounces@mailman.xmission.com] on behalf of Henry Baker [hbaker1@pipeline.com] Sent: Saturday, December 3, 2016 7:28 AM To: math-fun@mailman.xmission.com Subject: [EXTERNAL] [math-fun] propositional logic tautologies I'm a little rusty on my propositional logic, so I can't remember (if I ever knew) the answer to the following questions: 1. Is there an easy way to enumerate/generate (all and only) *tautologies* in more-or-less increasing complexity fashion? By complexity, I mean more-or-less increasing fashion wrt the number of distinct variables and the size of the expression. 2. What % of prop logic expressions (of a particular complexity) are tautologies? _______________________________________________ math-fun mailing list math-fun@mailman.xmission.com https://mailman.xmission.com/cgi-bin/mailman/listinfo/math-fun