Section 2: The Island of Knights and Knaves

We begin our study of logic with a puzzle. There is an island in which every inhabitant is either a knight or a knave. Knights always tell the truth, while knaves always lie. As a visitor, you came upon two inhabitants which we will call A and B. Person A says ``I am a knave or B is a knight.''. Can you determine what A and B are?

First of all, we get rid of the self reference, ``I'' in the statement made by A and write an equivalent statement:
``A is a knave or B is a knight.''
which we will call S. Thus A says statement S.

Now, by assumption, A is either a knight or a knave. Let's assume that A is a knave and see what happens.

Thus in saying ``I am a knave or B is a knight.'' A has told the truth. But this is impossible because we have assumed that A is a knave and so always lies. Therefore statement S must be false. That is, A cannot be a knave, and B cannot be a knight.

So assuming that A is a knave leads to an absurd situation. Thus A must not be a knave, and, since there are only knights and knaves, we conclude that A must be a knight.

Now this means that A is telling the truth and so statement S must be true. The first part ``A is a knave'' is clearly false. This means that the second part ``B is a knight'' must be true.

Thus, both A and B are knights.

Now most people who solve these kinds of puzzles for recreation would agree that this is a valid argument, that is, it does not make any logical errors in its reasoning, and comes to a correct conclusion. They would also agree that there is more to this argument than just the words above --- there is also a large collection of unstated assumptions and rules involved. Here are just a few that are used in the argument above.

Our task will be to clarify these and other properties of an argument. In the process we will be introducing a formal logical system called MIZAR MSE. Developing this formal system requires us to address issues of both syntax and semantics.

Syntax refers to the form of the sentences that we construct, while semantics refers to the meaning that we assign to the sentences. In general, issues of syntax can be addressed without introducing semantics. For example, one can determine that an English sentence is grammatically correct without actually understanding what it says. You simply check that the sentence does not break any rules of the grammar. In describing the syntax of MIZAR sentences and proofs we will use a special kind of grammar called Backus-Naur Form, or BNF for short.

Once one has a precise syntax, it is possible to address the issue of semantics --- that is, how do we give meaning to the sentences in the formal system. Usually there are many possible semantics for a given system, and so we must always be clear about which particular one is being used.

In general, we can associate two levels of semantics with a system. One level is fixed and unchanging. It deals with the meaning that we assign to connectives like and and or, and what it means for something to be a predicate or term. We call this the fixed semantics. The other level of semantics is variable and subject to differing interpretations. This variable part of the semantics specifies the kinds of things we want to talk about, and defines the meaning of each particular term and predicate used.

To give you some feel for what a formal argument in MIZAR looks like, here is a formal version of the argument above.


     given A, B being PERSON;

Opp: for a being PERSON holds Knight[a] iff not Knave[a];

    == These two statements form a translation of the sentence, said by A:
    == "I am a knave or B is a knight"

A1:  Knight[A] implies ( Knave[A] or Knight[B] );
A1': Knave[A] implies not ( Knave[A] or Knight[B] );


    == The question is what are A and B?

    == First we argue that A is a knight.

C1: Knight[A]
        assume 0: not Knight[A];
               1: Knave[A] by 0, Opp;
               2: not( Knave[A] or Knight[B]) by 1, A1';
               3: not Knave[A] by 2;
        thus contradiction by 1, 3;

    == Now we argue what B is.

S1: Knave[A] or Knight[B] by C1, A1;
S2: not Knave[A] by C1, Opp;
    Knight[B] by S1, S2;