for questions or link request: module admin

Further Theorems of Propositional Calculus

name: prophilbert3, module version: 1.00.00, rule version: 1.02.00, original: prophilbert3, author of this module: Michael Meyling

Description

This module includes proofs of popositional calculus theorems. The following theorems and proofs are adapted from D. Hilbert and W. Ackermann's `Grundzuege der theoretischen Logik' (Berlin 1928, Springer)

References

This document uses the results of the following documents:

Content

First distributive law (first direction):

1. Proposition
      (P ∨ (Q ∧ A)) → ((P ∨ Q) ∧ (P ∨ A))     (hilb36)

Proof:
1 (P ∧ Q) → P add proposition hilb24
2 (P ∧ A) → P replace proposition variable Q by A in 1
3 (B ∧ A) → B replace proposition variable P by B in 2
4 (Q ∧ A) → Q replace proposition variable B by Q in 3
5 (P → Q) → ((A ∨ P) → (A ∨ Q)) add axiom axiom4
6 (P → Q) → ((B ∨ P) → (B ∨ Q)) replace proposition variable A by B in 5
7 (P → C) → ((B ∨ P) → (B ∨ C)) replace proposition variable Q by C in 6
8 (D → C) → ((B ∨ D) → (B ∨ C)) replace proposition variable P by D in 7
9 (D → C) → ((P ∨ D) → (P ∨ C)) replace proposition variable B by P in 8
10 (D → Q) → ((P ∨ D) → (P ∨ Q)) replace proposition variable C by Q in 9
11 ((Q ∧ A) → Q) → ((P ∨ (Q ∧ A)) → (P ∨ Q)) replace proposition variable D by Q ∧ A in 10
12 (P ∨ (Q ∧ A)) → (P ∨ Q) modus ponens with 4, 11
13 (P ∧ Q) → Q add proposition hilb25
14 (P ∧ A) → A replace proposition variable Q by A in 13
15 (B ∧ A) → A replace proposition variable P by B in 14
16 (Q ∧ A) → A replace proposition variable B by Q in 15
17 (D → A) → ((P ∨ D) → (P ∨ A)) replace proposition variable C by A in 9
18 ((Q ∧ A) → A) → ((P ∨ (Q ∧ A)) → (P ∨ A)) replace proposition variable D by Q ∧ A in 17
19 (P ∨ (Q ∧ A)) → (P ∨ A) modus ponens with 16, 18
20 P → (Q → (P ∧ Q)) add proposition hilb28
21 P → (A → (P ∧ A)) replace proposition variable Q by A in 20
22 B → (A → (B ∧ A)) replace proposition variable P by B in 21
23 B → ((P ∨ A) → (B ∧ (P ∨ A))) replace proposition variable A by P ∨ A in 22
24 (P ∨ Q) → ((P ∨ A) → ((P ∨ Q) ∧ (P ∨ A))) replace proposition variable B by P ∨ Q in 23
25 (P → Q) → ((A → P) → (A → Q)) add proposition hilb1
26 (P → Q) → ((B → P) → (B → Q)) replace proposition variable A by B in 25
27 (P → C) → ((B → P) → (B → C)) replace proposition variable Q by C in 26
28 (D → C) → ((B → D) → (B → C)) replace proposition variable P by D in 27
29 (D → C) → (((P ∨ (Q ∧ A)) → D) → ((P ∨ (Q ∧ A)) → C)) replace proposition variable B by P ∨ (Q ∧ A) in 28
30 (D → ((P ∨ A) → ((P ∨ Q) ∧ (P ∨ A)))) → (((P ∨ (Q ∧ A)) → D) → ((P ∨ (Q ∧ A)) → ((P ∨ A) → ((P ∨ Q) ∧ (P ∨ A))))) replace proposition variable C by (P ∨ A) → ((P ∨ Q) ∧ (P ∨ A)) in 29
31 ((P ∨ Q) → ((P ∨ A) → ((P ∨ Q) ∧ (P ∨ A)))) → (((P ∨ (Q ∧ A)) → (P ∨ Q)) → ((P ∨ (Q ∧ A)) → ((P ∨ A) → ((P ∨ Q) ∧ (P ∨ A))))) replace proposition variable D by P ∨ Q in 30
32 ((P ∨ (Q ∧ A)) → (P ∨ Q)) → ((P ∨ (Q ∧ A)) → ((P ∨ A) → ((P ∨ Q) ∧ (P ∨ A)))) modus ponens with 24, 31
33 (P ∨ (Q ∧ A)) → ((P ∨ A) → ((P ∨ Q) ∧ (P ∨ A))) modus ponens with 12, 32
34 (P → (Q → A)) → (Q → (P → A)) add proposition hilb16
35 (P → (Q → B)) → (Q → (P → B)) replace proposition variable A by B in 34
36 (P → (C → B)) → (C → (P → B)) replace proposition variable Q by C in 35
37 (D → (C → B)) → (C → (D → B)) replace proposition variable P by D in 36
38 (D → (C → ((P ∨ Q) ∧ (P ∨ A)))) → (C → (D → ((P ∨ Q) ∧ (P ∨ A)))) replace proposition variable B by (P ∨ Q) ∧ (P ∨ A) in 37
39 (D → ((P ∨ A) → ((P ∨ Q) ∧ (P ∨ A)))) → ((P ∨ A) → (D → ((P ∨ Q) ∧ (P ∨ A)))) replace proposition variable C by P ∨ A in 38
40 ((P ∨ (Q ∧ A)) → ((P ∨ A) → ((P ∨ Q) ∧ (P ∨ A)))) → ((P ∨ A) → ((P ∨ (Q ∧ A)) → ((P ∨ Q) ∧ (P ∨ A)))) replace proposition variable D by P ∨ (Q ∧ A) in 39
41 (P ∨ A) → ((P ∨ (Q ∧ A)) → ((P ∨ Q) ∧ (P ∨ A))) modus ponens with 33, 40
42 (D → ((P ∨ (Q ∧ A)) → ((P ∨ Q) ∧ (P ∨ A)))) → (((P ∨ (Q ∧ A)) → D) → ((P ∨ (Q ∧ A)) → ((P ∨ (Q ∧ A)) → ((P ∨ Q) ∧ (P ∨ A))))) replace proposition variable C by (P ∨ (Q ∧ A)) → ((P ∨ Q) ∧ (P ∨ A)) in 29
43 ((P ∨ A) → ((P ∨ (Q ∧ A)) → ((P ∨ Q) ∧ (P ∨ A)))) → (((P ∨ (Q ∧ A)) → (P ∨ A)) → ((P ∨ (Q ∧ A)) → ((P ∨ (Q ∧ A)) → ((P ∨ Q) ∧ (P ∨ A))))) replace proposition variable D by P ∨ A in 42
44 ((P ∨ (Q ∧ A)) → (P ∨ A)) → ((P ∨ (Q ∧ A)) → ((P ∨ (Q ∧ A)) → ((P ∨ Q) ∧ (P ∨ A)))) modus ponens with 41, 43
45 (P ∨ (Q ∧ A)) → ((P ∨ (Q ∧ A)) → ((P ∨ Q) ∧ (P ∨ A))) modus ponens with 19, 44
46 (P → (P → Q)) → (P → Q) add proposition hilb33
47 (P → (P → A)) → (P → A) replace proposition variable Q by A in 46
48 (B → (B → A)) → (B → A) replace proposition variable P by B in 47
49 (B → (B → ((P ∨ Q) ∧ (P ∨ A)))) → (B → ((P ∨ Q) ∧ (P ∨ A))) replace proposition variable A by (P ∨ Q) ∧ (P ∨ A) in 48
50 ((P ∨ (Q ∧ A)) → ((P ∨ (Q ∧ A)) → ((P ∨ Q) ∧ (P ∨ A)))) → ((P ∨ (Q ∧ A)) → ((P ∨ Q) ∧ (P ∨ A))) replace proposition variable B by P ∨ (Q ∧ A) in 49
51 (P ∨ (Q ∧ A)) → ((P ∨ Q) ∧ (P ∨ A)) modus ponens with 45, 50
qed

