Froggy Problem Solved by underscores and barred premisses
Lewis Carroll's Froggy problem using the Dictionary given by Lewis Carroll. I have followed the method and roughly the presentation used by Carroll in "The Pigs and Balloons Problem" Book XIII Chapter XII as published by Bartley from a Carroll manuscript dated 7/2/93.
Bartley explains how to handle the case where a term appears in one premiss (say A) whereas its complement appears in two or more premisses (say B and C). In Carroll's terminology, premiss A is thus barred by premisses B and C. His rule is that a barred premiss may not be used until all the premisses barring it have been used. However, no mention is made of the case where both the term and its complement appear in two or more premisses. The solution I have devised, which seems to me logical and has the added merit that it seems to work, is as follows:Apply Carroll's original rule to determine barred premisses. After using a premiss, recreate the register omitting the used premiss and re-apply Carroll's rule to determine the new bars, but of course honouring the bars that still remain from the previous list.
Here is the symbolic form of the problem. I have divided Carroll's premisses 3,11 and 17 into their consituent parts as in Carroll's method of trees but I have renumbered the resulting premisses instead of using Carroll's notation of 3*, 3** etc.
New number
Carroll's number
Symbolic form of premiss
1
1
~s ~r
2
2
~m h d
3
3*
E ~a
4
4
l n ~v
5
5
z m c
6
6
t ~A
7
7
~s ~n c r
8
8
z v ~m
9
9
E ~w
10
10
v k m ~t
11
11*
E ~s
12
12
A B
13
13
k ~h ~n
14
14
r ~c
15
15
~v ~a ~h ~l
16
16
w ~t s ~n
17
17*
d ~e
18
18
s n ~b ~B
19
19
w e ~z
20
20
~t ~A ~r ~c n
21
3**
E k
22
11**
E ~c
23
11***
E n
24
17**
d ~k
The registry is now:
Entity
Appears in
Complement appears in
a
3 15
b
18
c
5 7
14 20 22
d
2 17 24
e
19
17
h
2
13 15
k
10 13 21
24
l
4
15
m
5 10
2 8
n
4 18 20 23
7 13 16
r
7 14
1 20
s
16 18
1 7 11
t
6
10 16 20
v
8 10
4 15
w
16 19
9
z
5 8
19
A
12
6 20
E
3 9 11 21 22 23
B
12
18
and the barred premises are as follows:
12
barred by
6 20
6
barred by
10 16 20
19
barred by
5 8
9
barred by
16 19
2
barred by
13 15
24
barred by
10 13 21
Using proposition 1 add ~s ~r to the solution string so the solution string becomes: ~s ~r
The registry is now:
Entity
Appears in
Complement appears in
a
3 15
b
18
c
5 7
14 20 22
d
2 17 24
e
19
17
h
2
13 15
k
10 13 21
24
l
4
15
m
5 10
2 8
n
4 18 20 23
7 13 16
r
7 14
20
s
16 18
7 11
t
6
10 16 20
v
8 10
4 15
w
16 19
9
z
5 8
19
A
12
6 20
E
3 9 11 21 22 23
B
12
18
and the barred premises are as follows:
12
barred by
6 20
6
barred by
10 16 20
20
barred by
7 14
19
barred by
5 8
9
barred by
16 19
2
barred by
13 15
24
barred by
10 13 21
Using proposition 7 add ~s ~n c r to the solution string so the solution string becomes: ~s ~r ~s ~n c r
The registry is now:
Entity
Appears in
Complement appears in
a
3 15
b
18
c
5
14 20 22
d
2 17 24
e
19
17
h
2
13 15
k
10 13 21
24
l
4
15
m
5 10
2 8
n
4 18 20 23
13 16
r
14
20
s
16 18
11
t
6
10 16 20
v
8 10
4 15
w
16 19
9
z
5 8
19
A
12
6 20
E
3 9 11 21 22 23
B
12
18
and the barred premises are as follows:
12
barred by
6 20
5
barred by
14 20 22
20
barred by
14
2
barred by
13 15
11
barred by
16 18
24
barred by
10 13 21
6
barred by
10 16 20
19
barred by
5 8
9
barred by
16 19
From the solution string ~s ~r ~s ~n c r we can delete "r" giving: ~s ~s ~n c
Using proposition 16 add w ~t s ~n to the solution string so the solution string becomes: ~s ~s ~n c w ~t s ~n
The registry is now:
Entity
Appears in
Complement appears in
a
3 15
b
18
c
5
14 20 22
d
2 17 24
e
19
17
h
2
13 15
k
10 13 21
24
l
4
15
m
5 10
2 8
n
4 18 20 23
13
r
14
20
s
18
11
t
6
10 20
v
8 10
4 15
w
19
9
z
5 8
19
A
12
6 20
E
3 9 11 21 22 23
B
12
18
and the barred premises are as follows:
12
barred by
6 20
5
barred by
14 20 22
20
barred by
14
2
barred by
13 15
11
barred by
18
24
barred by
10 13 21
13
barred by
4 18 20 23
6
barred by
10 20
19
barred by
5 8
9
barred by
19
From the solution string ~s ~s ~n c w ~t s ~n we can delete "s" giving: ~n c w ~t ~n
Using proposition 18 add s n ~b ~B to the solution string so the solution string becomes: ~n c w ~t ~n s n ~b ~B
The registry is now:
Entity
Appears in
Complement appears in
a
3 15
b
c
5
14 20 22
d
2 17 24
e
19
17
h
2
13 15
k
10 13 21
24
l
4
15
m
5 10
2 8
n
4 20 23
13
r
14
20
s
11
t
6
10 20
v
8 10
4 15
w
19
9
z
5 8
19
A
12
6 20
E
3 9 11 21 22 23
B
12
and the barred premises are as follows:
12
barred by
6 20
5
barred by
14 20 22
20
barred by
14
2
barred by
13 15
24
barred by
10 13 21
13
barred by
4 20 23
6
barred by
10 20
19
barred by
5 8
9
barred by
19
From the solution string ~n c w ~t ~n s n ~b ~B we can delete "n" giving: c w ~t s ~b ~B
Using proposition 14 add r ~c to the solution string so the solution string becomes: c w ~t s ~b ~B r ~c
The registry is now:
Entity
Appears in
Complement appears in
a
3 15
b
c
5
20 22
d
2 17 24
e
19
17
h
2
13 15
k
10 13 21
24
l
4
15
m
5 10
2 8
n
4 20 23
13
r
20
s
11
t
6
10 20
v
8 10
4 15
w
19
9
z
5 8
19
A
12
6 20
E
3 9 11 21 22 23
B
12
and the barred premises are as follows:
12
barred by
6 20
5
barred by
20 22
2
barred by
13 15
24
barred by
10 13 21
13
barred by
4 20 23
6
barred by
10 20
19
barred by
5 8
9
barred by
19
From the solution string c w ~t s ~b ~B r ~c we can delete "c" giving: w ~t s ~b ~B r
Using proposition 11 add E ~s to the solution string so the solution string becomes: w ~t s ~b ~B r E ~s
The registry is now:
Entity
Appears in
Complement appears in
a
3 15
b
c
5
20 22
d
2 17 24
e
19
17
h
2
13 15
k
10 13 21
24
l
4
15
m
5 10
2 8
n
4 20 23
13
r
20
s
t
6
10 20
v
8 10
4 15
w
19
9
z
5 8
19
A
12
6 20
E
3 9 21 22 23
B
12
and the barred premises are as follows:
12
barred by
6 20
5
barred by
20 22
2
barred by
13 15
24
barred by
10 13 21
13
barred by
4 20 23
6
barred by
10 20
19
barred by
5 8
9
barred by
19
From the solution string w ~t s ~b ~B r E ~s we can delete "s" giving: w ~t ~b ~B r E
Using proposition 20 add ~t ~A ~r ~c n to the solution string so the solution string becomes: w ~t ~b ~B r E ~t ~A ~r ~c n
The registry is now:
Entity
Appears in
Complement appears in
a
3 15
b
c
5
22
d
2 17 24
e
19
17
h
2
13 15
k
10 13 21
24
l
4
15
m
5 10
2 8
n
4 23
13
r
s
t
6
10
v
8 10
4 15
w
19
9
z
5 8
19
A
12
6
E
3 9 21 22 23
B
12
and the barred premises are as follows:
12
barred by
6
5
barred by
22
2
barred by
13 15
24
barred by
10 13 21
13
barred by
4 23
6
barred by
10
19
barred by
5 8
9
barred by
19
From the solution string w ~t ~b ~B r E ~t ~A ~r ~c n we can delete "r" giving: w ~t ~b ~B E ~t ~A ~c n
Using proposition 10 add v k m ~t to the solution string so the solution string becomes: w ~t ~b ~B E ~t ~A ~c n v k m ~t
The registry is now:
Entity
Appears in
Complement appears in
a
3 15
b
c
5
22
d
2 17 24
e
19
17
h
2
13 15
k
13 21
24
l
4
15
m
5
2 8
n
4 23
13
r
s
t
6
v
8
4 15
w
19
9
z
5 8
19
A
12
6
E
3 9 21 22 23
B
12
and the barred premises are as follows:
12
barred by
6
5
barred by
22
2
barred by
13 15
24
barred by
13 21
13
barred by
4 23
19
barred by
5 8
9
barred by
19
8
barred by
4 15
Using proposition 6 add t ~A to the solution string so the solution string becomes: w ~t ~b ~B E ~t ~A ~c n v k m ~t t ~A
The registry is now:
Entity
Appears in
Complement appears in
a
3 15
b
c
5
22
d
2 17 24
e
19
17
h
2
13 15
k
13 21
24
l
4
15
m
5
2 8
n
4 23
13
r
s
t
v
8
4 15
w
19
9
z
5 8
19
A
12
E
3 9 21 22 23
B
12
and the barred premises are as follows:
5
barred by
22
2
barred by
13 15
24
barred by
13 21
13
barred by
4 23
19
barred by
5 8
9
barred by
19
8
barred by
4 15
From the solution string w ~t ~b ~B E ~t ~A ~c n v k m ~t t ~A we can delete "t" giving: w ~b ~B E ~A ~c n v k m ~A
Using proposition 4 add l n ~v to the solution string so the solution string becomes: w ~b ~B E ~A ~c n v k m ~A l n ~v
The registry is now:
Entity
Appears in
Complement appears in
a
3 15
b
c
5
22
d
2 17 24
e
19
17
h
2
13 15
k
13 21
24
l
15
m
5
2 8
n
23
13
r
s
t
v
8
15
w
19
9
z
5 8
19
A
12
E
3 9 21 22 23
B
12
and the barred premises are as follows:
5
barred by
22
2
barred by
13 15
24
barred by
13 21
13
barred by
23
19
barred by
5 8
9
barred by
19
8
barred by
15
From the solution string w ~b ~B E ~A ~c n v k m ~A l n ~v we can delete "v" giving: w ~b ~B E ~A ~c n k m ~A l n
Using proposition 12 add A B to the solution string so the solution string becomes: w ~b ~B E ~A ~c n k m ~A l n A B
The registry is now:
Entity
Appears in
Complement appears in
a
3 15
b
c
5
22
d
2 17 24
e
19
17
h
2
13 15
k
13 21
24
l
15
m
5
2 8
n
23
13
r
s
t
v
8
15
w
19
9
z
5 8
19
A
E
3 9 21 22 23
B
and the barred premises are as follows:
5
barred by
22
2
barred by
13 15
24
barred by
13 21
13
barred by
23
19
barred by
5 8
9
barred by
19
8
barred by
15
From the solution string w ~b ~B E ~A ~c n k m ~A l n A B we can delete "A" giving: w ~b ~B E ~c n k m l n B
From the solution string w ~b ~B E ~c n k m l n B we can delete "B" giving: w ~b E ~c n k m l n
Using proposition 15 add ~v ~a ~h ~l to the solution string so the solution string becomes: w ~b E ~c n k m l n ~v ~a ~h ~l
The registry is now:
Entity
Appears in
Complement appears in
a
3
b
c
5
22
d
2 17 24
e
19
17
h
2
13
k
13 21
24
l
m
5
2 8
n
23
13
r
s
t
v
8
w
19
9
z
5 8
19
A
E
3 9 21 22 23
B
and the barred premises are as follows:
5
barred by
22
2
barred by
13
24
barred by
13 21
13
barred by
23
19
barred by
5 8
9
barred by
19
From the solution string w ~b E ~c n k m l n ~v ~a ~h ~l we can delete "l" giving: w ~b E ~c n k m n ~v ~a ~h
Using proposition 8 add z v ~m to the solution string so the solution string becomes: w ~b E ~c n k m n ~v ~a ~h z v ~m
The registry is now:
Entity
Appears in
Complement appears in
a
3
b
c
5
22
d
2 17 24
e
19
17
h
2
13
k
13 21
24
l
m
5
2
n
23
13
r
s
t
v
w
19
9
z
5
19
A
E
3 9 21 22 23
B
and the barred premises are as follows:
5
barred by
22
2
barred by
13
24
barred by
13 21
13
barred by
23
19
barred by
5
9
barred by
19
From the solution string w ~b E ~c n k m n ~v ~a ~h z v ~m we can delete "m" giving: w ~b E ~c n k n ~v ~a ~h z v
From the solution string w ~b E ~c n k n ~v ~a ~h z v we can delete "v" giving: w ~b E ~c n k n ~a ~h z
Using proposition 22 add E ~c to the solution string so the solution string becomes: w ~b E ~c n k n ~a ~h z E ~c
The registry is now:
Entity
Appears in
Complement appears in
a
3
b
c
5
d
2 17 24
e
19
17
h
2
13
k
13 21
24
l
m
5
2
n
23
13
r
s
t
v
w
19
9
z
5
19
A
E
3 9 21 23
B
and the barred premises are as follows:
2
barred by
13
24
barred by
13 21
13
barred by
23
19
barred by
5
9
barred by
19
Using proposition 5 add z m c to the solution string so the solution string becomes: w ~b E ~c n k n ~a ~h z E ~c z m c
The registry is now:
Entity
Appears in
Complement appears in
a
3
b
c
d
2 17 24
e
19
17
h
2
13
k
13 21
24
l
m
2
n
23
13
r
s
t
v
w
19
9
z
19
A
E
3 9 21 23
B
and the barred premises are as follows:
2
barred by
13
24
barred by
13 21
13
barred by
23
9
barred by
19
From the solution string w ~b E ~c n k n ~a ~h z E ~c z m c we can delete "c" giving: w ~b E n k n ~a ~h z E z m
Using proposition 19 add w e ~z to the solution string so the solution string becomes: w ~b E n k n ~a ~h z E z m w e ~z
The registry is now:
Entity
Appears in
Complement appears in
a
3
b
c
d
2 17 24
e
17
h
2
13
k
13 21
24
l
m
2
n
23
13
r
s
t
v
w
9
z
A
E
3 9 21 23
B
and the barred premises are as follows:
2
barred by
13
24
barred by
13 21
13
barred by
23
From the solution string w ~b E n k n ~a ~h z E z m w e ~z we can delete "z" giving: w ~b E n k n ~a ~h E m w e
Using proposition 9 add E ~w to the solution string so the solution string becomes: w ~b E n k n ~a ~h E m w e E ~w
The registry is now:
Entity
Appears in
Complement appears in
a
3
b
c
d
2 17 24
e
17
h
2
13
k
13 21
24
l
m
2
n
23
13
r
s
t
v
w
z
A
E
3 21 23
B
and the barred premises are as follows:
2
barred by
13
24
barred by
13 21
13
barred by
23
From the solution string w ~b E n k n ~a ~h E m w e E ~w we can delete "w" giving: ~b E n k n ~a ~h E m e E
Using proposition 17 add d ~e to the solution string so the solution string becomes: ~b E n k n ~a ~h E m e E d ~e
The registry is now:
Entity
Appears in
Complement appears in
a
3
b
c
d
2 24
e
h
2
13
k
13 21
24
l
m
2
n
23
13
r
s
t
v
w
z
A
E
3 21 23
B
and the barred premises are as follows:
2
barred by
13
24
barred by
13 21
13
barred by
23
From the solution string ~b E n k n ~a ~h E m e E d ~e we can delete "e" giving: ~b E n k n ~a ~h E m E d
Using proposition 23 add E n to the solution string so the solution string becomes: ~b E n k n ~a ~h E m E d E n
The registry is now:
Entity
Appears in
Complement appears in
a
3
b
c
d
2 24
e
h
2
13
k
13 21
24
l
m
2
n
13
r
s
t
v
w
z
A
E
3 21
B
and the barred premises are as follows:
2
barred by
13
24
barred by
13 21
Using proposition 13 add k ~h ~n to the solution string so the solution string becomes: ~b E n k n ~a ~h E m E d E n k ~h ~n
The registry is now:
Entity
Appears in
Complement appears in
a
3
b
c
d
2 24
e
h
2
k
21
24
l
m
2
n
r
s
t
v
w
z
A
E
3 21
B
and the barred premises are as follows:
24
barred by
21
From the solution string ~b E n k n ~a ~h E m E d E n k ~h ~n we can delete "n" giving: ~b E k ~a ~h E m E d E k ~h
Using proposition 2 add ~m h d to the solution string so the solution string becomes: ~b E k ~a ~h E m E d E k ~h ~m h d
The registry is now:
Entity
Appears in
Complement appears in
a
3
b
c
d
24
e
h
k
21
24
l
m
n
r
s
t
v
w
z
A
E
3 21
B
and the barred premises are as follows:
24
barred by
21
From the solution string ~b E k ~a ~h E m E d E k ~h ~m h d we can delete "m" giving: ~b E k ~a ~h E E d E k ~h h d
From the solution string ~b E k ~a ~h E E d E k ~h h d we can delete "h" giving: ~b E k ~a E E d E k d
Using proposition 21 add E k to the solution string so the solution string becomes: ~b E k ~a E E d E k d E k
The registry is now:
Entity
Appears in
Complement appears in
a
3
b
c
d
24
e
h
k
24
l
m
n
r
s
t
v
w
z
A
E
3
B
and the barred premises are as follows:
There are no bars
Using proposition 24 add d ~k to the solution string so the solution string becomes: ~b E k ~a E E d E k d E k d ~k
The registry is now:
Entity
Appears in
Complement appears in
a
3
b
c
d
e
h
k
l
m
n
r
s
t
v
w
z
A
E
3
B
and the barred premises are as follows:
There are no bars
From the solution string ~b E k ~a E E d E k d E k d ~k we can delete "k" giving: ~b E ~a E E d E d E d
So we are left with only the retinends, giving us the desired conclusion of as required