Sunday, October 5, 2014

The following gives us a proof of ECpqANpq with an adaptation of an idea in Arthur Prior's Formal Logic p. 65-66.

First formation rules:
  1. All lower case letters of the Latin alphabet are formulas.
  2. If x is a formula, then δx is a formula.
  3. If x is a formula, then Nx is a formula.
  4. If x and y are formulas, then C x y is a formula (spaces can get ignored or inserted freely).
Let "0" stand for falsity, and "1" for truth. We have the following matrix for implication "C", disjunction (or equivalently alternation) "A", and negation "N".
C | 0  1|  A| 0  1|  N
----------------------
0 | 1  1|  0| 0  1|  1
1*| 0  1|  1| 1  1|  0
This gives us the equations C00 =1, C01=1, C10=0, C11=1, A00=0, A01=1, A10=1, A11=1, N0=1, N1=0.
δ stands for a functioral variable. Paraphrasing Prior, where x is a formula, δx stands for any truth-function into which δ enters as argument. δa stands for any truth-function of b, such as Nb, Abb, Aab, CNba, CCbcCCabCac. δb can also stand for b itself. Substitution for δ occurs by putting the argument of δ into the position where an " ' " symbol appears. The notation x/y indicates that x is to get substituted with y for all instances of x in the formula in which x appears. For example, the substitution instruction δ/C ' ' in δr yields Crr. δ/C ' A ' p in C δr δp yields C CrArp CpApp. The substitution δ/' in say C δp δ1 just has us dropping δ yielding Cp1. δ/A ' C ' ' in C δp A δq δ Na yields C ApCpp A AqCqq CNaANaNa.
Note that the valuation function "v", v(C x y)=C v(x) v(y). Also, for the valuation function v(δx)=δv(x).
Now it turns out that the following is a meta-theorem.
Meta-Theorem 1: If v(x)=v(y), then v(C δx δy)=1. In other words, if x=y, then C δx δy follows.
Demonstration: Suppose v(x)=v(y). Since v(C00)=1, and v(C11)=1, it follows that for all p, v(Cpp)=1. Substituting p/δx in Cpp we then obtain that v(C δx δx)=1. Since v(C x y)=C v(x) v(y), it then follows that C v(δx) v(δx)=1. Since v(δx)=δv(x), it then follows that C δv(x) δv(x)=1. By the initial supposition, we then obtain that C δv(x) δ v(y)=1. Since v(δx)=δv(x) we then obtain that
C v(δx) v(δy)=1. From v(C x y)=C v(x) v(y) we thus obtain that v(C δx δy)=1. Therefore, if v(x)=v(y), then v(C δx δy)=1.
The upshot here comes as that an equation like Cxy=z gives us C δz δCxy. The suggested formulas from the above equations immediately following the table along with the axioms "C δ0 C δ1 δp" and "1", and "C Cpq C Cqp Epq" give us an axiom set here.
Let the notation 1 x/y * C 2-3 indicate that in formula 1 x gets substituted with y. This matches the formula which starts with C has 2 as its next part, and 3 as its last part. We then detach formula 3. The notation 4 x/y C 5-C 6-7 indicates that 4 matches the formula C5-C6-7. Since we already have formulas 5 and 6, we thus detach formula 7.
To see how the plan of writing the deduction proceeds, I'll write out the following calculation:
                         |-C C00 AN00=C 1 AN00=C 1 A10=C 1 1=1
            |-C C0q AN0q-|
            |            |-C C01 AN01=C 1 AN01=C 1 A11=C 1 1=1
 C Cpq ANpq-|
            |            |-C C10 AN10=C 0 AN10=C 0 A00=C 0 0=1
            |-C C1q AN1q-|
                         |-C C11 AN11=C 1 AN11=C 1 A01=C 1 1=1.
Now, to write out a deduction, we can basically move left to right here. From 1, we'll deduce C11. Then from C11 we'll deduce C 1 A10. Then C 1 AN00. Then C C00 AN00. Once we get C C01 AN01, then since we have C C00 AN00, we can get C C0q AN0q. But, I'll skip some steps here which gives us a simpler proof. Here goes:
1 1.
2 C δ1 δC00.
3 C δ1 δC01.
4 C δ0 δC10.
5 C δ1 δC11.
6 C δ0 δA00.
7 C δ1 δA01.
8 C δ1 δA10.
9 C δ1 δA11.
10 C δ1 δN0.
11 C δ0 δN1.
12 C Cpq C Cqp Epq.
13 C δ0 C δ1 δp. (this is not an axiom or theorem in intuitionistic logic).
2 δ/' * C1-14
14 C00.
3 δ/' * C1-15
15 C01.
13 δ/C0' * C14-C15-16
16 C0p.
5 δ/' * C1-17
17 C11.
13 δ/C'1 * C15-C17-18
18 Cp1.
18 p/C00 * 19
19 C C00 1.
8 δ/C C00 ' * C19-20
20 C C00 A10.
10 δ/C C00 A'0 * 20-21
21 C C00 AN00.
18 p/C01 * 22
22 C C01 1.
9 δ/CC01' * C22-23
23 C C01 A11.
10 δ/C C01 A'1 * C23-24
24 C C01 AN01.
13 δ/ C C0' AN0', p/q * C21-C24-25 
25 C C0q AN0q.
16 p/AN10 * 26
26 C 0 AN10.
4 δ/C ' AN10 * C26-27
27 C C10 AN10.
18 p/C11 * 28
28 C C11 1.
7 δ/C C11 ' * C28-29
29 C C11 A01.
11 δ/C C11 A'1 * C29-30
30 C C11 AN11.
13 δ/C C1' AN1', p/q *C27-C30-31
31 C C1q AN1q.
14 δ/C C'q AN'q * C25-C31-32
32 C Cpq ANpq.
18 p/AN00 * 33
33 C AN00 1.
2 δ/C AN00 ' * C33-34
34 C AN00 C00.
18 p/AN01 * 35
35 C AN01 1.
3 δ/C AN01 ' * C35-36
36 C AN01 C01.
13 δ /C AN0' C0', p/q * C34-C36-37
37 C AN0q C0q.
6 δ/C'0 * C14-38
38 C A00 0.
11 δ/C A'0 0 * C38-39
39 C AN10 0.
4 δ/C AN10 ' * C39-40
40 C AN10 C10.
18 p/AN11 * 41
41 C AN11 1.
5 δ/C AN11 ' * C41-42
42 C AN11 C11.
13 δ/C AN1' C1', p/q * C40-C42-43
43 C AN1q C1q.
37 δ/C AN'q C'q * C37-C43-44
44 C ANpq Cpq.
 12 p/Cpq, q/ANpq * C32-C44-45
45 E Cpq ANpq.

No comments:

Post a Comment