A Logic of Non-Monotone Inductive Definitions MARC DENECKER K.U.Leuven, Belgium EUGENIA TERNOVSKA Simon Fraser University, Canada 5 0 0 Well-known principles of induction include monotone induction and different sorts of non- 2 monotone inductionsuchasinflationaryinduction,inductionoverwell-foundedsetsanditerated induction. Inthiswork,wedefinealogicformalizinginductionoverwell-foundedsetsandmono- n tone and iterated induction. Just as the principle of positive induction has been formalized in a J FO(LFP),andtheprincipleofinflationaryinductionhasbeenformalizedinFO(IFP),thispaper formalizes the principleof iterated induction ina new logic for Non-Monotone Inductive Defini- 3 tions (ID-logic). The semantics of the logic is strongly influenced by the well-founded semantics 1 oflogicprogramming. OurmainresultconcernsthemodularitypropertiesofinductivedefinitionsinID-logic. Specif- ] I ically, we formulate conditions under which a simultaneous definition ∆ of several relations is A logically equivalent to a conjunction of smaller definitions ∆1∧···∧∆n with disjoint sets of . defined predicates. The difficulty of the result comes from the fact that predicates Pi and Pj s definedin∆iand∆j,respectively,maybemutuallyconnectedby simultaneousinduction. Since c logic programming and abductive logic programming under well-founded semantics are proper [ fragmentsofourlogic,ourmodularityresultsareapplicablethereaswell. 1 CategoriesandSubjectDescriptors: ... [...]: ... v 5 2 0 1 0 1. INTRODUCTION 5 This paper fits into a broad project aiming at studying general forms of inductive 0 definitions and their role in diverse fields of mathematics and computer science. / s Monotone inductive definitions andinductive definability havebeen studied exten- c : sively in mathematical logic [Moschovakis 1974a; Aczel 1977]. The algebraic foun- v dations for monotone induction are laid by Tarski’s fixpoint theory of monotone i X lattice operators [Tarski 1955]. The notion of inductive definition is the under- r lying concept in fixpoint logics [Gurevich and Shelah 1986; Dawar and Gurevich a 2002] which found its applications in e.g. database theory [Abiteboul et al. 1995] and descriptive complexity theory [Immerman 1999; Ebbinghaus and Flum 1999]. Author’s address: M.Denecker, Department of Computer Science, K.U.Leuven, elestijnenlaan 200A, B-3001 Heverlee, Belgium. Phone: +32 16 327544 — Fax: +32 16 327996. email: [email protected] Author’saddress: Permission to make digital/hard copy of all or part of this material without fee for personal or classroom use provided that the copies are not made or distributed for profit or commercial advantage,theACMcopyright/servernotice,thetitleofthepublication,anditsdateappear,and notice is given that copying is by permissionof the ACM, Inc. To copy otherwise, to republish, topostonservers,ortoredistributetolistsrequirespriorspecificpermissionand/orafee. (cid:13)c 2008ACM1529-3785/2008/0700-0001 $5.00 ACMTransactionsonComputationalLogic,Vol.V,No.N,February2008,Pages1–50. · 2 Marc Deneckerand Eugenia Ternovska Logicswithfixpointconstructsto represent(monotone)inductive andco-inductive definitions play a central role as query and specification languages in the area of verification of dynamic systems using modal temporal loics such as the µ-calculus [Kozen 1983]. Induction axioms have been used succesfully in the context of prov- ing properties of protocols using specialised automated reasoning tools [Paulson 1998]. The concept of definitions and definitional knowledge is also fundamental in the area of description logics [Brachman and Levesque 1982], the class of logics that evolved out of semantic networks. Importantly, complexity results in fixpoint logic and logic programming suggest that inductive definitions often combine high expressivitywithlowcomplexity. Thus,itappearsthatthenotionofdefinitionand its inductive generalisations emerges as a unifying theme in many areas of math- ematics and computational logic. Hence, its study could improve insight in the interrelations between these areas and lead to synergy between them. In this paper, we are concerned with non-monotone inductive definitions. A familiar example of a non-monotone inductive definition is the definition of the satisfaction relation |= between a truth assignment I and a formula. In case of propositional logic, this relation is defined by induction over the subformula order on formulas: - I |=p if p∈I, - I |=ψ∧φ if I |=ψ and I |=φ, - I |=ψ∨φ if I |=ψ or I |=φ, - I |=¬ψ if I 6|=ψ. This inductive definition is non-monotone because of its last rule, which adds the pair (I,¬ψ) to the truth relation if the pair (I,ψ) does not belong to it. This is an example of an inductive definition over a well-founded order. Recently, the au- thors of [Denecker 1998; Denecker et al. 2001a] investigated certain non-monotone formsofinductivedefinitionsinmathematicsandpointedoutthatsemanticalstud- ies in the area of logic programming might contribute to a better understanding of such generalised forms of induction. In particular, it was argued that the well- foundedsemanticsoflogicprogramming[VanGelderetal.1991]extendsmonotone induction and formalises and generalises non-monotone forms of induction such as induction over well-founded sets and iterated induction [Feferman 1970; Buchholz etal.1981]. In[Deneckeretal.2000;Deneckeretal.2004],thewell-foundedseman- tics was further generalised into a fixpoint theory of general non-monotone lattice operators. This theory, called approximation theory, generalises Tarski’s theory of fixpoints of monotone lattice operators and provides the algebraic foundation of the principle of iterated induction. Later, it turned out that the same principle is fundamental in an area of artificial intelligence concerned with using logic for knowledge representation — non-monotonic reasoning1. In particular, [Denecker et al. 2000; Denecker et al. 2003] demonstrated that the semantics of three major 1The term “non-monotone” has a different meaning in the context of inductive definitions than in the context of non-monotone reasoning. A logic is non-monotone when adding formulas to a theory may not preserve inferred formulas. A monotone definition is one inducing a monotone operator. In fact, the fragment of monotone inductive definitions in ID-logic is a non-monotone logic. ACMTransactionsonComputationalLogic,Vol.V,No.N,February2008. · A Logic of Non-Monotone Inductive Definitions 3 approaches to non-monotonic reasoning, default logic [Reiter 1980], autoepistemic logic [Moore 1985] and logic programming [Lloyd 1987] are described by approxi- mationtheory. Thus,generalisedinductive definitions alsoplayafundamentalrole in the semantics of knowledge representation formalisms. Inaseminalpaperonknowledgerepresentation,BrachmanandLevesque[Brach- man and Levesque 1982]had observedthat definitional knowledge is an important component of human expert knowledge. Motivated by this work, the author of [Denecker2000]extendedclassicallogicwithnon-monotoneinductivedefinitionsin ordertodemonstratethatgeneralnon-monotoneinductiveformsofdefinitionsalso play an important role in knowledge representation. In this paper, we extend this work. The contributions of the paper are the following: —WeformalizetheprincipleofiteratedinductioninanewlogicforNon-Monotone Inductive Definitions (ID-logic). This logic is an extension of classical logic with non-monotone inductive definitions, and is a generalisationof the logic that was defined in [Denecker 2000]. —We demonstrate that different classes of definitions can be correctly and unifor- mally formalised in our logic. To achieve this goal, we present an alternative formalisationof these classes in classicalfirst- or second-orderlogic, and provide an equivalence-preserving transformation from ID-logic to these formalisations. —Westudymodularitypropertiesofnon-monotoneinductivedefinitionsinID-logic and provide a set of techniques that allow one to break up a big definition into a conjunction of smaller and simpler definitions. The main result of the paper is a set of formal conditions that guarantee that a simultaneousdefinitionofseveralpredicatescanbe splitupintothe conjunctionof components of this definition, each component defining some subset of the defined predicates. In addition, our theorems provide conditions under which joining a set of definitions for distinct sets of predicates into one simultaneous definition of all these predicates is equivalence preserving. The problemthat we study is similar to that studied in [Verbaeten et al. 2000], but our results are uniformally stronger in the sense that they are proven for a more expressive logic and under more general conditions. Theresultsareimportantbecausemodularityisacrucialpropertyinformalveri- ficationandknowledgerepresentation[Reichgelt1991]. Forexample,itisimportant to be able to specify a complex synamic system by describing its components in independent modules which can then be conjoined to form a correctdescription of the complete system. Thus, the operation of joining modules should preserve the correctness of the component modules. The dual operation of splitting a complex theoryintoanequivalentsetofsmallermodulesisequallyimportant. Itallowsone toinvestigatecomplextheoriesbystudyingitsmodulesindependently,andreduces the analysis of the correctness of the complex theory to the much simpler problem of analysing the correctness of its modules. The paper is structured as follows. In Section 2, we discuss various forms of induction and their formalisations. This discussion provides the intuitions and the motivation for defining the new logic. Section 3.1 introduces some preliminaries from logic and lattice theory. In section 4, we extend classical logic with the gen- eralised non-monotone definitions. In section 6, the modularity of the definition ACMTransactionsonComputationalLogic,Vol.V,No.N,February2008. · 4 Marc Deneckerand Eugenia Ternovska expressions is investigated. In section 7, we present equivalence-preserving trans- formations from ID-logic to first-order and second-order logic for different familiar types of definitions. Here, the modularity techniques developed in the previous section are used as a tool to prove correctness of the transformations. 2. FORMAL STUDY OF INDUCTIVE DEFINITIONS Mathematical induction refers to a class of effective construction techniques used in mathematics. There, a set is frequently defined as the limit of a process of iterating some operation. Often, mathematicians describe such a construction by aninductivedefinition. Thecoreofaninductivedefinitioninmathematicsconsists of one or more basic rules and a set of inductive rules. Basic rules represent base casesoftheinductionandaddelementsto thedefinedsetinanunconditionalway; inductive rules addnew elements to the set if one canestablishthe presence orthe absence of other elements in the set. The defined set is obtained as the limit of some process of iterated application of these rules. In this section, we discuss various forms of such inductive definitions and how theyareformalised. Thenwemotivateandpreviewanewformallogicofdefinitions. Thesectionispartiallybasedonideaspresentedearlierin[Denecker1998;Denecker et al. 2001a]. 2.1 Monotone Inductive Definitions. Inamonotoneinductivedefinition,thepresenceofnewelementsinthesetdepends onlyonthepresenceofotherelementsinthedefinedset,notontheabsenceofthose. Thedefinedsetistheleastsetclosedunderapplicationoftherules. Suchdefinitions are frequent in mathematics. A standard example is the transitive closure of a directed graph: The transitiveclosureT ofadirectedgraphGisinductively definedas G the set of edges (x,y) satisfying the following rules: —(x,y)∈T if (x,y)∈G; G —(x,y)∈T if for some vertex z, (x,z),(z,y)∈T . G G Other typical examples are the the definition of a subgroup generated by a set of group elements, or the definitions of a term, formula, etc. in logic. Monotone inductive definitions have been studied extensively in mathematics [Moschovakis1974a;Aczel 1977]. In [Moschovakis1974a],such a definition is asso- ciated with a formula ϕ(x¯,X). Intuitively, this formula encodes all the conditions underwhichtuplex¯belongstothedefinedpredicateX. Theformulaϕ(x¯,X)must be positive in X, that is no occurrence of X may appear in the scope of an odd number of occurrences of the negation symbol ¬. For instance, for the transitive closure example above we have: ϕ ((x,y),T ):=G(x,y)∨∃z(T (x,z)∧T (z,y)). trans G G G Each disjunct in this formula formally expresses the condition of one of the rules in the informal definition. Given a structure I which interprets all constant symbols, the formula ϕ(x¯,X) characterisesanoperatorΓ mappingarelationRtotherelationR′ consisting ϕ(x¯,X) ACMTransactionsonComputationalLogic,Vol.V,No.N,February2008. · A Logic of Non-Monotone Inductive Definitions 5 of tuples a¯ such that ϕ(a¯,R) is true in I. In general, Γ may have multiple ϕ(x¯,X) fixpoints, but the fact that ϕ(x¯,X) is a positive formula implies that the operator is monotone and has a least fixpoint, which is the relation inductively defined by ϕ(x¯,X). A logic to represent monotone inductive definitions is the least fixpoint logic FO(LFP) (see, e.g. [Ebbinghaus and Flum 1999]). 2.2 Inductive Definitions over a Well-Founded Order. In a non-monotone inductive definition, the presence of new elements in the set depends on the absence of certain elements in the defined set. An example of such a definition is the definition of the truth relation given in the introduction. Let us consider another definition with a similar structure. The setofevennumbersisdefinedbyinductionoverthe standardorder ≤ on the natural numbers: —0 is an even number; —n+1 is an even number if n is not an even number. Thedefinitionsofevennumbersandof|=areexamplesofinductivedefinitionsover well-founded orders. Such a definition describes the membership of an element in the defined relation in terms of the presence or absence of elements in the defined relationthatarestrictlysmallerwithrespecttosomewell-founded(pre-)order. By applying this definition to the minimal elements and then iterating it for higher levels, the defined predicate can be constructed, even if some inductive rules are non-monotone. This type of inductive definitions is fundamentally different from monotone inductive definitions. Indeed, the set defined by a monotone inductive definitioncanbecharacterisedastheleastsetclosedundertherules. Incontrast,a definition over a well-founded order does not characterise a unique least set closed underits rules. Forinstance,{0,2,4,6,...}and{0,1,3,5,7,...}arebothminimal sets closed under the above rules. Usingthesamerepresentationmethodologytorepresentthisinductivedefinition as in the monotonic case, we would obtain the formula ϕ (x,E):=x=0∨∃y(x=S(y)∧¬E(y)). even In the context of the natural numbers, the operator characterised by this formula is non-monotone and maps any set S of natural numbers to the set consisting of 0 and all successors of all numbers in the complement of S. This is a non-monotone operator which has the set of even numbers as unique fixpoint. In general, the set defined by this type of inductive definitions can be characterised as the unique fixpoint of the operator associated to the definition. This will be formalised in section 7. Other examples of non-monotone inductive definitions over well-founded orders are given in [Denecker et al. 2001a]. They include a definition of the concept of a rank of an element in a well-founded set (the rank of an element x is the least ordinal strictly larger than the rank of all y < x), and a definition of the levels of a monotone operator in the least fixpoint construction. Although induction over a well-founded set is a common principle in mathematics, to our knowledge it has not been studied explicitly in mathematical logic. However, we will argue below that it can be seen as a simple form of iterated induction. ACMTransactionsonComputationalLogic,Vol.V,No.N,February2008. · 6 Marc Deneckerand Eugenia Ternovska 2.3 Inflationary Induction. In order to extend his theory of inductive definitions to the class of all defini- tions (monotone and non-monotone), Moschovakis [Moschovakis 1974b] proposed the following approach. The idea is to associatewith an arbitraryformula ϕ(x¯,X) (possibly non-positive) the operator Γ′ , where ϕ(x¯,X) Γ′ (R):=Γ (R)∪R. ϕ(x¯,X) ϕ(x¯,X) Operator Γ′ is not monotone, but it is inflationary, that is, for every R, ϕ(x¯,X) R ⊆ Γ′ (R). Thus, by iterating this operator starting at the empty relation, ϕ(x¯,X) an ascending sequence can be constructed. This sequence eventually reaches a fixpoint of Γ′ . This fixpoint was later called the inflationary fixpoint, and ϕ(x¯,X) the correspondinglogicFO(IFP)wasintroduced[GurevichandShelah1986]. This logic introduces inflationary, and its dual, deflationary, fixpoint constructs. The inflationaryfixpointlogicplayedanimportantroleindescriptivecomplexitytheory and has been used to characterize the complexity class PTIME [Immerman 1986; Livchak 1983; Vardi 1982]. Inflationary induction and induction over a well-founded order are two different principles. Consider, for example, the definition of the even numbers presented above. The formula ϕ is a natural representation of this definition. However, even the inflationary fixpoint [IFP ϕ ]t¯is the set of all natural numbers. Indeed, x¯,E even ∅∪Γ (∅)=NandN∪Γ (N)=N. Eventhoughitispossibletowritedowna ∆even ∆even definitionofthe evennumbersusinginflationaryfixpoints,suchanencodingwould beneithernaturalnordirect. Itwouldnotreflectthewayinwhichmathematicians expressinductionoverawell-foundedorder. Sinceourgoalistoformalisethelatter sort of induction in a way that reflects the natural rule-based structure in which mathematicians represent such definitions, this paper will not be concerned with inflationaryfixpoints. For examples where inflationaryand deflationaryinductions naturallyappear,weaddressthereadertotheworkbyGr¨adelandKreutzer[Gra¨del and Kreutzer 2003]. 2.4 Iterated Inductive Induction. The basic idea underlying induction is to iterate a basic construction step until a fixpoint is reached. In an iterated induction, this basic construction step itself is a monotone induction. That is, an iterated inductive definition constructs an object as the limit of a sequence of constructive steps, each of which itself is a monotone induction. One can formulate the intuition of the iterated induction of a structure also in the following way. Given a mathematical structure M of 0 functions and relations, a positive or monotone inductive definition defines one or morenewrelationsintermsofM . Thedefinitionofthesenewrelationsmaydepend 0 positively or negatively on the relations given in M . Once the interpretation of 0 the new relationsisfixed, M canbe extended withthese, yielding anew extended 0 structure M . On top of this structure, again new relations may be defined in the 1 similar way as before. The definition of these new predicates may now depend positively or negatively on the relations that were defined in M . This modular 1 principle can be iterated arbitrarily often, possibly a transfinite number of times. We call this informal principle the principle of Iterated Induction. In general, an ACMTransactionsonComputationalLogic,Vol.V,No.N,February2008. · A Logic of Non-Monotone Inductive Definitions 7 iterated inductive definition must describe, in a finite way, a possibly transfinite sequence of monotone or positive definitions of sets. If the definition of a set depends (positively or negatively) on another defined set, then this other set must be defined in an earlier definition in this sequence. An example of an iterated inductive definition mentioned in [Denecker et al. 2001a]isthedefinitionofthestabletheoryofsomepropositionaltheoryT. Basically, this is the standard concept of deductive closure of a propositional theory T under a standard set of inference rules augmented with two additional inference rules: ⊢ψ 6⊢ψ and . ⊢Kψ ⊢¬Kψ Note that the second rule is non-monotone. The stable theory of T is a deduc- tivelyclosedmodaltheorywhichcontainsexplicitformulasrepresentingwhetherT “knows” a formula ψ or not. It can be viewed as the set of formulas known by an ideally rationalagent with perfect introspection whose base beliefs are represented by T. Letusconsiderthisinductionprocessinmoredetail. Wedefinethemodalnesting depthofaformulaF asthelengthnofthe longestsequence(KF ,KF ,...,KF ) 1 2 n such that F contains KF and F contains KF for each 1≤i<n. The start of 1 i i+1 the iterated induction is a monotone induction closing T under the propositional logic inference rules. This yields a deductively closed set T of propositional for- 0 mulas of modal nesting depth 0. Next we apply the two modal inference rules to infer modal literals Kψ or ¬Kψ, for each propositional formula ψ. After comput- ing these literals,we reapplythe first stepand derive,using the standardinference rules, all logical consequences with modal nesting depth being less or equal to 1. Thisprocesscannowbeiteratedforformulaswithincreasingmodalnestingdepth. The result of this construction process is the stable theory of T and contains for- mulas of arbitrary modal nesting depth. It was shown in [Marek 1989] that the stable theory of T is exactly the collection of all modal formulas that are true in thepossibleworldsetW consistingofallmodelsofT. Moreprecisely,itholdsthat thestabletheoryofT isthe setofallmodalformulasF suchthatforthecollection W of models of T and for each model M ∈W, it holds that W,M |=F. Iterated Induction is a generalisation of monotone induction. It is also related to induction over a well-founded order. The link is seen if we split up a definition ofthe latter kindin aninfinite number ofdefinitions, eachdefining a single ground atom, and ordering or stratifying2 these definitions in a sequence compatible with the well-ordering. For example, even numbers could be defined by the following iterated definition: (0) 0 is even (1) 1 is even if 0 is not even (2) 2 is even if 1 is not even ... (n+1) n+1 is even if n is not even ... 2This stratification corresponds to the notion of local stratification in logic programming [Przy- musinski1988]. ACMTransactionsonComputationalLogic,Vol.V,No.N,February2008. · 8 Marc Deneckerand Eugenia Ternovska Clearly, the iterated induction described here constructs the set of even numbers. Wecanthusviewaninductivedefinitioninawell-foundedsetasaniteratedinduc- tive definitionconsistingofasequence ofnon-inductive (recursion-free)definitions. Iterated induction is more general than induction over a well-founded set because positive recursion within one level may be involved (as illustrated by the stable theory example). Thelogicalstudyofiteratedinductionwasstartedin[Kreisel1963]andextended inlater studies ofso-calledIteratedInductive Definitions (IID) in [Feferman1970], [Martin-L¨of1971],and[Buchholzetal.1981]. The IID formalismdefined in[Fefer- man 1970; Buchholz et al. 1981] is a formalism to define sets of natural numbers through iterated induction. To represent an iterated inductive definition of a set H, one associates with each natural number an appropriatelevel index, an ordinal number. Thislevelindexcanbeunderstoodastheindexofthesubdefinitionwhich determines whether the number belongs to the defined set or not. The iterated in- ductivedefinitionisdescribedbyafiniteparametrisedformulaϕ(n,x,P,H),where n represents a level index, x is a natural number, P is a unary predicate variable with only positive occurrences in ϕ and ranging over natural numbers, and H is the defined relation represented as a binary predicate ranging over tuples (n,x) of naturalnumbersxandtheirlevelindicesn. Theformulaϕ(n,x,P,H)encodesthat n is the level index of x, and x can be derived (using the inductive definition with level index n) from the set P and the restriction of H to tuples with level index < n. Using ϕ, the set H is characterised by two axioms. The first one expresses that H is closed under ϕ: ∀n∀x (ϕ(P(σ)/H(n,σ))→H(n,x)). Inthisformula,ϕ(P(σ)/H(n,σ))(whereσisanarbitraryterm)denotestheformula obtained from ϕ by substituting H(n,σ) for each expression P(σ). The secondaxiomis a second-orderaxiomexpressingthat for eachn, the subset {x | (n,x)∈H} of N is the least set of natural numbers closed under ϕ: ∀n∀P [∀x (ϕ→P(x))→∀x (H(n,x)→P(x))]. As an example, let us encode the non-monotone definition of even numbers in the IID-formalism. It is a definition by induction on the standard order of natural numbers which means that we can take a natural number and its level index to be identical. The formula ϕ to be inserted in the axioms above is3: (n=0∧x=0)∨∃y(n=s(y)∧x=s(y)∧¬H(y,y)∧y <n). This formula represents that (n,x) can be derived if x and its level index n are identical and if x=0 or if the predecessor of x is not even. 2.5 A Preview of ID-Logic Inthispaper,wedesignalogicforformalisingseveralformsofinductivedefinitions. Just as the principle of Monotone Induction has been formalised in FO(LFP), the principle of Inflationary Induction has been formalized in FO(IFP), the principles 3The formula doesn’t contain the predicate variable P because this is a definition over a well- foundedorderwhichdoesnotinvolvemonotoneinduction. ACMTransactionsonComputationalLogic,Vol.V,No.N,February2008. · A Logic of Non-Monotone Inductive Definitions 9 of Induction over a well-founded order and Iterated Induction are captured by our logic. We call it a Logic for Non-Monotone Inductive Definitions (ID-logic). The logic is designed as an extention of classical logic with definitions. A defini- tion will be represented as a set of rules of the form: ∀x¯(P(x¯)←ψ), where P is a relational symbol defined by the definition, and ψ an arbitrary first- order formula. For example, the non-monotone definition of even numbers will be represented by the set: ∀x(E(x)←x=0), . (cid:26)∀x(E(s(x))←¬E(x))(cid:27) From a representational point of view, this syntax has some interesting features: —Rule-based representation. Formalisationsof definitions in ID-logic preserve the rule-based structure of definitions in mathematics. Stated differently, rules in a mathematical definition can be formalised in a modular way by definitional rules in an our logic. —Uniform formalisation of different types of definitions. Syntax and se- manticsofID-logicisdesignedforuniformformalisationofnon-inductive(recursion- free)definitions,positiveormonotoneinductivedefinitions,definitionsoverwell- founded sets and iterated inductive definitions. —No explicit level mapping. A model of an ID-logic definition is constructed following the natural dependency order on defined atoms that is induced by the rules. As a consequence, and contrary to the IID-formalism of the previous section, there is no need to explicitly represent a level mapping of an iterated inductive definition. —Simultaneous induction. Consider for example the following simultaneous inductive definition of even and odd numbers: ∀x(E(x)←x=0), ∀x(E(s(x))←O(x)),. ∀x(O(s(x)) ←E(x))  —A logic with second-order variables. ID-logicallows second-order variables and quantification. As an example, consider the following sentence of ID-logic: ∀x(P(x)←x=0), ∃P( ∧∀x P(x)). (cid:26)∀x(P(s(x)) ←P(x))(cid:27) This axiom, stating that the least set P containing 0 and closed under the suc- cessoroperationcontainsalldomainelements,is anID-logicformalisationofthe second-order induction axiom of the natural numbers. ThemaindifferencesbetweenID-logicandtheIID-formalismofSection2.4areits rule-based nature and the absence of an explicit encoding of a level mapping. The rules of an inductive definition induce an implicit dependency order on the defined atoms. For example, in the definition of even numbers, the rule ∀x(E(s(x)) ← ¬E(x)) induces adependencyofeachatomE[n+1]ontheatomE[n]. Notice that the transitive closure of this dependency relation corresponds with the standard ACMTransactionsonComputationalLogic,Vol.V,No.N,February2008. · 10 Marc DeneckerandEugenia Ternovska order of the natural numbers, the well-founded order over which the set of even numbers is defined by this definition. This suggests that the encoding of the level mapping in the IID-formalism only adds redundant information to the definition. In ID-logic, the construction of the model of a definition proceeds by following theimplicitdependencyorderthatisinducedbytherules. Thetechniquetodothis was developed in logic programming. In [Denecker 1998; Denecker et al. 2001a], Deneckerproposedthethesisthatthewell-foundedsemanticsoflogicprogramming [VanGelderetal.1991]providesageneralandrobustformalizationoftheprinciple of iterated induction. In Section 4, we recall this argument and show how the construction of the well-founded model can be seen as an iterated induction which follows the natural dependency order induced by the rules. 3. PRELIMINARIES 3.1 Preliminaries from Logic We begin by fixing notation and terminology for the basic syntactic and semantic notions related to first- and second-order logic. We assume an infinite supply of distinct symbols, which are classified as follows: 1. Logical symbols: a) Parentheses: (,); b) Logical connectives: ∧, ¬; c) Existential quantifier: ∃; d) Binary equality symbol: = (optional); e) Two propositional symbols: t and f. 2. Non-logical symbols: a) countably many object symbols. Object symbols are denoted by low-case letters; b) for each positive integer n > 0, countably many n-ary function symbols of arity n. Function symbols are denoted by low-case letters; c) foreachpositiveintegern,countablymanyn-aryrelationsymbols,alsocalled predicate or set symbols of arity n. We use upper-case letters to denote pred- icates. Asusual,weidentifyobjectsymbolswith0-aryfunctionsymbolsandpropositional symbols with predicate symbols of arity 0. Remark 3.1. In most parts of this paper, we do not make a formal distinction betweenvariableandconstantsymbols. Symbolsoccurringfreeinaformulacanbe viewedasconstants;symbolsinthescopeofaquantifiercanbeviewedasvariables. In examples, we tend to quantify over x, y, X, Y, and leave c, g, f and P, Q free and treat them as constants. Wedefineavocabularyasanysetofnon-logicalsymbols. Wedenotevocabularies by τ, τo,.... We shall denote the set of function symbols of τ by τ , and we use ∆ fn σ, σ , σ etc., to refer to an arbitrary symbol of the vocabulary. We write σ¯ to 1 2 denote asequence ofsymbols(σ ,σ ,...)or,depending onthe context,simply the 1 2 set of symbols {σ ,σ ,...}. Likewise, X¯ denotes a sequence or a set of relational 1 2 ACMTransactionsonComputationalLogic,Vol.V,No.N,February2008.