First distributive law (second direction):

2. Proposition
      ((P ∨ Q) ∧ (P ∨ A)) → (P ∨ (Q ∧ A))     (hilb37)

Proof:
1 P → (Q → (P ∧ Q)) add proposition hilb28
2 P → (A → (P ∧ A)) replace proposition variable Q by A in 1
3 B → (A → (B ∧ A)) replace proposition variable P by B in 2
4 Q → (A → (Q ∧ A)) replace proposition variable B by Q in 3
5 (P → Q) → ((A ∨ P) → (A ∨ Q)) add axiom axiom4
6 (P → Q) → ((B ∨ P) → (B ∨ Q)) replace proposition variable A by B in 5
7 (P → C) → ((B ∨ P) → (B ∨ C)) replace proposition variable Q by C in 6
8 (D → C) → ((B ∨ D) → (B ∨ C)) replace proposition variable P by D in 7
9 (D → C) → ((P ∨ D) → (P ∨ C)) replace proposition variable B by P in 8
10 (D → (Q ∧ A)) → ((P ∨ D) → (P ∨ (Q ∧ A))) replace proposition variable C by Q ∧ A in 9
11 (A → (Q ∧ A)) → ((P ∨ A) → (P ∨ (Q ∧ A))) replace proposition variable D by A in 10
12 (P → Q) → ((A → P) → (A → Q)) add proposition hilb1
13 (P → Q) → ((B → P) → (B → Q)) replace proposition variable A by B in 12
14 (P → C) → ((B → P) → (B → C)) replace proposition variable Q by C in 13
15 (D → C) → ((B → D) → (B → C)) replace proposition variable P by D in 14
16 (D → C) → ((Q → D) → (Q → C)) replace proposition variable B by Q in 15
17 (D → ((P ∨ A) → (P ∨ (Q ∧ A)))) → ((Q → D) → (Q → ((P ∨ A) → (P ∨ (Q ∧ A))))) replace proposition variable C by (P ∨ A) → (P ∨ (Q ∧ A)) in 16
18 ((A → (Q ∧ A)) → ((P ∨ A) → (P ∨ (Q ∧ A)))) → ((Q → (A → (Q ∧ A))) → (Q → ((P ∨ A) → (P ∨ (Q ∧ A))))) replace proposition variable D by A → (Q ∧ A) in 17
19 (Q → (A → (Q ∧ A))) → (Q → ((P ∨ A) → (P ∨ (Q ∧ A)))) modus ponens with 11, 18
20 Q → ((P ∨ A) → (P ∨ (Q ∧ A))) modus ponens with 4, 19
21 (P → (Q → A)) → (Q → (P → A)) add proposition hilb16
22 (P → (Q → B)) → (Q → (P → B)) replace proposition variable A by B in 21
23 (P → (C → B)) → (C → (P → B)) replace proposition variable Q by C in 22
24 (D → (C → B)) → (C → (D → B)) replace proposition variable P by D in 23
25 (D → (C → (P ∨ (Q ∧ A)))) → (C → (D → (P ∨ (Q ∧ A)))) replace proposition variable B by P ∨ (Q ∧ A) in 24
26 (D → ((P ∨ A) → (P ∨ (Q ∧ A)))) → ((P ∨ A) → (D → (P ∨ (Q ∧ A)))) replace proposition variable C by P ∨ A in 25
27 (Q → ((P ∨ A) → (P ∨ (Q ∧ A)))) → ((P ∨ A) → (Q → (P ∨ (Q ∧ A)))) replace proposition variable D by Q in 26
28 (P ∨ A) → (Q → (P ∨ (Q ∧ A))) modus ponens with 20, 27
29 (D → (P ∨ (Q ∧ A))) → ((P ∨ D) → (P ∨ (P ∨ (Q ∧ A)))) replace proposition variable C by P ∨ (Q ∧ A) in 9
30 (Q → (P ∨ (Q ∧ A))) → ((P ∨ Q) → (P ∨ (P ∨ (Q ∧ A)))) replace proposition variable D by Q in 29
31 (D → C) → (((P ∨ A) → D) → ((P ∨ A) → C)) replace proposition variable B by P ∨ A in 15
32 (D → ((P ∨ Q) → (P ∨ (P ∨ (Q ∧ A))))) → (((P ∨ A) → D) → ((P ∨ A) → ((P ∨ Q) → (P ∨ (P ∨ (Q ∧ A)))))) replace proposition variable C by (P ∨ Q) → (P ∨ (P ∨ (Q ∧ A))) in 31
33 ((Q → (P ∨ (Q ∧ A))) → ((P ∨ Q) → (P ∨ (P ∨ (Q ∧ A))))) → (((P ∨ A) → (Q → (P ∨ (Q ∧ A)))) → ((P ∨ A) → ((P ∨ Q) → (P ∨ (P ∨ (Q ∧ A)))))) replace proposition variable D by Q → (P ∨ (Q ∧ A)) in 32
34 ((P ∨ A) → (Q → (P ∨ (Q ∧ A)))) → ((P ∨ A) → ((P ∨ Q) → (P ∨ (P ∨ (Q ∧ A))))) modus ponens with 30, 33
35 (P ∨ A) → ((P ∨ Q) → (P ∨ (P ∨ (Q ∧ A)))) modus ponens with 28, 34
36 (P ∨ A) → ((P ∨ Q) → ((P ∨ P) ∨ (Q ∧ A))) elementary equivalence in 35 at 1 of hilb14 with hilb15
37 (P ∨ A) → ((P ∨ Q) → (P ∨ (Q ∧ A))) elementary equivalence in 36 at 1 of hilb11 with hilb12
38 (D → ((P ∨ Q) → (P ∨ (Q ∧ A)))) → ((P ∨ Q) → (D → (P ∨ (Q ∧ A)))) replace proposition variable C by P ∨ Q in 25
39 ((P ∨ A) → ((P ∨ Q) → (P ∨ (Q ∧ A)))) → ((P ∨ Q) → ((P ∨ A) → (P ∨ (Q ∧ A)))) replace proposition variable D by P ∨ A in 38
40 (P ∨ Q) → ((P ∨ A) → (P ∨ (Q ∧ A))) modus ponens with 37, 39
41 (P → (Q → A)) → ((P ∧ Q) → A) add proposition hilb29
42 (P → (Q → B)) → ((P ∧ Q) → B) replace proposition variable A by B in 41
43 (P → (C → B)) → ((P ∧ C) → B) replace proposition variable Q by C in 42
44 (D → (C → B)) → ((D ∧ C) → B) replace proposition variable P by D in 43
45 (D → (C → (P ∨ (Q ∧ A)))) → ((D ∧ C) → (P ∨ (Q ∧ A))) replace proposition variable B by P ∨ (Q ∧ A) in 44
46 (D → ((P ∨ A) → (P ∨ (Q ∧ A)))) → ((D ∧ (P ∨ A)) → (P ∨ (Q ∧ A))) replace proposition variable C by P ∨ A in 45
47 ((P ∨ Q) → ((P ∨ A) → (P ∨ (Q ∧ A)))) → (((P ∨ Q) ∧ (P ∨ A)) → (P ∨ (Q ∧ A))) replace proposition variable D by P ∨ Q in 46
48 ((P ∨ Q) ∧ (P ∨ A)) → (P ∨ (Q ∧ A)) modus ponens with 40, 47
qed

