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, the only mention made of the case where both the term and its complement appear in two or more premisses is in Book XII, Ch III (on page 296 of Bartley's book) where Carroll refers to it as a "Barred Group". [Many thanks to Dr. Francine F. Abeles of Kean University for sending me this reference]. 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 numberCarroll's numberSymbolic form of premiss
11~s ~r
22~m h d
33E ~a
43*E k
54l n ~v
65z m c
76t ~A
87~s ~n c r
98z v ~m
109E ~w v
1110k m ~t
1211E ~s
1311*E ~c
1411**E n
1512A B
1613k ~h ~n
1714r ~c
1815~v ~a ~h ~l
1916w ~t s ~n
2017d ~e
2117*d ~k
2218s n ~b ~B
2319w e ~z
2420~t ~A ~r ~c n
The registry is now:
EntityAppears inComplement appears in
a3 18
b22
c6 8 13 17 24
d2 20 21
e23 20
h2 16 18
k4 11 16 21
l5 18
m6 11 2 9
n5 14 22 24 8 16 19
r8 17 1 24
s19 22 1 8 12
t7 11 19 24
v9 10 5 18
w19 23 10
z6 9 23
A15 7 24
E3 4 10 12 13 14
B15 22
and the barred premises are as follows:
7 barred by11 19 24
23 barred by6 9
15 barred by7 24
2 barred by16 18
21 barred by4 11 16
10 barred by19 23
Using proposition 1 add ~s ~r to the solution string
so the solution string becomes:
~s ~r
The registry is now:
EntityAppears inComplement appears in
a3 18
b22
c6 8 13 17 24
d2 20 21
e23 20
h2 16 18
k4 11 16 21
l5 18
m6 11 2 9
n5 14 22 24 8 16 19
r8 17 24
s19 22 8 12
t7 11 19 24
v9 10 5 18
w19 23 10
z6 9 23
A15 7 24
E3 4 10 12 13 14
B15 22
and the barred premises are as follows:
7 barred by11 19 24
23 barred by6 9
15 barred by7 24
2 barred by16 18
21 barred by4 11 16
10 barred by19 23
24 barred by8 17
Using proposition 8 add ~s ~n c r to the solution string
so the solution string becomes:
~s ~r ~s ~n c r
The registry is now:
EntityAppears inComplement appears in
a3 18
b22
c6 13 17 24
d2 20 21
e23 20
h2 16 18
k4 11 16 21
l5 18
m6 11 2 9
n5 14 22 24 16 19
r17 24
s19 22 12
t7 11 19 24
v9 10 5 18
w19 23 10
z6 9 23
A15 7 24
E3 4 10 12 13 14
B15 22
and the barred premises are as follows:
12 barred by19 22
15 barred by7 24
2 barred by16 18
21 barred by4 11 16
24 barred by17
7 barred by11 19 24
6 barred by13 17 24
23 barred by6 9
10 barred by19 23
From the solution string ~s ~r ~s ~n c r
we can delete "r" giving:
~s ~s ~n c
Using proposition 19 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:
EntityAppears inComplement appears in
a3 18
b22
c6 13 17 24
d2 20 21
e23 20
h2 16 18
k4 11 16 21
l5 18
m6 11 2 9
n5 14 22 24 16
r17 24
s22 12
t7 11 24
v9 10 5 18
w23 10
z6 9 23
A15 7 24
E3 4 10 12 13 14
B15 22
and the barred premises are as follows:
12 barred by22
15 barred by7 24
2 barred by16 18
21 barred by4 11 16
24 barred by17
7 barred by11 24
16 barred by5 14 22 24
6 barred by13 17 24
23 barred by6 9
10 barred by23
From the solution string ~s ~s ~n c w ~t s ~n
we can delete "s" giving:
~n c w ~t ~n
Using proposition 22 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:
EntityAppears inComplement appears in
a3 18
b
c6 13 17 24
d2 20 21
e23 20
h2 16 18
k4 11 16 21
l5 18
m6 11 2 9
n5 14 24 16
r17 24
s12
t7 11 24
v9 10 5 18
w23 10
z6 9 23
A15 7 24
E3 4 10 12 13 14
B15
and the barred premises are as follows:
15 barred by7 24
2 barred by16 18
21 barred by4 11 16
24 barred by17
7 barred by11 24
16 barred by5 14 24
6 barred by13 17 24
23 barred by6 9
10 barred by23
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 17 add r ~c to the solution string
so the solution string becomes:
c w ~t s ~b ~B r ~c
The registry is now:
EntityAppears inComplement appears in
a3 18
b
c6 13 24
d2 20 21
e23 20
h2 16 18
k4 11 16 21
l5 18
m6 11 2 9
n5 14 24 16
r24
s12
t7 11 24
v9 10 5 18
w23 10
z6 9 23
A15 7 24
E3 4 10 12 13 14
B15
and the barred premises are as follows:
15 barred by7 24
2 barred by16 18
21 barred by4 11 16
7 barred by11 24
16 barred by5 14 24
6 barred by13 24
23 barred by6 9
10 barred by23
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 12 add E ~s to the solution string
so the solution string becomes:
w ~t s ~b ~B r E ~s
The registry is now:
EntityAppears inComplement appears in
a3 18
b
c6 13 24
d2 20 21
e23 20
h2 16 18
k4 11 16 21
l5 18
m6 11 2 9
n5 14 24 16
r24
s
t7 11 24
v9 10 5 18
w23 10
z6 9 23
A15 7 24
E3 4 10 13 14
B15
and the barred premises are as follows:
15 barred by7 24
2 barred by16 18
21 barred by4 11 16
7 barred by11 24
16 barred by5 14 24
6 barred by13 24
23 barred by6 9
10 barred by23
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 24 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:
EntityAppears inComplement appears in
a3 18
b
c6 13
d2 20 21
e23 20
h2 16 18
k4 11 16 21
l5 18
m6 11 2 9
n5 14 16
r
s
t7 11
v9 10 5 18
w23 10
z6 9 23
A15 7
E3 4 10 13 14
B15
and the barred premises are as follows:
15 barred by7
2 barred by16 18
21 barred by4 11 16
7 barred by11
16 barred by5 14
6 barred by13
23 barred by6 9
10 barred by23
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 11 add k m ~t to the solution string
so the solution string becomes:
w ~t ~b ~B E ~t ~A ~c n k m ~t
The registry is now:
EntityAppears inComplement appears in
a3 18
b
c6 13
d2 20 21
e23 20
h2 16 18
k4 16 21
l5 18
m6 2 9
n5 14 16
r
s
t7
v9 10 5 18
w23 10
z6 9 23
A15 7
E3 4 10 13 14
B15
and the barred premises are as follows:
15 barred by7
2 barred by16 18
21 barred by4 16
16 barred by5 14
6 barred by13
23 barred by6 9
10 barred by23
Using proposition 7 add t ~A to the solution string
so the solution string becomes:
w ~t ~b ~B E ~t ~A ~c n k m ~t t ~A
The registry is now:
EntityAppears inComplement appears in
a3 18
b
c6 13
d2 20 21
e23 20
h2 16 18
k4 16 21
l5 18
m6 2 9
n5 14 16
r
s
t
v9 10 5 18
w23 10
z6 9 23
A15
E3 4 10 13 14
B15
and the barred premises are as follows:
2 barred by16 18
21 barred by4 16
16 barred by5 14
6 barred by13
23 barred by6 9
10 barred by23
From the solution string w ~t ~b ~B E ~t ~A ~c n k m ~t t ~A
we can delete "t" giving:
w ~b ~B E ~A ~c n k m ~A
Using proposition 15 add A B to the solution string
so the solution string becomes:
w ~b ~B E ~A ~c n k m ~A A B
The registry is now:
EntityAppears inComplement appears in
a3 18
b
c6 13
d2 20 21
e23 20
h2 16 18
k4 16 21
l5 18
m6 2 9
n5 14 16
r
s
t
v9 10 5 18
w23 10
z6 9 23
A
E3 4 10 13 14
B
and the barred premises are as follows:
2 barred by16 18
21 barred by4 16
16 barred by5 14
6 barred by13
23 barred by6 9
10 barred by23
From the solution string w ~b ~B E ~A ~c n k m ~A A B
we can delete "B" giving:
w ~b E ~A ~c n k m ~A A
From the solution string w ~b E ~A ~c n k m ~A A
we can delete "A" giving:
w ~b E ~c n k m
Using proposition 9 add z v ~m to the solution string
so the solution string becomes:
w ~b E ~c n k m z v ~m
The registry is now:
EntityAppears inComplement appears in
a3 18
b
c6 13
d2 20 21
e23 20
h2 16 18
k4 16 21
l5 18
m6 2
n5 14 16
r
s
t
v10 5 18
w23 10
z6 23
A
E3 4 10 13 14
B
and the barred premises are as follows:
2 barred by16 18
21 barred by4 16
16 barred by5 14
6 barred by13
23 barred by6
10 barred by23 5 18
From the solution string w ~b E ~c n k m z v ~m
we can delete "m" giving:
w ~b E ~c n k z v
Using proposition 5 add l n ~v to the solution string
so the solution string becomes:
w ~b E ~c n k z v l n ~v
The registry is now:
EntityAppears inComplement appears in
a3 18
b
c6 13
d2 20 21
e23 20
h2 16 18
k4 16 21
l18
m6 2
n14 16
r
s
t
v10 18
w23 10
z6 23
A
E3 4 10 13 14
B
and the barred premises are as follows:
2 barred by16 18
21 barred by4 16
16 barred by14
6 barred by13
23 barred by6
10 barred by23 18
From the solution string w ~b E ~c n k z v l n ~v
we can delete "v" giving:
w ~b E ~c n k z l n
Using proposition 18 add ~v ~a ~h ~l to the solution string
so the solution string becomes:
w ~b E ~c n k z l n ~v ~a ~h ~l
The registry is now:
EntityAppears inComplement appears in
a3
b
c6 13
d2 20 21
e23 20
h2 16
k4 16 21
l
m6 2
n14 16
r
s
t
v10
w23 10
z6 23
A
E3 4 10 13 14
B
and the barred premises are as follows:
2 barred by16
21 barred by4 16
16 barred by14
6 barred by13
23 barred by6
10 barred by23
From the solution string w ~b E ~c n k z l n ~v ~a ~h ~l
we can delete "l" giving:
w ~b E ~c n k z n ~v ~a ~h
Using proposition 13 add E ~c to the solution string
so the solution string becomes:
w ~b E ~c n k z n ~v ~a ~h E ~c
The registry is now:
EntityAppears inComplement appears in
a3
b
c6
d2 20 21
e23 20
h2 16
k4 16 21
l
m6 2
n14 16
r
s
t
v10
w23 10
z6 23
A
E3 4 10 14
B
and the barred premises are as follows:
2 barred by16
21 barred by4 16
16 barred by14
23 barred by6
10 barred by23
Using proposition 6 add z m c to the solution string
so the solution string becomes:
w ~b E ~c n k z n ~v ~a ~h E ~c z m c
The registry is now:
EntityAppears inComplement appears in
a3
b
c
d2 20 21
e23 20
h2 16
k4 16 21
l
m2
n14 16
r
s
t
v10
w23 10
z23
A
E3 4 10 14
B
and the barred premises are as follows:
2 barred by16
21 barred by4 16
16 barred by14
10 barred by23
From the solution string w ~b E ~c n k z n ~v ~a ~h E ~c z m c
we can delete "c" giving:
w ~b E n k z n ~v ~a ~h E z m
Using proposition 23 add w e ~z to the solution string
so the solution string becomes:
w ~b E n k z n ~v ~a ~h E z m w e ~z
The registry is now:
EntityAppears inComplement appears in
a3
b
c
d2 20 21
e20
h2 16
k4 16 21
l
m2
n14 16
r
s
t
v10
w10
z
A
E3 4 10 14
B
and the barred premises are as follows:
2 barred by16
21 barred by4 16
16 barred by14
From the solution string w ~b E n k z n ~v ~a ~h E z m w e ~z
we can delete "z" giving:
w ~b E n k n ~v ~a ~h E m w e
Using proposition 10 add E ~w v to the solution string
so the solution string becomes:
w ~b E n k n ~v ~a ~h E m w e E ~w v
The registry is now:
EntityAppears inComplement appears in
a3
b
c
d2 20 21
e20
h2 16
k4 16 21
l
m2
n14 16
r
s
t
v
w
z
A
E3 4 14
B
and the barred premises are as follows:
2 barred by16
21 barred by4 16
16 barred by14
From the solution string w ~b E n k n ~v ~a ~h E m w e E ~w v
we can delete "v" giving:
w ~b E n k n ~a ~h E m w e E ~w
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 20 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:
EntityAppears inComplement appears in
a3
b
c
d2 21
e
h2 16
k4 16 21
l
m2
n14 16
r
s
t
v
w
z
A
E3 4 14
B
and the barred premises are as follows:
2 barred by16
21 barred by4 16
16 barred by14
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 14 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:
EntityAppears inComplement appears in
a3
b
c
d2 21
e
h2 16
k4 16 21
l
m2
n16
r
s
t
v
w
z
A
E3 4
B
and the barred premises are as follows:
2 barred by16
21 barred by4 16
Using proposition 16 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:
EntityAppears inComplement appears in
a3
b
c
d2 21
e
h2
k4 21
l
m2
n
r
s
t
v
w
z
A
E3 4
B
and the barred premises are as follows:
21 barred by4
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:
EntityAppears inComplement appears in
a3
b
c
d21
e
h
k4 21
l
m
n
r
s
t
v
w
z
A
E3 4
B
and the barred premises are as follows:
21 barred by4
From the solution string ~b E k ~a ~h E m E d E k ~h ~m h d
we can delete "h" giving:
~b E k ~a E m E d E k ~m d
From the solution string ~b E k ~a E m E d E k ~m d
we can delete "m" giving:
~b E k ~a E E d E k d
Using proposition 4 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:
EntityAppears inComplement appears in
a3
b
c
d21
e
h
k21
l
m
n
r
s
t
v
w
z
A
E3
B
and the barred premises are as follows:
Using proposition 21 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:
EntityAppears inComplement appears in
a3
b
c
d
e
h
k
l
m
n
r
s
t
v
w
z
A
E3
B
and the barred premises are as follows:
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 Ea'b'd0 as required
Return to Lewis Carroll's Froggy problem