Quantifier free sets

[Zuhair]

I want to construct sets in a manner that is quantifier free.
The customary way of defining a set x after a predicate phi is as: For
all y. y e x <-> phi(y), where x do not occur free in phi(y).This has
the universal quantifier in it; in addition if we add Exist x before
the above formula then this statement also involves quantification. I
want to add sets to PRA to describe properties and relations between
naturals without being involved in any kind of quantification.

This can be done I assume in the following manner:

Add the symbol {} to the language of PRA that encloses only predicate
symbols, we stipulate:

if phi is a predicate symbol, then {phi} is a term.

Add membership symbol e.

Now we add the following axiom schemes to those of PRA:

Comprehension) let n=1,2,3,...;
if phi is a predicate symbol, and if phi(y) is a formula in which the
only variable symbol occurring free is y,and if {phi} do not occur
free in phi(y), then:

[(phi(y) -> y=x1 or...or y=xn) & (phi(y) -> natural(y))]
->
y e {phi} <-> phi(y)

is an axiom.

Extensionality) if phi, pi are predicate symbols, then:
[for all x. phi(x) <-> pi(x)] -> {phi}={pi}
is an axiom.

/

In this way we can add sets to PRA that of course needs no quantifiers
for their definition at all.

What the strength of "PRA + quantifier free sets of naturals" would
be?

Zuhair

[MoeBlee]

On Sep 25, 6:57 am, Zuhair <zaljo...@gmail.com> wrote:

> if {phi} do not occur
> free in phi(y),

What does "occur free" mean for '{phi}'? What is a bound occurrence of
{phi} as opposed to a free occurence?

natural(y)

What is your PRA definition of 'natural"?

MoeBlee

[Zuhair]

No definition, natural is a primitive one place predicate to be added
to the list of primitives of PRA, and all known axioms of PRA must be
relativised to naturals, and to this we add the above axioms

Zuhair

[Zuhair]

On Sep 25, 8:53 pm, MoeBlee <modem...@gmail.com> wrote:

> On Sep 25, 6:57 am, Zuhair <zaljo...@gmail.com> wrote:
>
> > if {phi} do not occur
> > free in phi(y),
>
> What does "occur free" mean for '{phi}'? What is a bound occurrence of
> {phi} as opposed to a free occurence?
>

Yes, you are right here, actually all variables are free in a
quantifier free context, but what I wanted to say is that y is the
only variable symbol that occurs in phi(y), and {phi} do not occur in
phi(y).

[Dan Christensen]

On Sep 25, 7:57 am, Zuhair <zaljo...@gmail.com> wrote:
> I want to construct sets in a manner that is quantifier free.

What is your motivation? What's wrong with quantifiers? They are easy
to use and make perfect sense to me.

Aren't you just introducing an alternate notation to express Ax P(x)
and Ex P(x)? Or are you somehow restricting FOL? Or are you
introducing new possibilities?

Dan
Download my DC Proof 2.0 software at http://www.dcproof.com

[Zuhair]

On Sep 26, 4:37 pm, Dan Christensen <Dan_Christen...@sympatico.ca>
wrote:

Yes the language of this theory is a restriction of FOL, it is
quantifier free FOL. I wanted sets to be defined in this language. My
motivation is that this can be done easily in the finite realm so I
wanted to formalize this. So we add the membership symbol to PRA and
the { } symbol of course to the language of PRA as I stated. and Then
define sets following the comprehension axiom.

Zuhair

[Dan Christensen]

On Sep 26, 11:08 am, Zuhair <zaljo...@gmail.com> wrote:
> On Sep 26, 4:37 pm, Dan Christensen <Dan_Christen...@sympatico.ca>
> wrote:
>
> > On Sep 25, 7:57 am, Zuhair <zaljo...@gmail.com> wrote:
>
> > > I want to construct sets in a manner that is quantifier free.
>
> > What is your motivation? What's wrong with quantifiers? They are easy
> > to use and make perfect sense to me.
>
> > Aren't you just introducing an alternate notation to express Ax P(x)
> > and Ex P(x)? Or are you somehow restricting FOL? Or are you
> > introducing new possibilities?
>

> Yes the language of this theory is a restriction of FOL, it is
> quantifier free FOL. I wanted sets to be defined in this language. My
> motivation is that this can be done easily in the finite realm so I
> wanted to formalize this.

Again, what do you see as the problem with the usual quantifiers?

[Zuhair]

