ndl-tutorial

Informations

• Publié par: Fiom
• Nombre de lectures: 19
• Langue: English

Extrait

Natural

Deduction

Language

Konstantine Arkoudas

August

7,

2004

Contents

1.1 What isNDL? . . . . . . . . . . . . . . . . . . . . . . . . . .1 1.2 InstallingNDL. . . . . . . . . . . . . . . . . . . . . . . . . .3 1.3 Interacting witnNDL. . . . . . . . . . . . . . . . . . . . . .3 1.3.1 Using the GUI . . . . . . . . . . . . . . . . . . . . . .3 1.3.2 UsingNDL. . . . . . . . . . . . . . . in batch mode .4 1.3.3 Loading files from the GUI . . . . . . . . . . . . . . . .4 1.4 Input phrases . . . . . . . . . . . . . . . . . . . . . . . . . . .4 1.5NDL. . . . . . . . . . . . . . . . . . . . . . . . . . . scripts .5 1.6 Signature declarations . . . . . . . . . . . . . . . . . . . . . .5 1.7 Terms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .7 1.8 Formulas . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .7 1.9 Proof syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . .8 1.10 Proof semantics . . . . . . . . . . . . . . . . . . . . . . . . . .11 1.10.1 The assumption base . . . . . . . . . . . . . . . . . . .11 1.10.2 Rule applications . . . . . . . . . . . . . . . . . . . . .12 1.10.3 Rules dealing with equality . . . . . . . . . . . . . . .15 1.10.4 Composite proofs . . . . . . . . . . . . . . . . . . . . .16 1.10.5 Conditional proofs . . . . . . . . . . . . . . . . . . . .17 1.10.6 Proofs by contradiction . . . . . . . . . . . . . . . . . .17 1.10.7 Conclusion-annotated proofs . . . . . . . . . . . . . . .18 1.10.8 Quantifier reasoning . . . . . . . . . . . . . . . . . . .18 1.11 Examples . . . . . . . . . . . . . . . . . . . . . . . . . . . . .21

1.1 What is NDL? NDL(Natural Deduction Language) is a formal language for expressing “Fitch-style” natural-deduction proofs [3] in first-order logic with equality. The proofs are machine-checkable.NDLis a “formal” language in that it has

1

a formal syntax, and, more importantly, a formal semantics. The semantics are given in Plotkin’s SOS 1 style and are centered around the notion of assumption bases, which is the hallmark of a whole family of proof languages known as DPLs (Denotational Proof Languges) [1].NDLis a simple DPL 2 for first-order logic. An assumption base is just a set of premises—a set of statements that we take for granted for the purposes of the proof. This is traditionally known in logic as a “context,” a notion that has been around for a while, in particular in connection with sequent systems, where the basic unit of inference is a pair (β, Fconsisting of a context and a conclusion.)  is novel about DPLs What is that the formal meaning—denotation—of a DPL proof is specifiedrelative to a given assumption base (context). That is,the meaning of a DPL proof is a function over assumption bases, in the same way that in denotational semantics the meaning of an imperative program is a function over stores. This turns out to be an apt viewpoint that is particularly conducive to giving a rigorous semantics to Fitch-style natural deduction. Unlike sequent sys- tems, where the manipulation of the context is explicit and burdens the user, the manipulation and threading of the context in systems such asNDLis implicit and relegated to the underlying semantics—again, much as the ma- nipulation and threading of the store in imperative languages is hidden from the user. In a DPL, every proof has a unique formal meaning. If the proof is sound, then its meaning is the conclusion established by the proof; if the proof is unsound, then its meaning iserror. To obtain that meaning, weevaluate the proof in a given assumption base. Evaluation will either produce the advertised conclusion, which will verify that the proof is sound, or else it will generate an error, which will indicate that the proof is unsound. Thus in DPLs evaluation is tantamount to proof checking. InNDL, in partic- ular, evaluation—and hence proof-checking—is guaranteed to terminate in quadratic time in the length of the proof (in the worst case). This tutorial pertains to a graphical Java-based implementation ofNDL. Versions are available for Windows, Linux, and the Mac operating systems. They can be obtained from theNDLweb page: www.cag.lcs.mit.edu/~kostas/dpls/ndl and distributed in accordance with GPL, the copyright licence of GNU. 1 “SOS” stands for “structured operational semantics.” 2 Technically,NDLis a type-αDPL [2]. 2

1.2 Installing NDL Note: You must have Java installed in your system in order to install and runNDL. Create a directory calledndlon your hard drive, download the appropri- ate distribution there, unpack it, and then typendlat your system’s prompt (or./ndl there are any problems or to Ifif you are on a Unix system). report any bugs, email me atiotk.eduinnttans.mumale@.

