Alpha Beta Epsilon

I will reply to all messages on this page, to avoid making a mess. Comments left on this page are subject to restructuring.

Welcome

Welcome!

Hello, Alpha Beta Epsilon, and welcome to Wikipedia! Thank you for your contributions. I hope you like the place and decide to stay. Here are some pages that you might find helpful:

• The five pillars of Wikipedia
• How to edit a page
• Help pages
• Tutorial
• How to write a great article
• Manual of Style

I hope you enjoy editing here and being a Wikipedian! Please sign your name on talk pages using four tildes (~~~~); this will automatically produce your name and the date. If you need help, check out Wikipedia:Questions, ask me on my talk page, or ask your question and then place {{helpme}} before the question on your talk page. Again, welcome!  – Oleg Alexandrov (talk) 15:05, 30 July 2007 (UTC)

Improvement

Dear Alpha Beta Epsilon, I really appreciate most of (but not all) the improvements you made to the Metamath page ("token" instead of "markup" doesn't mean the same thing for instance). However the way your rewrite my sentence about Russell and the proof of 2 + 2 = 4 seems - let's say - a bit strange. The original sentence was intended to be a sort of private joke (perhaps not very good I admit). I think it's no longer the case and I would prefer the parenthesis be removed in that case. Frédéric Liné —Preceding unsigned comment added by 83.202.6.30 (talk)

The Metamath book (available here) clearly refers to ${, $}, $c, $v, $f, and $e as a set of keyword tokens (see page 92). Upon reviewing lexical analysis and markup (which defines a markup language as "a type of language that describes a document's formatting"), it presently appears to me as though the word "token" would be a better choice.

I do not understand entirely what you mean by "parenthesis be removed". If you can remove the parentheses and restructure the statements, please feel free to do so. Wikipedia articles are not places for private jokes; it would be best if we keep the tone of each article as encyclopedic as possible. Also, I respectfully suggest that you sign your comments using ~~~~; see Wikipedia:Signatures for more information. — alpha^βε 21:25, 3 August 2007 (UTC)

The only problem with the term "token" is that I don't really understand what information it can bring to the reader: any file which carries a form or another of language is made of tokens : metamath is just like the others. What I meant using the expression "markup language" is that metamath uses a very simple grammar with few tokens in the spirit of html. Perhaps it would be better to explain this at length if the expression "markup language" is not clear.

There are also errors in your rewording of the substitution algorithm:

"axiomatic definition" means nothing. A definition is an axiom, so the word "definition" is enough.

"(2 + 2) = (2 + (1 + 1))" is not a hypothesis for "opreq2i" it is its consequence.

I think it's worth explaining with words what "opreq2i" means.

You have repeated twice the value of opreq2i. "if A = B, then (CFA) = (CFB)" means exactly the same thing that "if we have A = B as a premise, then we can infer (CFA) = (CFB)"

It's strange to say that opreq2i is applied to "(2 + 2) = (2 + (1 + 1))" it would be better to say that it is applied to "2 = ( 1 + 1 )" in fact.

Working backward is the *only* way to enter a proof with metamath, I don't understand what you mean by "in most cases".

Your explanation of the syntactical checking is not bad but not enough developped.

Frédéric Liné —Preceding unsigned comment added by 82.123.69.161 (talk)

Use of "markup language" to describe the syntax of the Metamath language is incorrect because a markup language describes a document's formatting (see my previous comment), and Metamath produces no documents of any kind. However, I did edit the article to make the fact that Metamath uses relatively few keyword tokens more clear.

By using the phrase "axiomatic definition", my aim was to clarify the fact that the definition was an axiom — a reader of the article might not know what an axiom is. The term is used in other documents; see the results of a Google search for "axiomatic definition". [1] If you continue to object to it, you may remove it yourself.

Indeed, (2 + 2) = (2 + (1 + 1)) is not a hypothesis, but a consequence. Thank you for notifying me of this error; I have corrected it. In a technical sense, a user does not have to work backwards to prove a theorem; he or she can enter the proof manually into the database and subsequently verify it. Again, however, you are welcome to remove the words "in most cases" if you feel it would be of tremendous benefit to the article to do so. — alpha^βε 21:47, 4 August 2007 (UTC)

Same thing: it needs to be developped to be clear. There is in fact a paragraph about definition somewhere else in the page. Tremendous, no. But a benefit yes. I will correct and if you don't mind I will correct the other points that bother me too. —Preceding unsigned comment added by 83.202.67.134 (talk)

Tone

As you have noticed I'm not anglo-saxon. Sometimes I'm not able to give a word its correct language level. So don't hesitate: help me to reword. I don't mind that you help me to change the Metamath page but I prefer that we speak together about those changes. Frédéric Liné