alternative 1st-order quantifier semantics
George Greene
the quantifiers as being instantiated to
Terms Of The Language
as opposed to the usual/standard
Elements of The Domain ?
For some signatures, this will empty the domain completely;
if you don't have a constant in the language then you will never
get any fully closed terms to quantify over.
Even if that fate is avoided, you could still wind up with
a grave paucity of of terms; without at least one positive-arity
function-
symbol, the constants will be the ONLY terms you have.
But suppose, just for non-triviality, that we are talking about-and-
only-about
first-order languages with both at least 1 constant and at least 1
function-
symbol; then, we will always have denumerably many distinct terms to
quantify over.
I imagine that this is significantly poorer/weaker than standard
classical FOL
over arbitrary/infinite/class domains whose elements provide the
quantifier-
instances, but still, I would like to know what happens with this
variant and
if it has a name (then I could google it).
Nam Nguyen
I'm not an expert here but my reaction-of-the-first-sight would be
that it wouldn't make any difference to the "standard classical
first-order _inference_". There are 2 reasons.
The first reason is that "inference" is part of the syntactical study of
FOL, while "quantification" is the semantical counterpart. For instance,
from Ax(~(Sx=0)] we could infer ExAy[~(Sy=x)] and so from Mx(%(Sx$0)] we
could infer BxMy[%(Sy$x)], as long as the symbols M, B, %, $ would play
the same syntactical roles as A, E, ~, = respectively. All this kind
of inferenceces would be invariant to the semantics of these symbols,
whether or not A, E, M, B mean "quantifiers" or "specifiers", or what
other semantics we might consistently come up with.
The second reason is that if we stay with the usual "quantifier" semantic
for A and E, then the existences of the terms are just the existences of
the individuals of the universe where the quantification would take place.
Iow, the set of terms now is the universe U of a model. Nothing seems
to be fundamentally different, from what I could gather.
George Greene
> The second reason is that if we stay with the usual "quantifier" semantic
> for A and E, then the existences of the terms are just the existences of
> the individuals of the universe where the quantification would take place.
Right.
> Iow, the set of terms now is the universe U of a model.
Right.
> Nothing seems to be fundamentally different, from what I could gather.
But it IS different.
In my version, the terms are the ONLY relevant universe.
You could have other universes by interpreting the terms to
refer to other kinds of things, but there is simply no NEED to.
The quantifier quantify by definition ONLY over the terms, so the
terms might as well be interpreted as themselves.
The difference between this and the standard is that in this version,
EVERY element of the domain HAS a term/NAME.
There is a sense in which this avoids Godelian incompleteness
because that depends very crucially on certain elements of the
domain (in non-standard models) NOT having term-names.
In PA+~Con(PA), for example, all the godel numbers for proofs
of false statements are NOT natural numbers and therefore do NOT
have term-names under the usual signature.
The standard quantifiers quantify over the whole domain, both named
and un-named terms. Therefore both more existentially-quantified
statements and fewer universally-quantified ones will be true under
the standard semantics than will be true under this revised term-based
one.
stevend...@yahoo.com
>
>What happens to standard classical first-order inference if you define
>the quantifiers as being instantiated to Terms Of The Language
>as opposed to the usual/standard Elements of The Domain?
Does that amount to the same thing as adding a structural induction
axiom? To explain what structural induction is, let's say that
a one-place predicate (formula with one free variable) Phi(x)
is "closed" if
1. For each constant symbol c, Phi(c) holds.
2. For each natural number n, for each n-ary
function symbol f,
Phi(x_1) & Phi(x_2) & ... & Phi(x_n) -> Phi(f(x_1, x2, ..., x_n))
Then structural induction is the implication, for each
one-place predicate Phi(x):
Phi is closed -> forall x, Phi(x)
(If there are only finitely many constant symbols and function
symbols, then "Phi is closed" is expressable as a single formula).
--
Daryl McCullough
Ithaca, NY
George Greene
> Does that amount to the same thing as adding a structural induction
> axiom?
Possibly, but I would hesitate to call "this" an "axiom".
It is an infinitar inference rule! That is not even standard at all!
> To explain what structural induction is,
Come on.
We know what structural induction is and it does not even require
adding any axioms.
You can define proof by induction without adding any semantic
axioms. What is necessary is for THE THEORY to have axioms
that support induction.
> let's say that
> a one-place predicate (formula with one free variable) Phi(x)
> is "closed" if
>
> 1. For each constant symbol c, Phi(c) holds.
> 2. For each natural number n, for each n-ary function symbol f,
Well, under the standard classical first-order paradigm, that
qualification is (fortunately) redundant (i.e. unnecessary and
therefore irrelevant): it is part of the definition of the paradigm
(and of a first-order LANGUAGE) that EVERY function symbol has a
natural arity.
> Phi(x_1) & Phi(x_2) & ... & Phi(x_n) -> Phi(f(x_1, x2, ..., x_n))
It does bear stressing that YOU CAN'T EVEN *SAY* THIS *IN* first-
order logic! This is NOT *an* axiom in any context where inference
rules have to have a finite number of premises! This is infinitely
many different axioms!
> Then structural induction is the implication, for each
> one-place predicate Phi(x):
>
> Phi is closed -> forall x, Phi(x)
Well, yes, this is almost that. The point is the terms are all you
care about. But this IS NOT the same as what I am talking about
because models in which things other than the terms ARE IN
THE DOMAIN are still ALLOWED and it is still NECESSARY
that they be counted in evaluating the truth-value of the
quantifiers. More to the point, because this involves something
schematic like phi, it only works for syntactically definable
predicates.
> (If there are only finitely many constant symbols and function
> symbols, then "Phi is closed" is expressable as a single formula).
That is a loose use of "expressable". Phi in fact isn't directly
talkable ABOUT
at all. And if the terms are the only things in the language, then
this infinitary
implication holds DESPITE whether the signature is or isn't also
infinite and
despite whole bunches of other things (like whether the predicate is
or isn't
linguistically definable).
Lots of things can be proved by structural induction (if the terms in
fact
have relevant underlying structure) withOUT talking about "an axiom"
to that effect.
George Greene
> a one-place predicate (formula with one free variable) Phi(x)
> is "closed" if
>
> 1. For each constant symbol c, Phi(c) holds.
We could specialize this to standard classical 1st-order PA.
There is an axiomatization in which + and x are ternary predicates
with axioms requiring them to be functional as well as associative
(in addition to the usual axioms that define them inductively,
specifying what n+0 and nx0 are, and what n+s(y) and n*s(y) are).
In this case, 0 and s(.) are 0-ary and 1-ary functors and are
The Only functors.
> 2. For each natural number n, for each n-ary
> function symbol f,
> Phi(x_1) & Phi(x_2) & ... & Phi(x_n) -> Phi(f(x_1, x2, ..., x_n))
So this would be phi(x) -> phi(s(x)) since s is the only f (there is
no
0-ary instance of this schema except maybe phi(0) ->phi(0); or would
it be for any n, phi(n) -> phi(0) ? That would be equivalent to just
phi(0) by itself.
In other words, THIS REDUCES TO THE REGULAR STANDARD
INDUCTION AXIOM in this context. Since ALL the terms have the
structure s(s(s(....(0)....))), structural induction over this
signature is
just regular induction.
So,
NO, it is NOT what I am talking about, since it still allows non-
standard models that have objects that these terms do not denote.
This still involves an inductive implication.
I am looking for a non-inductive definition of the quantifier
that just says that Phi(0)^Phi(s(0))^Phi(s(s(0)))...^... -> An[Phi
(n)],
where every term occurs in a conjunct on the left.
David Libert
See http://en.wikipedia.org/wiki/Substitutional_quantification
One interesting point about this logic. Suppose we take the usual Peano
axioms defining + and * over S = successor. All in the usual lanuage
of PA.
Then every closed term is provably equal to some iteration of S over 0.
So the term model is isomorphic to the standard model.
So considering the entailment relation of this this, over non-logical
axioms the defining axioms in PA (other than specially induction)
this logic entails all of true arithmetic.
So this swet of consequences of these finitely many axioms is not
arithmetic.
Daryl wrote later in this thread about structural induction. Those
would be conseuences in this logic. But those axioms of structural
induction closed off by usual first order would still have r.e.
conquences.
So this logic over those Peana axioms I noted is strictly more
powerful thant conventional first order + structural induction.
--
David Libert ah...@FreeNet.Carleton.CA
Alan Smaill
> I am looking for a non-inductive definition of the quantifier
> that just says that Phi(0)^Phi(s(0))^Phi(s(s(0)))...^... -> An[Phi
> (n)],
> where every term occurs in a conjunct on the left.
Carnap's omega rule gives you this as a rule of inference,
with infinitely many premisses.
see section 3 of:
http://www.utm.edu/research/iep/c/carnap.htm
also, related article by Neil Tennant:
http://philmat.oxfordjournals.org/cgi/content/full/nkm045v1
--
Alan Smaill
George Greene
> Then every closed term is provably equal to some iteration of S over 0.
>
> So the term model is isomorphic to the standard model.
Exactly.
In "true" arithmetic we want to quantify SPECIFICALLY over all AND
ONLY
the natural numbers. Under the standard quantifier semantics, we
are alternatively, with equal validity, quantifying "in parallel"
over any and all possible domains of all models.
> So considering the entailment relation of this this, over non-logical
> axioms the defining axioms in PA (other than specially induction)
> this logic entails all of true arithmetic.
Well, in the special case of PA, yes.
I was trying to ask about such a notion of quantification in general,
but this
particular case does highlight the problem.
I was trying to say something simpler (just the terms as opposed
to "anything") and wound up with something ridiculously stronger.
> Daryl wrote later in this thread about structural induction. Those
> would be conseuences in this logic. But those axioms of structural
> induction closed off by usual first order would still have r.e.
> consequences.
So we have gone far beyond r.e. here.
So is there no "logic" (that is even halfway tractable) that would
actually
be complete for the consequences under this notion
of quantification?
> So this logic over those Peana axioms I noted is strictly more
> powerful thant conventional first order + structural induction.
OK, it's strong, but is it too strong to be of any use?
Or is it actually good for something?
Thanks so much for the reference to the wikipedia article.
I am glad to learn that this is named "truth-value semantics"
and "substitutional quantification".
Jan Burse
> What happens to standard classical first-order inference if you define
> the quantifiers as being instantiated to
> Terms Of The Language
> as opposed to the usual/standard
> Elements of The Domain ?
This is common practice. It runs under the names term model,
henkin model, herbrand model, etc..
The mathematical reason for being able to do that is the
following: Every algebra is a quotient algebra of a
free algebra.
It translates basically as follows, instead of having
objects x and y from your domain, and x=y indicates
identity of your objects, you have objects equating to
terms, and x=y is an equivalence relation and congruence
over terms. Such that:
t = s :<=> evaluated t = evaluated s
Bye
George Greene
> This is common practice. '
No, it isn't.
> It runs under the names term model,
> henkin model, herbrand model, etc..
All those are INDIVIDUAL models under THE REGULAR semantics.
I am talking about an alternative interpretation of the quantifier
that admits ONLY term models and therefore winds up with
different consequences. It is a whole different semantics
and you cannot characterize it in terms of one model that also
occurs under the standard semantics.
>
> The mathematical reason for being able to do that is the
> following: Every algebra is a quotient algebra of a
> free algebra.
> It translates basically as follows, instead of having
> objects x and y from your domain, and x=y indicates
> identity of your objects, you have objects equating to
> terms,
Well, yes, it IS, indeed, that, but I completely fail to see
how that is a TRANSLATION of anything. It's just DIFFERENT
from the other way.
> and x=y is an equivalence relation and congruence over terms.
No, it isn't. It is syntactic equality of terms.
And you don't need equality for this in any case.
Any theory rich enough to be interesting is going to be
capable of DEFINING equality in any case. Though, of
course, if it is going to define a relation and spell it = ,
it had dangwell better be an equivalence relation.
> Such that:
>
> t = s :<=> evaluated t = evaluated s
"evaluated" is not even part of this.
Jan Burse
> On Dec 15, 11:27 am, Jan Burse <janbu...@fastmail.fm> wrote:
>> This is common practice. '
>
> No, it isn't.
>
>> It runs under the names term model,
>> henkin model, herbrand model, etc..
>
> All those are INDIVIDUAL models under THE REGULAR semantics.
Yes, under the regular semantics, and you can also view
it, as you asked. It needs a little bit thinking out of
the box, to accept that something that somebody is doing
has two views.
And detour over regular semantics is even not necessary,
it should be possible to do everything full proof theoretic,
thus not invoking the notion of model at all. One spin
off of such a doing is the L�wenheim Skolem theorem.
Look see when you are able to deal with quantifiers as
ranging over terms, you have already shown the L�wenheim
Skolem theorem. How many terms are there? Skolem Paradox
also follows. One could says its part of the basic canon of
logic nowadays.
Bye
Jan Burse
> On Dec 15, 11:27 am, Jan Burse <janbu...@fastmail.fm> wrote:
>> This is common practice. '
>
> No, it isn't.
>
>> It runs under the names term model,
>> henkin model, herbrand model, etc..
>
> All those are INDIVIDUAL models under THE REGULAR semantics.
> I am talking about an alternative interpretation of the quantifier
> that admits ONLY term models and therefore winds up with
> different consequences. It is a whole different semantics
> and you cannot characterize it in terms of one model that also
> occurs under the standard semantics.
Bottom line is, if you do it right, it will not wind
up with different consequences.
Bye
Jan Burse
>> and x=y is an equivalence relation and congruence over terms.
>
> No, it isn't. It is syntactic equality of terms.
Do you say that syntactic equality is not an aequality
relation AND also not a congruence (for function symbols).
Well damn it, that is something new. I thought I can verify
the following for syntactic equality:
x = x
x = y -> y = x
x = y & y = z -> x = z
So its is an aequality relation. Further you can easily
verify that:
x1=y1 & ... & xn=yn -> f(x1,..,xn) = f(y1,..,yn)
I know its very strange to ask the above for syntactic
equality, since it is so trivial that it holds. If I
use syntactic equalvalent elements to build a compound
then this compound is also syntactically equivalent.
But this is nothing else than congruence.
Bye