A form for the abbreviation rule form for disjunction (first direction):

3. Proposition
      (P ∨ Q) → ¬(¬P ∧ ¬Q)     (hilb38)

Proof:
1 P → P add proposition hilb2
2 Q → Q replace proposition variable P by Q in 1
3 (P ∨ Q) → (P ∨ Q) replace proposition variable Q by P ∨ Q in 2
4 (P ∨ Q) → ¬¬(P ∨ Q) elementary equivalence in 3 at 5 of hilb5 with hilb6
5 (P ∨ Q) → ¬¬(¬¬P ∨ Q) elementary equivalence in 4 at 8 of hilb5 with hilb6
6 (P ∨ Q) → ¬¬(¬¬P ∨ ¬¬Q) elementary equivalence in 5 at 11 of hilb5 with hilb6
7 (P ∨ Q) → ¬(¬P ∧ ¬Q) reverse abbreviation and in 6 at occurence 1
qed

A form for the abbreviation rule form for disjunction (second direction):

4. Proposition
      ¬(¬P ∧ ¬Q) → (P ∨ Q)     (hilb39)

Proof:
1 P → P add proposition hilb2
2 Q → Q replace proposition variable P by Q in 1
3 (P ∨ Q) → (P ∨ Q) replace proposition variable Q by P ∨ Q in 2
4 ¬¬(P ∨ Q) → (P ∨ Q) elementary equivalence in 3 at 2 of hilb5 with hilb6
5 ¬¬(¬¬P ∨ Q) → (P ∨ Q) elementary equivalence in 4 at 5 of hilb5 with hilb6
6 ¬¬(¬¬P ∨ ¬¬Q) → (P ∨ Q) elementary equivalence in 5 at 8 of hilb5 with hilb6
7 ¬(¬P ∧ ¬Q) → (P ∨ Q) reverse abbreviation and in 6 at occurence 1
qed

