Reflecting on Kennington's mistake, it became clear to me that in fact the notion of axiom is less obvious than it seems at first sight.
There is the case of stacks of systems such as natural deduction. After all, considering that the use as a premise of a statement on the stack is an axiom or not can be regarded as a matter of taste. But it has to be said that if we transform the stack into a context added to the left of the main proposal as in my previous post, well it becomes an axiom. Then there are the syntax stories. They are not usually considered as axiom problems but there are two facts that show that the boundary is not clear either. First metamath manages the syntax as it manages the proofs by rewriting rules. Then an ambiguity in syntax can lead to a non-consistent system, as Mario Carneiro recently pointed out. The formula 2 - 1 -1 -1 = 2 - 1 - 1 - 1 can be interpreted as ( 2 - 1) - 1 = 2 - ( 1 - 1) and therefore giving 0 = 2 which of course breaks your system down. An ambiguous syntactic system ultimately has the same consequences as an inconsistent system of axioms. Finally, there are the problems of provisos. Tarski showed that in a formalization with identity one can replace the substitutions normally made behind the scene by formulas and thus manage the substitutions in a transparent way in the proof itself http://us.metamath.org/mpeuni/mmset.html#Tarski Here again, the distinction between what belongs to axioms, theorems and proof and what belongs to the other elements of logic (management of a potential stack, syntax analysis, provisos checking, substitution algorithm) is imprecise. Hence my conclusion that what is an axiom and what is not can be universally defined only in a very vague way and that in practice the concept depends on the type of system used. -- FL -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/089de40b-5561-4717-ba07-c1a349a32f5e%40googlegroups.com.
