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 ]
 Charlie-Boo Posts: 1,635 Registered: 2/27/06
Re: LOGIC & MATHEMATICS
Posted: May 28, 2013 3:24 PM

On May 27, 2:24 pm, Zuhair <zaljo...@gmail.com> wrote:
> On May 26, 9:52 am, Zuhair <zaljo...@gmail.com> wrote:
>
>
>
>
>
>
>
>
>

> > 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.
>
> A posting to FOM about that subject:
>
> http://www.cs.nyu.edu/pipermail/fom/2013-May/017305.html

I'm not asking about what you propose to be called an instance of
reducing mathematics to logic. I am asking what the definition is in
general of what constitutes a reduction of mathematics to logic? Or
even a single branch of mathematics for a very small starting point?

If someone says to define what a base of computing is, I can't say
"Turing Machines" or "the C programming language". Those are instance
of bases of computing. In general, a base of computing must be an
enumeration of (representations of) the r.e. sets, and I can show how
each of these is just that.

What constitutes a reduction of mathematics to logic? Or some branch
of mathematics e.g. geometry or number theory?

C-B

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