The formal system on type includes the axiomatic system and the system of natural inferencea,nd on structure includes the formal language and the deductive device.As the builders of the formal system,different people have different philosophy background,theoretical object and purpose,and they might use different formal languages and deductive device,so we have various kinds of formal system,and in different system the arguments of the same theorem have different formula series.The formal language and the dudective device not only define for us the tool,the starting point and the basis of the formal argument,but also imply semantically the theoretical object and purpose of the builder,it will lead to illogic to put aside the specific formal syetem to talk about or argue a theorem.