By duality we get the second distributive law (first direction):

5. Proposition
      (P ∧ (Q ∨ A)) → ((P ∧ Q) ∨ (P ∧ A))     (hilb40)

Proof:
1 ((P ∨ Q) ∧ (P ∨ A)) → (P ∨ (Q ∧ A)) add proposition hilb37
2 (P → Q) → (¬Q → ¬P) add proposition hilb7
3 (P → A) → (¬A → ¬P) replace proposition variable Q by A in 2
4 (B → A) → (¬A → ¬B) replace proposition variable P by B in 3
5 (B → (P ∨ (Q ∧ A))) → (¬(P ∨ (Q ∧ A)) → ¬B) replace proposition variable A by P ∨ (Q ∧ A) in 4
6 (((P ∨ Q) ∧ (P ∨ A)) → (P ∨ (Q ∧ A))) → (¬(P ∨ (Q ∧ A)) → ¬((P ∨ Q) ∧ (P ∨ A))) replace proposition variable B by (P ∨ Q) ∧ (P ∨ A) in 5
7 ¬(P ∨ (Q ∧ A)) → ¬((P ∨ Q) ∧ (P ∨ A)) modus ponens with 1, 6
8 ¬(P ∨ ¬¬(Q ∧ A)) → ¬((P ∨ Q) ∧ (P ∨ A)) elementary equivalence in 7 at 5 of hilb5 with hilb6
9 ¬(P ∨ ¬¬(Q ∧ A)) → ¬(¬¬(P ∨ Q) ∧ (P ∨ A)) elementary equivalence in 8 at 12 of hilb5 with hilb6
10 ¬(P ∨ ¬¬(Q ∧ A)) → ¬(¬¬(P ∨ Q) ∧ ¬¬(P ∨ A)) elementary equivalence in 9 at 17 of hilb5 with hilb6
11 ¬(P ∨ ¬¬(Q ∧ B)) → ¬(¬¬(P ∨ Q) ∧ ¬¬(P ∨ B)) replace proposition variable A by B in 10
12 ¬(P ∨ ¬¬(C ∧ B)) → ¬(¬¬(P ∨ C) ∧ ¬¬(P ∨ B)) replace proposition variable Q by C in 11
13 ¬(D ∨ ¬¬(C ∧ B)) → ¬(¬¬(D ∨ C) ∧ ¬¬(D ∨ B)) replace proposition variable P by D in 12
14 ¬(D ∨ ¬¬(C ∧ ¬A)) → ¬(¬¬(D ∨ C) ∧ ¬¬(D ∨ ¬A)) replace proposition variable B by ¬A in 13
15 ¬(D ∨ ¬¬(¬Q ∧ ¬A)) → ¬(¬¬(D ∨ ¬Q) ∧ ¬¬(D ∨ ¬A)) replace proposition variable C by ¬Q in 14
16 ¬(¬P ∨ ¬¬(¬Q ∧ ¬A)) → ¬(¬¬(¬P ∨ ¬Q) ∧ ¬¬(¬P ∨ ¬A)) replace proposition variable D by ¬P in 15
17 (P ∧ ¬(¬Q ∧ ¬A)) → ¬(¬¬(¬P ∨ ¬Q) ∧ ¬¬(¬P ∨ ¬A)) reverse abbreviation and in 16 at occurence 1
18 (P ∧ (Q ∨ A)) → ¬(¬¬(¬P ∨ ¬Q) ∧ ¬¬(¬P ∨ ¬A)) elementary equivalence in 17 at 1 of hilb39 with hilb38
19 (P ∧ (Q ∨ A)) → (¬(¬P ∨ ¬Q) ∨ ¬(¬P ∨ ¬A)) elementary equivalence in 18 at 1 of hilb39 with hilb38
20 (P ∧ (Q ∨ A)) → ((P ∧ Q) ∨ ¬(¬P ∨ ¬A)) reverse abbreviation and in 19 at occurence 1
21 (P ∧ (Q ∨ A)) → ((P ∧ Q) ∨ (P ∧ A)) reverse abbreviation and in 20 at occurence 1
qed

