Search All of the Math Forum:

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

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
Re: LOGIC & MATHEMATICS
Posted: May 27, 2013 2:24 PM

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

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