Logic Statement Simplifiction

Question

For the following logical statements, find statements that are logically equivalent using fewer symbols.

P $ \land$ P

P $ \lor$ P

(P $\land$ ~P) $\lor$ Q

Answer 1

P $ \land$ P = P

P $ \lor$ P = P

(P $\land$ ~P) $\lor$ Q = Q

//Proved by truth tables

Answer 2

Your answer clearly works fine for what you wanted, so I've upvoted it and you can accept it in a few days if you wish. However, the assumption of only two truth values seems quite strong for this problem. The following formulas in Polish notation taken as axioms, with C-detachment and uniform substitution as the only rules of inference, allow for the deduction of the formulas EKxxx, EAxxx, and EAKxNxyy. They all hold for an intuitionistic propositional logic which does not not have any adequate finite-valued model (semantics).

Axiom 1 CxCyx

Axiom 2 CCxCyzCCxyCxz

Axiom 3 CKxyx

Axiom 4 CxCyKxy

Axiom 5 CKxNxy

Axiom 6 CxAyx

Axiom 7 CAxyCCxzCCyzz

Axiom 8 CCxyCCyxExy

I just input corresponding parenthesized formulas with a predicate "P" for provable into Prover9 and after 93.38 seconds, it has produced each of the corresponding formulas.

The notation $\alpha$/$\beta$ indicates that $\alpha$ gets uniformly substitute with $\beta$ throughout a given formula. The notation C$\alpha$-$\beta$ indicates that the formulas $\alpha$ and $\beta$ qualify as substitution instances of that form, with $\alpha$ already proved, and $\beta$ about to get detached. You might want to note how the law of identity Cxx gets used in this proof.

Axiom                    1     CxCyx    
Axiom                    2     CCxCyzCCxyCxz  
Axiom                    3     CKxyx
Axiom                    4     CxCyKxy
Axiom                    5     CKxNxy  
Axiom                    6     CxAyx
Axiom                    7     CAxyCCxzCCyzz
Axiom                    8     CCxyCCyxExy
2 z/x                    9     CCxCyxCCxyCxx
9 * C1-10               10     CCxyCxx
10 y/Cyx                11     CCxCyxCxx
11 * C1-12              12     Cxx
1 x/CKxNxy, y/z         13     CCKxNxyCzCKxNxy
13 * C5-14              14     CzCKxNxy
2 z/Kxy                 15     CCxCyKxyCCxyCxKxy
15 * C4-16              16     CCxyCxKxy
1 x/CxAyx, y/z          17     CCxAyxCzCxAyx
17 * C6-18              18     CzCxAyx
2 x/Axy, y/Cxz, z/CCyzz 19     CCAxyCCxzCCyzzCCAxyCxzCAxyCCyzz
19 * C7-20              20     CCAxyCxzCAxyCCyzz
2 x/Cxy, y/Cyx, z/Exy   21     CCCxyCCyxExyCCCxyCyxCCxyExy
21 * C8-22              22     CCCxyCyxCCxyExy
8 x/Kxy, y/x            23     CCKxyxCCxKxyEKxyx
23 * C3-24              24     CCxKxyEKxyx
20 x/KxNx               25     CCAKxNxyCKxNxzCAKxNxyCCyzz
14 z/AKxNxy, y/z        26     CAKxNxyCKxNxz
26 * C25-27             27     CAKxNxyCCyzz
22 x/Azy                28     CCCAzyyCyAzyCCAzyyEAzyy
18 x/CAzyy, x/y, y/z    29     CCAzyyCyAzy
28 * C29-30             30     CCAzyyEAzyy
16 y/x                  31     CCxxCxKxx
31 * C12-32             32     CxKxx

break:

1 x/Cxx                 33     CCxxCyCxx
33 * C12-34             34     CyCxx
2 x/AKxNxy, y/Cyz       35     CCAKxNxCCyzzCCAKxNxyCyzCAKxNxyz
35 * C27-36             36     CCAKxNxyCyzCAKxNxyz
24 y/x                  37     CCxKxxEKxxx
37 * C32-38             38     EKxxx
20 z/x                  39     CCAxyCxxCAxyCCyxx
34 y/Axy                40     CAxyCxx
39 * C40-41             41     CAxyCCyxx
2 x/Axy, y/Cyx, z/x     42     CCAxyCCyxxCCAxyCyxCAxyx
42 * C41-43             43     CCAxyCyxCAxyx
36 z/y                  44     CCAKxNxyCyyCAKxNxyy
34 y/AKxNxy             45     CAKxNxyCyy
45 * C44-46             46     CAKxNxyy
30 z/KxNx               47     CCAKxNxyyEAKxNxyy
47 * C46-48             48     EAKxNxyy
43 y/x                  49     CCAxxCxxCAxxx
34 y/Axx                50     CAxxCxx
49 * C50-51             51     CAxxx
30 z/x, y/x             52     CCAxxxEAxxx
52 * C50-53             53     EAxxx

