Google Groups no longer supports new Usenet posts or subscriptions. Historical content remains viewable.
Dismiss

A logically motivated theory

14 views
Skip to first unread message

Zuhair

unread,
May 18, 2013, 11:40:05 AM5/18/13
to
In this theory Sets are nothing but object extensions of some
predicate. This theory propose that for every first order predicate
there is an object extending it defined after some extensional
relation.

This goes in the following manner:

Define: E is extensional iff for all x,y: (for all z. z E x iff z E y)
-> x=y

where E is a primitive binary relation symbol.

Now sets are defined as

x is a set iff Exist E,P: E is extensional & for all y. y E x <-> P(y)

Axioms:

[1] If E, D are primitive binary relation symbols then:

E,D are extensional -> (For all x,y: (for all z. z E x iff z D y) ->
x=y).

is an axiom.

[2] If E, D are primitive binary relation symbols; P,Q are first order
language formulas in which x do not occur free, then

E,D are extensional ->
for all x ((for all y. y E x iff Q) & (for all y. y D x iff P)) ->
(for all y. P<->Q)

is an axiom

[3] If P is first order predicate, then

Exist E,x: E is extensional & for all y. y E x iff P(y)

is an axiom.

where E range over primitive binary relations only.

/

It is possible that this might interpret PA?

The whole motivation beyond this theory is to extend any first order
predicate by objects. It is a purely logical motivation. If this does
interpret PA and no inconsistency is shown with it, then PA can in a
sense be seen as a kind of a logical theory. IF we extend [3] to allow
infinitely long formulas, then possibly second order arithmetic would
be provable? if so then it would be a kind of a logical theory also.

All of that motivates logicism.

Zuhair

fom

unread,
May 18, 2013, 1:58:15 PM5/18/13
to
On 5/18/2013 10:40 AM, Zuhair wrote:
> In this theory Sets are nothing but object extensions of some
> predicate. This theory propose that for every first order predicate
> there is an object extending it defined after some extensional
> relation.
>
> This goes in the following manner:
>
> Define: E is extensional iff for all x,y: (for all z. z E x iff z E y)
> -> x=y
>
> where E is a primitive binary relation symbol.
>

So,

<X,E>

is a model of the axiom of extensionality.

> Now sets are defined as
>
> x is a set iff Exist E,P: E is extensional & for all y. y E x <-> P(y)
>

So,

xEX <-> ...

where

... is a statement quantifying over relations and predicates.

> Axioms:
>
> [1] If E, D are primitive binary relation symbols then:
>
> E,D are extensional -> (For all x,y: (for all z. z E x iff z D y) ->
> x=y).
>
> is an axiom.
>

So, for definiteness, let

E be membership

D be initial segment

in a theory for which every limit ordinal is a model.

> [2] If E, D are primitive binary relation symbols; P,Q are first order
> language formulas in which x do not occur free, then
>
> E,D are extensional ->
> for all x ((for all y. y E x iff Q) & (for all y. y D x iff P)) ->
> (for all y. P<->Q)
>
> is an axiom
>

You are referring to relations here using
free variables.

You probably mean 'axiom schema' here.


> [3] If P is first order predicate, then
>
> Exist E,x: E is extensional & for all y. y E x iff P(y)
>
> is an axiom.
>
> where E range over primitive binary relations only.
>

You are quantifying over relations here.

You probably mean 'axiom schema' here.

> /
>
> It is possible that this might interpret PA?
>
> The whole motivation beyond this theory is to extend any first order
> predicate by objects.

Could you please clarify this remark?

> It is a purely logical motivation.

Which logic? This is stronger than first-order
because of the quantifications.

Zuhair

unread,
May 18, 2013, 3:21:58 PM5/18/13
to
On May 18, 8:58 pm, fom <fomJ...@nyms.net> wrote:
> On 5/18/2013 10:40 AM, Zuhair wrote:
>
> > In this theory Sets are nothing but object extensions of some
> > predicate. This theory propose that for every first order predicate
> > there is an object extending it defined after some extensional
> > relation.
>
> > This goes in the following manner:
>
> > Define: E is extensional iff for all x,y: (for all z. z E x iff z E y)
> > -> x=y
>
> > where E is a primitive binary relation symbol.
>
> So,
>
> <X,E>
>
> is a model of the axiom of extensionality.
>
> > Now sets are defined as
>
> > x is a set iff Exist E,P: E is extensional & for all y. y E x <-> P(y)
>
> So,
>
> xEX <-> ...
>
> where
>
> ... is a statement quantifying over relations and predicates.

