The old Google Groups will be going away soon, but your browser is incompatible with the new version.
Message from discussion Quantifier free sets

From:
To:
Cc:
Followup To:
Subject:
 Validation: For verification purposes please type the characters you see in the picture below or the numbers you hear by clicking the accessibility icon.

More options Sep 25 2012, 7:57 am
Newsgroups: sci.logic, sci.math
From: Zuhair <zaljo...@gmail.com>
Date: Tue, 25 Sep 2012 04:57:24 -0700 (PDT)
Local: Tues, Sep 25 2012 7:57 am
Subject: Quantifier free sets
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.

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