Using OTTER, still an excellent assistant, the following got produced, which helped me to construct the above proof:

-----> EMPTY CLAUSE at 2.94 sec ----> 38809 [hyper,2,38788,14428,245] $F.

Length of proof is 20. Level of proof is 7.

---------------- PROOF ----------------

1 [] -P(C(x,y))| -P(x)|P(y).

2 [] -P(E(A(p,p),p))| -P(E(A(K(p,N(p)),q),q))| -P(E(K(p,p),p)).

3 [] P(C(x,C(y,x))).

4 [] P(C(C(x,C(y,z)),C(C(x,y),C(x,z)))).

5 [] P(C(K(x,N(x)),y)).

6 [] P(C(K(x,y),x)).

7 [] P(C(x,C(y,K(x,y)))).

8 [] P(C(x,A(y,x))).

9 [] P(C(A(x,y),C(C(x,z),C(C(y,z),z)))).

10 [] P(C(C(x,y),C(C(y,x),E(x,y)))).

14 [hyper,1,4,3] P(C(C(x,y),C(x,x))).

16 [hyper,1,3,5] P(C(x,C(K(y,N(y)),z))).

20 [hyper,1,4,7] P(C(C(x,y),C(x,K(x,y)))).

28 [hyper,1,3,8] P(C(x,C(y,A(z,y)))).

36 [hyper,1,4,9] P(C(C(A(x,y),C(x,z)),C(A(x,y),C(C(y,z),z)))).

40 [hyper,1,4,10] P(C(C(C(x,y),C(y,x)),C(C(x,y),E(x,y)))).

44 [hyper,1,10,6] P(C(C(x,K(x,y)),E(K(x,y),x))).

60 [hyper,1,14,8] P(C(x,x)).

104 [hyper,1,36,16] P(C(A(K(x,N(x)),y),C(C(y,z),z))).

110 [hyper,1,40,28] P(C(C(A(x,y),y),E(A(x,y),y))).

156 [hyper,1,20,60] P(C(x,K(x,x))).

161 [hyper,1,3,60] P(C(x,C(y,y))).

165 [hyper,1,4,104] P(C(C(A(K(x,N(x)),y),C(y,z)),C(A(K(x,N(x)),y),z))).

245 [hyper,1,44,156] P(E(K(x,x),x)).

268 [hyper,1,36,161] P(C(A(x,y),C(C(y,x),x))).

324 [hyper,1,4,268] P(C(C(A(x,y),C(y,x)),C(A(x,y),x))).

14389 [hyper,1,165,161] P(C(A(K(x,N(x)),y),y)).

14428 [hyper,1,110,14389] P(E(A(K(x,N(x)),y),y)).

38716 [hyper,1,324,161] P(C(A(x,x),x)).

38788 [hyper,1,110,38716] P(E(A(x,x),x)).

38809 [hyper,2,38788,14428,245] $F.

------------ end of proof -------------

Perhaps of interest, the proof analysis indicates that the most common used formula 3 here corresponds to Axiom 2 CCxCyzCCxyCxz. Also, formula 3 corresponds to Axiom 1 which gets used in two different ways, unlike say how formula 4 only gets used in one way. Formula 10 corresponding to axiom 8 CCxyCCyxExy also gets used in two different ways. Formula 8 corresponding to axiom 6 CxAyx only gets used in one way here, as one of the shorter significant expressions in a proof. From the context of some multi-valued logic, or even infinite-valued logic formula 268 stands out, since disjunction Axy gets defined as CCxyy. Also, CCxyy = CCyxx, so CAxyCCyxx is consistent with such. I will conjecture that a shorter proof under condensed detachment can get constructed, since I find CxCyy suspicious for a shortest proof.