Subwiki:Tabular proof format

From Ref
Jump to: navigation, search

The tabular proof format is used in presenting a number of proofs in the subject wikis. The typical tabular proof format looks something like this:

Step no. Assertion/construction Facts used Given data used Previous steps used Explanation Commentary
1 (assertion/construction of first step goes here) numbers/names of facts used in establishing the first assertion, if any, go here given data needed for the assertion/construction go here (none, since this is the first step) more elaboration, if necessary general commentary on the big picture, how the proof is flowing.
2 (assertion/construction of second step goes here) numbers/names of facts used in establishing the second assertion, if any, go here given data needed for the assertion/construction go here Step (1) (if it relies on terminology/assertions made in step (1)), otherwise, nothing more elaboration, if necessary general commentary on the big picture, how the proof is flowing.
3.. ... .. .. .. .. ..

This format is intended to allow people to peruse proofs at the desired level of depth, allowing for both eyeballing/scrolling and a detailed in-depth diagnostic understanding of proofs. Some aspects of the proof format are discussed below.

Columns

Step number and previous steps used column

The left column gives the step number. This is to allow easy cross-referencing to previous steps, which is done in the Previous steps used. For instance, if the fourth row (with number 4) has, in the Previous steps used column, the numbers of Steps (1) and (3), this means that the justification for Step (4) relies on using the assertion/construction of Step (3).

The step numbers are meant purely for an internal proof flow.

Assertion/construction column

The assertion/construction columns state the assertion/construction made in each step. The key idea is that a person can read only this column to get an idea of the proof, and ignore the explanation column. Further, whenever a step uses a previous step, it uses only the step as formulated in the assertion/construction column, and does not rely on the reasoning used in the explanation column. We can think of the assertion/construction column entry as the statement of an intermediate claim and the explanation column as the proof -- the key feature being that for later steps, it is the statement, not the proof, that matters.

All new notation intended for reference later in the proof (e.g., a new letter for a particular object or function) must be introduced in the assertion/construction column.

Facts used column

The Facts used column indicates, for every step, the facts that need to be used to justify the assertion or carry out the construction. Usually, these facts are listed using fact numbers, though sometimes fact names are also given. The fact numbers do not refer to previous step numbers, but rather to numbers used in a Facts used section that appears prior to the proof section on the page. The key distinction between Facts and Steps is that the facts have an independent existence outside of the statement being proved, and they usually have their own separate wiki page that is linked to in the Facts used section of the page.

The advantage of the Facts used column is that it allows both a determination of what facts are used in a particular step, and a quick determination of what steps use a particular fact.

The Facts used column does not usually contain additional information about how the fact is used to prove the assertion. That is done in the Explanation column.

Given data used column

This column provides, for each step, the given data used in establishing the assertion or construction made in that step. Given data here could include data about some object existing or satisfying some property. Given data differ from facts in that they do not have independent existence; they are just part of this particular step. They also differ from previous steps in that they are already given in the problem setup even before the proof begins.

Explanation column

This column explains how to arrive at the assertion or construction using the previous steps, given data, and facts. In some cases, no explanation is necessary -- these are cases where it is basically a modus ponens or other similar logical argument and there is no extra reasoning necessary. For instance, if the fact column states A implies B, and the given data column states that A is true in our case, then the assertion that B is true requires no additional justification.

In some cases, more details may be helpful, and the explanation column provides these. It may also include variable re-assignments (for instance, the fact may be in terms of variable objects, and the explanation may inlude the values to assign those variables to use the fact). The explanation may also include some caveats or simple algebraic manipulation. Sometimes, explanations may be long enough that they are hidden using a show/hide feature, so that only those interested in seeing the explanation details will view the explanation.

One key feature is that nothing within the explanation should be necessary for the later proof. If some intermediate conclusion reached within the explanation is to be used later, then the step should be split in two.

Commentary column

This column is not to be found in all proofs. It is optional and can be thought of as a kind of running commentary that a knowledgeable person might try to provide orally while explaining a proof. Commentary can explain the big picture ideas, the nature and motivation of steps, and can look ahead to how a step will fit in with later stuff.