A Consistent Theory of Arithmetic
RussellE
Ax (x in N -> (S(x) =/= "0"))
AxAy (x,y in N -> (S(x) = S(y) -> x = y))
Ax (x in N -> (x + "0" = x))
AxAy (x,y in N -> (x+S(y) = S(x+y)))
Ax (x in N -> (x * "0" = "0"))
AxAy (x,y in N -> (x*S(y) = (x*y)+x) )
Russell
- 2 many 2 count
Alan Smaill
It's weaker --
it does not follow that addition is commutative, for example.
There is also no guarantee that x + y is in N if x and y are --
you might want to remedy that.
(no need to quote the constant, of course)
> Russell
> - 2 many 2 count
--
Alan Smaill
RussellE
> RussellE <reaste...@gmail.com> writes:
> > Is the following theory weaker or stronger than Peano Arithmetic?
>
> > Ax (x in N -> (S(x) =/= "0"))
> > AxAy (x,y in N -> (S(x) = S(y) -> x = y))
> > Ax (x in N -> (x + "0" = x))
> > AxAy (x,y in N -> (x+S(y) = S(x+y)))
> > Ax (x in N -> (x * "0" = "0"))
> > AxAy (x,y in N -> (x*S(y) = (x*y)+x) )
> It's weaker --
> it does not follow that addition is commutative, for example.
> There is also no guarantee that x + y is in N if x and y are --
> you might want to remedy that.
No. The possibilty x+y is not in N is what I going for.
Russell
- logic must be idiot proof
Alan Smaill
Even when both x and y are in N ???
Do you want 0 in N, btw?
You don't even have that, so far.
What about if x in N, then s(x) in N?
> Russell
> - logic must be idiot proof
--
Alan Smaill
Frederick Williams
>
> Is the following theory weaker or stronger than Peano Arithmetic?
How about "not comparable with"? By which I mean that your theorems are
not a subset of PAs (because PA has no N) and PA's theorems are not a
subset of yours (because PA has an induction schema).
> Ax (x in N -> (S(x) =/= "0"))
> AxAy (x,y in N -> (S(x) = S(y) -> x = y))
> Ax (x in N -> (x + "0" = x))
> AxAy (x,y in N -> (x+S(y) = S(x+y)))
> Ax (x in N -> (x * "0" = "0"))
> AxAy (x,y in N -> (x*S(y) = (x*y)+x) )
--
When a true genius appears in the world, you may know him by
this sign, that the dunces are all in confederacy against him.
Jonathan Swift: Thoughts on Various Subjects, Moral and Diverting
JimmyJohn
<9a6a907b-8e6c-49e3...@k15g2000pri.googlegroups.com>,
RussellE <reas...@gmail.com> wrote:
Yes!
--
Science is based directly on objective physical evidence,
and nothing that is not based directly on objective physical evidence
can be science.
RussellE
wrote:
> RussellE wrote:
> > Is the following theory weaker or stronger than Peano Arithmetic?
>
> How about "not comparable with"? By which I mean that your theorems are
> not a subset of PAs (because PA has no N) and PA's theorems are not a
> subset of yours (because PA has an induction schema).
Sorry. I meant weaker than PA without induction.
My axioms define a new set, N.
Let F be the domain of functions.
Wouldn't my axioms be equivalent to PA-Induction
if we assume F=N?
RussellE
> RussellE <reaste...@gmail.com> writes:
> >> There is also no guarantee that x + y is in N if x and y are --
> >> you might want to remedy that.
> > No. The possibilty x+y is not in N is what I going for.
> Even when both x and y are in N ???
Yes. I want to be able to say x+y = zebra.
> Do you want 0 in N, btw?
I am still thinking about that one.
> You don't even have that, so far.
This is better than I imagined.
> What about if x in N, then s(x) in N?
Definately not.
RussellE
it has a model. I give a model for
these axioms:
Ax (x in N -> (S(x) =/= 0))
AxAy (x,y in N -> (S(x) = S(y) -> x = y))
Ax (x in N -> (x + 0 = x))
AxAy (x,y in N -> (x+S(y) = S(x+y)))
Ax (x in N -> (x * 0 = 0))
AxAy (x,y in N -> (x*S(y) = (x*y)+x) )
Let F be the domain for functions.
Let N be the set defined in the axioms.
I am going to ignore the obvious model
where N is the empty set.
I will assume 0 is a natural number.
F: {0,z}
N: {0}
S: S(0)=z, S(z)=0
+: 0+0=0, 0+z=z, z+0=z, z+z=0
*: 0*0=0, 0*z=0, z*0=0, z*z=z
These definitions satisfy the axioms.
Are these axioms consistent because
they have a model?
(Also, does the empty set count as a model?)
Rupert
The empty set is not usually considered to count as a model. It looks
as though you have provided a model for your axioms, so they are
consistent.
Marshall
I believe he considers {0} the carrier set, and so his functions
aren't closed.
Marshall
Alan Smaill
> On May 30, 1:06 pm, Frederick Williams <freddywilli...@btinternet.com>
> wrote:
>> RussellE wrote:
>
>> > Is the following theory weaker or stronger than Peano Arithmetic?
>>
>> How about "not comparable with"? By which I mean that your theorems are
>> not a subset of PAs (because PA has no N) and PA's theorems are not a
>> subset of yours (because PA has an induction schema).
>
> Sorry. I meant weaker than PA without induction.
> My axioms define a new set, N.
They mention a new set -- they do not define it --
I can't even tell if 0 in N or not.
> Let F be the domain of functions.
> Wouldn't my axioms be equivalent to PA-Induction
> if we assume F=N?
In PA we have (the analogue of) 0 in N, and that
if x,y in N, then x+y is in N. You don't.
> Russell
> - 2 many 2 count
--
Alan Smaill
Alan Smaill
> On May 30, 12:57 pm, Alan Smaill <sma...@SPAMinf.ed.ac.uk> wrote:
>> RussellE <reaste...@gmail.com> writes:
>
>> >> There is also no guarantee that x + y is in N if x and y are --
>> >> you might want to remedy that.
>
>> > No. The possibilty x+y is not in N is what I going for.
>
>> Even when both x and y are in N ???
>
> Yes. I want to be able to say x+y = zebra.
Then you're not going to be weaker than N.
>> Do you want 0 in N, btw?
>
> I am still thinking about that one.
>
>> You don't even have that, so far.
>
> This is better than I imagined.
>
>> What about if x in N, then s(x) in N?
>
> Definately not.
Then you're not consistent with PA.
>
> Russell
> - logic must be idiot proof
--
Alan Smaill
Rupert
>
> - Show quoted text -
He said that the domain of discourse was {0,z} but the extension of
the predicate N was {0}.
Frederick Williams
>
> On May 30, 1:06 pm, Frederick Williams <freddywilli...@btinternet.com>
> wrote:
> > RussellE wrote:
>
> > > Is the following theory weaker or stronger than Peano Arithmetic?
> >
> > How about "not comparable with"? By which I mean that your theorems are
> > not a subset of PAs (because PA has no N) and PA's theorems are not a
> > subset of yours (because PA has an induction schema).
>
> Sorry. I meant weaker than PA without induction.
> My axioms define a new set, N.
Really? Let's see it then, let's see
N =df ...
where ... features only symbols from the language of your axioms bar
'N'.
> Let F be the domain of functions.
What do you mean by 'the domain of functions'? Do you mean the A in
notation such as this:
f:A -> B;
or are you quantifying over functions, and you mean the domain of
quantification?
> Wouldn't my axioms be equivalent to PA-Induction
> if we assume F=N?
I'll give you another reason why your theory is not weaker than
PA-Induction: if it were each of your theorems would need to be a
theorem of PA-Induction, but
Ax (x in N -> (S(x) =/= "0"))
is not a theorem of PA-Induction because the language of PA-Induction
has no 'in'. Please don't just announce that your axioms define 'in';
because I'll reply:
Really? Let's see it then, let's see
x in y <-> ...
where ... features only symbols from the language of your axioms bar
'in'.
Frederick Williams
Yes. So your consistent theory of arithmetic is an arithmetic of just
two "things" 0 and z? Well done.
MoeBlee
It's in a different language from the language of first order PA.
First order PA does not have the symbol 'N'.
Nor does first order PA have a symbol:
"0"
Rather first order language has a symbol:
0
You continue to butcher the use/mention distinction, even in the
OPPOSITE direction that it usally butchered when it is butchered.
This has been explained to you, but you continue to ignore while you
post as an ignorant fool.
MoeBlee
MoeBlee
> I meant weaker than PA without induction.
If all you mean is the question whether PA without induction is weaker
than PA, then the answer is 'yes'.
MoeBlee
MoeBlee
> axioms:
>
> Ax (x in N -> (S(x) =/= 0))
> AxAy (x,y in N -> (S(x) = S(y) -> x = y))
> Ax (x in N -> (x + 0 = x))
> AxAy (x,y in N -> (x+S(y) = S(x+y)))
> Ax (x in N -> (x * 0 = 0))
> AxAy (x,y in N -> (x*S(y) = (x*y)+x) )
>
> Let F be the domain for functions.
For a model, the domain for the function mapped to by an n-place
function symbol is the entire set of n-tuples on the universe.
> Let N be the set defined in the axioms.
It is not clear what you mean by "the set defined by axioms".
> I am going to ignore the obvious model
> where N is the empty set.
First, give the universe for your model.
> I will assume 0 is a natural number.
There is the SYMBOL '0' and there is the natural number zero. Be clear
of the distinction. Your theory uses the SYMBOL '0'.
> F: {0,z}
Such and F is not how a model is given.
Do you mean that F is the UNIVERSE of the model?
> N: {0}
> S: S(0)=z, S(z)=0
> +: 0+0=0, 0+z=z, z+0=z, z+z=0
> *: 0*0=0, 0*z=0, z*0=0, z*z=z
Maybe this is what you mean (and, as an informality, I'll use '0' '+',
and "*' both as the symbol in the language and for the object,
function, and function, respectively, for the model) :
universe = F = {0 z}
But what is z? Are you assuming that z is some object DIFFERENT from
0? I will assume that you do mean that z is some object DIFFERENT from
0.
'N' maps to {0}
'S' maps to {<0 z> <z 0>}
'+' maps to {<<0 0> 0> <<0 z> z> <<z 0> z> <<z z> 0>}
'*' maps to {<<0 0> 0> <<0 z> 0> <<z 0> 0> <<z z> z>}
MoeBlee
MoeBlee
> you have provided a model for your axioms
His model is a model of said axioms only if 0 and z are different
objects, which he didn't specify. I suppose, though, that we are to
assume that z is some object that is not 0.
MoeBlee
RussellE
Thanks.
So, I can exhibit a model of any finite
size using modular arithmetic.
For example, I can define models
for {0,1,z}, (0,1,2,z}, {0,1,2,3,z}, etc.
What happens when I have F={0,1,2,...,z}
and N={0,1,2,...}? Is my theory still
consistent? The finite models have
finite proofs of consistency, but I
am guessing the infinite "modeL" does not.
Does having finite models make it easier
to prove my theory has infinite models?
Russell
- Integers are an illusion
RussellE
wrote:
> RussellE wrote:
> Yes. So your consistent theory of arithmetic is an arithmetic of just
> two "things" 0 and z? Well done.
I am not trying to do arithematic.
I am looking for a finite length proof
of the consistency of PA.
My theory is consistent because
it has a finite model. If my theory
can prove the consistency of PA,
then there is a finite length proof
of the consistency of PA.
I will probably need a much bigger
set than {0,z}.
Rupert
Your theory cannot prove the consistency of PA. Your theory can be
interpreted in PA, so if your theory could prove the consistency of
PA, then so could PA, and that is not the case.
If you are interested in proofs of the consistency of PA you should
look at Gentzen's proof. Gentzen's proof can be done in PRA together
with transfinite induction up to epsilon-null.
RussellE
> On Jun 1, 2:28 pm, RussellE <reaste...@gmail.com> wrote:
>
>
>
>
>
> > On May 31, 5:45 am, Frederick Williams <freddywilli...@btinternet.com>
> > wrote:
>
> > > RussellE wrote:
> > > Yes. So your consistent theory of arithmetic is an arithmetic of just
> > > two "things" 0 and z? Well done.
>
> > I am not trying to do arithematic.
> > I am looking for a finite length proof
> > of the consistency of PA.
>
> > My theory is consistent because
> > it has a finite model. If my theory
> > can prove the consistency of PA,
> > then there is a finite length proof
> > of the consistency of PA.
>
> > I will probably need a much bigger
> > set than {0,z}.
>
> > Russell
> > - 2 many 2 count
>
> Your theory cannot prove the consistency of PA. Your theory can be
> interpreted in PA, so if your theory could prove the consistency of
> PA, then so could PA, and that is not the case.
Showing PA can prove its own consistency
is pretty much the point of my theory.
> If you are interested in proofs of the consistency of PA you should
> look at Gentzen's proof. Gentzen's proof can be done in PRA together
> with transfinite induction up to epsilon-null.- Hide quoted text -
I want to use finite induction.
I think I have to use a non-standard model of PA.
Rupert
Well, I don't see any way in which you've come even close to showing
that, and I have excellent grounds for thinking that it is not
possible, because I know that if PA can prove its own consistency then
it follows that PA is inconsistent.
MoeBlee
>
> What happens when I have F={0,1,2,...,z}
> and N={0,1,2,...}? Is my theory still
> consistent?
A theory is a set of sentences closed under the entailment relation.
By definition, a theory is consistent if and only if there is no
sentence P such that both P and ~P are in the theory. We prove also
that a theory is consistent if and only there is a model (for the
language of the theory) such that every sentence of the theory is true
in that model. That is, a theory is consistent if and only if it has a
model. That a theory has many different models has does not threaten
the consistency of the theory.
> The finite models have
> finite proofs of consistency,
What does that MEAN? Models are not things we examine for consistency
or inconsistency.
> but I
> am guessing the infinite "modeL" does not.
What are you TALKING about?
> Does having finite models make it easier
> to prove my theory has infinite models?
The compactness theorem is that if a theory has models of arbitrarily
large finite cardinalities then the the theory has an infinite model.
MoeBlee
MoeBlee
> I am looking for a finite length proof
> of the consistency of PA.
A proof is finite in length by definition of "proof".
I gave a Z\{R} set theory proof of the consistency of PA in Z set
theory in a post several months ago. Or look at various textbooks for
other proofs based on Gentzen's approach.
By the way, the mere showing of a proof is trivial. Just adopt the
axiom Con(PA). So what matters is what AXIOMS (of the meta-system) and/
or RULES (for the meta-system) are used in a consistency proof.
All proofs are finite, by definition of "proof", but a FINITISTIC
proof is one that is not just finite but also uses only certain very
restricted principles (axioms and rules, if formalized). The
incompleteness theorem may be understood to guide us that there is no
finitistic proof of the consistency of PA.
> My theory is consistent because
> it has a finite model. If my theory
> can prove the consistency of PA,
> then there is a finite length proof
> of the consistency of PA.
Every proof is of finite length. And of course there are all kinds of
proofs of the consistency of PA. But there is no FINITISTIC proof of
the consistency of PA.
MoeBlee
MoeBlee
> Showing PA can prove its own consistency
> is pretty much the point of my theory.
Your theory shows no such thing.
You're an ignoramus.
MoeBlee
Frederick Williams
If this is true:
> So, I can exhibit a model of any finite
> size using modular arithmetic.
Then there is an infinite model.
> Does having finite models make it easier
> to prove my theory has infinite models?
--
Frederick Williams
> I am looking for a finite length proof
Good. They're certainly the best kinds of proof.
> of the consistency of PA.
>
> [...] If my theory
> can prove the consistency of PA,
> then there is a finite length proof
> of the consistency of PA.
Such proofs already exist.
Rotwang
> On May 31, 11:28 pm, RussellE<reaste...@gmail.com> wrote:
>
>> I am looking for a finite length proof
>> of the consistency of PA.
>
> A proof is finite in length by definition of "proof".
At the risk of further confusing Russell, there do exist such things as
infinite proofs in infinitary logic, don't there? See e.g.
http://en.wikipedia.org/wiki/Infinitary_logic
If we have an inference rule whose set of premises is infinite then we
also need to allow proofs indexed by infinite ordinals for that rule to
be applicable.
MoeBlee
> there do exist such things as
> infinite proofs in infinitary logic
There can be lots of things, but the context here is ordinary first
order logic and/or ordinary mathematical (including meta-mathematical)
proof.
MoeBlee
RussellE
> On May 31, 11:28 pm, RussellE <reaste...@gmail.com> wrote:
> All proofs are finite, by definition of "proof", but a FINITISTIC
> proof is one that is not just finite but also uses only certain very
> restricted principles (axioms and rules, if formalized). The
> incompleteness theorem may be understood to guide us that there is no
> finitistic proof of the consistency of PA.
Thank you. I should have said I am looking
for a finitistic proof of the consistency of PA.
Doesn't the incompleteness theorem say if
there is a finistic "proof" of Con(PA) then PA
is inconsistent?
Am I correct in assuming any theory
with a finite model has a finitistic
proof of consistency?
Nam Nguyen
> On May 31, 11:28 pm, RussellE<reaste...@gmail.com> wrote:
>
>> I am looking for a finite length proof
>> of the consistency of PA.
>
> A proof is finite in length by definition of "proof".
>
> I gave a Z\{R} set theory proof of the consistency of PA in Z set
> theory in a post several months ago. Or look at various textbooks for
> other proofs based on Gentzen's approach.
>
> By the way, the mere showing of a proof is trivial. Just adopt the
> axiom Con(PA). So what matters is what AXIOMS (of the meta-system) and/
> or RULES (for the meta-system) are used in a consistency proof.
>
> All proofs are finite, by definition of "proof", but a FINITISTIC
> proof is one that is not just finite but also uses only certain very
> restricted principles (axioms and rules, if formalized).
This is my first time seeing your clarification by what it means
by "FINITISTIC", which is good because I thought it'd mean just
"finite" of 1st order syntactical proofs.
By what you said then a "finitistic" proof is not a 1st order proof,
because it must use some "principles". Right?
> The
> incompleteness theorem may be understood to guide us that there is no
> finitistic proof of the consistency of PA.
>
>> My theory is consistent because
>> it has a finite model. If my theory
>> can prove the consistency of PA,
>> then there is a finite length proof
>> of the consistency of PA.
>
> Every proof is of finite length. And of course there are all kinds of
> proofs of the consistency of PA.
Yes. CON(PA) is proven in an inconsistent theory.
So much for the fact that there's a proof of "the consistency
of PA".
Read: to the extend that there's no _finite_ 1st order proof
of a consistency, because rules of inference would yield no
non-theorem, no formula would _literally_ mean the consistency
of any formal theory!
> But there is no FINITISTIC proof of the consistency of PA.
More to the point there's no finite proof of the _possible_
consistency of PA!
--
----------------------------------------------------
There is no remainder in the mathematics of infinity.
NYOGEN SENZAKI
----------------------------------------------------
RussellE
wrote:
> RussellE wrote:
> > So, I can exhibit a model of any finite
> > size using modular arithmetic.
> Then there is an infinite model.
Thanks.
Does the Compactness Theorem
have a finitistic proof?
http://en.wikipedia.org/wiki/Compactness_theorem
What would an infinite model of
my axioms look like?
For example, can I define a model of
my axioms using:
F: {0,1,2,...,z)
N: {0,1,2,...}
Would the existence of a model
of my axioms where N is the
standard set of natural numbers
prove the consistency of PA?
RussellE
Does any theory with a finite
number of axioms and a finite
model have a finitistic proof
of consistency?
Russell
- Never never means never in set theory
Rupert
> On Jun 1, 8:57 am, Frederick Williams <freddywilli...@btinternet.com>
> wrote:
>
> > RussellE wrote:
> > > So, I can exhibit a model of any finite
> > > size using modular arithmetic.
> > Then there is an infinite model.
>
> Thanks.
> Does the Compactness Theorem
> have a finitistic proof?http://en.wikipedia.org/wiki/Compactness_theorem
>
No, but almost. It has a proof in a theory called WKL_0.
> What would an infinite model of
> my axioms look like?
>
I think the natural numbers are a model, aren't they?
> For example, can I define a model of
> my axioms using:
>
> F: {0,1,2,...,z)
> N: {0,1,2,...}
>
> Would the existence of a model
> of my axioms where N is the
> standard set of natural numbers
> prove the consistency of PA?
>
No, you would need to exhibit a model of PA to do that. To do model
theory of PA you of course need to work in a theory stronger than PA.
MoeBlee
> Doesn't the incompleteness theorem say if
> there is a finistic "proof" of Con(PA) then PA
> is inconsistent?
By the second incompleteness theorem, if PA is consistent, then there
is not a finitistic proof of the consistency of PA.
And, since finitistic reasoning does not give false results, if PA is
not consistent, then there is not a finitistic proof of the
consistency of PA.
So there is not a finitistic proof of the consistency of PA.
Meanwhile, by other reasoning, we proof the consistency of PA. And, by
ordinary mathematical observation, we see that PA is consistent since,
by ordinary mathematical observation, we see that all the axioms of PA
are true of the natural numbers.
In sum:
(1) PA is consistent.
(2) PA proves "If PA is consistent, then there is not a proof in PA
that PA is consistent".
(3) There is not a finitistic proof that PA is consistent.
> Am I correct in assuming any theory
> with a finite model has a finitistic
> proof of consistency?
Hmm, I'm not sure, but I think (?) that might be right.
But, of course, PA does not have any finite models.
MoeBlee
Frederick Williams
> have a finitistic proof?
What do you mean by a finitistic proof? You may have said elsewhere,
sorry if I missed it.
MoeBlee
> On 01/06/2011 8:47 AM, MoeBlee wrote:
> This is my first time seeing your clarification by what it means
> by "FINITISTIC", which is good because I thought it'd mean just
> "finite" of 1st order syntactical proofs.
I don't know why you would think that.
> By what you said then a "finitistic" proof is not a 1st order proof,
> because it must use some "principles". Right?
No. First, 'finitistic' is an informal notion that one might or might
not consider to be formalized by PRA. But PRA is a first order
theory.
Of course, first order proof is done only with finite strings of
symbols. But a finitistic proof is even stricter: Not just that only
finite strings of symbols are used, but the axioms that are used
assert only about such things as finite strings (or, as finite strings
are coded by natural numbers, etc.). One may consider this to captured
by PRA.
The notion of "finitistic" here is, broadly speaking, the one Hilbert
was concerned with (not necessarily that Hilbert himself invented the
notion of "finitistic").
> > Every proof is of finite length. And of course there are all kinds of
> > proofs of the consistency of PA.
>
> Yes. CON(PA) is proven in an inconsistent theory.
>
> So much for the fact that there's a proof of "the consistency
> of PA".
And the consistency of PA is proven in certain consistent theories,
including some that are not as trivial as merely axiomatized by
"Con(PA)".
As to the epistemological value of formal proofs of consistency, I
have not made any claims. Merely I've said, that there are certain
theories (not just inconsistent ones and not just trival ones) such
that there is a proof in those theories of the consistency of PA.
Franzen gives a good discussion of the basic epistemological aspects
in his book.
> Read: to the extend that there's no _finite_ 1st order proof
> of a consistency,
No, of course there are first order theories in which the consistency
of PA is provable. And every such proof is finite. It's a finite
sequence of finite sequences of symbols. There are proofs (proofs ARE
finite) of the consistency of PA, but there is no FINITISTIC proof of
the consistency of PA.
> because rules of inference would yield no
> non-theorem, no formula would _literally_ mean the consistency
> of any formal theory!
I don't know what you mean by that.
There are first order theories in which there is a sentence that is
arithmetically true if and only if PA is consistent, and said sentence
is a theorem of the theory.
Of course, there is no proof in the MERE first order predicate
calculus of the consistency in PA. That is, yes, we must have some
first order non-logical axioms for a first order proof of the
consistency of PA.
> > But there is no FINITISTIC proof of the consistency of PA.
>
> More to the point there's no finite proof of the _possible_
> consistency of PA!
I don't know what you mean by that. Do you have some modal logic
regarding 'possibility' in mind?
Anyway, of course, a formal proof is finite, and there are formal
proofs of the consistency of PA. However there is not a FINITISTIC
proof of the consistency of PA.
MoeBlee
Nam Nguyen
> On Jun 1, 9:20 pm, Nam Nguyen<namducngu...@shaw.ca> wrote:
>> On 01/06/2011 8:47 AM, MoeBlee wrote:
>
>> This is my first time seeing your clarification by what it means
>> by "FINITISTIC", which is good because I thought it'd mean just
>> "finite" of 1st order syntactical proofs.
>
> I don't know why you would think that.
Because textbooks such as Shoenfield's doesn't use such definition,
(if I'm not mistaken), which seems to be so foreign to the
standard concept of FOL _proof_.
>> By what you said then a "finitistic" proof is not a 1st order proof,
>> because it must use some "principles". Right?
>
> No. First, 'finitistic' is an informal notion that one might or might
> not consider to be formalized by PRA. But PRA is a first order
> theory.
You've basically answered "Yes" to my question: if a 'finitistic' proof
is "an informal notion" then it's not a _formal_ "1st order proof",
which is what I asked.
>
> Of course, first order proof is done only with finite strings of
> symbols. But a finitistic proof is even stricter: Not just that only
> finite strings of symbols are used, but the axioms that are used
> assert only about such things as finite strings (or, as finite strings
> are coded by natural numbers, etc.). One may consider this to captured
> by PRA.
>
> The notion of "finitistic" here is, broadly speaking, the one Hilbert
> was concerned with (not necessarily that Hilbert himself invented the
> notion of "finitistic").
>
>>> Every proof is of finite length. And of course there are all kinds of
>>> proofs of the consistency of PA.
>>
>> Yes. CON(PA) is proven in an inconsistent theory.
>>
>> So much for the fact that there's a proof of "the consistency
>> of PA".
>
> And the consistency of PA is proven in certain consistent theories,
> including some that are not as trivial as merely axiomatized by
> "Con(PA)".
Here we go a full circle again. If, say, T |- CON(PA), can we prove
CONT(T) in T?
>
> As to the epistemological value of formal proofs of consistency, I
> have not made any claims. Merely I've said, that there are certain
> theories (not just inconsistent ones and not just trival ones) such
> that there is a proof in those theories of the consistency of PA.
>
> Franzen gives a good discussion of the basic epistemological aspects
> in his book.
>
>> Read: to the extend that there's no _finite_ 1st order proof
>> of a consistency,
>
> No, of course there are first order theories in which the consistency
> of PA is provable. And every such proof is finite.
You're mistaken, because it seems you don't understand the standard
syntactical definitions of consistency.
> It's a finite
> sequence of finite sequences of symbols. There are proofs (proofs ARE
> finite) of the consistency of PA, but there is no FINITISTIC proof of
> the consistency of PA.
>
>> because rules of inference would yield no
>> non-theorem, no formula would _literally_ mean the consistency
>> of any formal theory!
>
> I don't know what you mean by that.
There are 2 _extremely-easy-to-understand_ clauses separated by a comma
in that sentence: which one can't you comprehend?
>
> There are first order theories in which there is a sentence that is
> arithmetically true if and only if PA is consistent, and said sentence
> is a theorem of the theory.
I'm not talking anything about "true" here in this context of
syntactical definition of (in)consistency. The technical mistake
you seem to make here is somehow we can establish beyond doubt
the _possible/maybe_ consistency of PA is equivalent to some formula
being true. That's not a knowledge: that's merely an assumption!
>
> Of course, there is no proof in the MERE first order predicate
> calculus of the consistency in PA. That is, yes, we must have some
> first order non-logical axioms for a first order proof of the
> consistency of PA.
>
>>> But there is no FINITISTIC proof of the consistency of PA.
>>
>> More to the point there's no finite proof of the _possible_
>> consistency of PA!
>
> I don't know what you mean by that. Do you have some modal logic
> regarding 'possibility' in mind?
There's no need to invoke the concept of model at all here, for this.
All you need to recognize is what I said before about rules of inference
would yield no non-theorem!
>
> a formal proof is finite, and there are formal
> proofs of the consistency of PA.
Which is erroneous of course, as I've already explained right above!
MoeBlee
> On 02/06/2011 9:10 AM, MoeBlee wrote:
>
> > On Jun 1, 9:20 pm, Nam Nguyen<namducngu...@shaw.ca> wrote:
> >> On 01/06/2011 8:47 AM, MoeBlee wrote:
>
> >> This is my first time seeing your clarification by what it means
> >> by "FINITISTIC", which is good because I thought it'd mean just
> >> "finite" of 1st order syntactical proofs.
>
> > I don't know why you would think that.
>
> Because textbooks such as Shoenfield's doesn't use such definition,
> (if I'm not mistaken),
The subject is covered not so much in first textbooks in mathematical
logic but rather in books and articles that discuss such foundational
matters in a more general context. The notions of "finitistic",
"finitistic methods", "finitistic principles", finitistic proof", et.
al are widespread in the literature.
> which seems to be so foreign to the
> standard concept of FOL _proof_.
There is nothing foreign (well, okay, Hilbert was German ;-)) about
the notion of finitistic proof and it does not conflict the notion of
proof in a first order system.
> >> By what you said then a "finitistic" proof is not a 1st order proof,
> >> because it must use some "principles". Right?
>
> > No. First, 'finitistic' is an informal notion that one might or might
> > not consider to be formalized by PRA. But PRA is a first order
> > theory.
>
> You've basically answered "Yes" to my question: if a 'finitistic' proof
> is "an informal notion" then it's not a _formal_ "1st order proof",
> which is what I asked.
The notion of "finitistic" is itself an informal notion. However, a
finitistic proof ordinarily would be formalized in a first order
theory, specifically PRA.
> > Of course, first order proof is done only with finite strings of
> > symbols. But a finitistic proof is even stricter: Not just that only
> > finite strings of symbols are used, but the axioms that are used
> > assert only about such things as finite strings (or, as finite strings
> > are coded by natural numbers, etc.). One may consider this to captured
> > by PRA.
>
> > The notion of "finitistic" here is, broadly speaking, the one Hilbert
> > was concerned with (not necessarily that Hilbert himself invented the
> > notion of "finitistic").
>
> >>> Every proof is of finite length. And of course there are all kinds of
> >>> proofs of the consistency of PA.
>
> >> Yes. CON(PA) is proven in an inconsistent theory.
>
> >> So much for the fact that there's a proof of "the consistency
> >> of PA".
>
> > And the consistency of PA is proven in certain consistent theories,
> > including some that are not as trivial as merely axiomatized by
> > "Con(PA)".
>
> Here we go a full circle again. If, say, T |- CON(PA), can we prove
> CONT(T) in T?
T |- Con(PA) does not itself entail T |- Con(T).
Whether T |- Con(T) depends on what T is.
> > As to the epistemological value of formal proofs of consistency, I
> > have not made any claims. Merely I've said, that there are certain
> > theories (not just inconsistent ones and not just trival ones) such
> > that there is a proof in those theories of the consistency of PA.
>
> > Franzen gives a good discussion of the basic epistemological aspects
> > in his book.
>
> >> Read: to the extend that there's no _finite_ 1st order proof
> >> of a consistency,
>
> > No, of course there are first order theories in which the consistency
> > of PA is provable. And every such proof is finite.
>
> You're mistaken, because it seems you don't understand the standard
> syntactical definitions of consistency.
There's nothing mistaken in what I said there, and I'm using the
ordinary definition of 'consistent'.
> > It's a finite
> > sequence of finite sequences of symbols. There are proofs (proofs ARE
> > finite) of the consistency of PA, but there is no FINITISTIC proof of
> > the consistency of PA.
>
> >> because rules of inference would yield no
> >> non-theorem, no formula would _literally_ mean the consistency
> >> of any formal theory!
>
> > I don't know what you mean by that.
>
> There are 2 _extremely-easy-to-understand_ clauses separated by a comma
> in that sentence: which one can't you comprehend?
What you mean by "literally" there as opposed to the simple matter
that, given certain theories T, there do exist formulas that are
arithmetically true if and only if T is consistent.
> > There are first order theories in which there is a sentence that is
> > arithmetically true if and only if PA is consistent, and said sentence
> > is a theorem of the theory.
>
> I'm not talking anything about "true" here in this context of
> syntactical definition of (in)consistency.
When we say "P means T is consistent", we may mean there that P is
arithmetically true if and only if T is consistent.
> The technical mistake
> you seem to make here is somehow we can establish beyond doubt
> the _possible/maybe_ consistency of PA is equivalent to some formula
> being true.
I said nothing about "doubt" or "beyond doubt" there. In any case, you
can look in many a basic textbook in mathematical logic to see how a
formula is given that is arithmetically true if and only if a certain
theory T is consistent.
> That's not a knowledge: that's merely an assumption!
No, I'm not merely ASSUMING that there is such a formula. Rather, such
a formula is constructed and then it's easy enough (in context) to
prove that said formula is arithmetically true if and only if T is
consistent.
> > Of course, there is no proof in the MERE first order predicate
> > calculus of the consistency in PA. That is, yes, we must have some
> > first order non-logical axioms for a first order proof of the
> > consistency of PA.
>
> >>> But there is no FINITISTIC proof of the consistency of PA.
>
> >> More to the point there's no finite proof of the _possible_
> >> consistency of PA!
>
> > I don't know what you mean by that. Do you have some modal logic
> > regarding 'possibility' in mind?
>
> There's no need to invoke the concept of model at all here,
I didn't mention models there. I asked whether there is a modal logic
you reference for the notion of "possibility" here.
> for this.
> All you need to recognize is what I said before about rules of inference
> would yield no non-theorem!
By definition, everything derivable in a system (with its rules and
axioms) is a theorem of the system. So what?
> > a formal proof is finite, and there are formal
> > proofs of the consistency of PA.
>
> Which is erroneous of course, as I've already explained right above!
Your "explanations" show again that you don't understand a damn thing
about this subject.
You're hopeless.
MoeBlee
MoeBlee
> On Jun 2, 8:38 pm, Nam Nguyen <namducngu...@shaw.ca> wrote:
> > if a 'finitistic' proof
> > is "an informal notion" then it's not a _formal_ "1st order proof",
> The notion of "finitistic" is itself an informal notion. However, a
> finitistic proof ordinarily would be formalized in a first order
> theory, specifically PRA.
See, for example: www.mv.helsinki.fi/home/praatika/Godel.DOC
"Hilbert made two fundamental distinctions. First, he distinguished
between unproblematic and contentful finitistic mathematics and
contentless infinistic mathematics. It is now usual to assume that
finitistic mathematics is essentially captured by Primitive Recursive
Arithmetic PRA."
MoeBlee
RussellE
> On Jun 2, 1:08 pm, RussellE <reaste...@gmail.com> wrote:
> > Thanks.
> > Does the Compactness Theorem
> > have a finitistic proof?http://en.wikipedia.org/wiki/Compactness_theorem
>
> No, but almost. It has a proof in a theory called WKL_0.
>
> > What would an infinite model of
> > my axioms look like?
>
> I think the natural numbers are a model, aren't they?
I am not sure. I am actually looking for a finite model.
My axioms restrict the axioms of PA to a
set I call N. I am trying to figure out what
my axioms can prove about PA.
A non-standard model of PA has a
non-standard natural number.
Let's call it e. My axioms would
have a finite (in the non-standard model)
model of size e:
F: {0,1,2,...,e}
N: {0,1,2,...}
N will have some non-standard
natural numbers as well as all
of the standard natural numbers.
Would this prove the consistency
of PA for the standard natural numbers?
Rupert
> On Jun 2, 12:18 am, Rupert <rupertmccal...@yahoo.com> wrote:
>
> > On Jun 2, 1:08 pm, RussellE <reaste...@gmail.com> wrote:
> > > Thanks.
> > > Does the Compactness Theorem
> > > have a finitistic proof?http://en.wikipedia.org/wiki/Compactness_theorem
>
>
> > > What would an infinite model of
> > > my axioms look like?
>
> > I think the natural numbers are a model, aren't they?
>
> I am not sure. I am actually looking for a finite model.
>
> My axioms restrict the axioms of PA to a
> set I call N. I am trying to figure out what
> my axioms can prove about PA.
>
> A non-standard model of PA has a
> non-standard natural number.
> Let's call it e. My axioms would
> have a finite (in the non-standard model)
> model of size e:
>
> F: {0,1,2,...,e}
> N: {0,1,2,...}
>
No. Your domain of discourse has to be closed under addition and
multiplication.
> N will have some non-standard
> natural numbers as well as all
> of the standard natural numbers.
>
> Would this prove the consistency
> of PA for the standard natural numbers?
>
You're already assuming the consistency of PA when you assume that a
nonstandard model of PA exists. You need to work out in which
metatheory you want to try to prove the consistency of PA.
Frederick Williams
> A non-standard model of PA has a
> non-standard natural number.
> Let's call it e.
e is greater than any standard natural number, so -
> My axioms would
> have a finite (in the non-standard model)
> model of size e:
>
> F: {0,1,2,...,e}
- what do those three dots mean?
RussellE
wrote:
> RussellE wrote:
> > A non-standard model of PA has a
> > non-standard natural number.
> > Let's call it e.
>
> e is greater than any standard natural number, so -
>
> > My axioms would
> > have a finite (in the non-standard model)
> > model of size e:
>
> > F: {0,1,2,...,e}
>
> - what do those three dots mean?
It means all the natural numbers
less than e (in this model).
This is all of the standard natural numbers
and a lot of non-standards one.
Frederick Williams
But you wrote "My axioms would have a finite (in the non-standard model)
model of size e". F is not finite.
RussellE
wrote:
> RussellE wrote:
> > > > F: {0,1,2,...,e}
>
> > > - what do those three dots mean?
>
> > It means all the natural numbers
> > less than e (in this model).
>
> > This is all of the standard natural numbers
> > and a lot of non-standards one.
>
> But you wrote "My axioms would have a finite (in the non-standard model)
> model of size e". F is not finite.
Isn't e finite in the non-standard model?
e is a natural number in the model.
I assume e has a successor and
(probably a lot of) predecessors
between it and the "standard"
natural numbers.
Can the "standard" natural numbers
be defined in a non-standard model?
I would guess they can't be defined.
Frederick Williams
> Isn't e finite in the non-standard model?
> e is a natural number in the model.
> I assume e has a successor and
> (probably a lot of) predecessors
> between it and the "standard"
> natural numbers.
What kind of non-standard model are you interested in? The countable
ones have order type
omega + (omega* + omega) times eta
where omega is the type of the (standard) natural numbers, omega* is
omega "backwards" and eta is the type of the (standard) rational
numbers. I know very little about uncountable non-standard models.
> Can the "standard" natural numbers
> be defined in a non-standard model?
What does it mean: to define something in a model?
> I would guess they can't be defined.
--
MoeBlee
> model
Why don't you learn what a model IS? Wait, first you have to learn (in
this particular context) what a first order language is and a certain
amount of basic set theory. Why don't you do that? Wait, you already
answered that. So let's deal with that. You think it's only good if
you figure it out for yourself (which, I guess includes continually
asking other people on Internet discussion groups) and not directly
from a book. Where did this bibliophobia start with you, Russell? Did
you suffer some kind of trauma involving a book when you were a child?
Was your entire family attacked and eaten by a shelf of rabid books or
something?
MoeBlee