Section 5: Arguments

An argument is a systematic attempt to convince someone (possibly yourself) that if certain things are assumed to be true then something else must also be true. The statements we assume to be true are called assumptions, premises, or hypotheses. The statements that we wish to justify are called conclusions or theses. In essence, an argument is attempting to establish that the following sentence is true:

``If the assumptions are true then the conclusion must also be true.''

An argument begins with a number of assumptions. These are sentences that we assume are true. It then proceeds by a sequence of steps. At each step, a new true sentence is established by applying an inference rule to one or more of the preceding sentences.

Since every step introduces a true sentence, all sentences in an argument are true --- either by assumption or as a result of an inference (applying an inference rule). There is one caveat that we must keep in mind --- each sentence is true only in the context it was written. Taken out of context the sentence may be false, or more likely, meaningless.

Arguments, by their very nature, start by assuming that the premises are true. If not, and one or more are false, it hardly makes sense to continue the argument. This certainly occurs in real life --- how often have you tried to sway the opinion of someone who doesn't even agree with your basic assumptions? But an argument can still be correct, that is its conclusion follows logically from it premises, even if the premises are wrong, and especially so if the premises are self-contradictory. This is very important to remember. All a correct argument does is: it expresses a relationship between the premises and the conclusion, it says nothing at all about the truth of the premises.

5.1: The Structure of MIZAR Arguments

Let us begin by looking at a simple argument that formalizes the one we did in our explanation of implies.

ex06.mse
TRY IT!
environ 
        == This is where the premises of the argument are placed
        == each of these sentences is assumed to be true. 

        == First we introduce the names of the objects involved
        == in the argument.  These names are global constants.

    given A, B, C being PERSON;

        == Then we state the logical relationships between the objects.

    P0: Knight[A];
    P1: Knight[A] implies Knave[B];
    P2: Knave[B]  implies Knight[C];

        == Now we start the reasoning part of the argument.
begin 

    S1: Knave[B] by P0, P1; 
    S2: Knight[C] by S1, P2;

The single most important thing to remember about an argument is that every statement is true within the context it is written. No consistent proof system ever permits you to write down a statement that is false in its context.

An argument proceeds in two phases. First you state your premises as a collection of formulas that are assumed to be true. This sets up the initial environment or context for the proof. Thus if we are assuming that Fred is a knight, we might include the axiom

A1: Knight[Fred];

in the proof environment. If one of your premises is more naturally stated as a falsehood, you will have to recast it so that it can be stated as a true assumption. For example if Fred is not a knave you might include the axiom:

A2: not Knave[Fred];

The next phase of the proof consists of the actual reasoning, broken down into a number of steps. Each step consists of a proposition and its justification. The proposition is an assertion that within the current context some specific logical formula is true. The justification uses facts already established to support the proposition. Implicit in the justification is the use of one or more rules of inference.

The basic structure of a MIZAR proof follows this general pattern. In MIZAR an argument is called an Article.

Article   ::=   environ
     Environment
[   begin
     TextProper
]

The Environment contains all of the assumptions and declarations used in the argument that follows in the TextProper. (Note that the begin TextProper part is optional.)

The environment consists of zero or more global constant declarations and axioms.

Environment   ::=   {
  Axiom ; |
  GlobalConstantsDeclaration ;
}

The GlobalConstantsDeclaration introduces names of some objects of specified sorts whose properties are discussed in the rest of text. Some of these properties are stated as axioms. An axiom is a named formula which we assume to be true. Grammatically, an axiom looks like:

Axiom   ::=   LabelId : Formula

The TextProper consists of one or more Statements separated by semicolons.

TextProper   ::=   { Statement ; }+

We begin by considering the simplest type of a Statement, which is the CompactStatement with SimpleJustification and has the following shape.

Proposition    SimpleJustification

where a proposition consists of an optional label followed by a formula:

Proposition   ::=   [ LabelId : ] Formula

Every proposition that we write must be justified. The SimpleJustification directly appeals to some inference rule and has the form

SimpleJustification   ::=   [ by Reference { , Reference } ]

Reference   ::=   LabelId

A simple justification can be empty, in which case its truth is (supposedly) obvious. (The other kind of justification uses a proof. We leave it till later.)

