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). > > To speak about this idea in more formal terms, we'll add a monadic > 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 > added. > > 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.