1.3 Interacting witn NDL 1.3.1 Using the GUI From top to bottom, the main window ofNDLconsists of: •Themenu bar, which has four items:File,Edit,Options, andHelp. •Theinput area, which is a scrollable text buffer for user input. •The twobuttonsProcessandClear; and •theoutput area, which is an uneditable text buffer where the system prints out its responses. Typically, the user interacts with the program as follows: 1. The user types one or more inputphrasesP 1 ∙ ∙ ∙P n in the input area. Optionally, the phrases may be separated by periods. Section 1.4 spec- ifies what are the possible input phrases. 2. The user presses theProcessbutton. 3. The program sequentially processes the phrases contained in the input area, and prints the results in the output area. 4. The user presses theClearbutton to clear the input and output areas, and the process starts anew with step 1.

3

1.3.2 Using NDL in batch mode It is not necessary to use the graphical interface ofNDL one. Instead, can invokeNDL Let’s assume that the currentin so-called “batch mode.” directory is theNDLdirectory (c:\ndlin a Windows system, or~/ndlin a Unix system). Then if filefoocontains aNDLscript (see section 1.5), then typingndl fooat a DOS prompt (or./ndl fooat a Unix prompt) will load the filefoo, process the variousNDLphrases in it sequentially, and display the results to the standard output device (usually the screen). The user can choose to redirect the output to a file instead of the screen by specifying a second file name as the last command-line argument toNDL, as inndl foo.in foo.out. Note that any previous contents offoo.outwill be lost.

1.3.3 Loading files from the GUI Another way to process the contents of an entire file containing a NDL script is to chooseLoadfrom theFileoption of the main menu, and then use the graphical interface to browse your directory and select the appropriate file. Loading a file has the effect of opening up the file and processing all the phrases contained in it sequentially, sending the results to the output text area.

1.4 Input phrases An inputphraseis one of the following: 1. AdeductionD . Thesyntax and semantics of deductions will be covered in Section 1.9 and Section 1.10, respectively. (Terminological note: in this document the terms “deduction” and “proof” will be used inter- changeably.) 2. Asignature declaration. These are covered in Section 1.6. 3. Anassertionis simply a string of the form . This assertF 1 , . . . , F n where eachF i is aformula(formulas are discussed in Section 1.8).

4

1.5 NDL scripts A script is a sequence of phrases (signature declarations and/or assertions and/or deductions), possibly separated by periods. The following is a sample script: Constants Mary, Tom. Functions f:1, g:2. Relations P:1, Q:1, loves:2. assert (forall x (Tom loves x)). assume Mary loves Tom begin specialize (forall x (Tom loves x)) with Mary; both Tom loves Mary, Mary loves Tom end HereConstants Tom, MaryintroducesTomandMaryasconstant sym- bols. The phraseFunctions f:1, g:2declaresfandgto befunction sym- bols the declaration Similarly,of arity 1 and 2, respectively.Relations P:1, Q:1, R:2declaresPandQto be unaryrelation symbols(of arity 1) andloves to be a binary relation symbol (of arity 2). The keywordassumemarks the beginning of a deduction; we will cover deductions in Section 1.9.

1.6 Signature declarations Asignatureis a collection ofconstant symbolsand/orfuction symbolsand/or relation symbols symbols are just identifiers, where an identifier. Lexically, will be understood as any finite sequence of letters, digits, or underscores (_) that begins with a letter. 3 Constant symbolsc 1 , . . . , c n for anyn >0 can be introduced with the phrase Constantsc 1 , . . . , c n 3 With the exception of some predefined symbols such as numerals,=,+, etc.

5

For example: Constants pi, joe, ann, d23 Function symbolsf 1 , . . . , f n can be introduced with the phrase Functionsf 1 :r 1 , . . . , f n :r n wherer i is thearityoff i (the number of arguments that must be supplied in an application off i ). Example: Functions father:1,average:2 Hereaverageis declared to be a binary function symbol, andfathera unary one. Relation symbolsR 1 , . . . , R n can be introduced with the phrase RelationsR 1 :r 1 , . . . , R n :r n where againr i is the arity ofR i  instance, the phrase. For Relations male:1, likes:2, between:3 declaresmaleto be a unary relation,likesto be a binary relation, and betweento be a ternary one. Symbols can also be introduced via the GUI, by choosingSignature underOptionsat the top menu bar. NDLcomes with certain predefined symbols: 1.Predefined constant symbols:All numerals0,1,2,. . . 2.Predefined unary function symbols:^,!,++, --,$, @,? 3.Predefined binary function symbols:+, -, *, /, %,@ 4.Predefined binary relation symbols:=, !=, <, <=, >, >=, ==, &&,|| Note thatNDLwill ignore any attempts to redeclare a symbol that has already been introduced. The user can inspect the current signature at any given time by choosing Optionsfollowed byView current signaturefrom the top menu bar.

6

1.7 Terms Avariableis any identifier that is neither a reserved word (such asassume orexists will use the) nor a symbol (constant, function, or relation). We lettersx, y, z, andwas typical variables. Atermis either a constant symbol, or a variable, or else it is an expression of the formf(t 1 ,...,t n ), wherefis a function symbol of aritynand each t i is a term. We will use the letterssandtas typical variables. For instance,joe,father(joe), andaverage(x,y)are all legal terms. NDLallows infix syntax for all binary function symbols, e.g.x average y and2 + 5are alternative notations foraverage(x,y)and+(2,5). Subex- pressions in nested infix applications must be parenthesized, e.g.,2 * (5 + x).

1.8 Formulas There are three types of formulas inNDL:atomic formulas(or simply atoms);sentential formulas; andquantified formulas. We explain each in turn: 1. An atom is either the constanttrue; or the constantfalse; or else it is of the formR(t 1 ,. . .,t n ), whereRis a relation symbol of aritynand t 1 , . . . , t n  Anare terms. example of an atom isbetween(x,y,z). Infix notation is allowed in the case of binary relation symbols, for instance foo = 2 x * 3 < 15 father(joe) loves mary 2. A sentential formula is either: (a) anegation~Ffor any formulaF; (b) aconjunctionF 1 &F 2 for any formulasF 1 , F 2 ; (c) adisjunctionF 1 \/F 2 for any formulasF 1 , F 2 ; (d) aconditionalF 1 ==>F 2 for any formulasF 1 , F 2 ; or (e) abiconditionalF 1 <==>F 2 for any formulasF 1 , F 2 .

7

The negation sign ˜ binds tighter than all other four connectives. Con- junctions and disjunctions have equal precedence, bind tigher than con- ditionals and biconditionals, and associate to the right. Conditionals and biconditionals have equal precedence and associate to the right. Accordingly, A & ~B \/ C ==> D & E is parsed as [A & ((~B) \/ C)] ==> [D & E] To override these conventions, use parentheses or square brackets. 3. A quantified formula is either of the form(forallx F)(auniversal quantification); or(existsx F)(aexistential quantification) for any variablexand formulaF can also be used for grouping, so. Brackets we can write[existsx F]instead of(existsx F). We will use the lettersFandGas typical formulas. We assume the reader is familiar with notions such as free and bound variable occurrences. These are defined in the standard way. Two formulas are said to bealphabetically equivalentiff each can be obtained from the other by consistently renaming bound variables. Alphabetically equivalent formulas will be viewed as identical. We writeF[x7→t] to denote the formula obtained fromFby replacing every occurrence ofxin it by the term t, renaming bound variables if necessary in order to avoid variable capture.

1.9 Proof syntax The following grammar describes the syntax ofNDLproofs: D::=RuleApp|assumeF D|p-pesboausdusrF D|D 1 ;D 2 |FBYD|beginDend |pick-anyx D |pick-witnesswfor (existsx F)D |specialize (forallx F) witht |ex-generalize (existsx F) fromt |congf(s 1 ,...,s n ) =f(t 1 ,...,t n ) froms 1 =t 1 ,...,s n =t n = |rel-congR(t 1 ,...,t n ) fromR(s 1 ,...,s n ),s 1 =t 1 ,...,s n t n

8

where the syntax of inferencerule applicationsis as follows: RuleApp::=modus-ponensF==>G,F |modus-tollensF==>G,~G | ~double-negation ~F |absurdF,~F |left-andF&G |right-andF&G |bothF,G |left-eitherF,G |right-eitherF,G |casesF 1 \/F 2 ,F 1 ==>G,F 2 ==>G |left-iffF<==>G |right-iffF<==>G |equivF==>G,G==>F |reft |swaps=t |trant 1 =t 2 ,t 2 =t 3

Proofs of the formD 1 ;D 2 are calledcomposite. Proofs of the form assumeF D are calledconditional(orhypothetical) proofs. The formulaFis called the hypothesisand the subproofDis called thebodyof the conditional proof. We say that the bodyDrepresents thescopeof the hypothesisF. Proofs of the formsuppose-absurdF Dare called proofsby contradiction with. As conditional proofs,Fis called thehypothesisandD—the scope ofF—is called thebody. Proofs of the form pick-anyx D are calleduniversal generalizations. We refer to the variablexas aneigen- variable of the form. Proofs pick-witnesswfor (existsx F)D

9

are calledexistential specializations. We refer to the variablewas thewitness variable; we also say thatw of the form Proofsis an eigenvariable. specialize (forallx F) witht are calleduniversal specializations, while proofs of the form ex-generalize (existsx F) fromt are calledexistential generalizations of the form. ProofsFBYDare called conclusion-annotatedproofs. assume,suppose-absurd,pick-any,pick-witness, andBYall bind tighter than the composition operator;. For example, assume A claim A; claim true is parsed as the composition ofassume A claim Aandclaim true,not as the hypothetical proof withAas the hypothesis and the composition claim A; claim trueas the body. The composition operator;associates to the right, meaning that D 1 ;D 2 ;D 3 is parsed as D 1 ;(D 2 ;D 3 ) (1.1) and not as (D 1 ;D 2 );D 3 (1.2) This is an important convention, because proof composition inNDLisnot associative—proofs (1.1) and (1.2) do not have the same semantics. This will become more clear in the sequel. These conventions can be overriden by usingbegin–endpairs. Finally, we note thatpick-anyandpick-witnessare variable-binding constructs; they introduce variablescope particular, in a deduction of the. In form pick-anyx D we say that the scope of the eigenvariablexis the deductionD. And in a deduction of the form pick-witnesswfor (existsx F)D 10