I am wondering (and I suspect Henry is wondering) whether there is any faster way than testing all possibilities. In particular, is there a "grammar" of tautologies? Perhaps a small set of axioms could be used to generate all tautologies. For example, if A is a tautology and B is a tautology, then A^B is a tautology, and so is AvC no matter what C says. So that's two axioms. If we had a monotonic axiom set (that is, composed of axioms which always produced strings longer than their inputs) which generated all tautologies, then it's easy to write a fast algorithm to produce all tautologies in length order. On Sat, Dec 3, 2016 at 2:33 PM, Schroeppel, Richard <rschroe@sandia.gov> wrote:
#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
_______________________________________________ math-fun mailing list math-fun@mailman.xmission.com https://mailman.xmission.com/cgi-bin/mailman/listinfo/math-fun