User:Frédéric Liné

From Wikipedia, the free encyclopedia

This idea has to be placed somewhere so I store it here for the moment.

Metamath, in contrast to software like Otter, cannot prove a theorem automatically. It can only verify proofs for correctness, and such proofs must be entered by a user.[1] , Metamath presents proofs in a simple, step-by-step format.[2][3].

[edit] =

Here is an example of what Metamath does exactly. Suppose you want to prove ( A \cup \varnothing ) = A (theorem un0). You start with the theorem noel which says that \lnot x \in \varnothing . Then you decide to apply the propositional calculus rule biorfi which says that if you have \lnot \varphi then you can derive ( \psi \leftrightarrow ( \psi \lor \varphi ) ). To apply biorfi Metamath checks that \lnot x \in \varnothing and \lnot \varphi can match. Obviously the \lnot in one of the formula corresponds to the \lnot in the other so it remains to check that \varphi can match x \in \varnothing . \varphi in Metamath is declared as a well formed formula variable and Metamath can check that x \in \varnothing is a well formed formula (I won't do that here but for that purpose Metamath uses the same sort of rules I'm explaining here). When a formula and a variable are of the same species (here both are well formed formulas Metamath accepts to match them. So since the premises of biorfi matches \lnot x \in \varnothing Metamath accepts to apply biorfi. It will simply substitute \varphi by x \in \varnothing in the conclusion. And the user specifies that ψ must be replaced by x \in A . The result is ( x \in A \leftrightarrow ( x \in A \lor x \in \varnothing ) ) . The checking of the first is now finish. As you can see Metamath has only compared formulas to ess if they can match and substitute variables by their corresponding subformulas. Checking the rest of the proof uses the same devices.


Then, continuing with bicomi, id est the commutative law for biimplication. bicomi stipulates that if you have ( \varphi \leftrightarrow \psi ) then you can infer ( \psi \leftrightarrow \varphi ) . The last step uses unecri. That theorem says that if you have ( ( ( x \in A ) \lor ( x \in B ) ) \leftrightarrow x \in C ) then you can infer A \cup B = C

This explanation doesn't take into consideration the syntactical checking but in fact it is not different from the rest.

Note: In fact except for the hypotheses and the conclusion there is nothing that looks like a formula in a Metamath proof. A proof for Metamath is only a list of inference rules. The reason is that knowing the hypotheses and the applied inference rules we can always know what the conclusion formula is. However since human beings like seeing a formula from time to time I have added them.

This section is currently modified. Please don't remove...

[edit] Brief tour of the set.mm database

You have been told that all mathematics could be derived from a handful of axioms. But you have perhaps never seen that concretely. In fact it is perhaps even difficult for you to have a clear idea of how all mathematics can be derived so. Reading text books often doesn't help because matters are presented independently in the loose and literate mathematical style that hides how everything is connected, and it's difficult to imagine how different fields like logic and set theory can cooperate together to make you able to prove topology theorems for instance. Metamath is the device that will make you able to have a very precise picture of how all that sort of things work together.

In the rest of the section I'll try to give a small guided tour of set.mm.

propositional calculus In metamath there is no special symbol for definition. The biimplication is used instead. But it means that there is a problem: how to define the biimplication itself. Here is the solution: df-bi

predictate calculus I will leave predicate calculus rather untouched however I don't resist to show on an example that an implication is not an inference ( as it can be so often believed ). Here is a counterexample: 19.20.html, 19.20i.html. In one case the antecedent has to be quantified whereas in the other the premisse doesn't need it. Substitution is not a primitive of metamath and has a definition like the other objects :df-sb. However in set.mm the substitution operator is rarely used.

Zermelo-Fraenkel set theory The axiom of the Zermelo-Fraenkel set theory belongs to set.mm; here is for instance the axiom of extensionality: ax-ext. The concepts that closely depend from a specific axiom just follow it. It allows to link easily the axioms and their immediate consequences. For instance the uniqueness of the empty set (zfnuleu) only depends on the axiom of extensionality. set.mm used a lot class abstraction, more than what is accustomed in a normal text book. Here is the definition of class abstraction: df-clab. Then usual classes used in set theory are derived from the axioms: intersection df-in, power class df-pw ordered pair,df-op, relation df-rel, function df-fun and so on. Famous set theory theorems are proved like pigeonhole principle and Cantor's theorem.

... to be completed.

[edit] Underlying philosophy

Metamath is a generic program because of its underlying philosophy. The Church-Turing thesis says that "Every function which would naturally be regarded as computable can be computed by a Turing machine." Since checking a proof can be viewed as a "function which would 'naturally be' regarded as computable", the Church-Turing thesis implies that proof checking can be done by the simple "read and write" algorithm described by a Turing machine. Following this principle Metamath does no more than read a set of formulas, compare them with the hypotheses of a rule of inference and write the conclusion. The assumed universality of the Church-Turing thesis ensures that any logic can be checked using Metamath including non-standard logics like lambda calculus, or 'natural' deduction.

This design also explains why substitutions of set variables and bound variables checking are not managed by the software. Any time one needs a theorem which substitutes set variables by others or which checks if variables are bound, one needs to prove it. Axioms have been designed to allow that type of proof.

The only exception in Metamath to this Church-Turing philosophy is the presence of a device to deal with distinct variables (the so called $d statement). According to the Church-Turing thesis this device is not strictly necessary and a system has been realized where this device is not used[4]. However such a system is difficult to work with and the $d statements have been added for the users' convenience. These statements add syntactic clarity to the language, but do not change its expressive power.