No ... is a statement quantifying over objects.
>
> > Axioms:
>
> > [1] If E, D are primitive binary relation symbols then:
>
> > E,D are extensional -> (For all x,y: (for all z. z E x iff z D y) ->
> > x=y).
>
> > is an axiom.
>
> So, for definiteness, let
>
> E be membership
>
> D be initial segment
>
> in a theory for which every limit ordinal is a model.
>
> > [2] If E, D are primitive binary relation symbols; P,Q are first order
> > language formulas in which x do not occur free, then
>
> > E,D are extensional ->
> > for all x ((for all y. y E x iff Q) & (for all y. y D x iff P)) ->
> > (for all y. P<->Q)
>
> >   is an axiom
>
> You are referring to relations here using
> free variables.
>
> You probably mean 'axiom schema' here.
>
I mean the closure over all those free varaibles per each Q and P is
an axiom.
Of course [2] is a schema.
> > [3] If P is first order predicate, then
>

> > Exist E,x: E is extensional & for all y. y E x iff P(y)
>
> > is an axiom.
>
> > where E range over primitive binary relations only.
>
> You are quantifying over relations here.
>
Correct.
> You probably mean 'axiom schema' here.

Of course, an axiom for each P.
>
> > /
>
> > It is possible that this might interpret PA?
>
> > The whole motivation beyond this theory is to extend any first order
> > predicate by objects.
>
> Could you please clarify this remark?
>
Yes, for EVERY first order predicate P there will be an object X such
that there exist an extensional relation E such that for all y. y E X
iff P(y).

Now from the above axioms this X would represent an object that
*uniquely* stands for P.

> > It is a purely logical motivation.
>
> Which logic?  This is stronger than first-order
> because of the quantifications.
>

Yes, still it is logic, the main motivation is a logical one that of
having object representatives of Predicates, for example denote P* to
be the object representing predicate P, what we want is the following

P*=Q* iff P<->Q

Now this is copying a logical relation (biconditional) into equality
between objects. So we are mirroring logical stuff at the object
level.

According to this theory of course we have each object P* being
"definable" in terms of some extensional relation E. so we have the
following definition:

P*=X iff Exist E. E is extensional & for all y. y E X iff P(y)

Zuhair

fom

unread,
May 18, 2013, 3:38:49 PM5/18/13
to
On 5/18/2013 2:21 PM, Zuhair wrote:
> On May 18, 8:58 pm, fom <fomJ...@nyms.net> wrote:
>> On 5/18/2013 10:40 AM, Zuhair wrote:
>>
>>> In this theory Sets are nothing but object extensions of some
>>> predicate. This theory propose that for every first order predicate
>>> there is an object extending it defined after some extensional
>>> relation.
>>
>>> This goes in the following manner:
>>
>>> Define: E is extensional iff for all x,y: (for all z. z E x iff z E y)
>>> -> x=y
>>
>>> where E is a primitive binary relation symbol.
>>
>> So,
>>
>> <X,E>
>>
>> is a model of the axiom of extensionality.
>>
>>> Now sets are defined as
>>
>>> x is a set iff Exist E,P: E is extensional & for all y. y E x <-> P(y)
>>
>> So,
>>
>> xEX <-> ...
>>
>> where
>>
>> ... is a statement quantifying over relations and predicates.
>
> No ... is a statement quantifying over objects.
>>

How so? The formula seems to have an
existential quantifier applying to a
relation and a subformula with the
quantified 'E' as a free variable:

'E is extensional'

Using 'R' for "Relation", I read

Ax(Set(x) <-> EREP(extensional(R) /\ Ay(yRx <-> P(y))))





Zuhair

unread,
May 18, 2013, 3:43:50 PM5/18/13
to
On May 18, 8:58 pm, fom <fomJ...@nyms.net> wrote:
I'll expand on that. The motivation of this theory is to 'define'
objects that uniquely corresponds to first order logic predicates,i.e
for each first order predicates P,Q there exist objects P* and Q* such
that P*=Q* iff for all x. P(x)<->Q(x)

We want to do that for EVERY first order predicate P.

The plan is to stipulate the existence of multiple PRIMITIVE binary
extensional relations, each one of those would play the role of a set
membership relation after which object representative of predicates
are defined.

