-
-
Notifications
You must be signed in to change notification settings - Fork 3
/
Copy paths5proofs.txt
73 lines (58 loc) · 3.78 KB
/
s5proofs.txt
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
[ Note: All lines before the first line
containing a semicolon are ignored
and can be used for comment headers. ]
Proof system configuration: pmGenerator -c -n -N -1 -s CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp (or "-N 1" for faster – but incomplete – generation via outruling consecutive necessitation steps)
SHA-512/224 hash: d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f (or 360ceff28c45b2d8ea630fc79a7dad68b04acdceaf41521e9f6ecd95)
Command to reduce: pmGenerator -c -n -N -1 -s CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp -r data/s5proofs.txt data/s5proofs-reducer.txt -d -a SD data/s5proofs-reducer.txt data/s5proofs.txt data/s5proofs-result-all.txt -l -d -w
or: pmGenerator -c -n -N 1 -s CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp -r data/s5proofs.txt data/s5proofs-reducer.txt -d -a SD data/s5proofs-reducer.txt data/s5proofs.txt data/s5proofs-result-all.txt -l -d -w
Command to reassemble: pmGenerator -c -n -N -1 -s CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp -a SD data/empty.txt data/s5proofs.txt data/s5proofs-result-all.txt -l -d -w
or: pmGenerator -c -n -N 1 -s CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp -a SD data/empty.txt data/s5proofs.txt data/s5proofs-result-all.txt -l -d -w
Note that these proofs may also be reducible from S5 without N-rule (configuration without "-N <limit or -1>", hash f3080a7440bc4f7a8149647365da7c36fea7e287fa6b198737e9837d).
Some proofs may even be reducible from systems with proper subsets of the same axioms. But since proofs with axioms missing from the system cannot be parsed,
one would have to place the proof files of a subsystem in a system with all here used axioms, and address the latter system.
(P -> (Q -> P)); ! Axiom 1 by Frege (CpCqp)
(P -> (Q -> P)); ! Result of proof
1; ! 1 step
((P -> (Q -> R)) -> ((P -> Q) -> (P -> R)))
; ! Axiom 2 by Frege (CCpCqrCCpqCpr)
((P -> (Q -> R)) -> ((P -> Q) -> (P -> R))); ! Result of proof
2; ! 1 step
((~ P -> ~ Q) -> (Q -> P))
; ! Axiom 3 for Frege by Łukasiewicz (CCNpNqCqp)
((~ P -> ~ Q) -> (Q -> P)); ! Result of proof
3; ! 1 step
(□ P -> P); ! Axiom T (CLpp)
(□ P -> P); ! Result of proof
4; ! 1 step
(□ (P -> Q) -> (□ P -> □ Q)); ! Axiom K by Kripke (CLCpqCLpLq)
(□ (P -> Q) -> (□ P -> □ Q)); ! Result of proof
5; ! 1 step
(◇ P -> □ ◇ P); ! Axiom 5 by Lewis (CMpLMp, i.e. CNLNpLNLNp)
(~ □ ~ P -> □ ~ □ ~ P); ! Result of proof
6; ! 1 step
(P -> □ ◇ P); ! Axiom B by Brouwer (CpLMp, i.e. CpLNLNp)
(P -> □ ~ □ ~ P); ! Result of proof
DD2D16D3DD2D14DD2DD2D13DD2D1311; ! 31 steps
(□ P -> □ □ P); ! Axiom 4 by Lewis (CLpLLp)
(□ P -> □ □ P); ! Result of proof
DD2D1D5NDD2D1D5NDD2DD2D13DD2D1311D3DD2D1D3DD2DD2D13DD2D1311DD2D1D5DD5
NDD2D13DD2D1D2D1D3DD2DD2D13DD2D1311DD2D1DD22D2DD2D13DD2D1311ND5ND3DD2
DD2D13DD2D13116DD2D16D3DD2D14DD2DD2D13DD2D1311; ! 184 steps
(□ P -> ◇ P); ! Axiom D (CLpMp, i.e. CLpNLNp)
(□ P -> ~ □ ~ P); ! Result of proof
DD2D1D3DD2D14DD2DD2D13DD2D13114; ! 31 steps
(P -> ◇ P); ! Alternative to axiom T (CpMp, i.e. CpNLNp)
(P -> ~ □ ~ P); ! Result of proof
D3DD2D14DD2DD2D13DD2D1311; ! 25 steps
(◇ ◇ P -> ◇ P)
; ! Alternative to axiom 4 (CMMpMp, i.e. CNLNNLNpNLNp of CNLNNLpNLp)
(~ □ ~ ~ □ P -> ~ □ P); ! Result of proof
DD2D14D3DD2D1D3DD2DD2D13DD2D1311DD2D1D5ND3DD2DD2D13DD2D1311DD2D1D5NDD
2D1D5NDD2DD2D13DD2D1311D3DD2D1D3DD2DD2D13DD2D1311DD2D1D5DD5NDD2D13DD2
D1D2D1D3DD2DD2D13DD2D1311DD2D1DD22D2DD2D13DD2D1311ND5ND3DD2DD2D13DD2D
131166; ! 213 steps
(~ □ P -> □ ~ □ P); ! Alternative to axiom 5 (CNLpLNLp)
(~ □ P -> □ ~ □ P); ! Result of proof
DD2D1D5DD5NDD2D13DD2D1D2D1D3DD2DD2D13DD2D1311DD2D1DD22D2DD2D13DD2D131
1ND5ND3DD2DD2D13DD2D1311DD2D16D3DD2D1D3DD2DD2D13DD2D1311DD2D1D5NDD2DD
2D13DD2D1311DD2DD2D13DD2D1311; ! 167 steps