On Sep 26, 9:23 pm, Dan Christensen <Dan_Christen...@sympatico.ca>

Ideal symbols

[Frederick Williams]

Isn't it more a case of Zuhair seeing something positive in PRA, viz
that it is thought to capture finitistic reasoning and is therefore
"safe"?

--
Where are the songs of Summer?--With the sun,
Oping the dusky eyelids of the south,
Till shade and silence waken up as one,
And morning sings with a warm odorous mouth.

[Zuhair]

On Sep 26, 10:59 pm, Frederick Williams

lets say: safest!

Zuhair

[zuhair]

On Sep 25, 2:57 pm, Zuhair <zaljo...@gmail.com> wrote:
> I want to constructsetsin a manner that isquantifierfree.

> The customary way of defining a set x after a predicate phi is as: For
> all y. y e x <-> phi(y), where x do not occurfreein phi(y).This has

> the universalquantifierin it; in addition if we add Exist x before

> the above formula then this statement also involves quantification. I

> want to addsetsto PRA to describe properties and relations between

> naturals without being involved in any kind of quantification.
>
> This can be done I assume in the following manner:
>
> Add the symbol {} to the language of PRA that encloses only predicate
> symbols, we stipulate:
>
> if phi is a predicate symbol, then {phi} is a term.
>
> Add membership symbol e.
>
> Now we add the following axiom schemes to those of PRA:
>
> Comprehension) let n=1,2,3,...;
> if phi is a predicate symbol, and if phi(y) is a formula in which the

> only variable symbol occurringfreeis y,and if {phi} do not occurfreein phi(y), then:

>
> [(phi(y) -> y=x1 or...or y=xn) & (phi(y) -> natural(y))]
> ->
> y e {phi} <-> phi(y)
>
> is an axiom.
>
> Extensionality) if phi, pi are predicate symbols, then:
> [for all x. phi(x) <-> pi(x)] -> {phi}={pi}
> is an axiom.
>
> /
>

> In this way we can addsetsto PRA that of course needs no quantifiers

> for their definition at all.
>
> What the strength of "PRA +quantifierfreesetsof naturals" would
> be?
>
> Zuhair

Na, I think the above is wrongly states, we needs sets defined after
quantifier free formulas and in a quantifier free context, a simple
trial would be the following.

To the language of FOL- (=FOL - quantifiers + {|}) add the following
rule.

If phi(x,y1...yn)is a formula in which x,y1,...,yn are the sole
variables in it, then

{x|phi(x,y1...yn)} is a term.

The intended meaning for {x|phi(x,y1...yn)} is the set of all quine
atoms that satisfy phi.

Now add extra-logical symbols =,e to represent equality and
membership, and add identity axioms stated in the usual manner for
first order logic, add the following axioms:

Axiom of Singletons: y e x -> y e y

Axiom of Membership: y e y & z e y -> y=z

Comprehension axiom schema: n=1,2,3,...;if phi is a predicate symbol
and {y|phi(y)} do not occur in phi(y) then
[y e {y|phi(y)} <-> y e y & phi(y)] is an axiom.

Define 0: 0={x|~x=x}

Axiom of Extensionality: {z|(z e A & ~z e B) or (z e B & ~ z e A)} = 0
-> A=B

Axiom of Ordered pairs (characteristic property):
(a,b)=(c,d) -> a=c & b=d

Axiom of Relations: a e a & b e b -> (a,b) e (a,b)

Axiom of Numbers: x=#y -> x e x

Define:
AxB = {y |~ {a| a e A & ~ {b|b e B & y=(a,b)} = 0}=0}

Define:

F:A-bij->B

<->

{y| y e F & ~ y e AxB}=0

{a| a e A & {b| b e B, (a,b) e F} e {b|b e B, (a,b) e F}}=A

{b| b e B & {a|a e A, (a,b) e F} e {a|a e A, (a,b) e F}}=B

That was the definition of: F is a bijection from A to B.

Axiom of Equality of numbers: F:A-bij->B -> #A=#B

Inequality of numbers: F:A-bij->C & {x|x e C & ~x e B}=0 & ~B=C -> #A
< #B

#A < #B -> ~ #A=#B

Def(>): #A > #B <-> #B < #A

x=#A & y=#B & B disjoint A & z=#AUB -> x + y = z

x=#A & y=#B & z=#AxB -> x * y = z

-----------------------------------------

