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). > > > 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. > > 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?