Note that in MIZAR, we need only reference the statements necessary to justify the proposition. The related inference rule is figured out automatically by the MIZAR processor. Consider the following example:

ex08.mse
TRY IT!
environ
    given x, y, z being THING;
    A1: A[x] & B[y];
    A2: B[y] & C[z];
begin
    1: A[x] by A1;
    2: C[z] by A2;
    3: A[x] & C[z] by 1,2;

In this proof, we implicitly use two inference rules. One that says if A[x] & B[y] is true, then A[x] is true. The other says that if A[x] is true, and C[z] is true, then A[x] & C[z] is true.

We can write the first of these inference rules as:

A[x] & B[y]
A[x], B[y]

and the second as:

A[x], C[z]
A[x] & C[z]

The notation means that if the all of the formulae above the line (called premises) appear in the proof so far, you can then write in the proof any of the statements that appear below the line (called conclusions). To illustrate the generality of each inference rule we use greek letters to refer to arbitrary formulae that have (implicit) parentheses around them. To reiterate, every inference rule has the form

phi0, phi1, . . . , phim
psi0, psi1, . . . , psin

and is interpreted as saying that if all of the formulae phi0, . . ., phim are true then you can conclude a conjunction of any number of the statements psi0, . . ., psin. In a MIZAR text, there is no need (and there is no way) to specify the name of a rule of inference. The MIZAR processor knows (almost all) the rules. Often, the writer of the proof will add comments indicating what inference rules were applied. An application of an inference rule in a MIZAR text is built according to the following general pattern.

k0:       phi0       . . .
k1:       phi1       . . .
. . .
. . .
. . .
km:       phim       . . .

With all the formulae labelled k0, k1, . . .,km available for reference we can add new lines to our argument, some of which look like:

      psi0      by k0, k1, . . ., km;  == Name the rule here

or

      psi1 & psi3      by k0, k1, . . ., km;  == Name the rule here

or

      psi0 & psi1 & . . . & psin      by k0, k1, . . ., km;  == Name the rule here

Unfortunately, the notion of context somewhat complicates the use of the inference rules with regard to referencing premises. To understand context, we have to introduce the notion of visibility. But first let us look at some basic inference rules.

5.2: Basic Inference Rules

An argument is constructed one statement at a time, and has the shape of an optionally labeled formula followed by a justification. Since formulae vary widely in their form, we would expect to have a number of methods for adding new statements. For each of the logical connectives we have a rule that under the appropriate conditions lets us add a formula with that connective as the main one. Such rules are called introduction rules.

Conversely, since we may wish to make a reference to a formula of arbitrary shape in our argument, we have rules that under the appropriate conditions let us make a reference to the formula. These rules are called elimination rules.

We will start with a very special rule that is rarely useful.

5.2.1: Rewriting or Repetition, RE

Everyone would agree that once we establish a formula as true in a certain context, there is no need to repeat the argument in order to get the formula in another place, provided the context has not been changed.


Example:

            . . .
        14: Knave[John] . . .
            . . .
        17: Knave[John]  by 14;        == Rule: RE
            . . .
Label 14 must be visible when we make the reference (see 6.4). Also, we must be sure that the person named John at label 14 is the same person mentioned at label 17.

5.2.2: Negation Elimination, NE

This rule is also known as double negation elimination.

not not

In words: once we have the formula negated twice, we can drop both nots.

The box, , may contain an arbitrary formula provided that

not not

has the same structure as

not not ( )

To see this point note that the formula

not not Knave[John] or Knight[Mary]

cannot be used as a premise for applying NE as the main connective in the formula is or and not not not. Example:

            . . .
        14: not not Knave[John] . . .
            . . .
        17: Knave[John]  by 14;        == Rule: NE
            . . .

5.2.3: Negation Introduction, NI

This rule is quite complex and will be defined later in section 6.2.

5.2.4: Conjunction Elimination, CE

&
,

The premise of this inference rule must have & as the main connective. Example:

            . . .
        4: Knave[John] & Knight[Mary] . . .
            . . .
        5: Knight[Mary] by 4;        == Rule: CE
            . . .
        7: Knave[John]  by 4;        == Rule: CE
            . . .

5.2.5: Conjunction Introduction, CI

,
& , &