I didn't find a way yet to characterize exponentiation, but if we add
another membership relation E and another abstraction {||}, and
axiomatise:

y E {x||phi(x)} <-> y subset of V & phi(y)

Then exponentiation can be characterized as:

x=#A, y=#B , z=#{r|~{C|| C subset of A & r:B-surj->C}=0} ->
x ^ y = z

Possibly exponentiation and hyperexponentiation requires higher and
higher membership relations with corresponding abstractions denoting
corresponding extensions.

Zuhair

[Graham Cooper]

On Oct 9, 4:09 am, zuhair <zaljo...@yahoo.com> wrote:
>
> Axiom of Extensionality: {z|(z e A & ~z e B) or (z e B & ~ z e A)} = 0
> -> A=B
>

No not, because

~( z e B ) -> ( z e SET }

/\
||
\/

ALL(x) ALL(z) ( ~( x = z ) ^ ( x e B ) ) -> ( z e SET )

you cannot remove ALL(X) from extensionality
as you must range over all members, and using NOT()
is not a workaround.

Herc

[George Greene]

On Sep 25, 7:57 am, Zuhair <zaljo...@gmail.com> wrote:

> I want to construct sets in a manner that is quantifier free.

This is not possible. Literally, this cannot happen.
This does not happen even in contexts where it claims to be happening,
such as
http://en.wikipedia.org/wiki/Primitive_recursive_arithmetic
The first line of this wikipedia article says,
>> Primitive recursive arithmetic, or PRA,
>> is a quantifier-free formalization of the natural numbers.
>> It was first proposed by Skolem[1] as a formalization of
>> his finitist conception of the foundations of arithmetic,
>> and it is widely agreed that all reasoning of PRA is finitist.
but that's JUST FALSE -- it ISN'T quantifier-free.
It just uses substitutional first-order quantification instead of the
traditional domain-independent kind. Of these two, the one bound
to a pre-specified infinite domain (the one you and PRA are using,
substitutional
quantification) is decidedly the inferior from the perspective of
logical tractability.
Wherefore see also
http://www.umsu.de/wo/2003/204
and
http://en.wikipedia.org/wiki/Truth-value_semantics

> The customary way of defining a set x after a predicate phi is as: For
> all y. y e x <-> phi(y), where x do not occur free in phi(y).This has
> the universal quantifier in it; in addition if we add Exist x before
> the above formula then this statement also involves quantification. I
> want to add sets to PRA to describe properties and relations between
> naturals without being involved in any kind of quantification.

PRA already arguably does that. You can already define predicates on
naturals in PRA.
You can also do that in a way that eliminates logical connectives in
favor of equations,
which makes the predicates look less "predicative", but the point is,
it is inherent
in this that = is the only predicate you need.

[Zuhair]

On Oct 8, 11:42 pm, George Greene <gree...@email.unc.edu> wrote:
> On Sep 25, 7:57 am, Zuhair <zaljo...@gmail.com> wrote:
>
> > I want to construct sets in a manner that is quantifier free.
>
> This is not possible.  Literally, this cannot happen.
> This does not happen even in contexts where it claims to be happening,

> such ashttp://en.wikipedia.org/wiki/Primitive_recursive_arithmetic

> The first line of this wikipedia article says,>> Primitive recursive arithmetic, or PRA,
> >>  is a quantifier-free formalization of the natural numbers.
> >> It was first proposed by Skolem[1] as a formalization of
> >> his finitist conception of the foundations of arithmetic,
> >> and it is widely agreed that all reasoning of PRA is finitist.
>
> but that's JUST FALSE -- it ISN'T quantifier-free.
> It just uses substitutional first-order quantification instead of the
> traditional domain-independent kind.  Of these two, the one bound
> to a pre-specified infinite domain (the one you and PRA are using,
> substitutional
> quantification) is decidedly the inferior from the perspective of
> logical tractability.
> Wherefore see alsohttp://www.umsu.de/wo/2003/204

> andhttp://en.wikipedia.org/wiki/Truth-value_semantics

>
> > The customary way of defining a set x after a predicate phi is as: For
> > all y. y e x <-> phi(y), where x do not occur free in phi(y).This has
> > the universal quantifier in it; in addition if we add Exist x before
> > the above formula then this statement also involves quantification. I
> > want to add sets to PRA to describe properties and relations between
> > naturals without being involved in any kind of quantification.
>
> PRA already arguably does that.  You can already define predicates on
> naturals in PRA.
> You can also do that in a way that eliminates logical connectives in
> favor of equations,
> which makes the predicates look less "predicative", but the point is,
> it is inherent
> in this that = is the only predicate you need.

