CZFC is a version of ZFC with an intrinsic handling of context. This makes it easy for both machines and humans, dealing with formal proofs. Mathdialog is a computer implementation of the CZFC set theory.

A proof in CZFC is a list of logic-commands. In Mathdialog there are two types of proof the human-to-machine proofs and the machine-to-human proofs. The first one help users to find the CZFC proof (see the The Interesting and Fun Game of Mathdialog Proofse), the second one is an interactive hypertext environment that helps other users to understand the proof in a natural mathematical language that is, users doesn't need to know CZFC or Mathdialog to understand it.

Logic-commands are the building blocks of proofs. In the human-to-machine proofs, they generate hypotheses and/or new goals and mirror each proof step used in mathematical books. A logic-command is a step in a proof that models some step in books such as proof by contradiction, brig a definition, instantiate a quantified formula, etc. For example, if the present goal is SUBSET(A,B) ==> BG(x,B) then the logic-command IF_RED[] place BG(x,B) as a new goal and SUBSET(A,B) as a new hypothesis.

There are not inference rules in Mathdialog, deductions are done through logic-commands. All logic-commands are described in the Logic-commands Reference Guide.

A proof in CZFC is a list or sequence of logic-commands. All logic-commands are explained in the Logic-commands Reference Guide.

A human-to-machine proof is a dialog between humans and machines that helps the former to find a CZFC proof. This dialog take place in the mathdialog.com web GUI that enable users to send sentences to Mathdialog and get a response from it. The proof starts when the user write and send a theorem (one of the kind of sentences Mathdialog understand) in the command window, it responds by displaying the theorem hypotheses and its thesis in the black board, the latter is the proof main goal. Then, the user write and send logic-commands (another kind of sentences Mathdialog understand) one by one until Mathdialog responds with a hypothesis that matches the main goal.

A machine-to-human proof is a hypertext interactive environment where almost all necessary facts to understand the proof are at the user finger tips. You do not have to know CZFC nor Mathdialog to understand them.

To write theorems and some definitions, you have to follow the following syntax depending of the type of object you want to write. In what follow: LABEL is a string with no blank spaces, the theorem or definition name. LFA is a List of Atomic Formulas, they are the theorem or definition hypotheses for humans and the theorem local context for Mathdialog. FORMULA is a logical formula. VAR_LIST is the list of variables in its respective LFA. For example, the informal syntax for theorems is: THEOR[LABEL;LFA;FORMULA] Notice that, in Mathdialog, even the most insignificant theorem (there are not corollaries, lemmas, etc) has a name and one or more hypotheses. A formula alone does not make sense in Mathdialog, it must have a context. In theorems and, as we will see next, definitions, LFA has this functionality. For predicates, the informal syntax is: DEF_PRED[LABEL;LFA;LABEL(VAR_LIST) <==> FORMULA] For comprehension sets the informal syntax is: DEF_OBC[LABEL;LFA;LABEL(VAR_LIST) = {BG(x,TERM):FORMULA} Suppose TH_EX_UN is the name (label) of a theorem of existence and uniqueness, then informal syntax for a existential object is: DEF_OBE[LABEL;LFA;LABEL(VAR_LIST) = TH_EX_UN] In Mathdialog, this definition and the theorem TH_EX_UN must be seen as one object (even though a theorem of existence and uniqueness can exists without a existential object definition), in particular the LFA of the theorem TH_EX_UN and the LFA of this definition must literally match.

A machine-to-human proof is an interactive environment where you control the steps flow and helps you to solve your doubts about that proof. When you read a proof in a book and you don't understand a step or where a hypothesis come from, you have to wait to ask to your teacher. Instead, in a machine-to-human proof you have all the facts to understand it at your finger tips.

You don't have to. Everybody can consult machine-to-human proofs. However if you want formulate a new definition or a new theorem to start a human-to-machine proofs, you have to be logged. One of the incentives to prove theorems in Mathdialog is that your name will be associated to that theorem, the more important the theorem you prove the bigger prestige you will have. At the present stage, all theorems are elementary. Its importance depends of the development one is making on a given time. When a logged user consults a machine-to-human proof the correspondent human-to-machine proof is displayed in a floating window, this is useful to learn about how to make human-to-machine proofs.

There are two types of windows, one is the background fixed windows, in the human-to-machine proofs they are the blackboard and the command window, in the machine-to-human proofs they are the goal, the hypotheses and the step windows. The other type of windows are the floating windows, you can resize them by dragging the lower right corner, you can also move them by dragging its title-bar.

That cannot be done, you have to choice a list element and delete the resulting window.

A floating window cannot be closed if it has a child. The number in title-bar indicate if it has a parent. For example the numbers 1.2, 1.4.1 and 2.3 mean that they parents are 1, 1.4 and 2 respectively.

A child of a floating window is a floating window that contains a definition or theorem related to its parent. For example if a floating window contains the partial order definition: Definition of: P_ORDER; If RELAT_IN(R,A), then we will say that P_ORDER(R,A) if and only if ANTISYMMETRIC(R,A) AND REFLEXIVE(R,A) AND TRANSITIVE(R,A) and you want to see the definition of REFLEXIVE, just select it, hover consuls in the main menu and click "The selected name". The REFLEXIVE definition will appear in a new floating window that is a child of the one with the P_ORDER definition.

The Mathdialog GUI does not works with touch screen devices such as tablets or mobile phones. mathdialog.com has been tested with Firefox, Chrome, Opera, Vivaldi, Edge and Safari web browsers.

Mathdialog.com has been tested with Firefox, Chrome, Opera, Vivaldi, Edge and Safari web browsers.

The web mathdialog.com is just the user interface, the red button means the browser cannot connect to the Mathdialog program. There are many reasons for this but it must be temporary, at most 5 minutes, if it takes longer a huge problem is happening. It also happen with incompatible browsers.