The Math Forum

Search All of the Math Forum:

Views expressed in these public forums are not endorsed by NCTM or The Math Forum.

Math Forum » Discussions » sci.math.* » sci.math

Topic: Typed Extensional logic and PA
Replies: 0  

Advanced Search

Back to Topic List Back to Topic List

Posts: 2,665
Registered: 6/29/07
Typed Extensional logic and PA
Posted: May 21, 2013 3:54 PM
  Click to see the message monospaced in plain text Plain Text   Click to reply to this topic Reply

A typed predicate symbol is a predicate symbol labeled after its

So P_i mean the i_th order predicate.

Now typed predicates when definable must be defined after a typed
formula which is a formula in which all predicates are also typed in a
manner delineating their order.

For example the predicate Q definable after "Exist P. P(x) & ~P(y)" ,
this formula is untyped since P ranges over all kinds of predicates
whether definable after first order or second order formulas.

While the formula "Exist P1. P1(x) & ~P1(y)" is a typed second order

Now we'll maintain that Extensions of predicates are only possible if
they are definable after typed formulas or otherwise being primitive
first order predicates, i.e. only fulfilled by objects.

Typing of predicates is stipulated recursively we start with primitive
predicates having objects as their arguments, those are labeled as
typed first order predicates, then also we'll have definable typed
first order predicates those are definable after formulas in which no
quantification occurs over predicate symbols, now typed second order
predicates are those definable after formulas having quantification
over objects or typed first order predicates, etc....

Accordingly I'll propose the following:

If Pi is a typed predicate then, ePi is a term.


i=1,2,3,..., j=1,2,3,....
ePi = eQj iff (for all x. Pi(x) <-> Qj(x))

ePi is read as the "extension of Pi"

Then define 'membership' in an untyped manner as:

x E y iff Exist P. P(x) & eP=y

Notice that a binary predicate symbol E has been defined in untyped
manner to mirror "fulfillment" of predicates in the object world.

However it is nice to see that this system doesn't entail that the
predicate E can have an extension, so we are not forced to have
something like eE, because E is untyped. This is important because the
'fulfillment' of predicates is itself not a predicate, the article
"is" in Socrates is a man, and also in white is a color, is an
'assertion' and not a predicate, so "is" doesn't have an extension to
represent it. This is acceptable I think. Similarly the relation E
defined to parallel "is" in predication must not have an extension
since "is" is not a predicate.

I call the above Typed Extensional Logic "TEL". And I consider it as
"logic" since I don't see a clear 'extra-logical' concept involved. So
if PA is interpreted in TEL
then clearly PA is logical!


Point your RSS reader here for a feed of the latest messages in this topic.

[Privacy Policy] [Terms of Use]

© The Math Forum at NCTM 1994-2017. All Rights Reserved.