An Approach of Formalizing Mathematics by Reformulations - A Proposal for QED -
Manfred Kerber · 1995
ly logical meta-level characterizations of all admitted logical systems are necessary. These characterization would make use of meta-formulae of the kind formula j ("' j ") which stands for the fact that ' j is a formula in the formal system S j . Correspondingly predicates \\Pi j ("\\Delta ` j \\Gamma"; ß j ), standing for ß j is a proof for \\Delta ` j \\Gamma in the formal system S j , can be employed. Of course, the meta-language has to be rich enough that the notions of formula and proof can be defined in it. For instance, if we have some derivability relations like \\Delta 1 ` j \\Gamma 1 ; : : : ; \\Delta n ` j \\Gamma n \\Delta ` j \\Gamma RULE j k and ; \\Delta ` j \\Gamma AXIOM j k we have the following formulae in the meta-language in order to axiomatize the notion of proof \\Pi j ("h\\Delta 1 i ` j h\\Gamma 1 i"; ß 1 ) : : : \\Pi j ("h\\Delta n i ` j h\\Gamma n i"; ß n ) ! \\Pi j ("h\\Deltai ` j h\\Gammai"; RULE j k (ß 1 ; : : : ; ß n )) \\Pi...