One of the axiom sets for two-valued propositional calculus got discovered by Wajsberg, which with some letter substitution would become as follows:
A1: CxCyx
A2: CCxCyzCCxyCxz
A3W: CCCx00x
It turns out that A3W consists of a special case in that a more general tautology A3 can get formulated in the sense that we can obtain A3W by uniform substitution from A3, but we cannot obtain A3 by uniform substitution from A3W. A3 is as follows:
A3: CCCxy0x
The notation of a letter or constant on the left side of a '/' with a letter or constant on the blank indicates that we will substitute whatever lies on the left with whatever lies on the right.
To check the soundness of A3 we can set up the following equations:
C00 = 1, C10 = 0, C01 = 1, C11 = 1.
A3 x/0 y/0 yields CCC0000. So, CCC0000 = CC100 = C00 = 1.
A3 x/0 y/1 yields CCC0100. So, CCC0100 = CC100 = C00 = 1.
A3 x/1 y/0 yields CCC1001. So, CCC1001 = CC001 = C11 = 1.
A4 x/1 y/1 yields CCC1101. So, CCC1101 = CC101 = C01 = 1.
Consequently, CCCxy0x is a tautology.
Now we substitute y with 0 in A3 obtaining CCCx00x.
Therefore, since the above axiom set of Wajsberg consists of an axiom set for C-0 propositional calculus, it follows that {CxCyx, CCxCyzCCxyCxz, CCCxy0x} makes for an axiom set for C-0 propositional calculus under the rules of uniform substitution and detachment.
The author wants to note that N1: {CxCyx, CCxCyzCCxyCxz, CNCxyx} is not a basis for C-N propositional calculus. To see this we only need to check that if we define N as follows N0 = 0, and N1 = 0, then CNCxyx = 1. But, the law of Clavius CCNxxx, with x/0 becomes CCN000, and
CCN000 = CC000= C10 = 0. Thus, the law of Clavius is not derivable in system N1 under uniform substitution and detachment.
There is no law of Clavius in the definition-free C-0 calculus. But, if we have the definition Cx0 = Nx, then the sense of the law of Clavius gets captured by CCCx0xx.
Wednesday, September 21, 2016
Friday, September 16, 2016
Consider the following sequence of forms.
Cab, CaCbc, ... CaCb...Cxy.
Suppose that we have some well-formed formula **W** which unifies with one of the above forms, which we'll call **X**.
Meta-Thereom: If the last letter of **X** corresponds to a tautology in **W**, then **W** is a tautology.
Meta-Proof: First, we'll consider the case when **X** is Cab. By hypothesis, b is a tautology. Thus, Cab=Ca1. Ca1=1, so Cab is a tautology.
Consider the case where **W** unifies with CaCbc. By hypothesis c is a tautology. So, CaCbc=CaCb1. Now since Cb1=1 also, CaCb1=Ca1. Ca1 unifies with Cab. By the previous case Cab is thus a tautology. So, CaCbc is a tautology. Consequently, **W** is a tautology.
Suppose that the result holds where **W** unifies with CaCb...Cxy. We consider the successor form of CaCb...CxCyz, which is now **X**. By hypothesis z is a tautology, so CaCb...CxCyz= Ca...CxCy1. Ca...CxCy1=Ca...Cx1, since Cy1=1. Ca...Cx1 unifies with CaCb...Cxy. CaCb...Cxy is a tautology by hypothesis, so, Ca...CxCy1 is a tautology. Consequently, under the supposition, CaCb...CxCyz is a tautology.
Therefore, the meta-theorem holds.
Some examples:
CaCbCcCdCeCfCgChCiCjCpCqp is a tautology,
CaCbCcCdCeCfCgChCiCjCpp is a tautology
Further application: Let 1 qualify as a tautology. If we try to evaluate a well-formed formula to see if it is a tautology not, we check the last place of the formula. If we replace that letter with 1, and if it has a form in the above sequence of forms, it will qualify as a tautology. Thus, if it is not a tautology, we replace the last letter with 0. If that expression can or does evaluate to 0, then the original well-formed formula is not a tautology. Otherwise, it does qualify as a tautology.
Cab, CaCbc, ... CaCb...Cxy.
Suppose that we have some well-formed formula **W** which unifies with one of the above forms, which we'll call **X**.
Meta-Thereom: If the last letter of **X** corresponds to a tautology in **W**, then **W** is a tautology.
Meta-Proof: First, we'll consider the case when **X** is Cab. By hypothesis, b is a tautology. Thus, Cab=Ca1. Ca1=1, so Cab is a tautology.
Consider the case where **W** unifies with CaCbc. By hypothesis c is a tautology. So, CaCbc=CaCb1. Now since Cb1=1 also, CaCb1=Ca1. Ca1 unifies with Cab. By the previous case Cab is thus a tautology. So, CaCbc is a tautology. Consequently, **W** is a tautology.
Suppose that the result holds where **W** unifies with CaCb...Cxy. We consider the successor form of CaCb...CxCyz, which is now **X**. By hypothesis z is a tautology, so CaCb...CxCyz= Ca...CxCy1. Ca...CxCy1=Ca...Cx1, since Cy1=1. Ca...Cx1 unifies with CaCb...Cxy. CaCb...Cxy is a tautology by hypothesis, so, Ca...CxCy1 is a tautology. Consequently, under the supposition, CaCb...CxCyz is a tautology.
Therefore, the meta-theorem holds.
Some examples:
CaCbCcCdCeCfCgChCiCjCpCqp is a tautology,
CaCbCcCdCeCfCgChCiCjCpp is a tautology
Further application: Let 1 qualify as a tautology. If we try to evaluate a well-formed formula to see if it is a tautology not, we check the last place of the formula. If we replace that letter with 1, and if it has a form in the above sequence of forms, it will qualify as a tautology. Thus, if it is not a tautology, we replace the last letter with 0. If that expression can or does evaluate to 0, then the original well-formed formula is not a tautology. Otherwise, it does qualify as a tautology.
Friday, September 2, 2016
Some Meta-Theory of Well Constructed Polish Meaningful Expressions:
For the following we'll use this definition.
1. All un-bolded small letters are meaningful expressions.
2. If x is a meaningful expression, then so is Nx.
3. If x is a meaningful expression, if y is a meaningful expression, then Cxy is meaningful expression.
From hereon, I'll abbreviate meaningful expression by MEXP. The length of a MEXP we define as the number of symbols it has.
Meta-Theorem 1: Every MEXP which has a C in it, has one more small letter than C in it.
Meta-Proof: Consider an arbitrary MEXP of type Cab.
Case 1: Cab has two small letters in it, or one small letter in two distinct positions. In either case it has one C and two small letters in it.
Case 2: Suppose that for any MEXP of length n it has type Ccd and it has one more small letter than C in it. Now consider any MEXP of length (n +1). It will either have type NCcd, CNcd, or type CcNd. In any of those cases, it will have same number of small letters as type Ccd since we only adjoined an N to the sequence of letters. Finally, consider any MEXP of length (n + 2). It will have one of the following types: NNCcd, NCNcd, NCcNd, CNNcd, CNcNd, CcNNd, CxCcd, or CCxcd. The cases which have N in them follow by our hypothesis of the MEXP having one more small letter than C in it. Now consider the last two cases. Since the length of the MEXP is (n + 2), and has one more C in it than Ccd, x will consist of a small letter only. And in every twenty-six of those subcases, CxCcd and CCxcd has one more small letter than C in it. This completes the argument that every MEXP has one more small letter than C in it.
Meta-Claim 2: The following algorithm is sufficient to determine whether or not a sequence of letters is a MEXP.
Description: We first assign 1 to any small letter. We also assign -1 to any C. We assign 0 to all instances of N.
Step 1: We look at the last letter of the MEXP and check if it's a small letter. If it is, then we continue. Otherwise, we halt. The sequence of letters is not a MEXP.
Step 2: We have a counter given a value of 1. We now proceed from the right hand side to the left adding numbers according to whether it consists of a C or N. If it at any point the counter equals 0, then we halt, and the sequence of letters it is not a MEXP. If we get to the last letter and the value is greater than 1, then it is not a MEXP. Otherwise, it is a MEXP.
Meta-Claim 3: The following algorithm is also sufficient to determine whether or not a sequence of letters is a MEXP.
Description: We assign -1 to any small letter. We also assign 1 to any C. We assign 0 to all instances of N.
Step 1: We first assign a value of 1 to a counter.
Step 2: Now we proceed from left to right changing the value of our counted by the above assignments. If our counter equals 0 at any point which is not the last letter of the sequence of letters, then halt it is not a MEXP. If the counter does not equal 0 at the last letter then it is not a MEXP. If the counter does equal 0 at the last letter then it is a MEXP.
Meta-Claim 4: If we use the second algorithm, that described in meta-claim 3, and it has type Ckj, then the k MEXP can get found as follows.
Step 1: We start with the letter in the sequence. If it is a MEXP, then stop, that is the MEXP we wanted.
Step 2: If it is not, then store that letter, and let's call it so_far.
Step 3: Adjoin the next letter in the sequence of letters to the end of so_far.
Step 4: Check to see if so_far is now a MEXP. If it is, then so_far is k. If, not, then goto step 3.
Meta-Theorem 2: Every MEXP ends with a small letter.
Argument: If it does not end with a small letter, then it did not get constructed by the three clauses above.
For the following we'll use this definition.
1. All un-bolded small letters are meaningful expressions.
2. If x is a meaningful expression, then so is Nx.
3. If x is a meaningful expression, if y is a meaningful expression, then Cxy is meaningful expression.
From hereon, I'll abbreviate meaningful expression by MEXP. The length of a MEXP we define as the number of symbols it has.
Meta-Theorem 1: Every MEXP which has a C in it, has one more small letter than C in it.
Meta-Proof: Consider an arbitrary MEXP of type Cab.
Case 1: Cab has two small letters in it, or one small letter in two distinct positions. In either case it has one C and two small letters in it.
Case 2: Suppose that for any MEXP of length n it has type Ccd and it has one more small letter than C in it. Now consider any MEXP of length (n +1). It will either have type NCcd, CNcd, or type CcNd. In any of those cases, it will have same number of small letters as type Ccd since we only adjoined an N to the sequence of letters. Finally, consider any MEXP of length (n + 2). It will have one of the following types: NNCcd, NCNcd, NCcNd, CNNcd, CNcNd, CcNNd, CxCcd, or CCxcd. The cases which have N in them follow by our hypothesis of the MEXP having one more small letter than C in it. Now consider the last two cases. Since the length of the MEXP is (n + 2), and has one more C in it than Ccd, x will consist of a small letter only. And in every twenty-six of those subcases, CxCcd and CCxcd has one more small letter than C in it. This completes the argument that every MEXP has one more small letter than C in it.
Meta-Claim 2: The following algorithm is sufficient to determine whether or not a sequence of letters is a MEXP.
Description: We first assign 1 to any small letter. We also assign -1 to any C. We assign 0 to all instances of N.
Step 1: We look at the last letter of the MEXP and check if it's a small letter. If it is, then we continue. Otherwise, we halt. The sequence of letters is not a MEXP.
Step 2: We have a counter given a value of 1. We now proceed from the right hand side to the left adding numbers according to whether it consists of a C or N. If it at any point the counter equals 0, then we halt, and the sequence of letters it is not a MEXP. If we get to the last letter and the value is greater than 1, then it is not a MEXP. Otherwise, it is a MEXP.
Meta-Claim 3: The following algorithm is also sufficient to determine whether or not a sequence of letters is a MEXP.
Description: We assign -1 to any small letter. We also assign 1 to any C. We assign 0 to all instances of N.
Step 1: We first assign a value of 1 to a counter.
Step 2: Now we proceed from left to right changing the value of our counted by the above assignments. If our counter equals 0 at any point which is not the last letter of the sequence of letters, then halt it is not a MEXP. If the counter does not equal 0 at the last letter then it is not a MEXP. If the counter does equal 0 at the last letter then it is a MEXP.
Meta-Claim 4: If we use the second algorithm, that described in meta-claim 3, and it has type Ckj, then the k MEXP can get found as follows.
Step 1: We start with the letter in the sequence. If it is a MEXP, then stop, that is the MEXP we wanted.
Step 2: If it is not, then store that letter, and let's call it so_far.
Step 3: Adjoin the next letter in the sequence of letters to the end of so_far.
Step 4: Check to see if so_far is now a MEXP. If it is, then so_far is k. If, not, then goto step 3.
Meta-Theorem 2: Every MEXP ends with a small letter.
Argument: If it does not end with a small letter, then it did not get constructed by the three clauses above.
Subscribe to:
Posts (Atom)