The second distributive law (second direction):

6. Proposition
      ((P ∧ Q) ∨ (P ∧ A)) → (P ∧ (Q ∨ A))     (hilb41)

Proof:
1 (P ∨ (Q ∧ A)) → ((P ∨ Q) ∧ (P ∨ A)) add proposition hilb36
2 (P → Q) → (¬Q → ¬P) add proposition hilb7
3 (P → A) → (¬A → ¬P) replace proposition variable Q by A in 2
4 (B → A) → (¬A → ¬B) replace proposition variable P by B in 3
5 (B → ((P ∨ Q) ∧ (P ∨ A))) → (¬((P ∨ Q) ∧ (P ∨ A)) → ¬B) replace proposition variable A by (P ∨ Q) ∧ (P ∨ A) in 4
6 ((P ∨ (Q ∧ A)) → ((P ∨ Q) ∧ (P ∨ A))) → (¬((P ∨ Q) ∧ (P ∨ A)) → ¬(P ∨ (Q ∧ A))) replace proposition variable B by P ∨ (Q ∧ A) in 5
7 ¬((P ∨ Q) ∧ (P ∨ A)) → ¬(P ∨ (Q ∧ A)) modus ponens with 1, 6
8 ¬((P ∨ Q) ∧ (P ∨ A)) → ¬(P ∨ ¬¬(Q ∧ A)) elementary equivalence in 7 at 13 of hilb5 with hilb6
9 ¬(¬¬(P ∨ Q) ∧ (P ∨ A)) → ¬(P ∨ ¬¬(Q ∧ A)) elementary equivalence in 8 at 4 of hilb5 with hilb6
10 ¬(¬¬(P ∨ Q) ∧ ¬¬(P ∨ A)) → ¬(P ∨ ¬¬(Q ∧ A)) elementary equivalence in 9 at 9 of hilb5 with hilb6
11 ¬(¬¬(P ∨ Q) ∧ ¬¬(P ∨ B)) → ¬(P ∨ ¬¬(Q ∧ B)) replace proposition variable A by B in 10
12 ¬(¬¬(P ∨ C) ∧ ¬¬(P ∨ B)) → ¬(P ∨ ¬¬(C ∧ B)) replace proposition variable Q by C in 11
13 ¬(¬¬(D ∨ C) ∧ ¬¬(D ∨ B)) → ¬(D ∨ ¬¬(C ∧ B)) replace proposition variable P by D in 12
14 ¬(¬¬(D ∨ C) ∧ ¬¬(D ∨ ¬A)) → ¬(D ∨ ¬¬(C ∧ ¬A)) replace proposition variable B by ¬A in 13
15 ¬(¬¬(D ∨ ¬Q) ∧ ¬¬(D ∨ ¬A)) → ¬(D ∨ ¬¬(¬Q ∧ ¬A)) replace proposition variable C by ¬Q in 14
16 ¬(¬¬(¬P ∨ ¬Q) ∧ ¬¬(¬P ∨ ¬A)) → ¬(¬P ∨ ¬¬(¬Q ∧ ¬A)) replace proposition variable D by ¬P in 15
17 ¬(¬(P ∧ Q) ∧ ¬¬(¬P ∨ ¬A)) → ¬(¬P ∨ ¬¬(¬Q ∧ ¬A)) reverse abbreviation and in 16 at occurence 1
18 ¬(¬(P ∧ Q) ∧ ¬(P ∧ A)) → ¬(¬P ∨ ¬¬(¬Q ∧ ¬A)) reverse abbreviation and in 17 at occurence 1
19 ¬(¬(P ∧ Q) ∧ ¬(P ∧ A)) → (P ∧ ¬(¬Q ∧ ¬A)) reverse abbreviation and in 18 at occurence 1
20 ((P ∧ Q) ∨ (P ∧ A)) → (P ∧ ¬(¬Q ∧ ¬A)) elementary equivalence in 19 at 1 of hilb39 with hilb38
21 ((P ∧ Q) ∨ (P ∧ A)) → (P ∧ (Q ∨ A)) elementary equivalence in 20 at 1 of hilb39 with hilb38
qed

Cross References

This document is used by the following documents: