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?

Argument:
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.

An argument involves objects or things (e.g. island inhabitants) which may have names (e.g. A, B). In this particular case, different names name different things. But this is not required, some things may have many names.
Things have properties (e.g. being a knight). For a given property, each thing either has it or not. Things cannot simultaneously have and not have a property.
An argument contains statements that can be true or false, depending on the context in which the statements are made.
It is absurd for a statement to be both true and false in the same context.
An argument begins by making some statements that set the context is which the argument is held. These statements are assumed to be true. Then, each step in the argument follows from the previous steps by employing some rule of inference.
Each correct step results in a new true statement, that is, everything we state in an argument is supposed to be true in the context in which it is stated.
Arguments may contain sub-arguments.
Simple statements can be composed into complicated statements by using connectives like and, or, and not. The meaning of the complicated statement depends on the the meaning of its constituent simple statements and the connectives used to construct the statement.
Statements can be manipulated in ways that preserve their meaning but change their form.

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.

kandk01.mse
TRY IT!

environ

     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] );

begin

    == The question is what are A and B?

    == First we argue that A is a knight.

C1: Knight[A]
    proof
        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;
    end;

    == 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;