Of course there is 'quantification' but there are not 'quantifiers',
I'm speaking about a logic that has all rules of first order logic
except that it has no quantifier symbols, of course the rule of
simultaneous substitution holds as usual in traditional first order
logic. And of course quantifier free first order logic is weaker than
the full first order logic

Zuhair

[Zuhair]

No this is wrong. To explain the matters, things go in the following
way.

{z|(z e A & ~z e B) or (z e B & ~ z e A)} = 0 -> A=B

We start substituting values of A and B, now at each substitution all
occurrences of A are replaced by the same value and so is for B. for
example replace A with r, and B with s where of course r and s are
CONSTANTS, then at that replacement we'll have:

{z|(z e r & ~z e s) or (z e s & ~ z e r)} = 0 -> s=r

Remember per replacement a variable is replaced by a CONSTANT and not
a variable standing for any object or set, so s and r above as I said
are CONSTANTS.

Now to understand the antecedent you need to go to Comprehension, and
this will be

y e {z|(z e r & ~z e s) or (z e s & ~ z e r)} <-> (y e r & ~y e s) or
(y e s & ~ y e r)

This goes for all substitutions of y.

This entails that {z|(z e r & ~z e s) or (z e s & ~ z e r)} is the set
of all objects (that can be named after constants of course) that are
in only one of s or r.

Now the antecedent above is saying that when such set is empty then
r=s,

Then you go repeat the substitution of A,B by other values and so on
till all constants are exhausted.

This is equivalent to Extensionality.

Zuhair

[George Greene]

On Oct 9, 2:22 am, Zuhair <zaljo...@gmail.com> wrote:
> And of course quantifier free first order logic is weaker than
> the full first order logic

It's NOT weaker!
It's just less TRACTABLE!
Because it's STRONGER!
The consequence-relation is UNdecidable!
It's MORE complex!
The "strength" of the "logic" is about what the "logic" FACTUALLY
IMPLIES, NOT
about the degree to which soem LAME SET OF INFERENCE RULES
*approximates* the consequence relation! -- THE POINT being that THE
ACTUAL
consequence relation is no longer compact!
The point being that going to this allegedly "simpler" place is no
simplification at all. The point being that THIS IS A STEP BACKWARDS,
IS NOT ANY kind of progress, and IS NOT WORTH BOTHERING WITH, unless
you are just obsessed with the standard model. And if you want to
deal with more-complex consequence relations -- if you can stomach THE
LOSS of recursivity, compactness, and negation-completeness -- THEN
YOU MIGHT AS WELL JUST GO *AHEAD* TO *2ND*-order, NOT FALSELY claim
you are doing something "simpler" or "weaker" THAN FIRST-order PA!

[George Greene]

On Oct 9, 2:22 am, Zuhair <zaljo...@gmail.com> wrote:

> Of course there is 'quantification' but there are not 'quantifiers',

Of course there is idiocy here, but there are not necessarily idiots
here.
I trust you understand that that was intended as damnation by faint
praise.

[Graham Cooper]

But all you have done is replace

A(X) ...p(X)...

/\
||
\/

~E(X) ...~p(X) ...

where
E(X) p(X)

stands for

FIND ANY VALUE FOR
p(X)


But in doing so, you have to search ALL VALUES OF X
just to check if ~p(X).


This is called NEGATION AS FAILURE.

Computationally, ALL(X) and NONE(X) are equivalent.
(WIDTH FIRST = CHECK ALL VALUES)

I.E NOT(P(X)) or what I call NONE(P(X))

is effectively a Quantifier.

Herc

[zuhair]

> Na, I think the above is wrongly states, we needssetsdefined afterquantifierfreeformulas and in aquantifierfreecontext, a simple

> trial would be the following.
>
> To the language of FOL- (=FOL - quantifiers + {|}) add the following
> rule.
>
> If phi(x,y1...yn)is a formula in which x,y1,...,yn are the sole
> variables in it, then
>
> {x|phi(x,y1...yn)} is a term.
>
> The intended meaning for {x|phi(x,y1...yn)} is the set of all quine
> atoms that satisfy phi.
>
> Now add extra-logical symbols =,e to represent equality and
> membership, and add identity axioms stated in the usual manner for
> first order logic, add the following axioms:
>
> Axiom of Singletons: y e x -> y e y
>
> Axiom of Membership: y e y & z e y -> y=z
>
> Comprehension axiom schema: n=1,2,3,...;if phi is a predicate symbol
> and {y|phi(y)} do not occur in phi(y) then
> [y e {y|phi(y)} <-> y e y & phi(y)] is an axiom.

