INTRODUCTION
************
Given unary predicate S and binary predicate F, and objects 0
and 1 such that:
(1) ALL(a):[S(a) <=> a=0]
(2) ~1=0
(3) ALL(a):[S(a) => EXIST(b):[S(b) & F(a,b) &
ALL(c):[S(c) => [F(a,c) => c=b]]]]
Then we have F(0,0) being true. What about F(1,0)? (See comment
at end)
By Dan Christensen
2021-12-04
PROOF
*****
Define: S and 0
1 ALL(a):[S(a) <=> a=0]
Axiom
Define: 1
2 ~1=0
Axiom
Define: F
3 ALL(a):[S(a) => EXIST(b):[S(b) &
F(a,b) & ALL(c):[S(c) => [F(a,c) => c=b]]]]
Axiom
Prove: S(0)
4 S(0) <=> 0=0
U Spec, 1
5 [S(0) => 0=0] & [0=0 => S(0)]
Iff-And, 4
6 0=0 => S(0)
Split, 5
7 0=0
Reflex
As Required:
8 S(0)
Detach, 6, 7
Prove: ~S(1)
9 S(1) <=> 1=0
U Spec, 1
10 [S(1) => 1=0] & [1=0 => S(1)]
Iff-And, 9
11 S(1) => 1=0
Split, 10
12 ~1=0 => ~S(1)
Contra, 11
As Required:
13 ~S(1)
Detach, 12, 2
Prove: F(0,0)
14 S(0) => EXIST(b):[S(b) & F(0,b) &
ALL(c):[S(c) => [F(0,c) => c=b]]]
U Spec, 3
15 EXIST(b):[S(b) & F(0,b) &
ALL(c):[S(c) => [F(0,c) => c=b]]]
Detach, 14, 8
16 S(x) & F(0,x) & ALL(c):[S(c) => [F(0,c) => c=x]]
E Spec, 15
17 S(x)
Split, 16
18 F(0,x)
Split, 16
19 ALL(c):[S(c) => [F(0,c) => c=x]]
Split, 16
20 S(x) <=> x=0
U Spec, 1
21 [S(x) => x=0] & [x=0 => S(x)]
Iff-And, 20
22 S(x) => x=0
Split, 21
23 x=0
Detach, 22, 17
As Required:
24 F(0,0)
Substitute, 23, 18
COMMENT
*******
Can we determine a truth value for, say, F(1,0)? No, not from
the above assumptions (lines 1-3).
Applying the definition of F for a=1, we obtain the following.
Note that we cannot use this result to infer
either the existence or non-existense of b since we already have
~S(1) (line 13).
25 S(1) => EXIST(b):[S(b) & F(1,b) &
ALL(c):[S(c) => [F(1,c) => c=b]]]
U Spec, 3