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

[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

[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.

[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