The main tool here is that comprehension axiom which is not written
correctly:

for n=1,2,3,...if phi(z,x1..xn)is a formula in which {y|phi(y,x1..xn)}
do not occur, and in which z,x1..xn are the sole variables occurring
in it, then

z e {y|phi(y,x1..xn)} <-> z e z & phi(z,x1..xn)

where phi(z,x1..xn) is obtained from the formula phi(y,x1..xn) by
replacing each occurrence of the variable symbol y in it by the
variable symbol z.

it would be nice if we can further restrict this schema to explicitly
define only finite sets.
/

Also a shred of an idea that occurred to me is that if it would be
possible to use special kinds of schemes in which variables can only
be substituted simultaneously across separate sentence of the
scheme,lets call it super-scheme

Super-scheme of DOMAIN:
If simultaneous substitution of x is assumed across sentences in the
below scheme, then one of those sentences is an axiom.

for n=1,2,3,.........

x= X_n.

To understand that, one could consider the whole schema as a one unit
although composed of different sentences, so if x is replaced by r for
example in sentence x=X_1 to become r=X_1, then when n=2 we must have
the same replacement of x by r to obtain r=X_2 and vice verse, and the
same goes across all values of n. and when we replace x by s for
example then this must be done simultaneously across the whole schema.
I don't know perhaps this is equivalent to some infinite quantifier
free first order language actually since what discriminate sentences
is simultaneous substitution.

This enforces X_1,X_2,... to range over the whole domain.
/

Another shred of idea, is that I'm seeing the set construction in
general is extensive, when we say for example the set of all oranges
in my hand, this formally translates to a statement that is not only
involved with the oranges in my hand but also to refute all other
objects from being members of that set, so there is virtually a scan
of the whole domain made just to grasp a simple notion of for example
two oranges in my hand, while the set itself is finite, the way it is
defined formally is potentially infinite, that is if not actually so,
and actually for the case of finite sets it looks as if the rejection
load is much more than the acceptance, which seems to be a long tale
that is not needed really. In ordinary day life we grasp finite sets,
heaps, collections, conglomerates, etc.. in a finitary way of
reasoning, and not by this exhaustive extensive manner.

Why we can't have a finite way of defining sets like saying for
example:

Construct Set X by the following Process:
Put K in X
Put L in X
.
.
.
Put J in X
STOP

This is easier procedure to define the set X, it is finite, the whole
scan of what is other than the members of the set which is what caused
the potential infinite process of defining sets traditionally, I say
the whole of that scan will be replaced by one word that is STOP,
which conveys what we want actually.

I don't know how to put this in appropriate formal context, but if one
succeeds along that line then we can deal with finite sets without
being involved in any procedure that range over the whole domain.

[Zuhair]

On Oct 8, 11:42 pm, George Greene <gree...@email.unc.edu> wrote:

> On Sep 25, 7:57 am, Zuhair <zaljo...@gmail.com> wrote:
>
> > I want to construct sets in a manner that is quantifier free.
>
> This is not possible.  Literally, this cannot happen.
> This does not happen even in contexts where it claims to be happening,

> such ashttp://en.wikipedia.org/wiki/Primitive_recursive_arithmetic

> The first line of this wikipedia article says,>> Primitive recursive arithmetic, or PRA,
> >>  is a quantifier-free formalization of the natural numbers.
> >> It was first proposed by Skolem[1] as a formalization of
> >> his finitist conception of the foundations of arithmetic,
> >> and it is widely agreed that all reasoning of PRA is finitist.
>
> but that's JUST FALSE -- it ISN'T quantifier-free.

PRA uses NO quantifier symbols at all, so it ***IS*** quantifier free,
since that what quantifier free means. Quantifier free first order
language is just a sub-language of full first order, the later is just
quantifier free first order + quantifier symbols + Inference rules
added about quantification related to quantifier symbols. There is no
doubt that quantifier free first order language is WEAKER than the
full version, this is crystal clear because the full version has all
rules of the free version plus other rules and those added rules
serves to further strengthen it over the free version. It seems that
you are simply confusing 'quantification' with having 'quantifiers'.
Again when we say quantifier free it doesn't mean 'quantification'
free, I said that many many times to you but it seems that you are
just not getting this particular point, of course there is
quantification in any subset of first order logic including the
quantifier free version, of course simultaneous substitution of
variables per sentences would serve as a mode of quantification,
that's clear, the point is that there are not Quantifier symbols, can
you just fathom that.

