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