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
The variable ‘R’ should be included in the list of variables of set
theory used in the proof.
MoeBlee
In article
<56301879-925c-41c3-a1aa-8830ea3d7…@d16g2000yqb.googlegroups.com>,
- Hide quoted text — Show quoted text -
MoeBlee <jazzm…@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.
- Hide quoted text — Show quoted text -
> 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
…
read more »
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
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!)
- Hide quoted text — Show quoted text -
>> 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
MoeBlee wrote:
> On Jul 5, 10:57 am, Nam Nguyen <namducngu…@shaw.ca> wrote:
>> 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!)
> Of course, if Z-R is inconsistent, then Z-R proves anything in the
> language of Z-R. My point is simply that whether Z-R is inconsistent
> or consistent at least we see that the above is an informal outline of
> a formal Z-R proof. If Z-R is inconsistent, then the above is an
> outline of a Z-R proof. And if Z-R is consistent, then the above is an
> outline of a Z-R proof. For that immediate purpose, that’s all that I
> need to say.
Well, then, PA is consistent can be proven in T = {(x=x) /\ ~(x=x)},
which I did mention already. That should settle the issue of formal
proof of PA’s consistency! Why bother with any thing as complicated
as Z-R or ZFC, or what have we?
In article
<c0b94c40-c6c0-4edf-916d-7fc31f249…@x27g2000yqb.googlegroups.com>,
MoeBlee <jazzm…@hotmail.com> wrote:
> 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.
Yes, I meant that.
> > 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.)
I am not talking about the physical or typographic shapes of symbols.
Just like we say the natural number 0 corresponds to the set {}, I want
to say the char ‘i’ corresponds to the set 105 and the char ‘f’
corresponds to the set 102 and the symbol "if" corresponds to the
function {<0,105>, <1,102>}, etc. Without going into details, I just
wanted to confirm that symbols, wffs, etc are really just sets in Z-R. I
am working at a very low level of what I am talking about, but I am
talking at a very hight level, saying what the actual low level things
are.
Your comment above about "typographic shapes" never entered my
consideration. I am trying to remain at a high level description of what
we would be doing at a low level.
> 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)).
That is given. But, that does not say what the symbols of PA in Z-R are.
In fact, I am saying that the symbols of PA in Z-R must be sets. The
symbol ‘e’ is not a set.
> > 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.
But, those symbols in Z-R are not the symbols in what we want to call PA
in Z-R.
> > 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.
If I throw that out, then I will have to go back to square one. Are you
sure you want me to throw that out?
- Hide quoted text — Show quoted text -
> > 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.
I was trying to be precise. I am taking sentences to be strings like
"===Sx Syy z zz" (that is, any list of characters to be used in our PA
within Z-R).
- Hide quoted text — Show quoted text -
> > 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.
But, this is exactly one of the points that I am not clear about. The
"false" that I am using here is a Z-R terminology, not something about
what we are doing for PA within Z-R.
I could say:
Theorem 1. It is false that {} in {}.
By that I mean:
Theorem 1. not ( {} in {} )
Again, I am not trying to be precise. But, in Z-R, I don’t have any
concept or definition of what "true" or "false" is. Do I need to
introduce these concepts at square one? I haven’t even mentioned
anything about proving anything consistent or not. I am just working
with sets, whether one set is an element of another set.
> 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.
I don’t won’t to forget about it. If I do, then I will have to go back
to square one. Just like for Golbach’s conjecture, given a number, I
need to be able to say it is even. Likewise, given a wff Q, I need to be
able to say that it is the negation of another wff R.
> The overall plan is this (all in Z-R):
> We define ‘model of a theory’.
This is exactly one of the points I am trying to figure out. I was
hoping to do a portion of the setup of stating and proving PA consistent
in the framework of Z-R.
In your terminology, I was trying to set up the apparatus to define what
a ‘theory’ is as an object in Z-R.
I was hoping that "model" would not be needed up to that point.
For example, with the set up that I presented, couldn’t I prove in Z-R
that there is no proof of less that 100 symbols that would prove a
contradiction "P and ~P" for some wff P? That is, I just enumerate the
255^100 proofs, select the proofs composed of wff sentences, filter out
the invalid proofs, and see if any of the valid proofs of what remains
has a last sentence of the form "P and ~P"?
- Hide quoted text — Show quoted text -
> 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
- Hide quoted text — Show quoted text -
MoeBlee wrote:
> On Jul 5, 11:52 am, Nam Nguyen <namducngu…@shaw.ca> wrote:
>> Well, then, PA is consistent can be proven in T = {(x=x) /\ ~(x=x)},
> Sure, but with the one technical quibble that the language for T
> provides a formulation of "PA is not consistent". But, yes, on the
> basic point, we agree.
>> which I did mention already. That should settle the issue of formal
>> proof of PA’s consistency! Why bother with any thing as complicated
>> as Z-R or ZFC, or what have we?
> Exactly! I mean that NOT sarcastically. This is part of what we’ve
> been saying ALL ALONG (in other threads, in various books, especially
> as well explained in Franzen’s incompleteness book).
So OK then. Do you now agree with me that:
[...] there’s no formal proof that PA is
consistent in a consistent theory (formal system)?
A clear answer and that would settle the discussion here.
- Hide quoted text — Show quoted text -
MoeBlee wrote:
> On Jul 5, 1:14 pm, Nam Nguyen <namducngu…@shaw.ca> wrote:
>> MoeBlee wrote:
>>> On Jul 5, 11:52 am, Nam Nguyen <namducngu…@shaw.ca> wrote:
>>>> Well, then, PA is consistent can be proven in T = {(x=x) /\ ~(x=x)},
>>> Sure, but with the one technical quibble that the language for T
>>> provides a formulation of "PA is not consistent". But, yes, on the
>>> basic point, we agree.
>>>> which I did mention already. That should settle the issue of formal
>>>> proof of PA’s consistency! Why bother with any thing as complicated
>>>> as Z-R or ZFC, or what have we?
>>> Exactly! I mean that NOT sarcastically. This is part of what we’ve
>>> been saying ALL ALONG (in other threads, in various books, especially
>>> as well explained in Franzen’s incompleteness book).
>> So OK then. Do you now agree with me that:
>> [...] there’s no formal proof that PA is
>> consistent in a consistent theory (formal system)?
>> A clear answer and that would settle the discussion here.
> I GAVE YOU a clear answer to that question in some detail in another
> thread. My answer does not take the form yes/no, for the reasons that
> can be seen in my fuller answer. Also, I just remarked in that thread
> that I’m not interested in responding to you in the manner of a
> deposition. I’m not going to give you bare "Yes"/"No" answers that
> require elaboration as to the actual sense and framework of the
> question.
That’s why our discussion in this thread (at least) goes around
and around, despite _your and mine_ wishes to the contrary: you simply
refused to answer direct to the point important but very easy to
understand question. (Btw, I already mentioned "I don’t know" is
a valid question too!)
For example, I’d answer "NO" (and already did) to the question.
And I’d provide to you a clear cut explanation if you ask. Basically
since _syntactically_ none of us can prove in meta level a disproof
of a formula in _any_ T, which is required as part of syntactical
definition of a T’s consistency, so the answer to the question must
be a NO.
See, I don’t have to invoke "another thread" or use the whole page
to summarize or explain my answer.
Again, MoeBlee, can you simply answer the question, as I’ve done so?
- Hide quoted text — Show quoted text -
MoeBlee wrote:
> On Jul 5, 1:46 pm, Nam Nguyen <namducngu…@shaw.ca> wrote:
>> MoeBlee wrote:
>>> On Jul 5, 1:14 pm, Nam Nguyen <namducngu…@shaw.ca> wrote:
>>>> MoeBlee wrote:
>>>>> On Jul 5, 11:52 am, Nam Nguyen <namducngu…@shaw.ca> wrote:
>>>>>> Well, then, PA is consistent can be proven in T = {(x=x) /\ ~(x=x)},
>>>>> Sure, but with the one technical quibble that the language for T
>>>>> provides a formulation of "PA is not consistent". But, yes, on the
>>>>> basic point, we agree.
>>>>>> which I did mention already. That should settle the issue of formal
>>>>>> proof of PA’s consistency! Why bother with any thing as complicated
>>>>>> as Z-R or ZFC, or what have we?
>>>>> Exactly! I mean that NOT sarcastically. This is part of what we’ve
>>>>> been saying ALL ALONG (in other threads, in various books, especially
>>>>> as well explained in Franzen’s incompleteness book).
>>>> So OK then. Do you now agree with me that:
>>>> [...] there’s no formal proof that PA is
>>>> consistent in a consistent theory (formal system)?
>>>> A clear answer and that would settle the discussion here.
>>> I GAVE YOU a clear answer to that question in some detail in another
>>> thread. My answer does not take the form yes/no, for the reasons that
>>> can be seen in my fuller answer. Also, I just remarked in that thread
>>> that I’m not interested in responding to you in the manner of a
>>> deposition. I’m not going to give you bare "Yes"/"No" answers that
>>> require elaboration as to the actual sense and framework of the
>>> question.
>> That’s why our discussion in this thread (at least) goes around
>> and around, despite _your and mine_ wishes to the contrary: you simply
>> refused to answer direct to the point important but very easy to
>> understand question. (Btw, I already mentioned "I don’t know" is
>> a valid question too!)
> We’re done, Nam.
If you say so (without giving an clear cut answer, even the framework,
you had sought for clarification, was confirmed to you)!
I’ve done my best to encourage a spirited discussion on foundational
problems!
- Hide quoted text — Show quoted text -
Nam Nguyen wrote:
> MoeBlee wrote:
>> On Jul 5, 1:46 pm, Nam Nguyen <namducngu…@shaw.ca> wrote:
>>> MoeBlee wrote:
>>>> On Jul 5, 1:14 pm, Nam Nguyen <namducngu…@shaw.ca> wrote:
>>>>> MoeBlee wrote:
>>>>>> On Jul 5, 11:52 am, Nam Nguyen <namducngu…@shaw.ca> wrote:
>>>>>>> Well, then, PA is consistent can be proven in T = {(x=x) /\ ~(x=x)},
>>>>>> Sure, but with the one technical quibble that the language for T
>>>>>> provides a formulation of "PA is not consistent". But, yes, on the
>>>>>> basic point, we agree.
>>>>>>> which I did mention already. That should settle the issue of formal
>>>>>>> proof of PA’s consistency! Why bother with any thing as complicated
>>>>>>> as Z-R or ZFC, or what have we?
>>>>>> Exactly! I mean that NOT sarcastically. This is part of what we’ve
>>>>>> been saying ALL ALONG (in other threads, in various books, especially
>>>>>> as well explained in Franzen’s incompleteness book).
>>>>> So OK then. Do you now agree with me that:
>>>>> [...] there’s no formal proof that PA is
>>>>> consistent in a consistent theory (formal system)?
>>>>> A clear answer and that would settle the discussion here.
>>>> I GAVE YOU a clear answer to that question in some detail in another
>>>> thread. My answer does not take the form yes/no, for the reasons that
>>>> can be seen in my fuller answer. Also, I just remarked in that thread
>>>> that I’m not interested in responding to you in the manner of a
>>>> deposition. I’m not going to give you bare "Yes"/"No" answers that
>>>> require elaboration as to the actual sense and framework of the
>>>> question.
>>> That’s why our discussion in this thread (at least) goes around
>>> and around, despite _your and mine_ wishes to the contrary: you simply
>>> refused to answer direct to the point important but very easy to
>>> understand question. (Btw, I already mentioned "I don’t know" is
>>> a valid question too!)
>> We’re done, Nam.
> If you say so (without giving an clear cut answer, even the framework,
> you had sought for clarification, was confirmed to you)!
> I’ve done my best to encourage a spirited discussion on foundational
> problems!
I might have meant "fruitful/result-oriented" instead of "spirited".
(Those who choose to read the following do so at their own risk. It
contains erratic rambling and pointless maundering. Some topical logical
babbling has been thrown in to fool the spam filter. (It would be very
helpful if those portions of this post had been marked somehow. It’s a
pity that they aren’t. I think it’s mostly the middle bits, but it’s
difficult to tell as reading what I’ve written puts me to sleep.) I
tried for half an hour to make it all — that is, all of the nonsensical
twaddle I’ve for some reason liberally peppered this post with, at
random junctions, although usually within parentheses, happily) hang
together, then gave up. I then tried again. Alas, I had in the meantime
forgotten what it was all about so it only made things worse. Next, I
decided it would be a good idea to read a logic text for a while — I
was trying to wrap my head around some erudite concepts of generalized
recursion theory — and have a few cigarettes. After that, I returned to
polishing this post, and proceeded to do so. I soon found out I had no
idea what I had been earlier writing about, why I had made the
"corrections" I had made, and so on, so with hindsight it wasn’t a great
idea. It was also not a huge success, judging by the result. My
apologies, (Plus, I promise to buy anyone who reads through this post a
few beers, making also a generous allowance to those who don’t like to
alcohol that they have the choice of an American beer if they so wish.))
William Hale <h…@tulane.edu> writes:
> At this point of time, my thinking is that the theory of PA can be
> made to correspond to something that can be given in ZFC. But my
> current thinking is that the theory of PA are metatheorems, rather
> than theorems of ZFC. I think I can see how the theory of PA and these
> metatheorems can be made to correspond to things in ZFC so that the
> metatheorems of the metatheory become theorems of ZFC. But, just like
> I don’t think the non-Euclidean geometer so work in Euclidean
> geometry, I don’t thing the mathematical logician should work in ZFC
> to do his thing. The logician is contemplating many axiom system with
> many different logical rules and many different deduction
> principles. The logician does not need to cast all of this into the
> ZFC system (even if it could be done).
But should the logician accept, say, theorems of the form
Theory T is inconsistent.
There are infinitely many twin primes.
and so on, on basis of their provability in ZF(C)? On what basis should
we accept as correct statements of the form
The statement P is provable in theory T.
The statement P is not provable in theory T.
It is undecidable in PA whether P is provable in theory T.
? Even medias res in contemplation of many many axiom systems and what
not, surely we should accept some such statements, reject some such
statements, remain undecided about some such statements. As a matter of
fact, we accept some such statements, reject some such statements and
steadfastly remain agnostic about some such statements, as with any
mathematical claims. We’re not here dealing with some strange
metaphysical assertions, after all, but with perfectly meaningful
mathematical claims: there’s a finite tree, graph, sequence (depending
on which way you swing when it comes to presenting formal proofs as
mathematical objects) meeting such and such mathematical
conditions. Surely whatever attitude we adopt towards claims and
assertions about finite trees, graphs, sequences, meeting
straightforwardly defined mathematical conditions, must extend also to
consistency statements. Whatever contemplating of different axiom
systems we may envisage is as relevant in case of the Kruskal tree
theorem, Dirilecht’s theorem, the fundamental theorem of analysis, as it
is in case of consistency theorems.
> I don’t think that the claim that ZFC is the foundation of standard
> mathematics includes proving PA is consistent.
Surely it does, since it’s a trivial exercise to prove PA consistent in
standard mathematics.
> I don’t require that logicians work in ZFC. I think that is an
> artificial requirement.
It’s an extremely artificial requirement. No one "works in" ZFC in any
literal sense. People just do mathematics in a way that, as it happens,
virtually always is formalizable in ZFC (or certain other standard
systems, e.g. in case of constructive or intuitionistic mathematics
(although even here we may note intuitionists and classical
mathematicians are happily agreed, in spite of their disagreement with
each other, and disagreement within, on what theories are
unproblematically consistent and on for what theories consistency is an
open problem, thanks, in no small part, to much work in proof theory
relating constructive and classical theories, which work, rather
curiously, is the main concern of a great many constructivists instead
the proving of constructive results as one might naively expect) in
intuitionistic analysis, constructive type theory, formalizations of
recursive mathematics), in so far as provability of results, suitably
formalized, is concerned.
(I again ask that the reader for patience, and also that they accept the
challenge of testing their hand, for no skill can develop without
practice and exercises that are on the verge of being impossible, their
keen skill at parsing, and of course, there being no implication my
readers are illiterate slobs, at easily understanding, making sense of,
and comprehensively comprehending arbitrarily deeply nested syntactic
constructions, finite instances of which can be discerned in the
preceding sentence. I ask only that they go about this task with a sense
of play and fun, as if children once again, shedding all needless cloths
of solemn adult seriousness (and pretentiousness) that serve no purpose
other than to conceal, or to reveal, so to speak, what is not really
there, creating a phantasm of cloth, of intimidating protruding alien
and inhuman shapes suggestive of false contours, impossible on a human
being, shedding these cloths that embody and implicitly, with their
gentle all-embracing embrace, imprison — for adulthood can’t escape its
shallow window dressing, the prison it’s made for itself out of all the
needless junk of the yonder year, of random fragments of speech that
were never meant to mean much which stuck for some random reason to the
mind of an impressionable child, many decades ago, this impossibility,
of escaping these thing, manifest in the very need to attempt to do so
at all — in them all that is grown-up, all the unsaid rules, about who
can wear this, who can wear that, about what can’t be even mentioned and
must be alluded to in hushed voices filled with intimate secrets (or a
promise of an intimate secret, one day, or perhaps of disappointment,
once you get old enough to know about these thing) their peddler doesn’t
even know they harbour, hushes from the abyss of memory so profound it
eludes the photoalbum residing instead in the irrational fear you have
of bees, the feeling of happiness the smell of butter in the morning
(but never at any other time) inexplicably brings to your little
brother, residing deep in the farthest recesses of their mind and
memories, in the most foldy of the folds of their neocortex folds,
inherited and passed through a nondescript chain of innumerable
nondescript ancestor, all of them who were equally bewildered by the
idea of hidden revelations, promised, but never, even when they get old
enough, revealed, the shared notion they should have figured it all out
on their own already making it impossible to ask, these hinted at
secrets that make them adult, make them special, make them capable of
making decisions for others, for taking responsibility, passed through
an equally hushed hint that this is not the done thing, this is the way
of man, this the way of woman, communicated steganographically by way of
an unenthusiastic, lukewarm compliment on a drawing or winning the
cricket match, words exchanged when they don’t think you can hear, a
gesture that goes unnoticed by everyone else but means the worlds,
whispers that clumsily yet so effectively point at the unsaid and
unutterable truth, the truth of a life that’s your not of your own
making, that you can’t make your life in your image, as we all wish —
and think true — when we’re children, that we must live a life
governed, shaped, molded, put in perspective — a silly, tragically
ill-headed putting this, since there’s no perspective for life, or,
rather, there are an indefinite number of perspectives, and no absolute
notion of a valid perspective, since like is both great, little, and
neither of these things, and is made of the unthinkable eons of
cosmological evolution, in as great degree as it is made of the
intoxicating feeling of kissing the one you love for the first time
(going for sleep for an extended period also gives one an intoxicated
feeling, and a tendency to ramble, but is not anywhere as pleasant,
which is why I don’t really recommend it for anyone), and tasting a
faint smell of tobacco and tooth-paste in the kiss, happy in the
knowledge there’s nothing essentially different to what the other person
is tasting, happy in the knowledge that in this most banal, common,
usual, everyday act there’s no difference between its occurrences if we
look at it from afar, but a whole veritable world of difference, a world
to learn, a world to enter into, not as a conqueror, but as an invited
guest, happy in all this when it’s you who’s kissing — with the
horrible, clinical, sterile idea of doing good, in the exact way your
parents understood it, which, for all their rebellion, got from their
parents, save for adding some inchoate bits of "No!" into it whenever
they were too badly burned, correcting some details got wrong (or not,
depending on how accurate your parents’ recollection is), some peculiar
folk ways, family traditions associated in the mind of your mother with
an unkindly aunt, a
…
read more »
- Hide quoted text — Show quoted text -
Aatu Koskensilta wrote:
> (Those who choose to read the following do so at their own risk. It
> contains erratic rambling and pointless maundering. Some topical logical
> babbling has been thrown in to fool the spam filter. (It would be very
> helpful if those portions of this post had been marked somehow. It’s a
> pity that they aren’t. I think it’s mostly the middle bits, but it’s
> difficult to tell as reading what I’ve written puts me to sleep.) I
> tried for half an hour to make it all — that is, all of the nonsensical
> twaddle I’ve for some reason liberally peppered this post with, at
> random junctions, although usually within parentheses, happily) hang
> together, then gave up. I then tried again. Alas, I had in the meantime
> forgotten what it was all about so it only made things worse. Next, I
> decided it would be a good idea to read a logic text for a while — I
> was trying to wrap my head around some erudite concepts of generalized
> recursion theory — and have a few cigarettes. After that, I returned to
> polishing this post, and proceeded to do so. I soon found out I had no
> idea what I had been earlier writing about, why I had made the
> "corrections" I had made, and so on, so with hindsight it wasn’t a great
> idea. It was also not a huge success, judging by the result. My
> apologies, (Plus, I promise to buy anyone who reads through this post a
> few beers, making also a generous allowance to those who don’t like to
> alcohol that they have the choice of an American beer if they so wish.))
> William Hale <h…@tulane.edu> writes:
> > At this point of time, my thinking is that the theory of PA can be
> > made to correspond to something that can be given in ZFC. But my
> > current thinking is that the theory of PA are metatheorems, rather
> > than theorems of ZFC. I think I can see how the theory of PA and these
> > metatheorems can be made to correspond to things in ZFC so that the
> > metatheorems of the metatheory become theorems of ZFC. But, just like
> > I don’t think the non-Euclidean geometer so work in Euclidean
> > geometry, I don’t thing the mathematical logician should work in ZFC
> > to do his thing. The logician is contemplating many axiom system with
> > many different logical rules and many different deduction
> > principles. The logician does not need to cast all of this into the
> > ZFC system (even if it could be done).
> But should the logician accept, say, theorems of the form
> Theory T is inconsistent.
> There are infinitely many twin primes.
> and so on, on basis of their provability in ZF(C)? On what basis should
> we accept as correct statements of the form
> The statement P is provable in theory T.
> The statement P is not provable in theory T.
> It is undecidable in PA whether P is provable in theory T.
> ? Even medias res in contemplation of many many axiom systems and what
> not, surely we should accept some such statements, reject some such
> statements, remain undecided about some such statements. As a matter of
> fact, we accept some such statements, reject some such statements and
> steadfastly remain agnostic about some such statements, as with any
> mathematical claims. We’re not here dealing with some strange
> metaphysical assertions, after all, but with perfectly meaningful
> mathematical claims: there’s a finite tree, graph, sequence (depending
> on which way you swing when it comes to presenting formal proofs as
> mathematical objects) meeting such and such mathematical
> conditions. Surely whatever attitude we adopt towards claims and
> assertions about finite trees, graphs, sequences, meeting
> straightforwardly defined mathematical conditions, must extend also to
> consistency statements. Whatever contemplating of different axiom
> systems we may envisage is as relevant in case of the Kruskal tree
> theorem, Dirilecht’s theorem, the fundamental theorem of analysis, as it
> is in case of consistency theorems.
> > I don’t think that the claim that ZFC is the foundation of standard
> > mathematics includes proving PA is consistent.
> Surely it does, since it’s a trivial exercise to prove PA consistent in
> standard mathematics.
> > I don’t require that logicians work in ZFC. I think that is an
> > artificial requirement.
> It’s an extremely artificial requirement. No one "works in" ZFC in any
> literal sense. People just do mathematics in a way that, as it happens,
> virtually always is formalizable in ZFC (or certain other standard
> systems, e.g. in case of constructive or intuitionistic mathematics
> (although even here we may note intuitionists and classical
> mathematicians are happily agreed, in spite of their disagreement with
> each other, and disagreement within, on what theories are
> unproblematically consistent and on for what theories consistency is an
> open problem, thanks, in no small part, to much work in proof theory
> relating constructive and classical theories, which work, rather
> curiously, is the main concern of a great many constructivists instead
> the proving of constructive results as one might naively expect) in
> intuitionistic analysis, constructive type theory, formalizations of
> recursive mathematics), in so far as provability of results, suitably
> formalized, is concerned.
> (I again ask that the reader for patience, and also that they accept the
> challenge of testing their hand, for no skill can develop without
> practice and exercises that are on the verge of being impossible, their
> keen skill at parsing, and of course, there being no implication my
> readers are illiterate slobs, at easily understanding, making sense of,
> and comprehensively comprehending arbitrarily deeply nested syntactic
> constructions, finite instances of which can be discerned in the
> preceding sentence. I ask only that they go about this task with a sense
> of play and fun, as if children once again, shedding all needless cloths
> of solemn adult seriousness (and pretentiousness) that serve no purpose
> other than to conceal, or to reveal, so to speak, what is not really
> there, creating a phantasm of cloth, of intimidating protruding alien
> and inhuman shapes suggestive of false contours, impossible on a human
> being, shedding these cloths that embody and implicitly, with their
> gentle all-embracing embrace, imprison — for adulthood can’t escape its
> shallow window dressing, the prison it’s made for itself out of all the
> needless junk of the yonder year, of random fragments of speech that
> were never meant to mean much which stuck for some random reason to the
> mind of an impressionable child, many decades ago, this impossibility,
> of escaping these thing, manifest in the very need to attempt to do so
> at all — in them all that is grown-up, all the unsaid rules, about who
> can wear this, who can wear that, about what can’t be even mentioned and
> must be alluded to in hushed voices filled with intimate secrets (or a
> promise of an intimate secret, one day, or perhaps of disappointment,
> once you get old enough to know about these thing) their peddler doesn’t
> even know they harbour, hushes from the abyss of memory so profound it
> eludes the photoalbum residing instead in the irrational fear you have
> of bees, the feeling of happiness the smell of butter in the morning
> (but never at any other time) inexplicably brings to your little
> brother, residing deep in the farthest recesses of their mind and
> memories, in the most foldy of the folds of their neocortex folds,
> inherited and passed through a nondescript chain of innumerable
> nondescript ancestor, all of them who were equally bewildered by the
> idea of hidden revelations, promised, but never, even when they get old
> enough, revealed, the shared notion they should have figured it all out
> on their own already making it impossible to ask, these hinted at
> secrets that make them adult, make them special, make them capable of
> making decisions for others, for taking responsibility, passed through
> an equally hushed hint that this is not the done thing, this is the way
> of man, this the way of woman, communicated steganographically by way of
> an unenthusiastic, lukewarm compliment on a drawing or winning the
> cricket match, words exchanged when they don’t think you can hear, a
> gesture that goes unnoticed by everyone else but means the worlds,
> whispers that clumsily yet so effectively point at the unsaid and
> unutterable truth, the truth of a life that’s your not of your own
> making, that you can’t make your life in your image, as we all wish —
> and think true — when we’re children, that we must live a life
> governed, shaped, molded, put in perspective — a silly, tragically
> ill-headed putting this, since there’s no perspective for life, or,
> rather, there are an indefinite number of perspectives, and no absolute
> notion of a valid perspective, since like is both great, little, and
> neither of these things, and is made of the unthinkable eons of
> cosmological evolution, in as great degree as it is made of the
> intoxicating feeling of kissing the one you love for the first time
> (going for sleep for an extended period also gives one an intoxicated
> feeling, and a tendency to ramble, but is not anywhere as pleasant,
> which is why I don’t really recommend it for anyone), and tasting a
> faint smell of tobacco and tooth-paste in the kiss, happy in the
> knowledge there’s nothing essentially different to what the other person
> is tasting, happy in the knowledge that in this most banal, common,
> usual, everyday act there’s no difference between its occurrences if we
> look at it from afar, but a whole veritable world of difference, a world
> to learn, a world to enter into, not as a conqueror, but as an invited
> guest, happy in all this when it’s you who’s kissing — with the
> horrible, clinical, sterile idea of doing good, in the exact way your
> parents understood it,
…
read more »
Aatu Koskensilta wrote:
> William Hale <h…@tulane.edu> writes:
>> But, I am not asking whether this is a viable approach. I am asking if
>> this is what you are doing. I understand that you will introduce
>> "model theory" to wrap up the proof. But, I am taking this
>> introduction of "model theory" to be similar to the introduction of
>> "complex number theory" to wrap up a proof in basic number theory (eg,
>> proving Fermat’s last theorem).
> I have already posted an outline of a proof where we need not invoke any
> model theory, indeed nothing beyond basic properties of naturals and an
> elementary infinitary inductive definition, stuff probably transparent
> to anyone who’s ever seen any inductive definitions in mathematics.
The unfortunate thing for us, however, is that "basic properties" of
the natural numbers have dual faces: one can also express the fundamental
theorem of arithmetic _without_ induction at all!
> Only an overexposure to formalities, or a bent mind — not that that’s
> necessarily a bad thing
> — can possibly lead one to doubt the
> legitimacy, correctness, evidence, sureness, of such mathematical
> constructions and see-for-yourself proofs thereof.
Difficulties in sciences in general were often marked by seemingly
contrasting realities: the relativity vs the absoluteness of the speed,
of light, the clock-work universe vs Heisenberg’s Uncertainty, the
wave vs particle duality of photons, etc… And in those difficult
times of knowledge, _only non-bias reconciliation of concepts_ would
prevail!
Today we’re facing the same kind of difficulty in FOL reasoning: the
seemingly irreconcilable induction nature of pCG expression, and the
non-induction counterpart of cGC.
If, in the name of familiarity of "ordinary" mathematics, we _discard_
one of them (the later) so that our reasoning life be somehow less
"burdened" then we have indeed failed what is the spirit of mathematics
and mathematical reasoning! Both then are condemned to the sorrow state
of eternal stagnation!
herbzet wrote:
> Just btw, my cousin set a collegiate record, back in the day, for
> continuous radio broadcasting, under the name of "Beau Harris" —
> five days with a lot of coffee and only a little dozing during long
> cuts.
> Just to give you something to shoot for …
http://en.wikipedia.org/wiki/KWUR#History
In article <87pqz1jsa0….@dialatheia.truth.invalid>,
Aatu Koskensilta <aatu.koskensi…@uta.fi> wrote:
Briefly, I think that you are saying I am wrong when I say that
logicians don’t work in ZFC. I agree that I was wrong.
I understand that you don’t like the term "work in ZFC" since
mathematicians don’t work in ZFC as such. But, I am using the term
"work" as a shorthand for what is meant when we say that ZFC serves as a
foundation for proving things in standard mathematics.
By standard mathematics, I was limiting myself to the areas of real
analysis, complex analysis, algebra, topology, and (differential)
geometry. That is, areas of mathematics discussed before 1900. I didn’t
include logic since its main results were done after 1900.
Let me give some more on what I mean by "work in ZFC". I think some
non-mathematicians think that a mathematician comes up with an informal
proof and that it may or may not be formalized. For example, a
mathematician might come up with an informal proof that that two natural
number always has a least common multiple. I think the non-mathematician
might then think in order to formalize this informal proof, one would
first decide what axioms system to use, say PA or ZFC. I object to this
viewpoint (if anyone actually even has it). The mathematician should
already have decided what axiom system he is working in, either PA or
ZFC, before he writes out his informal proof. If I were given the
exercise to prove that theorem in a class where I was learning PA, then
I would consider the theorems that have been proved in PA to come up
with a (informal) proof of existence of LCM. But, if I were given the
exercise to prove that theorem in a class where I was learning abstract
algebra (where ZFC is the foundation, since we talk about sets and Zorn
lemma a lot), then I would consider the theorems that have been proved
in ZFC to come up with a (informal) proof of the existence of LCM. These
two informal proofs would not be the same, and my thought process would
be different in the two cases. Thus, in the first case, I came up with
an informal proof working in PA, while in the second case, I came up
with an informal proof working in ZFC. I don’t like the idea of just
coming up with an informal proof, with no mention of the axiom system
being used. Of course, I realize that many mathematicians could care
less about all this when they prove things.
- Hide quoted text — Show quoted text -
> (Those who choose to read the following do so at their own risk. It
> contains erratic rambling and pointless maundering. Some topical logical
> babbling has been thrown in to fool the spam filter. (It would be very
> helpful if those portions of this post had been marked somehow. It’s a
> pity that they aren’t. I think it’s mostly the middle bits, but it’s
> difficult to tell as reading what I’ve written puts me to sleep.) I
> tried for half an hour to make it all — that is, all of the nonsensical
> twaddle I’ve for some reason liberally peppered this post with, at
> random junctions, although usually within parentheses, happily) hang
> together, then gave up. I then tried again. Alas, I had in the meantime
> forgotten what it was all about so it only made things worse. Next, I
> decided it would be a good idea to read a logic text for a while — I
> was trying to wrap my head around some erudite concepts of generalized
> recursion theory — and have a few cigarettes. After that, I returned to
> polishing this post, and proceeded to do so. I soon found out I had no
> idea what I had been earlier writing about, why I had made the
> "corrections" I had made, and so on, so with hindsight it wasn’t a great
> idea. It was also not a huge success, judging by the result. My
> apologies, (Plus, I promise to buy anyone who reads through this post a
> few beers, making also a generous allowance to those who don’t like to
> alcohol that they have the choice of an American beer if they so wish.))
> William Hale <h…@tulane.edu> writes:
> > At this point of time, my thinking is that the theory of PA can be
> > made to correspond to something that can be given in ZFC. But my
> > current thinking is that the theory of PA are metatheorems, rather
> > than theorems of ZFC. I think I can see how the theory of PA and these
> > metatheorems can be made to correspond to things in ZFC so that the
> > metatheorems of the metatheory become theorems of ZFC. But, just like
> > I don’t think the non-Euclidean geometer so work in Euclidean
> > geometry, I don’t thing the mathematical logician should work in ZFC
> > to do his thing. The logician is contemplating many axiom system with
> > many different logical rules and many different deduction
> > principles. The logician does not need to cast all of this into the
> > ZFC system (even if it could be done).
> But should the logician accept, say, theorems of the form
> Theory T is inconsistent.
> There are infinitely many twin primes.
> and so on, on basis of their provability in ZF(C)? On what basis should
> we accept as correct statements of the form
> The statement P is provable in theory T.
> The statement P is not provable in theory T.
> It is undecidable in PA whether P is provable in theory T.
Well, I thought the logician was not working in ZFC. For example, take
the deduction theorem in logic, which Enderton mentions in his book. I
thought that this was a metatheorem. I took the proof of "A -> A" that
used the deduction theorem and following the meta-proof of the deduction
theorem, I was able to eliminate the use of the deduction theorem and
just use the axioms given by Enderton to give a proof of "A -> A"
according to the definition of proof that Enderton stated.
Likewise, Enderton stated that you can cheat in a proof by just
referring to previous theorems as justification, without having to refer
back only to axioms (according to the definition of proof that Enderton
stated). This seemed like a meta-theorem also.
Whether these two meta-theorems needed to be proved ultimately in ZFC I
didn’t consider as necessary. Even now, I am not sure how they fit into
logic as a logician would discuss them.
I think that you are telling me that logicians have succumbed to using
ZFC like the other mathematicians have.
I understand and agree that the theory of Turing Machines are best done
in the framework of ZFC, where one defines a turing Machine as a tuple
of certain sets.
I am not so sure that the lambda calculus should be done in the
framework of ZFC (or even if you are saying that it is done in ZFC,
though I suspect that you would say it is).
- Hide quoted text — Show quoted text -
> ? Even medias res in contemplation of many many axiom systems and what
> not, surely we should accept some such statements, reject some such
> statements, remain undecided about some such statements. As a matter of
> fact, we accept some such statements, reject some such statements and
> steadfastly remain agnostic about some such statements, as with any
> mathematical claims. We’re not here dealing with some strange
> metaphysical assertions, after all, but with perfectly meaningful
> mathematical claims: there’s a finite tree, graph, sequence (depending
> on which way you swing when it comes to presenting formal proofs as
> mathematical objects) meeting such and such mathematical
> conditions. Surely whatever attitude we adopt towards claims and
> assertions about finite trees, graphs, sequences, meeting
> straightforwardly defined mathematical conditions, must extend also to
> consistency statements. Whatever contemplating of different axiom
> systems we may envisage is as relevant in case of the Kruskal tree
> theorem, Dirilecht’s theorem, the fundamental theorem of analysis, as it
> is in case of consistency theorems.
I guess I was misled by the term "meta", which you explain further down
should not be given too much significance. I was reading too much into
the term "meta".
> > I don’t think that the claim that ZFC is the foundation of standard
> > mathematics includes proving PA is consistent.
> Surely it does, since it’s a trivial exercise to prove PA consistent in
> standard mathematics.
Ok.
> > I don’t require that logicians work in ZFC. I think that is an
> > artificial requirement.
> It’s an extremely artificial requirement. No one "works in" ZFC in any
> literal sense.
I didn’t mean it in a literal sense. I was comparing it more to trying
to do non-Euclidean geometry in the framework of Euclidean geometry.
Even though it could be done, I think that is artificial.
As you are pointing out to me, you want to have ZFC provide the
framework for you to prove your (logical) theorems about (logical)
theories.
- Hide quoted text — Show quoted text -
> People just do mathematics in a way that, as it happens,
> virtually always is formalizable in ZFC (or certain other standard
> systems, e.g. in case of constructive or intuitionistic mathematics
> (although even here we may note intuitionists and classical
> mathematicians are happily agreed, in spite of their disagreement with
> each other, and disagreement within, on what theories are
> unproblematically consistent and on for what theories consistency is an
> open problem, thanks, in no small part, to much work in proof theory
> relating constructive and classical theories, which work, rather
> curiously, is the main concern of a great many constructivists instead
> the proving of constructive results as one might naively expect) in
> intuitionistic analysis, constructive type theory, formalizations of
> recursive mathematics), in so far as provability of results, suitably
> formalized, is concerned.
> (I again ask that the reader for patience, and also that they accept the
> challenge of testing their hand, for no skill can develop without
> practice and exercises that are on the verge of being impossible, their
> keen skill at parsing, and of course, there being no implication my
> readers are illiterate slobs, at easily understanding,
…
read more »
- Hide quoted text — Show quoted text -
Nam Nguyen wrote:
> Aatu Koskensilta wrote:
>> William Hale <h…@tulane.edu> writes:
>>> But, I am not asking whether this is a viable approach. I am asking if
>>> this is what you are doing. I understand that you will introduce
>>> "model theory" to wrap up the proof. But, I am taking this
>>> introduction of "model theory" to be similar to the introduction of
>>> "complex number theory" to wrap up a proof in basic number theory (eg,
>>> proving Fermat’s last theorem).
>> I have already posted an outline of a proof where we need not invoke any
>> model theory, indeed nothing beyond basic properties of naturals and an
>> elementary infinitary inductive definition, stuff probably transparent
>> to anyone who’s ever seen any inductive definitions in mathematics.
> The unfortunate thing for us, however, is that "basic properties" of
> the natural numbers have dual faces: one can also express the fundamental
> theorem of arithmetic _without_ induction at all!
>> Only an overexposure to formalities, or a bent mind — not that that’s
>> necessarily a bad thing
>> — can possibly lead one to doubt the
>> legitimacy, correctness, evidence, sureness, of such mathematical
>> constructions and see-for-yourself proofs thereof.
> Difficulties in sciences in general were often marked by seemingly
> contrasting realities: the relativity vs the absoluteness of the speed,
> of light, the clock-work universe vs Heisenberg’s Uncertainty, the
> wave vs particle duality of photons, etc… And in those difficult
> times of knowledge, _only non-bias reconciliation of concepts_ would
> prevail!
> Today we’re facing the same kind of difficulty in FOL reasoning: the
> seemingly irreconcilable induction nature of pCG expression, and the
> non-induction counterpart of cGC.
> If, in the name of familiarity of "ordinary" mathematics, we _discard_
> one of them (the later) so that our reasoning life be somehow less
> "burdened" then we have indeed failed what is the spirit of mathematics
> and mathematical reasoning! Both then are condemned to the sorrow state
> of eternal stagnation!
Not to mention that we would, in such case, brainwash our future
generations to what we today _believe_ as "ordinary", "self-evident",…
and rob them of the ability to discover for themselves what the natural
numbers might be. Or NOT be.