Search All of the Math Forum:

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

Notice: We are no longer accepting new posts, but the forums will continue to be readable.

Topic: LOGIC & MATHEMATICS
Replies: 96   Last Post: Jun 6, 2013 5:19 AM

 Messages: [ Previous | Next ]
 Zaljohar@gmail.com Posts: 2,665 Registered: 6/29/07
LOGIC & MATHEMATICS
Posted: May 26, 2013 2:52 AM

Frege wanted to reduce mathematics to Logic by extending predicates by
objects in a general manner (i.e. every predicate has an object
extending it).

symbol "e" ,denoting 'extension of' to the logical language, and
stipulate the following formation rule:

if P is a predicate symbol then eP is a term.

Then axiomatize:

eP=eQ iff (for all x. P(x) <-> Q(x)).

Now the 'membership' relation would be *defined* as:

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

This is a second order definition of course.

The base logic is second order with identity (axioms included) and e

This trial failed.

However there has been many trials to salvage it. The general frame of
all those trials is to restrict predicates eligible to have
extensions.

So the formation rule will be modified to:

If P is a\an ... predicate symbol then eP is a term.

Examples: Replace "..." in the above rule with the following:

(1) first order

(2) stratified

(3) Acyclic

By first order it is meant a predicate definable after a first order
formula.
By stratified it is meant that all symbols in the formula except the
logical connectives, quantifiers, punctuation, = and e will be labeled
with naturals in such a manner that variables linked by = receive the
same label, also any y and G in the formula y=eG will receive the same
label, while predicate symbols will be labeled one step higher than
their arguments, so if x is labeled with i, then P in P(x) must be
labeled with i+1. Of course all occurrence of the same symbol are
labeled by the same label.

Accordingly the formula defining E above is not stratified.

Acyclic means that an acyclic polygraph can be defined on the formula
such that each symbol (other than =,e,quantifier and the connectives
and punctuation) is represented by one node and an edge will be
stretched between any two nodes for each atomic formula having the
symbols they stand for as arguments of.

/

Now it is clear that all the above qualifications are strictly
syntactical and that they are connected to the issue of consistency of
second order logic itself, so they are mere logical issues, they are
not motivated by any so to say 'mathematical' concept per se.

Now I'm not sure of the strength of those approaches, but if they
prove to interpret PA, then we can say that a substantial bulk of
ordinary mathematics would be in some sense logical, since it would be
interpreted in a basically logical theory since making modifications
to ensure consistency of a fragment of second order logic is itself a
pure logical issue.

Another trial along the same general lines is the following, but I'm
not sure of it yet though.

We resort to typing predicates according to how they are defined, the
idea is to have a sort of recursive definitional typing.

object symbols shall be denoted by lower case.
predicate symbols shall be denoted in upper case
typed predicates shall be denoted by indexed predicate symbols.
starred predicate symbols represent Constant predicates
non starred predicate symbols represent Variables ranging over
Constant predicates of the same index.

for example: P1 is a variable symbol ranging over all Constant
predicates indexed with 1, so it ranges over Q1*, P1*, R1*,...., so it
can only be substituted by those.

While P1* range over ONE predicate only.

All first order logic formulas have all predicate symbols in them
being constant predicate symbols. And here they receive the index 1.
The only exception is = predicate which would be left untyped (thus it
range over all OBJECTS).

Formation rules of typed formulas:

Rule 1. All first order logic formulas if we index all predicates
(except =) in them with 1 and star them then they are typed formulas.

Example: for all x. P1*(x) -> x=eP1*

Rule 2. Un-starring predicate symbols in a typed formula results in a
typed formula.

Example: for all x. P1(x) -> x=eP1

is a typed formula.

Rule 3. quantifying over variable predicates of a typed formula
results in a typed formula

so "Exist P1. for all x. P1(x) -> x=eP1" is a typed formula.

Rule 4. If a formula F is a definitional formula of predicate Q after
a typed formula Gn (G has the highest index of a predicate in it being
n), and if all of those highest indexed predicates were constant
predicates and if Q received the same index n, then F is a typed
formula.

In general F is a definitional formula of predicate Q after typed
formula Gn means F is a formula of the form "For all x. Q(x) iff
Gn(x)".

Rule 5. For the same conditions in Rule 4, if any of the highest
indexed predicates in Gn is a variable symbol, then Q must receive
index n+1 in order for F to be a typed formula.

Examples:

For all x. Qi+1(x) iff ~ Exist Pi. Pi(ePi) & x=ePi

For all x. Qi(x) iff Pi*(x) & ~Gi*(x)

are typed formulas.

Rule 6: a typed predicate symbol (any predicate symbol in a typed
formula) only range over predicates that hold of OBJECTS only.

