SAT and proofs in propositional logic

Question

A naive view would ask why one should bother with proofs in propositional logic, since one can just use truth tables. One gets a little bit more sophisticated when one recalls that sizes of truth tables grow exponentially with the number of variables. Indeed, we have an NP-hard problem here. Is there any particular example of a formula of propositional logic whose universal validity is demonstrably expensive to establish but that has a short and elegant proof?

Answer 1

Given an indefinitely large number of propositional variables, many such formulas can get formulated in propositional logic via meta-theory. I use Polish notation in the following.

As Gerry Myerson pointed out one example would consist of:

C KaKb...Kyz KaKb...Kyz would qualify. But give the abbreviation there clear, this just consists of an instance of the weak law of identity Cxx. In other words the proof would go as follows:

axiom 1 Cxx
1 x / KaKbKcKdKeKfKgKhKiKjKkKlKmKnKoKpKqKrKsKtKuKvKwKxKyz * 2
2 C KaKbKcKdKeKfKgKhKiKjKkKlKmKnKoKpKqKrKsKtKuKvKwKxKyz
 KaKbKcKdKeKfKgKhKiKjKkKlKmKnKoKpKqKrKsKtKuKvKwKxKyz

Suppose that CxCyx is a thesis (axiom or theorem) of a propositional logic with enough variables. Then,

3) CaCbCcCdCeCfCgChCiCjCkClCmCnCoCpCqCrCsCtCuCvCxCyx is a theorem in such a system. Meta-logically, a proof is simple. We notice that from any theorem we can put a conditional sign 'C' and any meaningful expression before it. Since CxCyx is a theorem, by repeated applications of that principles, 3) is a theorem.

Suppose that CxCyz is logically equivalent CyCxz and we can replace any instance of CxCyz in any formula with CyCxz in any formula. The meta-theory here implies that any formula which has exactly two instances of 'x', follows a similar pattern will also be a theorem. As an easy example:

4) CaCbCcCdCeCfCgChCiCjCkClCmCnCoCpCqCrCsCtCuCxCvCyx is a formula.

But, so is,

5) CxCbCcCfCgChCiCjCkCdCeCoCpCqCsCtCrClCmCaCnCvCuCwx

As another example, let's consider the following:

6) CCabCCbcCCcdCCdeCCefCCfgCChiCCijCCjkCCklCClmCCmnCCnoCCopCCpqCCqrCCrsCCstCCtuCCuvCCvwCCwxCCxyCCyzCaz

Let's say that we can use resolution to determine the validity of the formula. This means that to check the above we just need to consider each antecedent as a clause. Or in other words Cab gets translated to the clause ANab, Cbc to the clause ANbc and so on. Then the following will prove the above:

1 ANab
2 ANbc
3 ANcd
4 ANde
5 ANef
6 ANfg
7 ANgh
8 ANhi
9 ANij
10 ANjk
11 ANkl
12 ANlm
13 ANmn
14 ANno
15 ANop
16 ANpq
17 ANqr
18 ANrs
19 ANst
20 ANtu
21 ANuv
22 ANvw
23 ANwx
24 ANxy
25 ANyz
26 a
27 Nz
28 b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s,
t, u, v, w, x, y, z by resolution from 26 and 1, then from the previous 
step and 2, then from the previous step and 3, and so on.
29 {} from the last step above and 27.

I think you will agree that even if we had to expand out every step in 28, that still ends up shorter than the truth tables.

We could also commute 6) in many ways and readily obtain theorems with twenty-six variables. We also didn't even bother to subscript variables with numerical symbols. Nor did we have to invoke large natural numbers.

As perhaps another example, suppose that we definition for meaningful expressions:

A meaningful expression is one of the following:

1. A small letter of the English ABCs.
2. A two-unit expression with 'N' as the first unit, and some meaningful expression $\alpha$ as the second unit.
3. A three-unit expression with 'A' or 'C' or 'K' as the first unit, some meaningful expression $\alpha$ as the second unit, and some meaningful expression $\beta$ as the third unit.

Nothing else is a meaningful expression. Suppose we have the following rules of inference with $\alpha$ and $\beta$ again standing for any meaningful expression.

1. Condensed detachment with CxCyx as always the major premiss.
2. We may replace any instance of C in any formula with AN in any meaningful expression (since C$\alpha$$\beta$ is logically equivalent to AN$\alpha$$\beta$).
3. We may replace any instance of C$\alpha$$\beta$ in any meaningful expression with NK$\alpha$N$\beta$ in any meaningful expression.
4. We may replace any instance of $\alpha$ in any formula with CC$\alpha$$\beta$$\alpha$ in any meaningful expression.

Note that in 4. $\beta$ could consist of any meaningful expression.

Suppose our only axiom is CxCyx. Then the following makes for a 17 step proof with a modest amount of symbols:

axiom   1 CxCyx
1, 1.   2 CaCbCcb
2, 1.   3 CaCbCcCdc
3, 1.   4 CaCbCcCdCed
4, 1.   5 CaCbCcCdCeCfe
5, 1.   6 CaCbCcCdCeCfCgf
6, 1.   7 CaCbCcCdCeCfCgChg
7, 1.   8 CaCbCcCdCeCfCgChCih
8, 1.   9 CaCbCcCdCeCfCgChCiCji
9, 2.  10 ANaCbCcCdCeCfCgChCiCji
10, 3. 11 ANaCbCcCdCeCfCgNKhNCiCji
11, 2. 12 ANaCbCcCdCeCfCgNKhNCiANji
13, 4. 13 ANaCCCbybCcCdCeCfCgNKhNCiANji
13, 2. 14 ANaCCCbybCcCdANeCfCgNKhNCiANji
14, 4. 15 ANaCCCbybCcCdANeCfCCCgugNKhNCiANji
15, 4. 16 ANaCCCCCbkbybCcCdANeCfCCCgugNKhNCiANji
16, 4. 17 ANCCaCzCoCpCCrstaCCCCCbkbybCcCdANeCfCCCgugNKhNCiANji

