[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?
#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
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
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
On 12/3/2016 6:28 AM, Henry Baker wrote:
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.
Wouldn't that be equivalent to enumerating all and only all proofs, which is impossible by Godel's theorem for axiom systems that allow induction. Brent
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
http://oeis.org/A256120 a(n) is the number of tautologies that are n symbols long in propositional calculus with the connectives not (~), and (*), or (+), implies (->) and if and only if (<->). On Sat, Dec 3, 2016 at 9:28 AM, Henry Baker <hbaker1@pipeline.com> wrote:
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
There's another way to check tautologies: Pick a variable, and substitute T for it. Then do the same thing, but substitute F. If both formulas are already in your list, then you have a new theorem. This can be run backwards as a non-shrink taut-gen algorithm: Use Clark's operators as a base, and generate all {T,F}-only formulas, sorting them into either the evaluates-to-T list or the evaluates-to-F list. Start each list with the formula T, or F. Grow new formulas by substituting any single instance of T with one of T&T, TvT, TvF, FvT, ~F, T->T, etc., or subbing an F with ~T, T&F, etc. To introduce variables, find pairs of True formulas whose operator structure & grouping match. Line up the formulas to match individual letters (T, F, or a prior variable). Any existing variables must also match. Variables don't match Ts or Fs. All T/F mismatches are replaced with the new variable V, and all F/T mismatches with ~V. The result goes into a True-formulas-with-variables list; whenever all the Ts and Fs are gone, we have a theorem. So we might have the True propositions T->T and F->F, and combine them to get P->P. We could build up P->(PvQ) in steps, from the intermediates P->(PvT) and P->(PvF). This could hardly be called efficient, but it is non-shrink. Rich ________________________________________ From: math-fun [math-fun-bounces@mailman.xmission.com] on behalf of W. Edwin Clark [wclark@mail.usf.edu] Sent: Saturday, December 3, 2016 2:31 PM To: math-fun Subject: [EXTERNAL] Re: [math-fun] propositional logic tautologies http://oeis.org/A256120 a(n) is the number of tautologies that are n symbols long in propositional calculus with the connectives not (~), and (*), or (+), implies (->) and if and only if (<->). On Sat, Dec 3, 2016 at 9:28 AM, Henry Baker <hbaker1@pipeline.com> wrote:
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
At 06:28 AM 12/3/2016, Henry Baker wrote:
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.
I thought about this during a long drive today and realized that there *can't* be an "efficient" (P) algorithm to enumerate all and only tautologies, else that algorithm would itself be useful to solve tautologies, and hence P=NP. So Rich's idea of generating formulae and then doing tautology-testing may well be nearly optimal.
What does it mean to "solve" a tautology? Is this somehow equivalent to boolean satisfiability? On Sat, Dec 3, 2016 at 9:36 PM, Henry Baker <hbaker1@pipeline.com> wrote:
At 06:28 AM 12/3/2016, Henry Baker wrote:
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.
I thought about this during a long drive today and realized that there *can't* be an "efficient" (P) algorithm to enumerate all and only tautologies, else that algorithm would itself be useful to solve tautologies, and hence P=NP.
So Rich's idea of generating formulae and then doing tautology-testing may well be nearly optimal.
_______________________________________________ math-fun mailing list math-fun@mailman.xmission.com https://mailman.xmission.com/cgi-bin/mailman/listinfo/math-fun
I would have guessed that any tautology can be reduced algorithmically to a simpler formula until it becomes p v ~p ??? (So that if the algorithm can't find such a reduction, then that proves it wasn't a tautology.) My main evidence to the contrary is that Rich didn't mention this. —Dan
On Dec 3, 2016, at 6:40 PM, Allan Wechsler <acwacw@gmail.com> wrote:
What does it mean to "solve" a tautology? Is this somehow equivalent to boolean satisfiability?
On Sat, Dec 3, 2016 at 9:36 PM, Henry Baker <hbaker1@pipeline.com> wrote:
At 06:28 AM 12/3/2016, Henry Baker wrote:
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.
I thought about this during a long drive today and realized that there *can't* be an "efficient" (P) algorithm to enumerate all and only tautologies, else that algorithm would itself be useful to solve tautologies, and hence P=NP.
So Rich's idea of generating formulae and then doing tautology-testing may well be nearly optimal.
True. In fact, you can go a step further and reduce (P v ~P) to T. The catch is that the simple algorithm requires, in effect, trying all combinations of the variables. The work is about 2^V for V variables. The Satisfiability problem asks "is there any choice of variables that makes the formula f(a,b,c,...) true?". The co-problem asks "is f(...) true for every combination?" SAT is verifiable if you can find one choice that works; co-SAT is refutable by one counterexample. But to confirm a tautology requires checking all examples, or some equivalent, mathematically sound, procedure. This limits verification to ~50 variables (depending on your computer and your patience). Similarly for a search for a SAT example. There are algorithms & heuristics that improve this situation somewhat, but the problems appear to be of exponential difficulty. There's an annual(?) contest of SAT-solvers; I think the best can handle hard problems of a few hundred variables. Easy problems can be much bigger, with thousands of variables. These have some real world uses. I don't think Henry expected to go beyond, say, 20 variables. A complete list of tautologies with even 10 variables and a few occurrences of each variable would be very big. Imagine a binary hypercube of dimension V, hypervolume 2^V cells. Your job is to completely cover the hypercube with bricks of volume 1/8 of the total, with overlap permitted. This might represent the truth-volume of the clause (C & ~F & H). Your formula has about 4.3 V clauses. Each has 3 variables, and the clauses are ORed together to make the formula. Is it a tautology? Observationally, it seems to be about a 50:50 proposition. 10 variables makes 960 clauses of this shape (8 for the negation patterns, times bin(10,3)=120 for the variable choices). Select 43 clauses at random: do they cover the whole hypercube? If 50% of the formulas do, that's .50 * bin(960,43) tautologies. Rich ---------- Quoting Dan Asimov <asimov@msri.org>:
I would have guessed that any tautology can be reduced algorithmically to a simpler formula until it becomes p v ~p ???
(So that if the algorithm can't find such a reduction, then that proves it wasn't a tautology.)
My main evidence to the contrary is that Rich didn't mention this.
?Dan
On Dec 3, 2016, at 6:40 PM, Allan Wechsler <acwacw@gmail.com> wrote:
What does it mean to "solve" a tautology? Is this somehow equivalent to boolean satisfiability?
On Sat, Dec 3, 2016 at 9:36 PM, Henry Baker <hbaker1@pipeline.com> wrote:
At 06:28 AM 12/3/2016, Henry Baker wrote:
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.
I thought about this during a long drive today and realized that there *can't* be an "efficient" (P) algorithm to enumerate all and only tautologies, else that algorithm would itself be useful to solve tautologies, and hence P=NP.
So Rich's idea of generating formulae and then doing tautology-testing may well be nearly optimal.
_______________________________________________ math-fun mailing list math-fun@mailman.xmission.com https://mailman.xmission.com/cgi-bin/mailman/listinfo/math-fun
participants (7)
-
Allan Wechsler -
Brent Meeker -
Dan Asimov -
Henry Baker -
rcs＠xmission.com -
Schroeppel, Richard -
W. Edwin Clark