Goedel numbering is incoherent as a concept. The difficulty, apparently not noticed, or ignored, lies in that logical and mathematical theories involve the concept of a variable. A variable consists of something which can vary. If something consists of a single object, then it cannot vary, for it is but one object. Thus, it is not coherent to think of a variable as representing a single object. A constant consists of a single object. But, Goedel numbering involves assigning a constant to what previously got intended as a variable.
Thus, since a variable can vary, if we could logically assign a constant to a variable such that we have a one to one correspondence between the variable and the constant, that would imply that the variable can no longer vary, since constants cannot vary.
Goedel numbering does not respect the structure of variables. Consequently, it cannot analyze variables. To understand logic and mathematics, the concept of a variable must get understood. Goedel numbering is a woefully inadequate tool for understanding mathematics and logic.
Suppose we look at something like the associative law for addition (or any universal law in logic or mathematics):
+(a, +(b, c)) = +(+(a, b), c).
How is it possible that we can infer that 1. +(65613, +(4, 3)) = +(+(65613, 4), 3) from that law?
How can we also infer that 2. +(567, +(28, 17)) = +(+(567, 28), 17)?
I answer that such is possible, because that law has variables 'a', 'b', and 'c' which range over all of the constants that we recognize as natural numbers, and because we take certain sequences of symbols and certain symbols as intending to convey natural numbers.
But, what would happen if we Goedel number the associative law? Whatever we correspond to 'a', to 'b', and to 'c' get intended as representing constants. But, constants don't range over anything. If we could get both 1. and 2. from the above, then whatever constant would correspond to the variable 'a', would somehow have to correspond to '65613' and then to '567'. A constant though consists of a single object, so we would have a single object corresponding to two objects such that the single object has enough structure to produce two objects, *while still remaining one object*. But, this just doesn't have any coherence. It is never the case that is possible that one object can equal two objects in terms of it's basic properties, since it is simply not possible for the natural number one to equal the natural number two.
Monday, October 31, 2016
Tuesday, October 11, 2016
The following I've learned with the help of the late William McCune's program Prover9 https://www.cs.unm.edu/~mccune/mace4/ 2005-2010.
In the following the symbol '0', given a context, stands for a constant false propositions. The sense behind the idea of '0' thus may get captured by the following sentence:
"When you are awake, The Earth is exactly the same as The Sun."
Suppose we consider the following basis for classical propositional logic. The small letters for this system only get taken from the second half of the English abc's for small letters. We might also subscript them with numeral symbols so long as each symbols can get clearly distinguished from other symbols.
1. C x Cyx. Recursive Meaningful Expression Prefixing
2. C CxCyz C Cxy Cxz. C-Distribution
3. C CCxy0 x. Arbitrary Implication to Falsum to the Antecedent of the Implication.
Suppose also we have the following definitions:
def. 1: Nx is defined as Cx0.
def. 2: Axy is defined as CCxyy.
def. 3: Kxy is defined as CCxCy00.
def. 4: Exy is defined as CCCxyCCyx00.
The third axiom along with the above definitions allows us to deduce a few theorems in just a few steps.
Applying def. 1 to 3. we obtain 4
4 C NCxy x. Negation of an arbitrary conditional to the antecedent of that conditional.
Now putting 0 in the place of y in 4 we obtain 5 (we can abbreviate that as x/0 * 5 following the scheme x/y * z, which I will use hereafter):
5 C NCx0 x.
Applying def. 4 to CNx0 in 5 we obtain 6:
6 C NNx x. Double negation to the small letter of the meaningful expression.
3 y/Cy0 * 7
7 C CCxCy00 x.
Applying def. 3 to CCxCy00 in 7 we obtain 8:
8 C Kxy x. Arbitrary conjunction to it's left meaningful expression.
1 y/Cyx * 9
9 C x CCyx x.
Applying def. 2 to CCyxx in 9 we obtain 10:
10 C x Ayx. Arbitrary proposition to a disjunction with that proposition on the right of the disjunction.
3 x/Cxy, y/CCyx0 * 11
11 C CCCxyCCyx00 Cxy.
Applying def. 4 to CCCxyCCyx00 in 11 we obtain 12:
12 C Exy Cxy. Arbitrary equivalence to a similar conditional.
In the following the symbol '0', given a context, stands for a constant false propositions. The sense behind the idea of '0' thus may get captured by the following sentence:
"When you are awake, The Earth is exactly the same as The Sun."
Suppose we consider the following basis for classical propositional logic. The small letters for this system only get taken from the second half of the English abc's for small letters. We might also subscript them with numeral symbols so long as each symbols can get clearly distinguished from other symbols.
1. C x Cyx. Recursive Meaningful Expression Prefixing
2. C CxCyz C Cxy Cxz. C-Distribution
3. C CCxy0 x. Arbitrary Implication to Falsum to the Antecedent of the Implication.
Suppose also we have the following definitions:
def. 1: Nx is defined as Cx0.
def. 2: Axy is defined as CCxyy.
def. 3: Kxy is defined as CCxCy00.
def. 4: Exy is defined as CCCxyCCyx00.
The third axiom along with the above definitions allows us to deduce a few theorems in just a few steps.
Applying def. 1 to 3. we obtain 4
4 C NCxy x. Negation of an arbitrary conditional to the antecedent of that conditional.
Now putting 0 in the place of y in 4 we obtain 5 (we can abbreviate that as x/0 * 5 following the scheme x/y * z, which I will use hereafter):
5 C NCx0 x.
Applying def. 4 to CNx0 in 5 we obtain 6:
6 C NNx x. Double negation to the small letter of the meaningful expression.
3 y/Cy0 * 7
7 C CCxCy00 x.
Applying def. 3 to CCxCy00 in 7 we obtain 8:
8 C Kxy x. Arbitrary conjunction to it's left meaningful expression.
1 y/Cyx * 9
9 C x CCyx x.
Applying def. 2 to CCyxx in 9 we obtain 10:
10 C x Ayx. Arbitrary proposition to a disjunction with that proposition on the right of the disjunction.
3 x/Cxy, y/CCyx0 * 11
11 C CCCxyCCyx00 Cxy.
Applying def. 4 to CCCxyCCyx00 in 11 we obtain 12:
12 C Exy Cxy. Arbitrary equivalence to a similar conditional.
Wednesday, September 21, 2016
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.
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.
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.
Wednesday, August 31, 2016
The late Elliot Mendelson's system in his Introduction to Mathematical Logic had an set of axiom schema for classical propositional which corresponds to the following set of axiom schema:
M1: (B -> (C -> B))
M2: ((B -> (C -> D)) -> ((B -> C) -> (B -> D)))
M3: (((~C) -> (~B)) -> (((~C) -> B) -> C))
The above are not axioms, but rather axiom schema. The only rule of inference is modus ponens: L is a direct consequence of B and (B -> C)...
What direct consequence means I find a bit hard to state, but the general idea seems that any wff deduced must get produced must using M1, M2, or M3 or use a direct consequence of one of a previous theorem produced using M1, M2, or M3 when using modus ponens. An indirect consequence such as making substitutions in a produced theorem is disallowed. For doing logic and writing formal proofs this has strong disadvantages, but it has the advantage of relative simplicity for metalogical theory.
After describing a definition of a statement letter, which I don't believe has relevance here, the following definition of a wff gets described:
2. (a) All statement letters are wfs.
(b) If B and C are wfs, then so are (~B) and (B -> C).
Now for the following meta-theorem we will need to check the abstract form for all consequences in this system. Basically as follows:
Case 1: Suppose that M1 gets used in a formal proof as the major premiss (the one having form... at a more abstract level, b). Then, at a more abstract level it will have form D1: (c -> b). I hasten to note that b here carries over from how B got instantiated as a wf in the first place. But, in this case, what gets produced has the form of a conditional.
Case 2: Suppose that M2 gets used in a formal proof as the major premiss. Then at a more abstract level, we infer to D2: ((b -> c) -> (b -> d)) with b, c, and d all having forms instantiated from how B, C, and D, got instantiated as wfs. This also has the form of a conditional.
Case 3: Suppose that M3 gets used in a formal proof as the major premiss. Then at a more abstract level, we infer to D3: (((~c) -> b) -> c) with c and b having forms instantiated from how C and B got instantiated as a wfs. This also has the form of a conditional.
Case 4: Suppose that D1: (c -> b) gets used in a formal proof as the major premiss, with b carrying over from how B got used to formally deduce a wf of the form D1: (c -> b). Then, we deduce D4: b. Since b carries over from how B got used, b must qualify as following the original plan of for the above three schema. b will thus qualify as a theorem directly instantiable from M1, M2, or M3. Each of those is a conditional. The minor premiss c qualifies as a theorem. By soundness, proposition 1.12 of Mendelson's book it qualifies as a tautology. Suppose that it consists of a statement letter. Now all tautologies can get checked by two values for their variables, and thus two truth values suffice for this logic. All statement letters may represent either the value of truth arbitrarily or the value of false arbitrary. Thus, for any statement letter we may select it's truth value at will. So, let us suppose that this b has the form of a statement letter. We thus can choose that b is not a tautology, contradicting soundness. Thus, b does not have the form of a statement letter. Checking the definition of a wf again thus implies that b either has form (~x) or (x -> y).
Suppose we selected a finite-valued or infinite-valued logic to model such a formal system. Then, we have many more choices to show that b either has form (~x) or (x -> y) similar to the above contradicting soundness.
Case 5: Suppose that D2: ((b -> c) -> (b -> d)) gets used in a formal proof as the major premiss, with b, c, and d all carrying over from B, C, and D how got used in a formal proof falling under case 2 following the original plan for wfs, and D5: (b -> c) corresponding to a substitution instance of M1, M2, or M3 following the original plan for wfs, or (b -> c) is one of the consequences of what has got produced by a formal theorem previously formally proved in the proof sequence. Then a meaningful expression with the form D5: (b -> d) follows, with b and d following the original plan for wfs corresponding to B and D in the formal deduction which used M2 as the major premiss to deduce ((b -> c) -> (b -> d)). D5 has the form of a conditional.
Case 6: Suppose that D3: (((~c) -> b) -> c) gets used in a formal proof as a premiss, with c and b carrying over from how C and B when M3 got used when M3 got used to deduce (((~c) -> b) -> c) in case 3, or ((~c) -> b) has the form of one of the consequences directly produced by the definition of a formal proof or is a substitution instance of M1, M2, or M3 following the original plan for wfs. Thus, a meaningful expression with the form D6: c would get proved.
Now, c is a formally produced theorem following the definition of a formal proof carrying over from how M3 got used above. By soundness of the system, proposition 1.12 of Mendelson's book, it follows that this c is a tautology. Now, similar to the above, all tautologies can get checked by two values for their variables, and thus two truth values suffice for this logic. All statement letters may represent either the value of truth arbitrarily or the value of falsity arbitrarily. Thus, for any statement letter we may select it's truth value at will. So, let us suppose that this c has the form of a statement letter. We thus choose that c takes on the value F. But, then c is not a tautology, contradicting soundness. But, soundness holds. Therefore, c has the form (~x) or the form (x -> y).
Meta-Corollary Interlude 1: If M3 gets used to produce D3, and then D3 once detached gets used to produce D6, then the antecedent of M3 has a proper subformula s (it's shorter in length than the antecedent) which also qualifies as a substitution instance of a formally provable theorem in the above system. So does the antecedent of D3. The antecedent of M3 is also inorganic, and so is the antecedent of D3.
Meta-Proof: By the above s and c qualify as the same formula. Since c got substituted or instantiated as some wf from C corresponding to c also, then s has shorter length (number of symbols) than the antecedent having form ((~b) -> (~c)). c having length 1 is shorter than ((~b) -> (~c)). Thus, c is a proper subformula. I would call such a formal proof, an extraction of a formula. The soundness meta-theorem holds. Thus, c is also a tautology. Inorganic (a term due to Wajsberg who noticed this property about Nicod's single axiom or what it would formally get property recast as) means that a formula has a proper subformula which is also a tautology. So, the antecedent of M3 is also inorganic.
Case 7: Suppose that D5: (b -> d) gets used in a formal proof as a premiss, with b and d carrying over from B and D in how M2 got used according to the plan for wfs for the first detachment from an instance of M2. Then, by a similar argument to the above concerning soundness, D7: b qualifies as a formal theorem. I note that it could have gotten produced as in the proof sequence and thus not qualify as an instance of M1, M2, or M3. By a similar argument to the above argument concerning soundness also, d qualifies as a formal theorem also and does not qualify as a variable. Consequently:
Meta-Corollary Interlude 2: If the original plan for axiom schema involves M2 getting used such that an instance of D2 gets produced, and then used as a major premiss, and then an instance of D5 gets produced and then used as a major premiss, then the original antecedent F1: (B -> (C -> *D*)) has a proper subformula which is a formal theorem, and thus is inorganic.
Meta-Proof: *D* is a subformula of F1. F1 has *D* inside of it. Thus, *D* is a proper subformula. By hypothesis it qualifies as provable. By soundness, it follows that F1 is inorganic.
General Meta-Claim: For Any Schematic Axiomatic Propositional Calculus Such That a Formal Proof Can Get Carried Out to the Last Place in Polish Notation Meaningful Expressions (if the only axiom were CpCNpq, still an unlimited system, the condition fails), Then If the Formal Theory is Sound Also and Has At Least A Two-Valued Model, Then That Last Schematic Variable for Well-Formed Formulas Will Have an Equiform Variable Somewhere Else In the Plan for Formulas (this isn't new, and probably the content of much, if not all of the above isn't either):
Argument: The last place in all Polish notation meaningful expressions are propositional variables. The soundness meta-theorem holds. Thus, if a formal proof gets carried out to the last place, and that variable doesn't appear anywhere else in the meaningful expression for the axiom schemata, then no substitutions for that last variable were required to carry out the formal proof. Thus, a formal proof using that axiom schemata could get changed to have no other place in the proof where that last variable appears. That is, no substitutions came as required in the last variable to carry out the formal proof. The soundness meta-theorem holds for the above, so the variable can get substituted by any truth value. We select falsity. Since the deduction gets carried out to that last point, we have a contradiction. Therefore, that variable will appear in at least one other place in the original axiom schemata.
Corollary: The Same Applies for the Last Propositional Variable in Mendelson's System Or In Reverse Polish Notation
Argument: Rewriting definitions of so that we have something in Mendelson's system or in reverse polish or many others preserves the sequence of propositional variables in the formula. Consequently, if the above argument qualifies as adequate, so does the corollary.
Now check the definition of a wff in Mendelson's book. For any formal proof, case 1. got ruled out by the analysis of cases 1-7 above. Now, I will note that the above might accurately get strongly criticized in some respects. I might need to have several different logical alphabets for formulas for this meta-proof to work out. They all look somewhat like this (a -> b) or like this (~a). But, notice that they got notated D1, D2, ..., D7. None of those symbols represent cardinal numbers. They aren't integers. They represent what can get thought of as the first logical order, the second logical order, and so on. So under at least one interpretation, they can get thought of as representing different logical alphabets.
I note that I believe that all forms of possible cases has to get analyzed for this meta-proof to go through. This indicates how a single axiom schemata can work out as simpler for some metalogical purposes, because then we have less cases to check. E. G. if we picked CCCpqrCCrpCsp, C0p as our axiom set, we would only need to stipulate that 0 models falsity in the semantics of the logic. Thus, 0 showing up somehow probably indicates that we had some string which wasn't a meaningful expression in the first place. So, we go check that and almost surely learn there wasn't a well-formed formula somewhere. We would also only need to check forms like CCabc, Cca, and s, which makes for three cases instead of seven. Three logical orders is simpler than seven logical orders, isn't it? Sure, there exist other disadvantages, but oh well.
The above implies the following:
Meta-Theorem on Mendelson's Formal System: There Do Not Exist Any Formal Proofs Which Yield A Statement Letter.
Consequently, all strings deduced in that system fall under the forms (~a) and (b -> c). Each of these forms has has a left parenthesis '(' and a right parenthesis ')'.
Therefore:
Meta-Theorem: Every formal theorem in Mendelson's formal axiomatic system begins with a left parenthesis '(' and ends with a right parenthesis ')'.
Also, string 1. on p. 28 is not an instance of axiom schema (A2). String 2. doesn't have a left parenthesis. So, the inference to 3. isn't in the formal system M. And 4. and 5. don't have a left parenthesis either. So, no step of his so-called, self-proclaimed "proof" in Lemma 1.8 belongs to L. And the rest of his talk about propositional calculi is plagued by the same sort of syntactical problem. When doing reasoning in formal systems, they have deep relevance. Strangely, Mendelson seems better with writing meaningful expressions when talking about matters of semantics.
Did any of Mendelson's students even challenge him and point out that his book didn't stick to his own definitions? If they did, did Mendelson just brush them off?
And how in the world could Kleene not have a definition of a well-formed formula or statement form or meaningful expression or some other term in his Mathematical Logic for beginners who may need clarity about syntax most *after* having written his Introduction to MetaMathematics where he at least has such a definition and even called his postulates "dramatis personae" which might suggest that he wasn't sticking to his definitions? But that is another matter.
M1: (B -> (C -> B))
M2: ((B -> (C -> D)) -> ((B -> C) -> (B -> D)))
M3: (((~C) -> (~B)) -> (((~C) -> B) -> C))
The above are not axioms, but rather axiom schema. The only rule of inference is modus ponens: L is a direct consequence of B and (B -> C)...
What direct consequence means I find a bit hard to state, but the general idea seems that any wff deduced must get produced must using M1, M2, or M3 or use a direct consequence of one of a previous theorem produced using M1, M2, or M3 when using modus ponens. An indirect consequence such as making substitutions in a produced theorem is disallowed. For doing logic and writing formal proofs this has strong disadvantages, but it has the advantage of relative simplicity for metalogical theory.
After describing a definition of a statement letter, which I don't believe has relevance here, the following definition of a wff gets described:
2. (a) All statement letters are wfs.
(b) If B and C are wfs, then so are (~B) and (B -> C).
Now for the following meta-theorem we will need to check the abstract form for all consequences in this system. Basically as follows:
Case 1: Suppose that M1 gets used in a formal proof as the major premiss (the one having form... at a more abstract level, b). Then, at a more abstract level it will have form D1: (c -> b). I hasten to note that b here carries over from how B got instantiated as a wf in the first place. But, in this case, what gets produced has the form of a conditional.
Case 2: Suppose that M2 gets used in a formal proof as the major premiss. Then at a more abstract level, we infer to D2: ((b -> c) -> (b -> d)) with b, c, and d all having forms instantiated from how B, C, and D, got instantiated as wfs. This also has the form of a conditional.
Case 3: Suppose that M3 gets used in a formal proof as the major premiss. Then at a more abstract level, we infer to D3: (((~c) -> b) -> c) with c and b having forms instantiated from how C and B got instantiated as a wfs. This also has the form of a conditional.
Case 4: Suppose that D1: (c -> b) gets used in a formal proof as the major premiss, with b carrying over from how B got used to formally deduce a wf of the form D1: (c -> b). Then, we deduce D4: b. Since b carries over from how B got used, b must qualify as following the original plan of for the above three schema. b will thus qualify as a theorem directly instantiable from M1, M2, or M3. Each of those is a conditional. The minor premiss c qualifies as a theorem. By soundness, proposition 1.12 of Mendelson's book it qualifies as a tautology. Suppose that it consists of a statement letter. Now all tautologies can get checked by two values for their variables, and thus two truth values suffice for this logic. All statement letters may represent either the value of truth arbitrarily or the value of false arbitrary. Thus, for any statement letter we may select it's truth value at will. So, let us suppose that this b has the form of a statement letter. We thus can choose that b is not a tautology, contradicting soundness. Thus, b does not have the form of a statement letter. Checking the definition of a wf again thus implies that b either has form (~x) or (x -> y).
Suppose we selected a finite-valued or infinite-valued logic to model such a formal system. Then, we have many more choices to show that b either has form (~x) or (x -> y) similar to the above contradicting soundness.
Case 5: Suppose that D2: ((b -> c) -> (b -> d)) gets used in a formal proof as the major premiss, with b, c, and d all carrying over from B, C, and D how got used in a formal proof falling under case 2 following the original plan for wfs, and D5: (b -> c) corresponding to a substitution instance of M1, M2, or M3 following the original plan for wfs, or (b -> c) is one of the consequences of what has got produced by a formal theorem previously formally proved in the proof sequence. Then a meaningful expression with the form D5: (b -> d) follows, with b and d following the original plan for wfs corresponding to B and D in the formal deduction which used M2 as the major premiss to deduce ((b -> c) -> (b -> d)). D5 has the form of a conditional.
Case 6: Suppose that D3: (((~c) -> b) -> c) gets used in a formal proof as a premiss, with c and b carrying over from how C and B when M3 got used when M3 got used to deduce (((~c) -> b) -> c) in case 3, or ((~c) -> b) has the form of one of the consequences directly produced by the definition of a formal proof or is a substitution instance of M1, M2, or M3 following the original plan for wfs. Thus, a meaningful expression with the form D6: c would get proved.
Now, c is a formally produced theorem following the definition of a formal proof carrying over from how M3 got used above. By soundness of the system, proposition 1.12 of Mendelson's book, it follows that this c is a tautology. Now, similar to the above, all tautologies can get checked by two values for their variables, and thus two truth values suffice for this logic. All statement letters may represent either the value of truth arbitrarily or the value of falsity arbitrarily. Thus, for any statement letter we may select it's truth value at will. So, let us suppose that this c has the form of a statement letter. We thus choose that c takes on the value F. But, then c is not a tautology, contradicting soundness. But, soundness holds. Therefore, c has the form (~x) or the form (x -> y).
Meta-Corollary Interlude 1: If M3 gets used to produce D3, and then D3 once detached gets used to produce D6, then the antecedent of M3 has a proper subformula s (it's shorter in length than the antecedent) which also qualifies as a substitution instance of a formally provable theorem in the above system. So does the antecedent of D3. The antecedent of M3 is also inorganic, and so is the antecedent of D3.
Meta-Proof: By the above s and c qualify as the same formula. Since c got substituted or instantiated as some wf from C corresponding to c also, then s has shorter length (number of symbols) than the antecedent having form ((~b) -> (~c)). c having length 1 is shorter than ((~b) -> (~c)). Thus, c is a proper subformula. I would call such a formal proof, an extraction of a formula. The soundness meta-theorem holds. Thus, c is also a tautology. Inorganic (a term due to Wajsberg who noticed this property about Nicod's single axiom or what it would formally get property recast as) means that a formula has a proper subformula which is also a tautology. So, the antecedent of M3 is also inorganic.
Case 7: Suppose that D5: (b -> d) gets used in a formal proof as a premiss, with b and d carrying over from B and D in how M2 got used according to the plan for wfs for the first detachment from an instance of M2. Then, by a similar argument to the above concerning soundness, D7: b qualifies as a formal theorem. I note that it could have gotten produced as in the proof sequence and thus not qualify as an instance of M1, M2, or M3. By a similar argument to the above argument concerning soundness also, d qualifies as a formal theorem also and does not qualify as a variable. Consequently:
Meta-Corollary Interlude 2: If the original plan for axiom schema involves M2 getting used such that an instance of D2 gets produced, and then used as a major premiss, and then an instance of D5 gets produced and then used as a major premiss, then the original antecedent F1: (B -> (C -> *D*)) has a proper subformula which is a formal theorem, and thus is inorganic.
Meta-Proof: *D* is a subformula of F1. F1 has *D* inside of it. Thus, *D* is a proper subformula. By hypothesis it qualifies as provable. By soundness, it follows that F1 is inorganic.
General Meta-Claim: For Any Schematic Axiomatic Propositional Calculus Such That a Formal Proof Can Get Carried Out to the Last Place in Polish Notation Meaningful Expressions (if the only axiom were CpCNpq, still an unlimited system, the condition fails), Then If the Formal Theory is Sound Also and Has At Least A Two-Valued Model, Then That Last Schematic Variable for Well-Formed Formulas Will Have an Equiform Variable Somewhere Else In the Plan for Formulas (this isn't new, and probably the content of much, if not all of the above isn't either):
Argument: The last place in all Polish notation meaningful expressions are propositional variables. The soundness meta-theorem holds. Thus, if a formal proof gets carried out to the last place, and that variable doesn't appear anywhere else in the meaningful expression for the axiom schemata, then no substitutions for that last variable were required to carry out the formal proof. Thus, a formal proof using that axiom schemata could get changed to have no other place in the proof where that last variable appears. That is, no substitutions came as required in the last variable to carry out the formal proof. The soundness meta-theorem holds for the above, so the variable can get substituted by any truth value. We select falsity. Since the deduction gets carried out to that last point, we have a contradiction. Therefore, that variable will appear in at least one other place in the original axiom schemata.
Corollary: The Same Applies for the Last Propositional Variable in Mendelson's System Or In Reverse Polish Notation
Argument: Rewriting definitions of so that we have something in Mendelson's system or in reverse polish or many others preserves the sequence of propositional variables in the formula. Consequently, if the above argument qualifies as adequate, so does the corollary.
Now check the definition of a wff in Mendelson's book. For any formal proof, case 1. got ruled out by the analysis of cases 1-7 above. Now, I will note that the above might accurately get strongly criticized in some respects. I might need to have several different logical alphabets for formulas for this meta-proof to work out. They all look somewhat like this (a -> b) or like this (~a). But, notice that they got notated D1, D2, ..., D7. None of those symbols represent cardinal numbers. They aren't integers. They represent what can get thought of as the first logical order, the second logical order, and so on. So under at least one interpretation, they can get thought of as representing different logical alphabets.
I note that I believe that all forms of possible cases has to get analyzed for this meta-proof to go through. This indicates how a single axiom schemata can work out as simpler for some metalogical purposes, because then we have less cases to check. E. G. if we picked CCCpqrCCrpCsp, C0p as our axiom set, we would only need to stipulate that 0 models falsity in the semantics of the logic. Thus, 0 showing up somehow probably indicates that we had some string which wasn't a meaningful expression in the first place. So, we go check that and almost surely learn there wasn't a well-formed formula somewhere. We would also only need to check forms like CCabc, Cca, and s, which makes for three cases instead of seven. Three logical orders is simpler than seven logical orders, isn't it? Sure, there exist other disadvantages, but oh well.
The above implies the following:
Meta-Theorem on Mendelson's Formal System: There Do Not Exist Any Formal Proofs Which Yield A Statement Letter.
Consequently, all strings deduced in that system fall under the forms (~a) and (b -> c). Each of these forms has has a left parenthesis '(' and a right parenthesis ')'.
Therefore:
Meta-Theorem: Every formal theorem in Mendelson's formal axiomatic system begins with a left parenthesis '(' and ends with a right parenthesis ')'.
Also, string 1. on p. 28 is not an instance of axiom schema (A2). String 2. doesn't have a left parenthesis. So, the inference to 3. isn't in the formal system M. And 4. and 5. don't have a left parenthesis either. So, no step of his so-called, self-proclaimed "proof" in Lemma 1.8 belongs to L. And the rest of his talk about propositional calculi is plagued by the same sort of syntactical problem. When doing reasoning in formal systems, they have deep relevance. Strangely, Mendelson seems better with writing meaningful expressions when talking about matters of semantics.
Did any of Mendelson's students even challenge him and point out that his book didn't stick to his own definitions? If they did, did Mendelson just brush them off?
And how in the world could Kleene not have a definition of a well-formed formula or statement form or meaningful expression or some other term in his Mathematical Logic for beginners who may need clarity about syntax most *after* having written his Introduction to MetaMathematics where he at least has such a definition and even called his postulates "dramatis personae" which might suggest that he wasn't sticking to his definitions? But that is another matter.
Sunday, August 28, 2016
For every condensed detachment proof, there exists a substitution and detachment proof.
If both the antecedent of the major premise, e. g. one having form Cα
β or (p → q) or (p) → (q) or pqC or C(p, q), or (p, q)i, etc., and the minor premise γ
qualify as equiform, then a condensed detachment proof corresponds to a
single step substitution and detachment proof. We just make a
detachment.
If the antecedent of the major premiseα
and the minor premiseγ
both require substitutions to transform them into equiform forms, then
we need to make two substitutions, and one detachment to expand the
condensed detachment proof into a substitution and detachment proof.
Examples of such a case would consist of taking CCzCNxNyCzCyx as the
major premise and CCNyyCNyx as the minor, which after condensed
detachment yields CCNyyCxy or any formula having the same relative
positions of the variables in the formula after condensed detachment,
such as CCNxxCyx or CCNaaCba, or if the major and minor premise looked
differently and appropriately so ((¬ f→ f) → (u → f)) etc. Or taking two copies of CCCCqrCprsCCpqs and then reproducing the condensed detachment of those two copies.
Often enough though, we only need to make one substitution in exclusively the major or the minor premise to expand the condensed detachment proof into a substitution and detachment proof. Thus, we require only two steps for an expansion of the condensed detachment proof into the corresponding substitution and detachment proof; a simultaneous substitution and a detachment.
Meta-Theorem 1: If exclusively the antecedent of the major premise or the minor premise have exactly one instance of any propositional variable throughout the antecedent or the major premise respectively, then for any condensed detachment proof, there exists a two line substitution and detachment proof.
Meta-Proof: A most general unifier can get found simply by substituting each variable in the antecedent of the major premise or in the minor premise whichever satisfies the hypothesis. Consequently, the substitution and detachment proof will only need one simultaneous substitution to make a detachment. Since the detachment qualifies as a step also, that makes for a two line proof as was to get metalogically demonstrated.
Meta-Corollary 1: Systems with formulas of any of the following: CpCqp, CCCpqrCqr, CCCpqqCCqpp, CCCpqrCCprr, CCCpqrCCrpp, CCpqCCqrCpr, CCpqCCrpCrq, CCpCqrCqCpr, CpCCpqq, CCpqCCCprqq, CpCCNqNpq and possibly many more do not have a last theorem under condensed detachment.
Discussion: This size of the question space is a bit small to contain much of a meta-proof. But, to see how this works fix the formula selected under condensed detachment and call it a. For formulas which have a in the antecedent, the meta-corollary follows directly from Meta-Theorem 1. For some others, the antecedent of a has bracket type Cα β , while any detached formula from a also has bracket type Cα β . For another set, the bracket type of the formula gets preserved under condensed detachment.
Given a condensed detachment proof, let us call the number of steps (lines in a proof) in any of the shortest corresponding substitution and detachment proofs, the condensed detachment expansion number, CoDEN, of a condensed detachment proof of a formula P, CoDEN(⊢ P), or just CoDEN for short.
Now, suppose we had a large number of condensed detachment proofs in classical propositional calculi... I don't know maybe a million or a billion or maybe just a hundred, or even just a few proof. What is the value of CoDEN over all of those proofs? If we took the limit of all formal proofs as n gets larger and larger, would CoDEN converge to a rational number or transcendental number? What would make for a suitable upper estimate and a lower estimate for CoDEN if using it to predicate the length of a minimal substitution and detachment proof from a condensed detachment proof? I'll guess between 2.0 and 2.5. Does it matter which set of formal proofs we select? Does selecting theories which have their formal theorems contained in classical propositional logic substantially alter the value of CoDEN? Using a program that I wrote, and perhaps I'll analyze some other proofs, the value of CoDEN for the proof here is 2.25.
Related paper
If both the antecedent of the major premise, e. g. one having form C
If the antecedent of the major premise
and the minor premise
Often enough though, we only need to make one substitution in exclusively the major or the minor premise to expand the condensed detachment proof into a substitution and detachment proof. Thus, we require only two steps for an expansion of the condensed detachment proof into the corresponding substitution and detachment proof; a simultaneous substitution and a detachment.
Meta-Theorem 1: If exclusively the antecedent of the major premise or the minor premise have exactly one instance of any propositional variable throughout the antecedent or the major premise respectively, then for any condensed detachment proof, there exists a two line substitution and detachment proof.
Meta-Proof: A most general unifier can get found simply by substituting each variable in the antecedent of the major premise or in the minor premise whichever satisfies the hypothesis. Consequently, the substitution and detachment proof will only need one simultaneous substitution to make a detachment. Since the detachment qualifies as a step also, that makes for a two line proof as was to get metalogically demonstrated.
Meta-Corollary 1: Systems with formulas of any of the following: CpCqp, CCCpqrCqr, CCCpqqCCqpp, CCCpqrCCprr, CCCpqrCCrpp, CCpqCCqrCpr, CCpqCCrpCrq, CCpCqrCqCpr, CpCCpqq, CCpqCCCprqq, CpCCNqNpq and possibly many more do not have a last theorem under condensed detachment.
Discussion: This size of the question space is a bit small to contain much of a meta-proof. But, to see how this works fix the formula selected under condensed detachment and call it a. For formulas which have a in the antecedent, the meta-corollary follows directly from Meta-Theorem 1. For some others, the antecedent of a has bracket type C
Given a condensed detachment proof, let us call the number of steps (lines in a proof) in any of the shortest corresponding substitution and detachment proofs, the condensed detachment expansion number, CoDEN, of a condensed detachment proof of a formula P, CoDEN(
Now, suppose we had a large number of condensed detachment proofs in classical propositional calculi... I don't know maybe a million or a billion or maybe just a hundred, or even just a few proof. What is the value of CoDEN over all of those proofs? If we took the limit of all formal proofs as n gets larger and larger, would CoDEN converge to a rational number or transcendental number? What would make for a suitable upper estimate and a lower estimate for CoDEN if using it to predicate the length of a minimal substitution and detachment proof from a condensed detachment proof? I'll guess between 2.0 and 2.5. Does it matter which set of formal proofs we select? Does selecting theories which have their formal theorems contained in classical propositional logic substantially alter the value of CoDEN? Using a program that I wrote, and perhaps I'll analyze some other proofs, the value of CoDEN for the proof here is 2.25.
Related paper
Subscribe to:
Posts (Atom)