When this inference rule is applied, the conclusion must have & as the main connective. Example:

            . . .
        2: Knave[John] . . .
            . . .
        9: Knight[Mary] . . .
            . . .
        24: Knave[John] & Knight[Mary] by 2, 9;        == Rule: CI
            . . .
        42: Knight[Mary] & Knave[John] by 2, 9;        == Rule: CI
            . . .

5.2.6: Disjunction Elimination, DE

Version 1:

or , not

Version 2:

or , not

These are two versions of the same rule. Although only one of them suffices, we introduce both, for convenience. This rule takes two premises, one of them must have or as the main connective, the other must be the negation of one of the disjuncts. Example:

            . . .
        4: Knave[John] or not Knight[Mary] . . .
            . . .
        5: not not Knight[Mary] . . .
            . . .
        7: Knave[John]  by 4, 5;        == Rule: DE
            . . .
        9: not Knave[John] . . .
            . . .
        10: not Knight[Mary] by 4, 9;    == Rule: DE
            . . .

5.2.7: Disjunction Introduction, DI


or , or

The conclusion of this rule must have or as the main connective. Example:

            . . .
        5: not Knight[Mary] . . .
            . . .
        7: Knave[John] or not Knight[Mary] by 5;           == Rule: DI
            . . .
        10: not Knight[Mary] or Loves[John, Mary] by  5;    == Rule: DI
            . . .

5.2.8: Implication Elimination, IE, or Modus Ponens, MP

, implies

This is probably the best known rule of inference. It takes two premises, one must have implies as the main connective, and the other must be the antecedent of the implication. Then the conclusion is the consequent of the implication. Example:

            . . .
        5: Knight[John] . . .
            . . .
        7: Knight[John] implies Loves[John, Mary] . . .
            . . .
        10: Loves[John, Mary] by  5, 7;    == Rule: IE
            . . .

5.2.9: Implication Introduction, II

Unfortunately this rule is quite complex and will be defined later in section 6.1.

5.2.10: Equivalence Elimination, EqE

Version 1:

iff ,

Version 2:

iff ,

Although only one of this rules suffices, we introduce both for convenience. One of the premises must be an equivalence, that is, a formula with iff as the main connective. Example:

            . . .
        5: Knight[John] . . .
            . . .
        7: Knight[John] iff Loves[John, Mary] & Knight[Mary] . . .
            . . .
        10: Loves[John, Mary] & Knight[Mary] by  5, 7;    == Rule: EqE
            . . .

5.2.11: Equivalence Introduction, EqI

implies , implies
iff

Example:

            . . .
        3: Loves[John, Mary] & Knight[Mary] implies Knight[John] . . .
            . . .
        7: Knight[John] implies Loves[John, Mary] & Knight[Mary] . . .
            . . .
        8: Knight[John] iff Loves[John, Mary] & Knight[Mary] by 3, 7;
                                                  == Rule: EqI
            . . .

5.2.12: Equality Elimination, =E

This rule will be defined later in section 7.3.

5.2.13: Equality Introduction, =I


alpha = alpha

for arbitrary object name alpha. Note that this rule does not have any premise. Example:

ex07.mse
TRY IT!
environ
        given x being aThing;
begin
        x = x;                == Rule: =I
                              == Note: There is no `by'.

5.2.14: Rules for Quantifiers

The inference rules for quantifiers will be defined in section 7.

5.3: Annotated Proofs

Here is a simple proof in which we have annotated each line with the inference rule underlying its justification. This level of detail is unnecessary, and is here simply to illustrate how various rules can be used. In fact, as is illustrated by the last line, breaking up the reasoning into such simple pieces is unnecessary as MIZAR understands how to reason about these kinds of formulas.

ex09.mse
TRY IT!
environ
    given x being Int;
    A1: A[x] or (B[x] implies C[x]);
    A2: not A[x] & (D[x] implies B[x]);
    A3: D[x];
begin
    1: not A[x] by A2;                    == Rule: CE
    2: D[x] implies B[x] by A2;           == Rule: CE
    3: B[x] by A3, 2;                     == Rule: MP
    4: B[x] implies C[x] by 1,A1;         == Rule: DE
    5: C[x] by 3,4;                       == Rule: MP

    6: B[x] & C[x] by 3, 5;               == Rule: CI
    7: B[x] or G[x] by 3;                 == Rule: DI

    6: C[x] by A1, A2, A3; == directly using Mizar's proof capability