Proposed experiment: You can generate all the short formulas, and discard most of the non-tauts quickly by testing them for all combinations of the variables in random order. Then look over the survivors for a systematic set of axioms: the shortest formulas are axioms; and include anything longer that isn't an immediate consequence of shorter stuff. I don't think this will work, but it's worth trying. Russell's original axioms for Prop Logic: P -> (P v Q) (P v P) -> P (P v Q) -> (Q v P) comm. (P v (Q v R)) -> ((P v Q) v R) assoc. (P -> Q) -> ((R v P) -> (R v Q)) becomes transitivity of -> I'm not sure I've got transitivity exactly right. True & False are not part of the language. The rule of inference is called Detachment: If you know P, and you know P -> Q, you may detach the P, and infer Q. You may also substitute any well-formed expression for a variable in the axioms, and thus the theorems. Complications: The base set of operators is Or+Not (v, ~); P -> Q is regarded as an abbreviation for ~P v Q. I think & is introduced later, as an abbreviation for ~(~P v ~Q). This introduces confusion about how to measure formula length. Also, Detachment makes formulas shorter. Some clever fellow noticed the lemma (Pv(PvQ)) -> (PvQ) or an equivalent, and used it to prove associativity from the other axioms, allowing a size reduction in the axiom set. The next edition of Russell was updated. I set up some computations to try to deduce the consequences of the smaller axiom set, hoping to find associativity as a theorem. I failed, though I got reasonably close. (This was ~1986.) The usual beauty metric for axiom sets is "fewest axioms". I don't know if work has been done to find non-shrink sets. Rich ________________________________________ From: math-fun [math-fun-bounces@mailman.xmission.com] on behalf of Allan Wechsler [acwacw@gmail.com] Sent: Saturday, December 3, 2016 1:10 PM To: math-fun Subject: Re: [math-fun] [EXTERNAL] propositional logic tautologies 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
_______________________________________________ math-fun mailing list math-fun@mailman.xmission.com https://mailman.xmission.com/cgi-bin/mailman/listinfo/math-fun