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
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,...;
[(phi(y) -> y=x1 or...or y=xn) & (phi(y) -> natural(y))]
is an axiom.
Extensionality) if phi, pi are predicate symbols, then:
/
In this way we can add sets to PRA that of course needs no quantifiers
What the strength of "PRA + quantifier free sets of naturals" would
Zuhair
You must Sign in before you can post messages.
To post a message you must first join this group.
Please update your nickname on the subscription settings page before posting.
You do not have the permission required to post.
| ||||||||||||||