details re Z-R |- PA consistent
in [Logic]
|
Prev: geometry template for infinite-line-ray to precision define infinite-number in Peano Axioms #627 Correcting Math
Next: The Necessary vs Contingent Distinction
From: MoeBlee on 3 Jul 2010 17:05 In recent threads it has been questioned whether ZFC proves the consistency of first order PA (called 'PA' in this post). This post provides a proof in Z-R (Z set theory without the axiom of regularity) of the consistency of PA, thus perforce ZFC proves the consistency of first order PA.. In order to be clear for certain posters less familiar with set theory and mathematical logic, we mention certain details that readers better informed may not require. Our proof is informal such that one who is adequately informed in basic predicate logic and basic set theory can see that it is formalizable Z-R. We make use of ordinary theorems of Z-R, such as those in Enderton's set theory book and those in his mathematical logic book, as such results in mathematical logic are formalizable in Z-R. As to what axioms are used in all the theorems deployed for this proof and in the argument itself here, we use identity theory as it is subsumed by Z-R and all the single axioms of Z-R and certain instances of the axiom schema of separation. Whether the proof can be done with a proper subset of these axioms, I don't opine. In any case, extensionality, schema of separation, union, and pairing are used even in the earliest theorems from the axioms, as proof such as this depends on certain of those theorems. The axiom of infinity is salient in deriving the existence of a least successor-inductive set that is the universe of the standard model for the language of PA. Notation: and terminology: In the language of set theory (which is the language of Z-R) extended by definitions: w (read 'omega') stands for the set of natural numbers O stands for the empty set u stands for the binary union operation # stands for the successor operation, e.g., n# = nu{n} + stands for the addition operation for natural numbers * stands for the multiplication operation for natural numbers |=_m P [[v]] stands (e.g.) for 'P is satisfied by m under v' I.e., the formula P is satisfied by the model m with the function v, where v is a function from the set of variables of the language (whatever given language) into the universe (see below) for the model m. We use the variables m P (read 'phi') v s c z p t T n k V in the language of set theory. In the language of PA, we have the primitives: 0 S + * We use the variables x y in the language of PA. Note: We use the typographical symbols '+' and '*' in both the language of set theory and in the language of PA. This is due to a limitation of ASCII not providing different fonts. These should be regarded as if written in different font in order. It should be clear from context which is intended in each occurrence. Also, we are not fastidious with use-mention and "corner brackets" unless it required to avoid ambiguity that can't be settled by the reader's exercise of common sense in reading mathematics in informal ASCII. We adopt Enderton's definition of a structure (model) for a language. A model for a language is a function from the set whose members are exactly the universal quantifier and the function and predicate symbols of the language, such that the universal quantifier is mapped to a non-empty set (the universe for the model), and each n-place function symbol is mapped to an n-place function on said non-empty set, and each n-place predicate symbol is mapped to an n-place relation on said non-empty set. So a model for the language of PA is a function: {<A s> <0 c> <S z> <+ p> <* t>} where 'A' is the universal quantifier for the language of P, s is a nonempty set, c is a member of s, z is a 1-place function for s, p is a 2-place function for s, and t is a 2-place function for s. For simpler notation, we may write the above model in tuple style: <s c z p t>. For a definition of 'true in a model' we refer to Enderton's logic book, since it would be too laborious to go through the steps toward such a definition in a posting such as this. We trust that the reader understands the definition of truth in a model (such as provided by Enderton) and that the reader will recognize how the proofs below work with this definition. (Those not familiar with this kind of thing will have to study a book such as Enderton's.) In Z-R we define the standard model for the language of PA as 'N', as follows: N = <w O # + *> We say a model m is a model OF a set of sentences T iff every member of T is true in m. If there is an m that is a model of a set of sentences T, then we say "T has a model". A theory is a set of sentences closed under entailment. IN Z-R we define 'PA' as the set of sentences (in the language described by the aforementioned primitives) that is the entailment- closure of these axioms (the universal closures of these): ~ 0 = Sx Sx = Sy -> x=y x+0 = x x+Sy = S(x+y) x*0 = 0 x*Sy = (x*y)+x and If P is a formula in the language, then all closures of the following are axioms: (P[0|x] & Ax(P -> P[Sx|x])) -> AxP If PA has a model m, then PA is consistent. Proof: If PA is inconsistent then there is a sentence P in the language of PA such that both P and ~P are in PA. But since m is a model of PA, both P and ~P are true in m. But that is impossible, since a sentence is true in a model iff the negation of the sentence is false in the model and no sentence is both true and false in a given model (which follows from how 'true in a model' is defined through definition by recursion). So we need only show that PA has a model. We show that M is a model of PA. Thus we need only show that M is a model of each of the axioms of PA (since entailment, by definition, preserves truth in a model): (1) ~ 0 = Sx Theorem of Z-R: ~ O = nu{n} Proof: n in nu{n} but n not in O. (2) Sx = Sy -> x=y Theorem of Z-R: (n in w & k in w & nu{n} = ku{k}) -> n=k Proof: Suppose j in n. So j in ku{k}. So j in k or j=k. Suppose j=k. So k in n. But n=k or n in k. So either n in n, which is impossible, or k in n and n in k, which is impossible. So j in k. So n is a subset of k. Mutatis mutandis to show k is a subset of n. Note: regularity not needed since when n and k are natural numbers. (3) x+0 = x Theorem of Z-R: n in w -> n+0 = n Proof: From the recursive definition of + for w. (4) x+Sy = S(x+y) Theorem of Z-R: (n in w & k in w) -> (n+k#) = (n+k)# Proof: From the recursive definition of + for w. (5) x*0 = 0 Theorem of Z-R: n in w -> n*O = O Proof: From the recursive definition of * for w. (6) x*Sy = (x*y)+x Theorem of Z-R: (n in w & k in w) -> (n*k#) = (n*k)+k Proof: From the recursive definition of * for w. (7) Suppose P is a formula in the language, then all closures of the following are PA axioms: (P[0|x] & Ax(P -> P[Sx|x])) -> AxP We need to show that every closure of (P[0|x] & Ax(P -> P[Sx|x])) -> AxP is true in N. Let V = the set of variables for the language of PA. By induction on the number of free variables in P, we need only show: For all v in V, we have |=_M (P[0|x] & Ax(P -> P[Sx|x])) -> AxP [[v]]. Suppose v in V. Show: |=_M (P[0|x] & Ax(P -> P[Sx|x])) -> AxP [[v]]. Suppose |=_M P[0|x] & Ax(P -> P[Sx|x]) [[v]]. Show: |=_M AxP [[v]]. Show: For all k in w, we have |=_M P [[v_k]] where v_k is exactly as v except v_k maps x to k. Induction on k: Holds for k=O, since we have |=_M (P[0|x] [[v]]. Suppose holds for k; show for k#: So we have |=_M P [[v_k]] where v_k is exactly as v except v_k maps x to k. Show |=_M P [[v_k#]] where v_k# is exactly as v except v_k# maps x to k#. We have |=_M Ax(P -> P[Sx|x]) [[v]]. So |=_M P -> P[Sx|x] [[v_k]]. So |=_M P[Sx|x] [[v_k]]. We note that by induction on terms, for a term R, the term designation of R[Sx|x] under v_k equals the term designation of R under v_k#. Then by induction on formulas, for a formula P, |=_M P[Sx|x] [[v_k]] iff |=_M P [[v_k#]]. So |=_M P [[v_k#]]. Note: I hope to afford time to discuss this post with anyone who has informed, coherent, and rational comments. But I might not defend this post from uninformed, incoherent, and irrational criticisms, especially from posters who have shown themselves over a good period of time to be uneducable and hopeless cranks. Experience has shown that certain of these people will not allow themselves to be properly informed on certain matters in set theory and mathematical logic. MoeBlee
From: MoeBlee on 3 Jul 2010 17:07 The variable 'R' should be included in the list of variables of set theory used in the proof. MoeBlee
From: William Hale on 3 Jul 2010 18:34 In article <56301879-925c-41c3-a1aa-8830ea3d7840(a)d16g2000yqb.googlegroups.com>, MoeBlee <jazzmobe(a)hotmail.com> wrote: > In recent threads it has been questioned whether ZFC proves the > consistency of first order PA (called 'PA' in this post). This post > provides a proof in Z-R (Z set theory without the axiom of regularity) > of the consistency of PA, thus perforce ZFC proves the consistency of > first order PA.. In order to be clear for certain posters less > familiar with set theory and mathematical logic, we mention certain > details that readers better informed may not require. Our proof is > informal such that one who is adequately informed in basic predicate > logic and basic set theory can see that it is formalizable Z-R. > > We make use of ordinary theorems of Z-R, such as those in Enderton's > set theory book and those in his mathematical logic book, as such > results in mathematical logic are formalizable in Z-R. > > As to what axioms are used in all the theorems deployed for this proof > and in the argument itself here, we use identity theory as it is > subsumed by Z-R and all the single axioms of Z-R and certain instances > of the axiom schema of separation. Whether the proof can be done with > a proper subset of these axioms, I don't opine. In any case, > extensionality, schema of separation, union, and pairing are used even > in the earliest theorems from the axioms, as proof such as this > depends on certain of those theorems. The axiom of infinity is salient > in deriving the existence of a least successor-inductive set that is > the universe of the standard model for the language of PA. > > Notation: and terminology: > > In the language of set theory (which is the language of Z-R) extended > by definitions: > > w (read 'omega') stands for the set of natural numbers > O stands for the empty set > u stands for the binary union operation > # stands for the successor operation, e.g., n# = nu{n} > + stands for the addition operation for natural numbers > * stands for the multiplication operation for natural numbers > > |=_m P [[v]] > stands (e.g.) for > 'P is satisfied by m under v' > I.e., the formula P is satisfied by the model m with the function v, > where v is a function from the set of variables of the language > (whatever given language) into the universe (see below) for the model > m. > > We use the variables > m > P (read 'phi') > v > s > c > z > p > t > T > n > k > V > in the language of set theory. > > In the language of PA, we have the primitives: > 0 > S > + > * > > We use the variables > x > y > in the language of PA. > > Note: We use the typographical symbols '+' and '*' in both the > language of set theory and in the language of PA. This is due to a > limitation of ASCII not providing different fonts. These should be > regarded as if written in different font in order. It should be clear > from context which is intended in each occurrence. Also, we are not > fastidious with use-mention and "corner brackets" unless it required > to avoid ambiguity that can't be settled by the reader's exercise of > common sense in reading mathematics in informal ASCII. > > We adopt Enderton's definition of a structure (model) for a language. > A model for a language is a function from the set whose members are > exactly the universal quantifier and the function and predicate > symbols of the language, such that the universal quantifier is mapped > to a non-empty set (the universe for the model), and each n-place > function symbol is mapped to an n-place function on said non-empty > set, and each n-place predicate symbol is mapped to an n-place > relation on said non-empty set. > > So a model for the language of PA is a function: > > {<A s> <0 c> <S z> <+ p> <* t>} > > where 'A' is the universal quantifier for the language of P, s is a > nonempty set, c is a member of s, z is a 1-place function for s, p is > a 2-place function for s, and t is a 2-place function for s. > > For simpler notation, we may write the above model in tuple style: <s > c z p t>. > > For a definition of 'true in a model' we refer to Enderton's logic > book, since it would be too laborious to go through the steps toward > such a definition in a posting such as this. We trust that the reader > understands the definition of truth in a model (such as provided by > Enderton) and that the reader will recognize how the proofs below work > with this definition. (Those not familiar with this kind of thing will > have to study a book such as Enderton's.) > > In Z-R we define the standard model for the language of PA as 'N', as > follows: > > N = <w O # + *> > > We say a model m is a model OF a set of sentences T iff every member > of T is true in m. > > If there is an m that is a model of a set of sentences T, then we say > "T has a model". > > A theory is a set of sentences closed under entailment. I am not familiar with what you are doing here. Let me state what I think you are doing at a very high level and you tell me whether I am on the right track. One subgoal is to define a set in Z-R that represents the wffs of PA. We must first agree on an alphabet of characters that we will use in these wffs. Let say we stipulate an alphabet of 255 characters (probably 50 would suffice). We associate distinct concrete sets with each of these 255 characters. For example, we call the set 97 'a', 98 'b', etc. We then define the set of all finite sequences of characters of the alphabet. A subset of these we will define to be PA_Wffs, namely those sentences that are well-formed according to the normal rules. We also want to define the set PA_Theorems of all PA_Wffs that can be derived using the rules of deduction in Z-R. All this can be done in Z-R of course. Then we want to prove the following theorem in Z-R: Theorem. It is false that there is some wff p in PA_Wffs such that (p and not p) is an element of PA_Theorems. I see that I need a Z-R function that takes wffs x and y and maps it to a wff that represents "x and y". Like, I need a Z-R function that takes a wff x and maps it to a wff that represents "not x". I believe that these things can be done in Z-R. Is the above correct? We can do this before we get into models, can't we? If I am not on the right track on what you are doing, don't say that you could do what I am suggesting. I am not interested in alternate ways to prove PA consistent in Z-R: I want to follow the particular proof that you are presenting. > > IN Z-R we define 'PA' as the set of sentences (in the language > described by the aforementioned primitives) that is the entailment- > closure of these axioms (the universal closures of these): > > ~ 0 = Sx > Sx = Sy -> x=y > x+0 = x > x+Sy = S(x+y) > x*0 = 0 > x*Sy = (x*y)+x > > and > > If P is a formula in the language, then all closures of the following > are axioms: > > (P[0|x] & Ax(P -> P[Sx|x])) -> AxP > > If PA has a model m, then PA is consistent. Proof: If PA is > inconsistent then there is a sentence P in the language of PA such > that both P and ~P are in PA. But since m is a model of PA, both P and > ~P are true in m. But that is impossible, since a sentence is true in > a model iff the negation of the sentence is false in the model and no > sentence is both true and false in a given model (which follows from > how 'true in a model' is defined through definition by recursion). > > So we need only show that PA has a model. We show that M is a model of > PA. Thus we need only show that M is a model of each of the axioms of > PA (since entailment, by definition, preserves truth in a model): > > (1) ~ 0 = Sx > Theorem of Z-R: > ~ O = nu{n} > Proof: > n in nu{n} but n not in O. > > (2) Sx = Sy -> x=y > Theorem of Z-R: > (n in w & k in w & nu{n} = ku{k}) -> n=k > Proof: > Suppose j in n. So j in ku{k}. So j in k or j=k. Suppose j=k. So k in > n. But n=k or n in k. So either n in n, which is impossible, or k in n > and n in k, which is impossible. So j in k. So n is a subset of k. > Mutatis mutandis to show k is a subset of n. > > Note: regularity not needed since when n and k are natural numbers. > > (3) x+0 = x > Theorem of Z-R: > n in w -> n+0 = n > Proof: > From the recursive definition of + for w. > > (4) x+Sy = S(x+y) > Theorem of Z-R: > (n in w & k in w) -> (n+k#) = (n+k)# > Proof: > From the recursive definition of + for w. > > (5) x*0 = 0 > Theorem of Z-R: > n in w -> n*O = O > Proof: > From the recursive definition of * for w. > > (6) x*Sy = (x*y)+x > Theorem of Z-R: > (n in w & k in w) -> (n*k#) = (n*k)+k > Proof: > From the recursive definition of * for w. > > (7) Suppose P is a formula in the language, then all closures of the > following are PA axioms: (P[0|x] & Ax(P -> P[Sx|x])) -> AxP > > We need to show that every closure of (P[0|x] & Ax(P -> P[Sx|x])) -> > AxP is true in N. > > Let V = the set of variables for the language of PA. > > By induction on the number of free variables in P, we need only show: > > For all v in V, we have |=_M (P[0|x] & Ax(P -> P[Sx|x])) -> AxP [[v]]. > > Suppose v in V. > Show: |=_M (P[0|x] & Ax(P -> P[Sx|x])) -> AxP [[v]]. > Suppose |=_M P[0|x] & Ax(P -> P[Sx|x]) [[v]]. > Show: |=_M AxP [[v]]. > Show: For all k in w, we have |=_M P [[v_k]] where v_k is exactly as v > except v_k maps x to k. > Induction on k: > Holds for k=O, since we have |=_M (P[0|x] [[v]]. > Suppose holds for k; show for k#: > So we have |=_M P [[v_k]] where v_k is exactly as v except v_k maps x > to k. > Show |=_M P [[v_k#]] where v_k# is exactly as v except v_k# maps x to > k#. > We have |=_M Ax(P -> P[Sx|x]) [[v]]. > So |=_M P -> P[Sx|x] [[v_k]]. > So |=_M P[Sx|x] [[v_k]]. > We note that by induction on terms, for a term R, > the term designation of R[Sx|x] under v_k equals > the term designation of R under v_k#. > Then by induction on formulas, for a formula P, > |=_M P[Sx|x] [[v_k]] iff > |=_M P [[v_k#]]. > So |=_M P [[v_k#]]. > > Note: I hope to afford time to discuss this post with anyone who has > informed, coherent, and rational comments. But I might not defend this > post from uninformed, incoherent, and irrational criticisms, > especially from posters who have shown themselves over a good period > of time to be uneducable and hopeless cranks. Experience has shown > that certain of these people will not allow themselves to be properly > informed on certain matters in set theory and mathematical logic. > > MoeBlee
From: MoeBlee on 5 Jul 2010 13:47 Hi William, First a note: Just to be clear, when I listed certain symbols in my post, I mean that those are AMONG the symbols of those languages; It is not to be construed that those lists exhaust the symbols of those languages. Some items from your post: > One subgoal is to define a set in Z-R that represents the wffs of PA. Or, we can be more definite and say not just that we find a set to "represent" PA, but rather we actually define a specific set that IS PA. > We > must first agree on an alphabet of characters that we will use in these > wffs. Yes, except I say 'symbols'. At least in my view, the particular typographic shapes we use merely indicate the actual symbols, as the symbols themselves are abstract set-theoretic objects. (See Enderton's remarks on what symbols are, as I adopt one of the options he allows.) But let's not get bogged down in that. Let's just agree that we have some notion of a certain set of symbols. The symbols for set theory are the logical symbols (the quantifier, connectives), the variables (denumerably many), and the predicate symbols ('=' and 'e' (for 'e' read as the epsilon symbol)). > Let say we stipulate an alphabet of 255 characters (probably 50 > would suffice). Actually, we have denumerably (countably infinite) many symbols., as I mentioned above. > We associate distinct concrete sets with each of these > 255 characters. For example, we call the set 97 'a', 98 'b', etc No, throw that out. It doesn't work that way at all. > We > then define the set of all finite sequences of characters of the > alphabet. Yes, the set of finite sequences of symbols of the alphabet. > A subset of these we will define to be PA_Wffs, Right. > namely those > sentences that are well-formed according to the normal rules. The set of sentences is a proper subset of the set of wffs. The sentences are the wffs that have no free variables. > We also > want to define the set PA_Theorems of all PA_Wffs that can be derived > using the rules of deduction in Z-R. All this can be done in Z-R of > course. Right. > Then we want to prove the following theorem in Z-R: > > Theorem. It is false that there is some wff p in PA_Wffs such that (p > and not p) is an element of PA_Theorems. Since we have a more exact notion of falsehood in play in the proof, just to be very clear, let's leave out the word 'false' in this particular place. Instead: Z-R theorem: There does not exist a formula P such that both P and ~P are in PA. (Remember, PA IS the set of theorems, in the language, from a certain set of axioms). > I see that I need a Z-R function that takes wffs x and y and maps it to > a wff that represents "x and y". Like, I need a Z-R function that takes > a wff x and maps it to a wff that represents "not x". I believe that > these things can be done in Z-R. Forget about that. It's not the way it works. The overall plan is this (all in Z-R): We define 'model of a theory'. Very roughly, a model of a theory T is a model FOR the language of T such that every member of T is mapped to the value 1 (1 for true, 0 for false) by a function that maps all sentences of the language of T to either 0 or 1 and as stipulated by the ordinary "Tarski method". We also prove (trivially) that if a theory has a model then the theory is consistent. We also prove (quite trivially) that if all the axioms of a theory are true in a given model then that model is a model of the theory that is the entailment-closure of those axioms. (And PA is the entailment- closure of a certain set of axioms.) Then we construct a specific model for the language of PA and show that that model is model of PA. We show that by showing that all the axioms of PA are true in said model. MoeBlee
From: Nam Nguyen on 5 Jul 2010 13:57
MoeBlee wrote: > Hi William, > >> Then we want to prove the following theorem in Z-R: >> >> Theorem. It is false that there is some wff p in PA_Wffs such that (p >> and not p) is an element of PA_Theorems. > > Since we have a more exact notion of falsehood in play in the proof, > just to be very clear, let's leave out the word 'false' in this > particular place. Instead: > > Z-R theorem: There does not exist a formula P such that both P and ~P > are in PA. (Remember, PA IS the set of theorems, in the language, from > a certain set of axioms). But how do we know ~"Z-R theorem" isn't provable in Z-R? Iow, how do we know Z-R is _syntactically_ consistent? (Otherwise it'd would be fruitless to prove the formula "Z-R theorem" above!) > >> I see that I need a Z-R function that takes wffs x and y and maps it to >> a wff that represents "x and y". Like, I need a Z-R function that takes >> a wff x and maps it to a wff that represents "not x". I believe that >> these things can be done in Z-R. > > Forget about that. It's not the way it works. > > The overall plan is this (all in Z-R): > > We define 'model of a theory'. Very roughly, a model of a theory T is > a model FOR the language of T such that every member of T is mapped to > the value 1 (1 for true, 0 for false) by a function that maps all > sentences of the language of T to either 0 or 1 and as stipulated by > the ordinary "Tarski method". > > We also prove (trivially) that if a theory has a model then the theory > is consistent. > > We also prove (quite trivially) that if all the axioms of a theory are > true in a given model then that model is a model of the theory that is > the entailment-closure of those axioms. (And PA is the entailment- > closure of a certain set of axioms.) > > Then we construct a specific model for the language of PA and show > that that model is model of PA. We show that by showing that all the > axioms of PA are true in said model. > > MoeBlee |