•
Hover cursor over text of this color to see a popup reference for the symbol or name. Click elsewhere to make the popup disappear.
• Expand and collapse sections of the argument using the
, 
, and other buttons.
• The axioms used to prove a given lemma (including the main Goal) are listed before the lemma or as children of the lemma. The ones listed before are those that define or introduce symbols that are used in the statement of the lemma (i.e. the ones that are required for understanding the lemma).
• An Assertion is an axiom that I expect to be uncontroversial relative to the axioms designated Assumption. It is a vague and subjective designation. If the language interpretation guide entries (the informal textual semantics) for the symbols that the axiom depends on do not make it clear to you that this axiom should be true, then you should criticize this designation. Depending on the specifics of your criticism, I can respond by improving the entries in the language interpretation guide for some of those symbols, or else by changing the designation to "Assumption" or "Claim".
• A Definitional Axiom is an axiom that should be be absolutely uncontroversial among the intended audience for this argument. Usually, if not always, it will have a very objective/mathematical character.
• ✓Lemma and ✓Goal denote sentences that have been formally proved (computer checkable) to be logical consequences of the definitions, axioms and lemmas that precede them, and the definitions, axioms and lemmas that are their children (immediate descendants only). A Lemma has an informal proof. A Claim is a statement that is used as a Lemma but has neither been formally nor informally proved.
• A Defn~ introduces a symbol together with a sentence that intuitively defines it, but does not technically yield a definitional extension of the theory. Usually such symbols could be turned into proper definitions with the use of a definite description operator.
• Expand and collapse sections of the argument using the
, , and other buttons.
• The axioms used to prove a given lemma (including the main Goal) are listed before the lemma or as children of the lemma. The ones listed before are those that define or introduce symbols that are used in the statement of the lemma (i.e. the ones that are required for understanding the lemma).
• An Assertion is an axiom that I expect to be uncontroversial relative to the axioms designated Assumption. It is a vague and subjective designation. If the language interpretation guide entries (the informal textual semantics) for the symbols that the axiom depends on do not make it clear to you that this axiom should be true, then you should criticize this designation. Depending on the specifics of your criticism, I can respond by improving the entries in the language interpretation guide for some of those symbols, or else by changing the designation to "Assumption" or "Claim".
• A Definitional Axiom is an axiom that should be be absolutely uncontroversial among the intended audience for this argument. Usually, if not always, it will have a very objective/mathematical character.
• ✓Lemma and ✓Goal denote sentences that have been formally proved (computer checkable) to be logical consequences of the definitions, axioms and lemmas that precede them, and the definitions, axioms and lemmas that are their children (immediate descendants only). A Lemma has an informal proof. A Claim is a statement that is used as a Lemma but has neither been formally nor informally proved.
• A Defn~ introduces a symbol together with a sentence that intuitively defines it, but does not technically yield a definitional extension of the theory. Usually such symbols could be turned into proper definitions with the use of a definite description operator.