Now the first axiom ensures that no 'distinct' objects can be defined
after equivalent predicates all across the membership relations, so
although we have many membership relation but yet any objects X,Y that
are co-extensional over relations E,D (i.e. for all z. z E X iff z D
Y) are identical!
The second axiom (schema of course) ensures that no object represent
non-equivalent Predicates, and so although we do have 'multiple'
membership relations (primitive extensional relations) however from
axiom schemas 1 and 2 this would ensure that each object defined after
any of those relations would stand 'uniquely' for a single predicate.

The last axiom scheme is just a statement ensuring the existence of an
object that extends each first order predicate after some membership
relation.

Those objects uniquely corresponding for first order predicates are to
be called as: Sets.

The point is that paradoxes are eliminated because of having
'multiple' extensional relations each standing as a membership
relation.

I'm not sure if that would interpret PA, but if it does, then PA can
be said to be a PURELY logical theory!

Now if (and this is a big if) we allow infinitely long formulas to
define first order predicates (infinitary first order languages) then
second order arithmetic 'might' follow. And I think if this is the
case, then second order arithmetic is also PURELY logical!

This mean that the bulk of traditional mathematics (most of which can
be formulated within proper subsets of second order arithmetic) is
purely logical!

However I don't think that higher mathematics can have a pure logical
motivation comparable to the above, the motivation behind those can be
said to be 'structural', or 'constructive' in the ideal sense that
I've presented in my latest philosophical notes on my website and to
this Usenet.

Zuhair

Zuhair

unread,
May 18, 2013, 3:52:18 PM5/18/13
to
I meant that P must be first order. There is no General so to say
membership relation E, there are separate different membership
relations all of which are 'primitive' relations.

Of course one might contemplate something like the following:

Define(E): x E X iff Exist R Exist P( extensional(R) /\ Ay(yRX <-
>P(y) /\ P(x) )

This E relation would be something like a 'general' membership
relation, but this is not acceptable here, because it is 'defined'
membership relation and not 'primitive'. When I'm speaking about
membership relations in the axioms I'm speaking about ones represented
by 'primitive' symbols and not definable ones.

Zuhair

fom

unread,
May 18, 2013, 6:47:50 PM5/18/13
to
I will refrain from making a long posting based on
my earlier mistaken impressions.

However, your remarks here suggest that you should take
a look at Quine's "New Foundations" and the interpretation
of stratified formulas. If you have Quine's book "Set Theory
and Its Logic" available to you, a couple of hours reading the
appropriate chapters and flipping forward to the definitions
in earlier chapters should give you some sense of the matter
as he saw it.

I believe it is Thomas Forster who is making his book
available online concerning NF, if you should become more
interested in Quine's theory.


fom

unread,
May 18, 2013, 7:39:16 PM5/18/13
to
Once again, I think you should take a look at NF by Quine.

Note that NF supports Fregean number classes.

You might find the following link informative:

http://plato.stanford.edu/entries/frege-logic/#6.4

The entire summary at that page is very well written.







Zuhair

unread,
May 19, 2013, 12:19:30 AM5/19/13
to
Yes I'm familiar with NF, actually I managed to further simplify it. I
coined the Acyclicity criterion, after which we can forsake
stratification altogether. See the joint article of Bowler, Randall
Holmes and myself on that subject, you can find it on Randal Holmes
home page and also on my website. Actually see:
http://math.boisestate.edu/~holmes/acyclic_abstract_final_revision.pdf

Anyhow here I'm trying to achieve something else, that of seeing that
PA can be interpreted in a LOGICAL theory. I view all the extensional
primitive relations in this theory as logical since all what they
function is to extend predicates. If we regard the second order
quantifier as logical, then that's it the major bulk of traditional
mathematics belongs to logic. I'm not sure if we can get without the
second order quantifier.

Anyhow I'm not sure of the remarks I've presented here, I might be
well mistaken, but matters look to go along that side. I'm just
conjecturing here.

DIVIDE and CONCUR

Zuhair

fom

unread,
May 19, 2013, 7:59:41 PM5/19/13
to
What exactly do you take to be "logical"?

For example, on the Fregean view, one is interpreting
the syllogistic hierarchy as extensional. This is a
typical mathematical view. However, Leibniz interprets
the syllogistic hierarchy as intensional, and, Lesniewski's
criticisms of Frege and Russell also lead to an intensional
interpretation.

What you are referring to as "second-order" is, for me,
a directional issue (extensional=bottom-up, intensional=top-down)
with respect to priority in the syllogistic hierarchy.

One often takes such questions for granted because
our textbooks provide such little background information.
We focus our attentions according to what we are taught.

John MacFarlane has written on this demarcation issue:

http://plato.stanford.edu/entries/logical-constants/

Historically, Aristotle is "intensional". This follows
from his claim that genera are prior to species. But,
the problems arise with the issue of "substance". The
notion of "substance" is associated with individuals and
grounds the syllogistic hierarchy predicatively.

So, there is an implicit tension in foundational studies
because of "first-order"/"second-order" or
"extensional"/"intensional" dichotomies.

That is why I am asking for some clarification as to
what you take to be "logical".

Thanks.








Ross A. Finlayson

unread,
May 19, 2013, 10:41:19 PM5/19/13
to
It seems both a tautology as "coming together" and identity as "being
as one" need to be accommodated, with each as of extensionality (being
equal). For the sweep of tautology from genera combining or as one to
next, then as to the locus of identity of speciation, again the
structures define the meaning of extensionality and its use. Here the
tautology defines equality: given the structure, while identity
defines equality: given the specific in representations.

