If anyone responds, probably their first task would be to formulate what questions I *should* be asking, then answer them.
I have long been bothered by the existence, or rather widespread use of, axiom schema. I shall address any remarks toward the induction scheme in PA, when a specific case is needed.
I have no objection to their use, except as a matter of taste and necessity. Of course their introduction was vital to matters such as results that depend on the existence of finite axiomatizations of a theory, vs necessarily infinite ones. That a finite axiomatization in FOL can be replaced by a single axiom, is obviously a cool thing.
However, I have never been fully convinced that an axiom scheme is really a "fully infinite" axiomatization. Philosophers of math often sieze on this point when questioning the legitimacy of "checking axioms against intuition", (or something similar), claiming that it is impossible even in principle, to check out an infinite number. If one pays attention to math philosophy, they may have a point. However, my queries here are more technical. The philosophical problems of infinite schema are usually pushed aside with references to 2nd-order axiomatizations, which can typically replace a scheme with a single axiom.
However, with 2nd-order logic, come 2nd-order interpretations in train. That means models whose items are sets of individuals, rather than individuals themselves. This observation has led Quine and others to declare that 2OL is just set theory in sheep's clothing.
So I was wondering, is it possible to replace the induction scheme with a single 2nd-order-looking axiom,
AP (P0 ^ (Ax Px => P(x+1)) => Ax Px ,
but with the understanding that the only predicates P that can be referred to in this way are those that can actually be WRITTEN in the language we are using. That is, alternatively, that the predicate quantifiers range over sets of individuals, but not ALL such sets, but merely sets "definable" in the language used. This would be using something between FOL and 2OL; we might cutely term it sequi-order logic!
I suspect that it makes a considerable difference whether, in defining the domain of P this way, one allows all sentences, or just those involving individuals only, without internal quantified predicates of their own. The latter looks to be sufficient for traditional FO PA, and the former look thoroughly impredicative, and may even lead to inconsistency for all I know, and in any event would presumably allow an awful lot more to be proved.
I also doubt whether this procedure would make any difference to those meta-theorems that depend on finite axiomatizability, even though in the new system schema are snuck in as single sesqui-order axioms. Presumably there would be some philosphical gain by using them, at least in the individals-only form mentioned above.
Well, that's my vague query, or set of queries.
If anyone can make sufficient head or tail of them to tell us what is known of thse, or whether the idea has ever been seriously studied, I would be most grateful!
<w.tay...@math.canterbury.ac.nz> wrote: >This is a very vague inquiry.
>If anyone responds, probably their first task would be to formulate >what questions I *should* be asking, then answer them.
>I have long been bothered by the existence, or rather widespread >use of, axiom schema. I shall address any remarks toward >the induction scheme in PA, when a specific case is needed.
>I have no objection to their use, except as a matter of taste >and necessity. Of course their introduction was vital to >matters such as results that depend on the existence of finite >axiomatizations of a theory, vs necessarily infinite ones. >That a finite axiomatization in FOL can be replaced by >a single axiom, is obviously a cool thing.
>However, I have never been fully convinced that an axiom scheme >is really a "fully infinite" axiomatization. Philosophers of >math often sieze on this point when questioning the legitimacy >of "checking axioms against intuition", (or something similar), >claiming that it is impossible even in principle, to check out >an infinite number.
Have you got a reference where someone expresses concern about this? Concern about something like, say, the induction schema in PA?
>If one pays attention to math philosophy, >they may have a point. However, my queries here are more >technical. The philosophical problems of infinite schema are >usually pushed aside with references to 2nd-order axiomatizations, >which can typically replace a scheme with a single axiom.
Or a reference where someone who was concerned about the above was _satisfied_ with this pushing aside to second-order logic? I can't imagine how a reasonable person could be worried about the first but have no problem with the second; the second seems if anything fuzzier than the first.
>However, with 2nd-order logic, come 2nd-order interpretations >in train. That means models whose items are sets of individuals, >rather than individuals themselves. This observation has led >Quine and others to declare that 2OL is just set theory in >sheep's clothing.
>So I was wondering, is it possible to replace the induction >scheme with a single 2nd-order-looking axiom,
>AP (P0 ^ (Ax Px => P(x+1)) => Ax Px ,
>but with the understanding that the only predicates P that >can be referred to in this way are those that can actually be >WRITTEN in the language we are using. That is, alternatively, >that the predicate quantifiers range over sets of individuals, >but not ALL such sets, but merely sets "definable" in the language >used. This would be using something between FOL and 2OL; >we might cutely term it sequi-order logic!
>I suspect that it makes a considerable difference whether, >in defining the domain of P this way, one allows all sentences, >or just those involving individuals only, without internal >quantified predicates of their own. The latter looks to be >sufficient for traditional FO PA, and the former look thoroughly >impredicative, and may even lead to inconsistency for all I know, >and in any event would presumably allow an awful lot more >to be proved.
>I also doubt whether this procedure would make any difference >to those meta-theorems that depend on finite axiomatizability, >even though in the new system schema are snuck in as single >sesqui-order axioms. Presumably there would be some philosphical >gain by using them, at least in the individals-only form >mentioned above.
>Well, that's my vague query, or set of queries.
>If anyone can make sufficient head or tail of them to tell >us what is known of thse, or whether the idea has ever been >seriously studied, I would be most grateful!
>-- Wondering William
David C. Ullrich
"Understanding Godel isn't about following his formal proof. That would make a mockery of everything Godel was up to." (John Jones, "My talk about Godel to the post-grads." in sci.logic.)
>So I was wondering, is it possible to replace the induction >scheme with a single 2nd-order-looking axiom,
>AP (P0 ^ (Ax Px => P(x+1)) => Ax Px ,
>but with the understanding that the only predicates P that >can be referred to in this way are those that can actually be >WRITTEN in the language we are using. That is, alternatively, >that the predicate quantifiers range over sets of individuals, >but not ALL such sets, but merely sets "definable" in the language >used. This would be using something between FOL and 2OL; >we might cutely term it sequi-order logic!
You can certainly come up with a first-order theory of arithmetic that looks second-order in the sense that it allows variables that range over sets of naturals. But having enriched the language to allow for set variables, you are stuck between two not completely satisfying alternatives:
1. You can make the theory finitely axiomatizable, but at the cost that the set variables are only allowed to range over sets definable in the *original* language.
2. You can make set variables range over *all* formulas, but at the cost that the new theory is no longer finitely axiomatizable. Basically, you have to introduce a "comprehension schema": for each formula Phi(x), you have a corresponding axiom E P (P(x) <-> Phi(x)).
The problem is that if you introduce quantification over sets of individuals, then you can express new formulas that are not equivalent to any formula in the original language. Comprehension won't hold for these new formulas unless you add an axiom saying so.
So your question was whether you can have an axiom
AP (P0 ^ (Ax Px => P(x+1)) => Ax Px
in which the set variables range over definable sets. If you mean definable in the *original* language, then the answer is yes. If you mean definable in the *new* language (with set variables), then the answer is yes if you allow infinitely many axioms, and no if you only have finitely many axioms.
I like the second order axiom better than the schema. With the schema you can't even define the natural numbers. It is when you say for all X in the induction that you get your set of natural numbers. The schema opens a pandora box of boring non-standard models etc...At least with the second order you get you set N and this is vindicated by categoricity results and you can at least claim that in your second order model, one can refer to things, concept which is lacking with the first order...
Bill Taylor <w.tay...@math.canterbury.ac.nz> writes: > So I was wondering, is it possible to replace the induction > scheme with a single 2nd-order-looking axiom,
> AP (P0 ^ (Ax Px => P(x+1)) => Ax Px ,
> but with the understanding that the only predicates P that > can be referred to in this way are those that can actually be > WRITTEN in the language we are using. That is, alternatively, > that the predicate quantifiers range over sets of individuals, > but not ALL such sets, but merely sets "definable" in the language > used. This would be using something between FOL and 2OL; > we might cutely term it sequi-order logic!
Sure. Just allow free predicate variables, and adopt a substitution rule, allowing one to infer for any formula A in the language, from a formula containing a free predicate variable P the formula obtained by replacing P with A (renaming variables to avoid clashes as usual).
> I also doubt whether this procedure would make any difference to > those meta-theorems that depend on finite axiomatizability, even > though in the new system schema are snuck in as single sesqui-order > axioms. Presumably there would be some philosphical gain by using > them, at least in the individals-only form mentioned above.
There is a clear philosophical gain: an axiom involving a free predicate variable formally expresses our willingness to accept the axiom for any property, in the original language, in an extended language we recognise as meaningful etc. We can also note that for example in set theory, with separation and replacement formulated using a free predicate variable, we obtain a free variable formulation of the transfinite recursion theorem, but not of the reflection schema, highlighting the fact that in the proof of the former we do not in fact rely on the syntactic structure of the formulas defining the relevant properties while in that of the latter we essentially do.
Especial thanks to Aatu for his very helpful and very (as always) clear accounting of the situation.
Aatu Koskensilta <aatu.koskensi...@uta.fi> wrote: >> So I was wondering, is it possible to replace the induction >> scheme with a single 2nd-order-looking axiom,
>> AP (P0 ^ (Ax Px => P(x+1)) => Ax Px ,
>> but with the understanding that the only predicates P that >> can be referred to in this way are those that can actually be >> WRITTEN in the language we are using. > Sure. Just allow free predicate variables,and adopt a substitution > rule, allowing one to infer for any formula A in the language, > from a formula containing a free predicate variable P the formula > obtained by replacing P with A [renaming to avoid clashes]
Exactly so! I thought a new substitution inference-rule would be the simplest way to do it. Thanks for the confirmation.
>> Presumably there would be some philosphical gain by using them, > There is a clear philosophical gain: an axiom involving a free > predicate variable formally expresses our willingness to accept > the axiom for any property,
Oh thank you! These have for long been my thoughts on the matter. All this talk I've seen about "not being able to check every instance of an infinite schema" have been hot air and nonsense then, as I've always considered.
> We can also note that for example in set theory, with separation > and replacement formulated using a free predicate variable, > we obtain a free variable formulation of the transfinite > recursion theorem, but not of the reflection schema, > highlighting the fact that in the proof of the former > we do not in fact rely on the syntactic structure of > the formulas defining the relevant properties while > in that of the latter we essentially do.
I don't really follow this point though, Aatu.
Is there a single largely-agreed "reflection schema" here? How does it go? Can you elaborate further please on how it differs from separation and replacement in this regard?
Bill Taylor <w.tay...@math.canterbury.ac.nz> writes: > Is there a single largely-agreed "reflection schema" here? How does > it go? Can you elaborate further please on how it differs from > separation and replacement in this regard?
The reflection schema for the language of ZFC is
for all x1, ..., xn there is an alpha s.t. x1, ..., xn in V_alpha and Phi[V_alpha](x1, ..., xn) iff Phi(x1, ..., xn)
where Phi[V_alpha] is the formula obtained from Phi by relativizing all quantifiers to V_alpha. Given replacement, all instances of the schema are provable in ZFC. The proof, for a formula Phi, basically consists of taking the closure of a V_beta containing the given x1, ..., xn under the Skolem functions for subformulas of Phi. Notice that the structure of the proof of an instance depends, in an essential way, on the syntactic structure of Phi.
The transfinite recursion schema, on the other hand, has the following form:
if Phi(x,y,z) defines a function G: V --> V, then Psi(Phi,x,y,z) defines a function F : On --> V such that F(alpha) = G({F(beta) | beta < alpha}).
In the proof of any instance we do not rely on the syntactic structure of Phi at all -- all we use is that it is functional. Using free predicate variables we can express the theorem as a single sentence, and we obtain a proof of this sentence simply by replacing Phi in the proof of any instance with the free predicate variable. The proof is, so to speak, uniform. And indeed, given that we accept replacement for any property we should be equally willing to accept transfinite recursion for any determinate functional relation between sets. Not so for reflection.
There is a theorem, that reflection and replacement are equivalent, that is, given all instances of reflection we can prove all instances of replacement and vice verse. However, this does not hold if we use free predicate variables. This reflects the fact that while we expect replacement to hold for any determinate meaningful property of sets, expressible in whatever language we find meaningful, the same does not hold for reflection -- or, at least, does not follow from what we might be take to be immediately evident on basis of our grasp of the iterative notion of set: Conceptually reflection is much stronger than replacement, and for some extensions of the language of set theory implies the existence of large cardinals (and for some is inconsistent). This is an observation we can make in context of NBG, or the free predicate variable formulation of ZFC, but which is obscured if we consider the usual axiomatisation of ZFC.
As to the justification of schemata such as we find in PA, ZFC and so on, I've written a bit about in my blog. You will also find an informative discussion in Torkel's _Inexhaustibility_.
|
