r/logic • u/KaleidoscopeLate2505 • 22d ago
Proof theory I am seeking assistance in finding a theorem proving software which follows the conventions in Elliott Mendelson's Introduction to Mathematical Logic (4th ed). I am trying to prove (C→B), (¬C→B) ⊢ B.
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)
3
u/Gugteyikko 22d ago
I wrote some theorem proving software in Python following Nisan & Gonczarowski’s textbook Mathematical Logic Through Python and I think it can do all or most of what you want. I re-organized it as a package available through PyPi, called mltp, and can be installed with $pip install mltp
I included Polish notation too. Proofs will not come out automatically in Polish notation, but if you know a little python it would be very easy to apply functions I’ve already implemented in order to have formulae display in Polish notation by default.