Then maybe it's a good idea that equality is achievable variously,
here somewhat inspired by Frege's basic systems as explicated in the
article fom references, and then that the methods used to so define
equality for elements of the same system may be interchangeable (self-
evident or series-evident, say) or not, along the lines of
implications of the transfer principle and assigning specific meanings
to for each/ for all / for every, and building into the universal
quantifier, or acknowledging as its construction, general support for
the contrapositive, with regards to existence and uniqueness of items,
in as to differentiating course-of-values and individuated
specification, then of course as relevant to impredicate, yet true,
features of the structure.

Then, as above, Al-Johar, that a particular object is defined by a
first-order predicate, one notion is that some n'th order predicate
(and N'th order), results in the same object, with that the first-
order predicate defines an object, for a representation, while the
n'th-order (as it were) predicate of the structure of the genera,
refers to the same individual, but it is not interchangeable the
evaluation of the predicates that so denote it without having that
acknowledged in the carriage of the structure.

What you describe is by no means irregular, and indeed that's rather
again the point that "pathological" structures like the Universe
_aren't_ regular, yet, their specification is of the most concise (eg,
for any x, x e U with quantification and containment, that a species
and genera of U applies to x with the inward view). Here then the
"outward" view as to the well-founded and constructle and the "inward"
view as of the total and continuous sees that: your system here is
much similar to Frege's: where's the system that accommodates both
representation: and context.

Then, with the goal to be a "logical" logical theory toward structures
of mathematical use: the elements of integer arithmetic have a total
structure, the context, a logical theory for all of these objects has
only logical objects in the theory, then, all the regular logical
theories start with the only absolute constant as empty instead of
all: the theory should be the same from where those are
indistinguishable.

Then, in terms of the arithmetic coding of some dually-self-
infraconsistent ur-object, for that there is a completed infinity: of
the general extension via deduction.

I'm glad to see your further developments in your theories, my
question is: what is the theory of Nothing and Everything at once? I
answer it with the "null axiom theory", a logical theory with no non-
logical axioms, "logical".

Regards,

Ross Finlayson

Zuhair

unread,
May 20, 2013, 3:37:30 PM5/20/13
to
I don't have a principled approach as regards demarcation of logic
yet. For now I'm content with saying that all fragments of first order
logic with identity (including all substitution instances by concrete
objects) are logical. I also maintain that having object extensions of
first order predicates is by itself logical since it just copies the
predicative content into the object world. A simple trial to do that
is to add a monadic symbol like "e" to the above language and
stipulate that

if G is a predicate symbol then eG is a term.

eG is read as "the extension of G".

stipulate the axiom:

eF=eG iff (for all x. F(x) <-> G(x))

To me this approach is perfectly logical.

We can use second order quantification to define a membership
relation:

x E y iff Exist G: G(x) & y=eG

where G ranges over first order predicate symbols.

In general we can define an i_th membership relation as:

x Ei y iff Exist Gi: Gi(x) & y=eGi

where Gi ranges over the i_th order predicate symbols.

So the membership relations so defined (in second order) only reflect
fulfillment of predicates after their order.