Of course some of the symbols I'm trying to figure out whether they
can be added to that quantifier free language like {|} etc.. these
actually results in completely another language in which we can say
that there is quantification almost equivalent to having a kind of
quantification by bounded quantifiers. Also in addition to that other
languages that I call quantifier free but that have infinitely long
sentences like infinite conjunctions\ dis-junction over labelled
constants, that is of course another story and perhaps those are
stronger than the usual FOL with only rules of formation of finite
formulas, I'm not sure really.

Again Quantifier free first order is weaker than the full version
because it is simply a sub-language of it, not only that, it is
actually 'strictly' weaker also.

Zuhair

[George Greene]

On Oct 10, 4:40 pm, Zuhair <zaljo...@gmail.com> wrote:
> PRA uses NO quantifier symbols at all, so it ***IS*** quantifier free,

You're LYING. The fact that a symbol is not typographically apparent
to the naked eye MEANS NOTHING.
That makes about as much sense as saying that if we're using
combinators,
I=SKK is "application-free" even though function-application is the
primary\
thing happening there. It makes about as much sense as saying that
it's parenthesis-free even thought that notation IS DEFINED as meaning
I=(SK)K.

Polynomials are often written
y=ax^2 + bx +c , and if what you are saying were defensible,
then THAT would be *multiplication*-free, because the only
SYMBOLS VISIBLY PRESENT are exponentiation, addition, and equality.

You're JUST WRONG.

The variables in (e.g.) PRA or any similar allegedly-quantifier-free
treatment
ARE universally quantified and the closest you can get to having what
you
want will be to admit that that the universal quantifiers involved are
a) substitutional (of terms from the language) rather than traditional
(over objects from a domain), and b) spelled with a length-0 name as
opposed to a length-1 one, AS MULTIPLICATION IS in the quadratic
example I gave, AND AS FUNCTION APPLICATION IS in the combinator
example I gave.

What this treatment is ACTUALLY free of is EXISTENTIAL quantifiers.
But the universal ones are still there, in an even MORE complicated
variant.

[George Greene]

On Oct 10, 4:40 pm, Zuhair <zaljo...@gmail.com> wrote:

>It seems that
> you are simply confusing 'quantification' with having 'quantifiers'.

It seems that you ARE LYING. And it seems that YOU are confusing
"not having quantifier symbols" with not having quantifiers.

> Again when we say

SHUT *UP* !!!

Who is *WE*?!???

There is YOU and then there is some lame-ass TRADITION OF SPEAKING
that may OR MAY NOT be defensible!

> quantifier free it doesn't mean 'quantification' free,

Except that according to the dictionary, IT DOES.
WORDS HAVE meanings INdependent of what some little
school may sloppily choose as local terminology.

> I said that many many times to you but it seems that you are
> just not getting this particular point,

It's not that I'm NOT GETTING it, it's that I DISAGREE.
AS DOES THE DICTIONARY.

> of course there is quantification in any subset of first order logic including the
> quantifier free version, of course simultaneous substitution of
> variables per sentences would serve as a mode of quantification,
> that's clear,

But what is NOT clear to you, or to the people using the jargon you
are also using, is that this "clear" fact CLEARLY means that you
CLEARLY SHOULD NOT be CALLING this "quantifier-free".

[Graham Cooper]

On Oct 11, 3:41 am, zuhair <zaljo...@yahoo.com> wrote:
>
> Why we can't have a finite way of defining sets like saying for
> example:
>
> Construct Set X by the following Process:
> Put K in X
> Put L in X
> .
> .
> .
> Put J in X
> STOP
>
> This is easier procedure to define the set X, it is finite, the whole
> scan of what is other than the members of the set which is what caused
> the potential infinite process of defining sets traditionally, I say
> the whole of that scan will be replaced by one word that is STOP,
> which conveys what we want actually.
>
> I don't know how to put this in appropriate formal context, but if one
> succeeds along that line then we can deal with finite sets without
> being involved in any procedure that range over the whole domain.
>

Try

http://pro1og.com/VTPROLOG.ZIP