Rule 7: if a formula is a typed formula, then ALL of its sub-formulas
are typed!

Rule 8: if Pi,Qj are typed formulas, then Pi|Qj is a typed formula.

where "|" is the Seffer stroke.

Rule 9: all propositional logic equivalents of any typed formula is a
typed formula.

So for example: " for all x. ~ [Qi+1(x) xor (~Exist Pi. Pi(ePi) &
x=ePi)]" is a typed formula.

Now the above process will recursively form typed formulas, and typed
predicates.

As if we are playing MUSIC with formulas.

Now we stipulate the extensional formation rule:

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

The idea behind extensions is to code formulas into objects and thus
reduce the predicate hierarchy into an almost dichotomous one, that of
objects and predicates holding of objects, thus enabling Rule 6.

What makes matters enjoying is that the above is a purely logically
motivated theory, I don't see any clear mathematical concepts involved
here, we are simply forming formulas in a stepwise manner and even the
extensional motivation is to ease handling of those formulas. A purely
logical talk.

The surprise is that Second order arithmetic is interpretable in the
above LOGICAL system.

Thus highly motivating Logicism!

So mathematics is formed in the womb of logic.

Frege was not far after all.

Date Subject Author
5/26/13 Zaljohar@gmail.com
5/26/13 namducnguyen
5/26/13 Zaljohar@gmail.com
5/26/13 namducnguyen
5/26/13 Peter Percival
5/26/13 namducnguyen
5/26/13 Peter Percival
5/26/13 namducnguyen
5/26/13 Zaljohar@gmail.com
5/28/13 Charlie-Boo
5/28/13 Charlie-Boo
5/26/13 Zaljohar@gmail.com
5/27/13 zuhair
5/27/13 fom
5/27/13 Zaljohar@gmail.com
5/27/13 fom
5/28/13 namducnguyen
5/28/13 Zaljohar@gmail.com
5/28/13 namducnguyen
5/29/13 Peter Percival
5/30/13 namducnguyen
5/30/13 Peter Percival
5/30/13 Peter Percival
5/30/13 namducnguyen
5/31/13 Peter Percival
5/30/13 Bill Taylor
5/30/13 Peter Percival
5/30/13 Zaljohar@gmail.com
5/30/13 Zaljohar@gmail.com
5/30/13 namducnguyen
5/31/13 Peter Percival
5/31/13 Zaljohar@gmail.com
5/31/13 LudovicoVan
5/31/13 fom
5/28/13 Peter Percival
5/28/13 namducnguyen
5/27/13 Charlie-Boo
5/27/13 fom
5/28/13 Charlie-Boo
5/28/13 fom
6/4/13 Charlie-Boo
6/4/13 fom
6/5/13 Zaljohar@gmail.com
5/28/13 Zaljohar@gmail.com
5/28/13 LudovicoVan
5/28/13 ross.finlayson@gmail.com
5/28/13 LudovicoVan
5/28/13 LudovicoVan
5/28/13 fom
5/29/13 LudovicoVan
5/29/13 fom
5/30/13 LudovicoVan
5/29/13 fom
5/30/13 LudovicoVan
5/30/13 fom
5/31/13 LudovicoVan
5/31/13 Zaljohar@gmail.com
5/31/13 LudovicoVan
5/31/13 ross.finlayson@gmail.com
6/1/13 LudovicoVan
6/1/13 namducnguyen
6/1/13 ross.finlayson@gmail.com
6/2/13 LudovicoVan
6/2/13 ross.finlayson@gmail.com
6/3/13 Shmuel (Seymour J.) Metz
6/3/13 ross.finlayson@gmail.com
6/4/13 LudovicoVan
6/4/13 namducnguyen
6/4/13 Peter Percival
6/5/13 Shmuel (Seymour J.) Metz
6/5/13 fom
6/6/13 Peter Percival
5/31/13 fom
6/1/13 LudovicoVan
6/1/13 fom
6/2/13 ross.finlayson@gmail.com
6/2/13 fom
6/2/13 Herman Rubin
6/2/13 fom
6/2/13 LudovicoVan
6/3/13 Herman Rubin
6/3/13 Peter Percival
6/4/13 Herman Rubin
6/4/13 Peter Percival
6/4/13 Peter Percival
6/1/13 fom
6/1/13 LudovicoVan
6/1/13 namducnguyen
6/5/13 Peter Percival
6/1/13 fom
6/2/13 LudovicoVan
6/2/13 fom
5/28/13 Zaljohar@gmail.com
5/28/13 Charlie-Boo
5/27/13 Zaljohar@gmail.com
5/28/13 Charlie-Boo
5/30/13 Zaljohar@gmail.com