Of course to justify such an approach one must show that fulfillment
of predicates differs after their order, which indeed is hard to show.
Since it seems that "is" in "Socrates is a man", is not really
different from "is" in "Triangle is a shape". Of course "is" here is
just another word for "fulfills being", so the sentences, completely
interpreted, are: "Socrates fulfills being a man", "Triangle fulfills
being a shape". Even more completely displayed those sentence are:

The object the name "Socrates" refers to -is- a man.

The predicate the name "Triangle" refers to -is- a shape.

It appears that the article "is" in both of the above sentences has
the same meaning, that of "fulfills being". And it seems that there is
no difference in this fulfillment per se between the two sentences.
However still it can be argued that fulfillment of predicates by
predicates is a different kind of concept from fulfillment of
predicates by objects, and that this difference is the same for higher
predicates fulfillment. And this can be a strong point since using
extensions in the same manner (that of concatenating the symbol e with
the predicate symbol) doesn't elucidate the difference between an
object and a predicate and between a predicate and a higher predicate,
which are agreeably must be Mirrored by different "sorts" of
extensions, so in absence of that difference we must show it by the
membership relation. Anyhow, the above stipulation of ordered
membership does in sense MIRROR the order of predicates, so in
principle it is inert and doesn't add something that is substantially
extra-logical, so it can be considered as logical. However saying its
logical really depends on whether the second order quantifier is inert
or not.

Regards

Zuhair








fom

unread,
May 20, 2013, 7:42:04 PM5/20/13
to
On 5/20/2013 2:37 PM, Zuhair wrote:
> On May 20, 2:59 am, fom <fomJ...@nyms.net> wrote:
>> On 5/18/2013 11:19 PM, Zuhair wrote:

<snip>

>>> http://math.boisestate.edu/~holmes/acyclic_abstract_final_revision.pdf
>>

I am still considering your other response,
but, I wanted to say that I began looking at
the paper.

I have little knowledge of NF. Your idea,
however, is almost obvious. So, it is the
kind of thing that gets overlooked. I look
forward to reading more to see how it develops.

Very nice.



fom

unread,
May 20, 2013, 9:23:56 PM5/20/13
to
This is where your statement

P*=Q* iff P<->Q

gets interesting.

Frege and Russell both pursued description theories. Russellian
description theory actually does not involve reference since it
had been formulated for logical realism (mutually exclusive
truth valuation). It is a type of quantifier that is either
instantiated or not instantiated.

So, when you address the question of "concreteness", many
issues become involved.

I will not pursue this. But as you know, Quine introduced his
set theory with an analysis of how identity becomes eliminable.

This is distinct from set theory as presented in Kunen or
Jech. Both introduce the axiom of extension with a conditional
and defer to the received paradigm of first-order logic for its
converse.

With regard to descriptions -- or, more precisely, denotations --
Zermelo's original paper treated identity in terms of denotations
in relation to singletons. Later developments changed the
description of the domain.

What I find interesting about your statement is that it is
relating a first-order relation (admittedly taken as a "logical"
symbol by some authors) with a zero-order connective.

I have thought about this a great deal in my own deliberations.

> I also maintain that having object extensions of
> first order predicates is by itself logical since it just copies the
> predicative content into the object world.

A review of Feferman's work suggested by Alan Smaill in
another thread described predicativism as a "framework"
applied to "something given".

Now, in Aristotle, one finds the observation that
interpreting universal quantification as a course-of-values
defeats the intention of the quantifier. It would
seem that empiricism demands this intepretation.

I am interpreting your statement along those lines. In
other words, following Frege one "cannot really say what
an object is". So, your notion of predicativism is taking
"the world" as given. Moreover, it is taking "the world"
pluralistically -- that is, "the world" is not given in
the singular.

Thus extensions are "witnesses". That is,
the objects that satisfy the concepts reflect the
formula,

Ex(phi(x)) -> phi(c)

where c is constant naming an instantiating object.

Would this summary reflect your views?

> A simple trial to do that
> is to add a monadic symbol like "e" to the above language and
> stipulate that
>
> if G is a predicate symbol then eG is a term.
>
> eG is read as "the extension of G".
>
> stipulate the axiom:
>
> eF=eG iff (for all x. F(x) <-> G(x))
>
> To me this approach is perfectly logical.
>

This corresponds to the usual interpretation
of Frege's distinction between the concept and
its extension.

