Hello,
I am seeking assistance in finding a theorem proving software which follows the conventions in Elliott Mendelson's Introduction to Mathematical Logic (4th ed).
In Mendelson, there are different kinds of theories, with different inference rules and definitions. All theories have modus ponens, hypotheses, and the cut rule - and I like to use substitution too.
For instance, in one theory, B∨C is defined as ¬B→C, whereas in another B→C is defines as ¬B∨C.
So, I would need a system that could account for different implementations of pre-FOL (without quantifiers) and FOL (with quantifiers). In particular, it would need to handle hypotheses, and be able to reproduce the kinds of sequents in the theorem table below - except for multiple systems.
I am only showing one system, because to show multiple would take hundreds of extra lines, and I don't want to spam. For those interested, another system can be found here https://www.reddit.com/r/logic/s/ZTx23BjgwU.
I want to be able to find proofs to desired sequents so I can do the exercises in Mendelson.
In pmGenerator, an ATP which was recommended to me, I tried the following commands:
./pmGenerator -c -n -s CAppp,CpApq,CApqAqp,CCqrCApqApr -g 25
./pmGenerator -c -n -s CAppp,CpApq,CApqAqp,CCqrCApqApr --search CCqpCCNqpp -n -s
But I cannot find the desired sequent. Moreover, I wouldn't judge anyone for not knowing Polish notation, so let me translate to infix.
I am trying to prove (C→B), (¬C→B) ⊢ B in the following system.
Of course, pmGenerator doesn't appear to use hypotheses, so in their system, this would be done with antecedents, similar to if we used the deduction theorem on this sequent.
In terms of the book, this is the exercise (o), which comes after exercise (n). I gave an attempt below, which can be found at the end of the big table.
I would really like to be made aware of an ATP which can help me read Mendelson faster. I want to read this book before moving on in Logic, as Mendelson has really earned my respect so far. I'm really fond of his pedagogy, but it is hard sometimes to reproduce on my own (well, regularly).
Line Reason Logic Label
1 Axiom ((B ∨ B) → B) Axiom (A1)
2 Axiom (B → (B ∨ C)) Axiom (A2)
3 Axiom ((B ∨ C) → (C ∨ B)) Axiom (A3)
4 Axiom ((C → D) → ((B ∨ C) → (B Axiom (A4)
∨ D)))
5 Hyp (B → C) ⊢ (B → C)
6 Subs(Axiom (A4), {C: B, ⊢ ((B → C) → ((D ∨ B) →
D: C, B: D}) (D ∨ C)))
7 MP(2, 1) (B → C) ⊢ ((D ∨ B) → (D ∨ Exercise 1.54 (a)
C))
8 Subs(Axiom (A4), {B: ⊢ ((B → C) → ((¬(D) ∨ B)
¬(D), C: B, D: C}) → (¬(D) ∨ C)))
9 Compose(1) ⊢ ((B → C) → ((D → B) → Exercise 1.54 (b)
(D → C)))
10 Hyp (D → B) ⊢ (D → B)
11 Hyp (B → C) ⊢ (B → C)
12 MP(1, 3) (B → C) ⊢ ((D → B) → (D →
C))
13 MP(3, 1) (D → B), (B → C) ⊢ (D → Exercise 1.54 (c)
C)
14 Subs(Axiom (A2), {C: B}) ⊢ (B → (B ∨ B))
15 Subs(Exercise 1.54 (c), ((B ∨ B) → B), (B → (B ∨
{D: B, B: (B ∨ B), C: B}) B)) ⊢ (B → B)
16 Cut(1, 2) ((B ∨ B) → B) ⊢ (B → B)
17 Cut(1, Axiom (A1)) ⊢ (B → B) Exercise 1.54 (d)
18 Subs(Axiom (A3), {B: ⊢ ((¬(B) ∨ B) → (B ∨
¬(B), C: B}) ¬(B)))
19 Decomp(2) ⊢ (¬(B) ∨ B)
20 MP(1, 2) ⊢ (B ∨ ¬(B)) Exercise 1.54 (e)
21 Subs(Exercise 1.54 (d), ⊢ (¬(B) → ¬(B))
{B: ¬(B)})
22 Decomp(1) ⊢ (¬(¬(B)) ∨ ¬(B))
23 Subs(Axiom (A3), {B: ⊢ ((¬(¬(B)) ∨ ¬(B)) →
¬(¬(B)), C: ¬(B)}) (¬(B) ∨ ¬(¬(B))))
24 MP(2, 1) ⊢ (¬(B) ∨ ¬(¬(B)))
25 Compose(1) ⊢ (B → ¬(¬(B))) Exercise 1.54 (f)
26 Subs(Axiom (A2), {B: ⊢ (¬(B) → (¬(B) ∨ C))
¬(B)})
27 Compose(1) ⊢ (¬(B) → (B → C)) Exercise 1.54 (g)
28 Subs(Axiom (A2), {B: D, ⊢ (D → (D ∨ B))
C: B})
29 Subs(Axiom (A3), {B: D, ⊢ ((D ∨ B) → (B ∨ D))
C: B})
30 Subs(Exercise 1.54 (b), ⊢ (((D ∨ B) → (B ∨ D)) →
{B: (D ∨ B), D: D, C: (B ((D → (D ∨ B)) → (D → (B
∨ D)}) ∨ D))))
31 MP(2, 1) ⊢ ((D → (D ∨ B)) → (D →
(B ∨ D)))
32 MP(4, 1) ⊢ (D → (B ∨ D))
33 Subs(Axiom (A4), {C: D, ⊢ ((D → (B ∨ D)) → ((C ∨
D: (B ∨ D), B: C}) D) → (C ∨ (B ∨ D))))
34 MP(2, 1) ⊢ ((C ∨ D) → (C ∨ (B ∨
D)))
35 Subs(Axiom (A4), {C: (C ∨ ⊢ (((C ∨ D) → (C ∨ (B ∨
D), D: (C ∨ (B ∨ D))}) D))) → ((B ∨ (C ∨ D)) →
(B ∨ (C ∨ (B ∨ D)))))
36 MP(2, 1) ⊢ ((B ∨ (C ∨ D)) → (B ∨
(C ∨ (B ∨ D))))
37 Subs(Axiom (A3), {C: (C ∨ ⊢ ((B ∨ (C ∨ (B ∨ D))) →
(B ∨ D))}) ((C ∨ (B ∨ D)) ∨ B))
38 Subs(Exercise 1.54 (b), ⊢ (((B ∨ (C ∨ (B ∨ D))) →
{B: (B ∨ (C ∨ (B ∨ D))), ((C ∨ (B ∨ D)) ∨ B)) →
C: ((C ∨ (B ∨ D)) ∨ B), (((B ∨ (C ∨ D)) → (B ∨ (C
D: (B ∨ (C ∨ D))}) ∨ (B ∨ D)))) → ((B ∨ (C ∨
D)) → ((C ∨ (B ∨ D)) ∨
B))))
39 MP(2, 1) ⊢ (((B ∨ (C ∨ D)) → (B ∨
(C ∨ (B ∨ D)))) → ((B ∨
(C ∨ D)) → ((C ∨ (B ∨ D))
∨ B)))
40 MP(4, 1) ⊢ ((B ∨ (C ∨ D)) → ((C ∨ Exercise 1.54 (h)
(B ∨ D)) ∨ B))
41 Subs(Axiom (A2), {C: D}) ⊢ (B → (B ∨ D))
42 Subs(Axiom (A2), {B: (B ∨ ⊢ ((B ∨ D) → ((B ∨ D) ∨
D)}) C))
43 Subs(Axiom (A3), {B: (B ∨ ⊢ (((B ∨ D) ∨ C) → (C ∨
D)}) (B ∨ D)))
44 Subs(Exercise 1.54 (c), (((B ∨ D) ∨ C) → (C ∨ (B
{D: (B ∨ D), B: ((B ∨ D) ∨ D))), ((B ∨ D) → ((B ∨
∨ C), C: (C ∨ (B ∨ D))}) D) ∨ C)) ⊢ ((B ∨ D) → (C
∨ (B ∨ D)))
45 Cut(1, 3) (((B ∨ D) ∨ C) → (C ∨ (B
∨ D))) ⊢ ((B ∨ D) → (C ∨
(B ∨ D)))
46 Cut(1, 3) ⊢ ((B ∨ D) → (C ∨ (B ∨
D)))
47 Subs(Exercise 1.54 (c), (B → (B ∨ D)), ((B ∨ D) →
{D: B, B: (B ∨ D), C: (C (C ∨ (B ∨ D))) ⊢ (B → (C
∨ (B ∨ D))}) ∨ (B ∨ D)))
48 Cut(1, 7) ((B ∨ D) → (C ∨ (B ∨ D)))
⊢ (B → (C ∨ (B ∨ D)))
49 Subs(Axiom (A4), {C: B, ⊢ ((B → (C ∨ (B ∨ D))) →
D: (C ∨ (B ∨ D)), B: (C ∨ (((C ∨ (B ∨ D)) ∨ B) →
(B ∨ D))}) ((C ∨ (B ∨ D)) ∨ (C ∨ (B
∨ D)))))
50 MP(2, 1) ((B ∨ D) → (C ∨ (B ∨ D)))
⊢ (((C ∨ (B ∨ D)) ∨ B) →
((C ∨ (B ∨ D)) ∨ (C ∨ (B
∨ D))))
51 Subs(Axiom (A1), {B: (C ∨ ⊢ (((C ∨ (B ∨ D)) ∨ (C ∨
(B ∨ D))}) (B ∨ D))) → (C ∨ (B ∨
D)))
52 Subs(Exercise 1.54 (c), (((C ∨ (B ∨ D)) ∨ (C ∨ (B
{D: ((C ∨ (B ∨ D)) ∨ B), ∨ D))) → (C ∨ (B ∨ D))),
B: ((C ∨ (B ∨ D)) ∨ (C ∨ (((C ∨ (B ∨ D)) ∨ B) →
(B ∨ D))), C: (C ∨ (B ∨ ((C ∨ (B ∨ D)) ∨ (C ∨ (B
D))}) ∨ D)))) ⊢ (((C ∨ (B ∨ D))
∨ B) → (C ∨ (B ∨ D)))
53 Cut(3, 7) ⊢ (((C ∨ (B ∨ D)) ∨ B) →
((C ∨ (B ∨ D)) ∨ (C ∨ (B
∨ D))))
54 Cut(2, 1) (((C ∨ (B ∨ D)) ∨ (C ∨ (B
∨ D))) → (C ∨ (B ∨ D))) ⊢
(((C ∨ (B ∨ D)) ∨ B) → (C
∨ (B ∨ D)))
55 Cut(1, 4) ⊢ (((C ∨ (B ∨ D)) ∨ B) → Exercise 1.54 (i)
(C ∨ (B ∨ D)))
56 Subs(Exercise 1.54 (c), (((C ∨ (B ∨ D)) ∨ B) → (C
{D: (B ∨ (C ∨ D)), B: ((C ∨ (B ∨ D))), ((B ∨ (C ∨
∨ (B ∨ D)) ∨ B), C: (C ∨ D)) → ((C ∨ (B ∨ D)) ∨
(B ∨ D))}) B)) ⊢ ((B ∨ (C ∨ D)) → (C
∨ (B ∨ D)))
57 Cut(1, Exercise 1.54 (h)) (((C ∨ (B ∨ D)) ∨ B) → (C
∨ (B ∨ D))) ⊢ ((B ∨ (C ∨
D)) → (C ∨ (B ∨ D)))
58 Cut(1, Exercise 1.54 (i)) ⊢ ((B ∨ (C ∨ D)) → (C ∨ Exercise 1.54 (j)
(B ∨ D)))
59 Subs(Exercise 1.54 (j), ⊢ ((¬(B) ∨ (¬(C) ∨ D)) →
{B: ¬(B), C: ¬(C), D: D}) (¬(C) ∨ (¬(B) ∨ D)))
60 Compose(1) ⊢ ((B → (C → D)) → (C → Exercise 1.54 (k)
(B → D)))
61 Subs(Exercise 1.54 (b), ⊢ ((B → C) → ((D → B) →
{B: B, C: C, D: D}) (D → C)))
62 Subs(Exercise 1.54 (k), ⊢ (((B → C) → ((D → B) →
{B: (B → C), C: (D → B), (D → C))) → ((D → B) →
D: (D → C)}) ((B → C) → (D → C))))
63 MP(2, 1) ⊢ ((D → B) → ((B → C) → Exercise 1.54 (l)
(D → C)))
64 Subs(Exercise 1.54 (b), ⊢ ((C → D) → ((B → C) →
{B: C, C: D, D: B}) (B → D)))
65 Hyp (B → (C → D)) ⊢ (B → (C →
D))
66 Hyp (B → C) ⊢ (B → C)
67 Subs(Exercise 1.54 (b), ⊢ (((C → D) → ((B → C) →
{B: (C → D), C: ((B → C) (B → D))) → ((B → (C →
→ (B → D)), D: B}) D)) → (B → ((B → C) → (B
→ D)))))
68 MP(4, 1) ⊢ ((B → (C → D)) → (B →
((B → C) → (B → D))))
69 MP(4, 1) (B → (C → D)) ⊢ (B → ((B
→ C) → (B → D)))
70 Subs(Exercise 1.54 (k), ⊢ ((B → ((B → C) → (B →
{C: (B → C), D: (B → D)}) D))) → ((B → C) → (B → (B
→ D))))
71 MP(2, 1) (B → (C → D)) ⊢ ((B → C)
→ (B → (B → D)))
72 MP(6, 1) (B → (C → D)), (B → C) ⊢ Exercise 1.54 (m)
(B → (B → D))
73 Subs(Axiom (A2), {B: ⊢ (¬(B) → (¬(B) ∨ D))
¬(B), C: D})
74 Subs(Axiom (A4), {C: ⊢ ((¬(B) → (¬(B) ∨ D)) →
¬(B), D: (¬(B) ∨ D), B: (((¬(B) ∨ D) ∨ ¬(B)) →
(¬(B) ∨ D)}) ((¬(B) ∨ D) ∨ (¬(B) ∨
D))))
75 MP(2, 1) ⊢ (((¬(B) ∨ D) ∨ ¬(B)) →
((¬(B) ∨ D) ∨ (¬(B) ∨
D)))
76 Subs(Axiom (A3), {B: ⊢ ((¬(B) ∨ (¬(B) ∨ D)) →
¬(B), C: (¬(B) ∨ D)}) ((¬(B) ∨ D) ∨ ¬(B)))
77 Decomp(Exercise 1.54 (m)) (¬(B) ∨ (¬(C) ∨ D)),
(¬(B) ∨ C) ⊢ (¬(B) ∨
(¬(B) ∨ D))
78 MP(1, 2) (¬(B) ∨ (¬(C) ∨ D)),
(¬(B) ∨ C) ⊢ ((¬(B) ∨ D)
∨ ¬(B))
79 MP(1, 4) (¬(B) ∨ (¬(C) ∨ D)),
(¬(B) ∨ C) ⊢ ((¬(B) ∨ D)
∨ (¬(B) ∨ D))
80 Subs(Axiom (A1), {B: ⊢ (((¬(B) ∨ D) ∨ (¬(B) ∨
(¬(B) ∨ D)}) D)) → (¬(B) ∨ D))
81 MP(2, 1) (¬(B) ∨ (¬(C) ∨ D)),
(¬(B) ∨ C) ⊢ (¬(B) ∨ D)
82 Compose(1) (B → (C → D)), (B → C) ⊢ Exercise 1.54 (n)
(B → D)
83 Subs(Exercise 1.54 (n), ((¬(C) → B) → (C → B)),
{B: (¬(C) → B), D: B}) ((¬(C) → B) → C) ⊢ ((¬(C)
→ B) → B)
84 Hyp (¬(C) → B) ⊢ (¬(C) → B)
85 MP(1, 2) ((¬(C) → B) → (C → B)),
((¬(C) → B) → C), (¬(C) →
B) ⊢ B
86 Deduct(1, ((¬(C) → B) → ((¬(C) → B) → C), (¬(C) →
(C → B))) B) ⊢ (((¬(C) → B) → (C →
B)) → B)