| Home | Grammar | Facts | Reasoning | Knowledge base | Software | Download |
The reasoning checking module of the Verish program recognizes six principles of reasoning, called Tabulate, Example, Generalize, Focus, Some, and Abbreviate, which are sufficient to prove every Fact. The first five principles are sufficient to prove every Absolute Fact. (This was first proved by Kurt Gödel, and is explained in a blog post.) Abbreviate is used for introducing or removing Abbreviations.
The principle used to obtain the Statement of each Statement Paragraph in a Development is indicated by the Reason in that Paragraph, and if this depends on previous Statements in the Development, assumed to be Facts, the Titles of the Statement Paragraphs containing those Statements are given as the Subjects of the Reason. Six of the seven Reasons correspond to the six principles of reasoning recognized by the reasoning checking module of the Verish program, and the seventh Reason is called Application omitted.
Each specified Title is searched for among the Titles of Paragraphs that are Active for the current Paragraph, starting at the most recent Active Opening Paragraph, if there is one, and working forwards, then if necessary going back to the second most recent Active Opening Paragraph, if there is one, and working forwards to the most recent, and so on, and finally, if necessary, starting at the start of the Development and working forwards. Thus the only Paragraph outside a Method Application that can refer to Statements within that Method Application is the Statement Paragraph that immediately follows that Method Application. This is also the only Paragraph outside a Method Application that can use a Definition Paragraph that is within that Method Application, and this is only possible if the Reason in that Statement Paragraph is Abbreviate.
Proofs can be organized as Applications of Methods. The Applications of some Methods, called Automatic Methods, can be generated automatically by the Verish program.
The six principles of reasoning are intended to be used in a Regular Development. The Verish program checks that the Development is Regular, and the justifications of the principles, given below, assume that the Development is Regular.
In a Regular Development, if a Statement Paragraph A is Active for another Paragraph B, and the Statement in A is a Fact, then that Statement is true for every Meaning that is Allowed by all the Definition Paragraphs that are Active for B. Thus if the Statement in each Statement Paragraph is justified by one of the first six Reasons, then the Statement in each Statement Paragraph is a Fact.
The Reason is either +Tb, or a Brief whose first Word is a Preposition whose Initial and Formatives are +Tb.
Every assignment of either true or false, independently, to the distinct Clauses in the present Statement and any specified previous Statements is tested. If the present Statement is true for every assignment which is consistent with the specified previous Statements, if any, being Facts, then the present Statement is also a Fact.
The Reason is +Ex.
The Statement has the form ) - A B C, where A is an Adverb that begins with [, B is a Sentence, and C is obtained from B by replacing every Object occurrence that is not Governed, of the Noun that Agrees with A, by a Phrase D, such that no Noun in D becomes Governed, when D replaces an occurrence in B of the Noun that Agrees with A.
For any Meaning of the Statement, all the occurrences of D in C, that have replaced occurrences in B of the Noun that Agrees with A, correspond to the same thing, so from the rules that determine whether a Sentence is true or false for a given Meaning, C is true if the Sentence A B is true. So the Statement is an Absolute Fact.
The Reason is a Brief whose first Word is +Gn/.
The Statement has the form A B, where A is an Adverb that begins with [ and B is the Statement specified by the Reason, and the Noun C that Agrees with A is not a Name in consequence of any Definition Paragraph that is Active for the current Paragraph.
If B is a Fact, then it is true for all Meanings that are Allowed by all the Definition Paragraphs that are Active for the Statement A B, so it will also be true for all Meanings that are Related to any of those Meanings, with reference to the Adverb A, unless the thing specified for the Noun C affects whether or not a Meaning is Allowed by one or more of those Definition Paragraphs. The Definition in a Definition Paragraph is not a Noun, so if C has a Verb occurrence in a Definition, that Definition is not a Phrase, so the only ways this could happen are if C is the Abbreviation of a Definition Paragraph whose Definition is a Phrase, or C is a Subject of the Abbreviation of a Definition Paragraph, or C has an Object occurrence in the Definition of a Definition Paragraph that is not a Governed occurrence, but is not a Subject of the Abbreviation of that Definition Paragraph.
The first and third of these cases are excluded by the requirement that C is not a Name in consequence of any Definition Paragraph that is Active for the Statement A B. And in the second case, the thing specified for C does not affect whether a Meaning is Allowed or not by a Definition Paragraph, because the requirements for a Meaning to be Allowed involve comparing the Abbreviation and the Definition, for all Meanings that are Similar to that Meaning, with reference to that Definition Paragraph.
The Reason is a Brief whose first Word is +Fc/.
The specified earlier Statement has the form A ) B C, where A is an Adverb that begins with [, and B and C are Sentences such that the Noun that Agrees with A has no Object occurrence in B that is not Governed, and the Statement has the form ) B A C.
For any Meaning of A ) B C, and any Meaning of ) B C that is Related to that Meaning, with reference to the Adverb A, B is true for the Related Meaning if and only if it is true for the original Meaning. If B is true for the original Meaning, then ) B A C is true for that Meaning. If B is false for the original Meaning, then A ) B C is true if C is true for every Related Meaning, and false otherwise, and ) B A C is also true if C is true for every Related Meaning, and false otherwise. Thus if A ) B C is true for a given Meaning, then ) B A C is also true for that Meaning.
The Reason is a Brief whose first Word is +Sm/.
The Statement and the specified earlier Statement are related by the replacement of one occurrence of three consecutive Words of the form - A - in one of the Statements, where A is an Adverb that begins with [, by B in the other Statement, where B is the Adverb obtained from A by replacing its [ by ].
Every Meaning of either Statement is also a Meaning of the other Statement, and for every Meaning of the Statements, each of the Statements is true for that Meaning if and only if the other Statement is true for that Meaning, so the new Statement is a Fact if the earlier Statement is a Fact.
The Reason is a Brief whose first Word is +Ab/.
The Statement and the specified earlier Statement are related by the replacement of one occurrence of a Sentence in one of the Statements by a Phrase in the other Statement, such that the first Word of the Phrase is Defined by a Definition Paragraph that is Active for the current Statement, and the replaced Sentence is formed from the Phrase in Accordance with that Definition Paragraph, such that the formation of the replaced Sentence is Legitimate.
For every Meaning that is Allowed by the Definition Paragraph that was used to obtain the current Statement from the specified earlier Statement, the Statements are either both true or both false. So for every Meaning that is Allowed by all the Definition Paragraphs that are Active for the current Paragraph, the Statements are either both true or both false. If the earlier Statement is a Fact, then it is true for every such Meaning, so the current Statement is also a Fact.
(The 5th requirement on a Regular Development means that if the current Paragraph is the first Paragraph after the end of a Method Application, and the Definition Paragraph that Defines the first Word of the Phrase is within that Method Application, then the current Paragraph must be the one that contains the replaced Sentence rather than the Phrase.)
The Reason is +Ao. It follows a Method whose Application is omitted, and does not specify a principle of reasoning.
The Method is +Pr. It can be used to improve the structure or enhance the organization of a Development.
The Applications of the Methods in the following list can be generated automatically by the Verish program, by use of the -addMthApps option, and they can be removed by use of the -rmMthApps option. The automatically generated Application of a Method can contain Methods that come earlier than that Method in the following list, and the Applications of those Methods will also be generated automatically. The reasoning in a Development that contains Methods in the following list whose Applications are omitted can be checked by use of the -chkwAo option.
The following list of automatic Methods is intended to grow steadily with time.
The Method is a Brief whose first Word is +Rp/.
The Statement is obtained from the specified earlier Statement by replacing all Object occurrences of a Noun A that are not Governed, by a Phrase B, such that no Noun in B becomes Governed, when B replaces an occurrence of A.
The Method is a Brief whose first Word is +Sa/.
The Statement has the form ) B - C A, and the specified earlier Statement has the form ) B - A, where A and B are Sentences, and C is an Adverb that begins with ], such that the Noun that Agrees with C has no Object occurrence in B that is not Governed.
The Method is a Brief whose first Word is +Sc/.
The Statement has the form ) - A C D, and the specified earlier Statement has the form ) - A B, where C is an Adverb that begins with ], and B is a Sentence obtained from D by replacing all Object occurrences in D that are not Governed, of the Noun that Agrees with C, by a Phrase E, such that no Noun in E becomes Governed in B.
The English and Verish text on this website is licensed for use under the Free Software Foundation Free Documentation License, and the software is licensed for use under the Free Software Foundation General Public License.
Page last updated 17 July 2022. Copyright (c) Chris Austin 1997 - 2022. Privacy policy