> We can use second order quantification to define a membership
> relation:
>
> x E y iff Exist G: G(x) & y=eG
>
> where G ranges over first order predicate symbols.
>
> In general we can define an i_th membership relation as:
>
> x Ei y iff Exist Gi: Gi(x) & y=eGi
>
> where Gi ranges over the i_th order predicate symbols.
>
> So the membership relations so defined (in second order) only reflect
> fulfillment of predicates after their order.
>

So, you do not use "general quantifiers". In other
words, Your predicativism is much like Russell's and
your multiplicity of extension relations corresponds
with typed quantifiers. Would that be correct?

The Lesniewskian criticism would correspond with
general quantification. Actually, it has to do with
existential import. In predicative logicism, the objects
are existentially prior to the class. For Lesniewski,
the class and its constituents are existentially
simultaneous.

But, Lesniewski did not describe it this way. He used
the extensional/intensional distinction. But, this notion
of predicativism seems more than simple extensionality
because of the typing of quantifiers.

> Of course to justify such an approach one must show that fulfillment
> of predicates differs after their order, which indeed is hard to show.
> Since it seems that "is" in "Socrates is a man", is not really
> different from "is" in "Triangle is a shape". Of course "is" here is
> just another word for "fulfills being", so the sentences, completely
> interpreted, are: "Socrates fulfills being a man", "Triangle fulfills
> being a shape". Even more completely displayed those sentence are:
>
> The object the name "Socrates" refers to -is- a man.
>
> The predicate the name "Triangle" refers to -is- a shape.
>
> It appears that the article "is" in both of the above sentences has
> the same meaning, that of "fulfills being". And it seems that there is
> no difference in this fulfillment per se between the two sentences.
> However still it can be argued that fulfillment of predicates by
> predicates is a different kind of concept from fulfillment of
> predicates by objects, and that this difference is the same for higher
> predicates fulfillment.

This is where Russellian description theory raises its
head. If singular denotation corresponds with a quantifier,
then there is no distinction between fulfillment by objects
and fulfillment by predicates. "Objects" instantiate
descriptions. Descriptions are "concrete" predications. The
hierarchy is a hierarchy of predications.

Maybe I have oversimplified this.

> And this can be a strong point since using
> extensions in the same manner (that of concatenating the symbol e with
> the predicate symbol) doesn't elucidate the difference between an
> object and a predicate and between a predicate and a higher predicate,
> which are agreeably must be Mirrored by different "sorts" of
> extensions, so in absence of that difference we must show it by the
> membership relation. Anyhow, the above stipulation of ordered
> membership does in sense MIRROR the order of predicates, so in
> principle it is inert and doesn't add something that is substantially
> extra-logical, so it can be considered as logical. However saying its
> logical really depends on whether the second order quantifier is inert
> or not.

When Brouwer criticized Hilbert's program, he described a
system of "twoness". Although he claimed to be implementing
a notion of Kant's a prioriness of time, the description is
far from Kantian. The sense of what you are describing reminds
me of Brouwer's statements (but not his motivating description).

Indeed, there is an initial "twoness". The posterior form for each
instance of "twoness" becomes the prior form for the next instance
of "twoness".

For Brouwer, this progression is that of "being" and of "coming to
be" in some Hegelian, or even Nietzchean sense. A typed hierarchy
does not reflect this temporal sense. But, its form of existential
priority is "uniform" with this same sense of "twoness". Each
pair of consecutive levels in the hierarchy has this relation. But,
the pairs overlap.

In any case, thank you for your clarifications.

You might find Russell's discussion of set existence and the axiom
of reducibility in the first edition of "Principia Mathematica" of
interest here. When set existence is presumed, the extensionality
relations are predicative. Of course, the axiom of reducibility
had been what Russell perceived as necessary for the "no-classes"
theory of the first edition. But the discussion seems vaguely
related to some of your remarks in this last paragraph. So, it
may be of interest.






Zuhair

unread,
May 21, 2013, 8:22:52 AM5/21/13
to
It must be:

x Ei+1 y iff Exist Gi: Gi(x) & y=eGi

Where Gi is a symbol ranging over i_th order predicates.

A kind of 'defined' typed membership relation after the order of
predicates.

I think this is powerful enough to interpret PA.

And I think this *is* logical.

Sets are just extensions of predicates.

However membership relation in sets must be typed after the order of
predicates they extend.

I'll see if another approach in which we have ONE membership relation
but typed extensions of predicates after their order, would be
feasible, since typing objects is simpler than typing relations.

Anyhow I need to review all of that more extensively.

Zuhair
0 new messages