The last step involves 'a' getting replaced by 'CCaCzCoCpCCrsta'. Here, CzCoCpCCrst is a meaningful expression since it has three units 'C', 'z', and 'CoCpCCrst' which are meaningful expressions, 'CoCpCCrst' is a meaningful expression since it has units 'C', 'o', and 'CpCCrst', with 'CpCCrst' having units 'C', 'p' and 'CCrst', with 'CCrst' having units 'C', 'Crs', and 't', with 'Crs' having units 'C', 'r', and 's'.

Rule 4 is valid as a rule of replacement since for all x, for all y, for all z, in the propositional domain of two-truth values, CxCCxyx is a theorem (since CxCzx is a theorem), and so is CCCxyxx.

I believe you also agree that the proof of the meaningful expression 17 here is much more elegant and shorter than proving such by truth tables.

Answer 2

The formation rules for the following will go:

1. All small letters of the ABCs qualify as meaningful expressions.
2. If $\alpha$ has the form of a meaningful expression, if $\beta$ has the form of a meaningful expression also, then so does C$\alpha$$\beta$.
3. Nothing else in what follows qualifies as a meaningful expression.

So, by clause 1, a, b, and c qualify as meaningful expressions. Since we have those, Cac makes for a meaningful expression by clause 2 and so does Cbc. By clause 2, CbCac is a meaningful expression. By clause 2 again, CCbCacCbc qualifies as a meaningful expression. By clause 2 again, CaCCbCacCbc qualifies as a meaningful expression.

Now, for a particular example, instead of a mere few as my previous answer has, and to dispel any notion that CpCqp is why I could do the above, I'll pick

CaCCbCacCbc

as our logical thesis to study. The rules of inference are just uniform substitution in the primitive logical thesis above and C-detachment:

"From a thesis of the form C$\alpha$$\beta$ and a thesis of the form $\alpha$ we may accept one of the form $\beta$."

The notation $\alpha$/$\beta$ indicates that $\alpha$ gets substituted with $\beta$. The notation C$\alpha$-$\beta$ indicates that we have meaningful expression $\alpha$ in the antecedent, and we will detach $\beta$.

axiom 
1 CaCCbCacCbc
1 b/d, c/e, a/CaCCbCacCbc * 2
2 CCaCCbCacCbcCCdCCaCCbCacCbceCde
2 * C1-3
3 CCdCCaCCbCacCbceCde
1 b/f, c/g, a/CCdCCaCCbCacCbceCde * 4
4 CCCdCCaCCbCacCbceCdeCCfCCCdCCaCCbCacCbceCdegCfg
4 * C3-5
5 CCfCCCdCCaCCbCacCbceCdegCfg
1 b/h, c/i, a/CCfCCCdCCaCCbCacCbceCdegCfg * 6
6 CCCfCCCdCCaCCbCacCbceCdegCfgCChCCCfCCCdCCaCCbCacCbceCdegCfgiChi
6 * C5-7
7 CChCCCfCCCdCCaCCbCacCbceCdegCfgiChi
1 b/j, c/k, a/CChCCCfCCCdCCaCCbCacCbceCdegCfgiChi * 8
8 CCChCCCfCCCdCCaCCbCacCbceCdegCfgiChiCCjCCChCCCfCCCdCCaCCbCacCbceCdegCfgiChikCjk
8 * C7-9
9 CCjCCChCCCfCCCdCCaCCbCacCbceCdegCfgiChikCjk

Now thesis 9 has eleven variables, and thus it's truth table has a mere 2048 rows. But, it took us nine steps to prove thesis 9. The longest step in this proof has under 100 symbols. Thus, this proof has under 900 symbols total, and thus if we call the size of a proof the number of symbols it has, the size of this proof ends up easily less than half the number of rows for the truth table computation. If we continued in the pattern I've outlined with the proof, thesis 11 would have 13 variables, and thus it's truth table would have 8192 rows. But, the ratio of the size of a proof (total number of symbols) to the number of the rows for thesis 11 has decreased from what it would have equaled for thesis 9. And if we had an unending sequence of proofs in this way and as many variables as natural numbers, it would end up that the ratio of the size of a proof after a number of steps to the number of rows in a truth table, converges to 0.

For an even greater discrepancy here, just find some thesis of the full propositional calculus which has a single letter only in the antecedent, that letter also belongs to the consequent, and even more letters in the consequent than thesis 1 above. But, as a particular example, I hope the above suffices.

Edit: As some other examples where truth tables quickly become even more expensive than formal proofs we might pick: CpCCpCqrCCsqCsr as our thesis to make into our axiom, or CpCCpqCCqrCCrss, or CpCCrqCCqsCCstCCprt or even

CaCCabCCbcCCcdCCdeCCefCCfgCCghCChiCCijCCjkCCklCClmCCmnCCnoCCopCCpqCCqrr.

So even if this answer does not provide enough of an example, perhaps the method behind the answer does.