run VTPROLOG.COM

and enter

@ RUSSELL.
?- selfish(X).
;

You can copy this to a text file RUSSELL.PRO

-----------RUSSELL.PRO----------

e(X,abstract) :- abstract(X).
e(X,curriculum) :- curriculum(X).
e(X,animals) :- animals(X).
e(X,selfish) :- selfish(X).
e(X,r) :- r(X).

abstract(art).
abstract(emotion).
abstract(abstract).

curriculum(teaching).
curriculum(discipline).
curriculum(curriculum).

animals(dog).
animals(cat).

e(X,selfish) :- e(X,X).

-----END RUSSELL.PRO----


This will tell you the elements of the set of all sets that contain
themselves.

Herc

[Zuhair]

On Oct 12, 10:53 pm, George Greene <gree...@email.unc.edu> wrote:
> On Oct 10, 4:40 pm, Zuhair <zaljo...@gmail.com> wrote:
>
> >It seems that
> > you are simply confusing 'quantification' with having 'quantifiers'.
>
> It seems that you ARE LYING.  And it seems that YOU are confusing
> "not having quantifier symbols" with not having quantifiers.
>

Quantifiers as customarily used in logic are by definition "symbols",
so if you don't have quantifier symbols in your language then you
don't have quantifiers. The ordinary first order logic have quantifier
symbols and rules of inference about those quantifiers. By "quantifier
free" variant it is only meant that there is no quantifier "symbols:
in that language and of course no inference rules about those symbols
since non is there.

You may disagree to the terminology that's OK, but what I'm speaking
about precisely is how term 'quantifier free' (although you call
"jargon") is customarily used, when it is said that PRA is defined in
a quantifier free version of FOL, it just means it is defined in a
version of FOL that do not possess quantifier symbols, that's all. And
yes of course there are all kinds of objections under heaven that can
be raised against this terminology like the Dictionary doesn't agree,
not commonly understood as,... and the like. All those objections are
somewhat sensible, but it doesn't really affect what is on the table
so far.

In quantifier free FOL, you don't have any symbol representing
universal quantification or existential quantification. However there
is "Quantification" of course, and this can be seen by noticing that
the variables are "ranging" over a domain! and this is a form of
subtle quantification by itself, and it is universal in a sense. But
still there is no explicit quantifier symbol to represent this subtle
kind of universal quantification, so for example you cannot use
negation in a manner as to derive existential quantification, the
absence of symbols for quantification (i.e. quantifiers) does affect
the machinery of the language, it WEAKENS it further, for instance, as
you mentioned, you cannot speak of existential quantification, unless
perhaps by some very twisted ways in some particular instances like by
using constants or functions, or (Skolem_Herbrand)ization, etc....

I hope that helps

Zuhair

[Graham Cooper]

On Oct 14, 5:17 pm, Zuhair <zaljo...@gmail.com> wrote:
>
> In quantifier free FOL, you don't have any symbol representing
> universal quantification or existential quantification. However there
> is "Quantification" of course, and this can be seen by noticing that
> the variables are "ranging" over a domain! and this is a form of
> subtle quantification by itself, and it is universal in a sense. But
> still there is no explicit quantifier symbol to represent this subtle
> kind of universal quantification, so for example you cannot use
> negation in a manner as to derive existential quantification, the
> absence of symbols for quantification (i.e. quantifiers) does affect
> the machinery of the language, it WEAKENS it further, for instance, as
> you mentioned, you cannot speak of existential quantification, unless
> perhaps by some very twisted ways in some particular instances like by
> using constants or functions, or (Skolem_Herbrand)ization, etc....
>
> I hope that helps
>
> Zuhair

Right pure PROLOG is weaker than quantified logic as a VAR is used to
find a value that EXISTS over ALL possible solutions.

SUBSET is impossible in pure PROLOG, but simply by adding
NOT(predicate(..))

then full FOL quantification is possible.

------------------------------------

> You have to use BAGOF and LIST RECURSION (for SUBSET)

[JAN]

Or negation as failure:
FOL:
forall x(male(x) <-> rower(x)

Prolog
?- \+ (male(X), \+ rower(X)), \+ (rower(Y), \+ male(Y)).

Some Prolog systems (*) even provide a shortcut:
forall(X,Y) :- \+ (X, \+ Y).
?- forall(male(X),rower(X)), forall(rower(Y), male(Y)).



Cheers!
Herc