Automating Quantified Conditional Logics in HOL

1 Introduction

Conditional logics (CL), known also as logics of normality or typicality, have many applications including action planning, counterfactual reasoning, default reasoning, deontic reasoning, metaphysical modeling and reasoning about knowledge. While there is broad literature on propositional CLs only a few authors have addressed first-order extensions, those include Delgrande [1998] and Friedman et al. [2000].

This paper presents (in Sec. 2)-as first contribution-a notion of quantified conditional logics (QCLs) that includes quantification over propositional and first-order variables, a combination that has not been addressed yet. An adequate semantics of conditionality ()) is achieved by adapting selection function semantics [Stalnaker, 1968; Chellas, 1975]. Regarding quantification over individuals constant domains and varying domains are supported. The treatment of propositional quantification is inspired by Fitting's [2002] work on quantified modal logics. Employing propositional quantification is particularly useful for flexible automation of objectand meta-level reasoning. For example, 'syntactic' conditional logic axioms such as 8P(P ) P) (cf. Ex. 2) can simply be postulated and even interesting meta-properties, including correspondence and dependence/independence results for such axioms can be automatically established. When combining logics, bridge principles play a crucial role. Using propositional quantification such bridge principles can again be simply postulated as axioms. In traditional systems they are often most challenging to implement.

⇤This work has been supported by the German Research Foundation under grant BE2501/9-1.

A semantic embedding of propositional CLs in classical higher-order logic HOL (Church's [1940] type theory; cf. Sec. 3) has been presented by Benzm¨uller et al. [2012a]. This embedding exploits the natural correspondence between selection function semantics and HOL. In fact, selection function semantics can be seen as an higher-order extension of well-known Kripke semantics for modal logic and cannot be naturally embedded into first-order logic.

This paper extends-as second contribution-the embedding of Benzm¨uller et al. [2012a] to also include quantification over propositional and individual variables, the latter w.r.t. constant nd varying domains (Sec. 4). This embedding of QCL in HOL is shown sound and complete (in Sec. 5).

So far, the work on first-order CLs has focused mainly on theory and practically available prover implementations do not exist. Due to the timeliness and the broad range of CL applications, implementations and evaluations of respective provers should be strongly fostered though.

Therefore this paper offers-as third contribution-an elegant solution to automate QCLs with off-the-shelf theorem provers and model finders for HOL. A unique feature of the embeddings-based approach is that it supports both reasoning at the object-level and at the meta-level. This will be illus-

A discussion of related and future work concludes the paper (in Secs. 7 and 8).

2 Quantified Conditional Logics

Propositional CLs are extended with quantification over propositional variables and over individual variables. Regarding the latter constant domains (every possible world has the same domain) and varying domains (different possible worlds may have different domains) are supported; in this regard the framework below is related to that of Delgrande [1998]. However, the inclusion of propositional quantification is novel. The gained expressivity is of crucial significance for the automation of QCLs with HOL provers and model finders (cf. Sec. 6).

DEF. 2.1 (QCL) Let IV be a set of first-order (individual) variables, PV a set of propositional variables, and SYM a set of predicate symbols of any arity. Formulas of QCL are given by the following grammar (where Xi 2 IV↪ P 2 PV↪ k 2 SYM, and where ) represents conditionality):

From this set of primitive connectives, other logical connectives can be introduced as abbreviations: for example, '^ , ' ! (material implication), ' $ and 2' abbreviate ≻(≻' _ ≻ ), ≻' _ , (' ! ) ^ ( ! ') and ≻' ) ', respectively. 8co and 8va are associated with constant domain and variable domain quantification. For ⇤ 2 ¶co↪ va♦, 9⇤X' abbreviates ≻8⇤X≻'. Syntactically, QCL can be seen as a generalization of quantified multimodal logic where the index of modality ) is a formula of the same language. For instance, in (' ) ) ) δ the subformula ' ) is the index of the second occurrence of ).

Regarding semantics, different formalizations have been proposed (see [Nute, 1980]). The work presented here builds on selection function semantics [Stalnaker, 1968; Chellas, 1975], which is based on possible world structures and has been successfully used by Olivetti et al. [2007] to develop proof methods for some propositional CLs.

DEF. 2.2 (Interpretation) An interpretation is a structure M = hS↪ f↪D↪D0 ↪Q↪ Ii where, S is a set of possible items called worlds, f : S ⇥ 2S 7! 2S is the selection function, D is a non-empty set of individuals (the constant first-order domain), D0 is a function that assigns a non-empty subset D0 (w) of D to each possible world w (the D0 (w) are the varying domains), Q is a non-empty collection of subsets of W (the propositional domain), and I is a classical interpretation function where for each n-ary predicate symbol k, I(k↪ w) ✓ Dn .

DEF. 2.3 (Assignment) A variable assignment g = (gi ↪ gp ) is a pair of maps where, gi : IV 7! D maps each individual variable in IV to an object in D, and gp : PV 7! Q maps each propositional variable in PV to a set of worlds in Q.

DEF. 2.4 (Satisfiability) Satisfiability of a formula ' for an interpretation M = hS↪ f↪D↪D0 ↪Q↪ Ii, a world s 2 S, and a variable assignment g = (gi ↪ gp ) is denoted as M↪ g↪ s ♣= ' and defined as follows, where [a◁Z]g denotes the assignment identical to g except that ([a◁Z]g)(Z) = a:

DEF. 2.5 (Model, validity) An interpretation M = hS↪ f↪D↪ D0 ↪Q↪ Ii is a QCL model if for every variable assignment g and every formula ', the set of worlds ¶s 2 S ♣ M↪ g↪ s ♣= '♦

is a member of Q. (This requirement, which is inspired by Fitting [2002], Def. 3.5, ensures a natural correspondence to Henkin models in HOL; cf. Sec. 5 and Footnote 4; cf. also Benzm¨uller and Paulson [2013].) As usual, a conditional formula ' is valid in a QCL model M = hS↪ f↪D↪D0 ↪Q↪ Ii, denoted with M ♣= ', iff for all worlds s 2 S and variable assignments g holds M↪ g↪ s ♣= '. A formula ' is a valid, denoted ♣= ', iff it is valid in every QCL model.

f is defined to take ['] (called the proof set of ' w.r.t. a given QCL model M) instead of '. This approach has the consequence of forcing the so-called normality property: given a QCL model M, if ' and '0 are equivalent (i.e., they are satisfied in the same set of worlds), then they index the same formulas w.r.t. to the)modality. The axiomatic counterpart of the normality condition is given by the rule (RCEA)

Moreover, it can be easily shown that the above semantics forces also the following rules to hold:

QCK (cf. CK in [Chellas, 1980]) denotes the minimal QCL closed under rules RCEA, RCEC and RCK. In what follows, only QCLs extending QCK are considered.

3 Classical Higher-Order Logic (HOL)

HOL is a logic based on simply typed λ-calculus [Church, 1940; Andrews, 2009]. The set T of simple types in HOL is usually freely generated from a set of basic types ¶o↪ i♦ using the function type constructor shortrightarrow. Here a set of basic types ¶o↪ i↪ u♦ is considered instead, where o denotes the type of Booleans, and where i and u denote some non-empty domains. Without loss of generality, i will later be associated with a set of worlds and u with a domain of individuals.

DEF. 3.1 (HOL) Let ↵↪ β↪ o 2 T. The terms of HOL are defined by the grammar (c↵ denotes typed constants and X↵ typed variables distinct from c↵):

Complex typed terms are constructed via abstraction and application. The primitive logical connectives are ≻oshortrightarrowo↪ _oshortrightarrowoshortrightarrowo and ⇧(↵shortrightarrowo)shortrightarrowo (for each type ↵). From these, other logical connectives can be introduced as abbreviations: for example, ^ and ! abbreviate the terms λAλB≻(≻A _ ≻B) and λAλB ≻A_B, etc. HOL terms of type o are called formulas. Binder notation 8X↵ so is used as an abbreviation for ⇧(↵shortrightarrowo)shortrightarrowoλX↵so. Type information as well as brackets may be omitted in the remainder if obvious from the context. Substitution of a term A↵ for a variable X↵ in a term Bβ is denoted by [A◁X]B, where it is assumed that the bound variables of B avoid variable capture. Well known operations and relations on HOL terms include β⌘-normalization and β⌘-equality, denoted by s =β⌘ t.

The following definition of HOL semantics closely follows the standard literature [Andrews, 2009; 1972a; 1972b].

DEF. 3.2 (Frame) A frame is a collection ¶D↵♦↵2T of nonempty sets called domains such that Do = ¶T↪ F♦ where T represents truth and F falsehood, Di 6= ; and Du 6= ; are chosen arbitrary, and D↵shortrightarrowβ are collections of total functions mapping D↵ into Dβ.

DEF. 3.3 (Interpretation) An interpretation is a tuple h¶D↵♦↵2T ↪ Ii where ¶D↵♦↵2T is a frame and where function I maps each typed constant symbol c↵ to an appropriate element of D↵, which is called the denotation of c↵. The denotations of ≻↪ _ and ⇧(↵shortrightarrowo)shortrightarrowo are always chosen as usual. (Moreover, the D↵shortrightarrow↵shortrightarrowo are required to contain the respective identity relations [Andrews, 1972b].)

DEF. 3.4 (Variable Assignment) A variable assignment φ maps variables X↵ to elements in D↵.

DEF. 3.5 (Henkin model) An interpretation is a Henkin model (general model) iff there is a binary valuation function V such that V (φ↪ s↵) 2 D↵ for each variable assignment φ and term s↵, and the following conditions are satisfied for all φ, variables X↵, constants c↵, and terms l↵shortrightarrowβ↪ r↵↪ sβ (for ↵↪ β 2 T): V (φ↪X↵) = φ(X↵), V (φ↪ c↵) = I(c↵), V (φ↪ l↵shortrightarrowβ r↵) = (V (φ↪ l↵shortrightarrowβ)V (φ↪ r↵)), and V (φ↪ λX↵sβ) represents the function fromD↵ into Dβ whose value for each argument z 2 D↵ is V (φ[z◁X↵]↪ sβ), where φ[z◁X↵] is that assignment such that φ[z◁X↵](X↵) = z and φ[z◁X↵]Yβ = φYβ when Yβ 6= X↵.

PROP. 3.6 If an interpretation H = h¶D↵♦↵2T ↪ Ii is an Henkin model the function V is uniquely determined and V (φ↪ s↵) 2 D↵ is called the denotation of s↵.

DEF. 3.7 (Standard model) H is called a standard model iff for all ↵ and β, D↵shortrightarrowβ is the set of all functions fromD↵ into Dβ. It is easy to verify that each standard model is also a Henkin model.

DEF. 3.8 (Validity) A formula A of HOL is valid in a Henkin model H iff V (φ↪A) = T for all variable assignments φ. In this case the notation H ♣= A is used. A is (Henkin) valid, denoted as ♣= A, iff H ♣= A for all Henkin models H. If S is a set of formulas, then S ♣= A expresses that H ♣= A holds for all Henkin models H with H ♣= B for all B 2 S.

PROP. 3.9 Let V be the valuation function of Henkin model H. The following properties hold for all variable assignments φ, terms so↪ to↪ l↵↪ r↵, and variables X↵↪W↵: V (φ↪ ≻so) = T iff V (φ↪ so) = F, V (φ↪ so _ to) = T iff V (φ↪ so) = T or V (φ↪ to) = T , V (φ↪ so ! to) = T iff V (φ↪ so) = F or V (φ↪ to) = T , V (φ↪ 8X↵so) = V (φ↪ ⇧(↵shortrightarrowo)shortrightarrowoλX↵so) = T iff for all v 2 D↵ holds V (φ[w◁W↵]↪ (λX↵so)W↵) = T, and if l↵ =β⌘ r↵ then V (φ↪ l↵) = V (φ↪ r↵).

4 Quantified Conditional Logics in HOL

QCL formulas are identified with certain HOL terms (predicates) of type (i shortrightarrow o). They can be applied to terms of type i, which are assumed to denote possible worlds. Type (i shortrightarrow o) is abbreviated as ⌧ in the remainder.

DEF. 4.1 (Embedding of QCL in HOL) The mapping b·c identifies QCL formulas ' with HOL terms b'c of type ⌧. The mapping is recursively defined:

P⌧ and X1 u ↪ ▷ ▷ ▷ ↪Xn u are variables and kunshortrightarrow⌧ is a constant symbol. ≻⌧shortrightarrow⌧ , _⌧shortrightarrow⌧shortrightarrow⌧ , )⌧shortrightarrow⌧shortrightarrow⌧ , ⇧co↪va (ushortrightarrow⌧)shortrightarrow⌧ and ⇧(⌧shortrightarrow⌧)shortrightarrow⌧ realize the QCL connectives in HOL. They abbreviate the following HOL terms: 1

⇧(⌧shortrightarrow⌧)shortrightarrow⌧ = λR⌧shortrightarrow⌧λVi8P⌧(RP V ) Constant symbol f in the mapping of ) is of type i shortrightarrow ⌧ shortrightarrow ⌧ . It realizes the selection function. Constant symbol eiw (for 'exists in world'), which is of type i shortrightarrow u shortrightarrow o, is associated with the varying domains. The interpretations of f and eiw are chosen appropriately below, cf. Def. 5.2. Moreover, for the varying domains a non-emptiness axiom is postulated:

The above mapping induces mappings bIVc, bPVc and bSYMc of the sets IV, PV and SYM respectively.

DEF. 4.2 (Embedding of the notion of validity) Analyzing the validity of a translated formula b'c for a world represented by term ti corresponds to evaluating the application (b'c ti). In line with Benzm¨uller et al. [2012a], validity is thus defined as vld⌧shortrightarrowo = λA⌧8Si(AS). With this definition, validity of a QCL formula ' in QCK corresponds to the validity of (vld b'c) in HOL, and vice versa. Further semantic notions such as countersatisfiable := λA⌧ ▷≻8Si▷(AS) can be introduced.

Note that the definition of ) can be further generalized as follows:

) = λfishortrightarrow⌧shortrightarrow⌧ λA⌧ λB⌧ λXi8Vi(f X A V ! B V ) Now, several selection function symbols f 1 ↪ ▷ ▷ ▷ ↪ f n can be introduced in the signature and ) can be instantiated with each of them leading to different, indexed conditional operators )f 1↪ ▷ ▷ ▷ ↪)f n. These indexed conditionals can now easily be associated with different axioms and properties, and they can be combined.

1 Note the predicate argument A of f in the term for )⌧shortrightarrow⌧shortrightarrow⌧ and the second-order quantifier 8P⌧ in the term for ⇧(⌧shortrightarrow⌧)shortrightarrow⌧ . FOL encodings of both constructs, if feasible, will be less natural.

5 Soundness and Completeness

To prove the soundness and completeness of the above embedding, a mapping from QCL models into Henkin models is employed. This mapping utilizes a corresponding mapping of QCL variable assignments into HOL variable assignments.

DEF. 5.1 (Mapping of Assignments) Let g = (gi : IV -! D↪ gp : PV -! Q) be a variable assignment for QCL. The corresponding variable assignment bgc = (bgi c : bIVc -! D↪ bgp c : bPVc -! Q) for HOL is defined such that bgc(Xu) = bgc(bXc) = g(X) and bgc(P⌧ ) = bgc(bPc) = g(P) for all Xu 2 bIVc and P⌧ 2 bPVc. Finally, bgc is extended to an assignment for variables Z↵ of arbitrary type by choosing bgc(Z↵) = d 2 D↵ arbitrary, if ↵ 6= u↪ ⌧ .

1. Let kunshortrightarrow⌧ = bkc for n-ary k 2 SYM and let Xiu = bXi c for Xi 2 IV, i = 1↪ ▷ ▷ ▷ ↪ n. Ikunshortrightarrow⌧ 2 Dunshortrightarrow⌧ is chosen such that (I kunshortrightarrow⌧ )(bgc(X1 u )↪ ▷ ▷ ▷ ↪ bgc(Xn u )↪w) = T for all worlds w 2 Di with M↪ g↪w ♣= k(X1 ↪ ▷ ▷ ▷ ↪Xn ), i.e., if hgi (X1 )↪ ▷ ▷ ▷ ↪ gi (Xn )i 2 I(k↪w). Otherwise, u )↪ ▷ ▷ ▷ ↪ bgc(Xn u )↪ w) = F .

DEF. 5.2 (Henkin model HM ) Given a QCL model M = hS↪ f↪ D↪ D0 ↪ Q↪ Ii. The Henkin model HM = h¶D↵♦↵2T ↪ Ii for M is defined as follows: Di is chosen as the set of possible worlds S, Du is chosen as the first-order domain D (cf. definition of bgi c and the remark in Def. 2.5), D⌧ is chosen as the set of sets of possible worlds Q (cf. definition of bgp c) 2 , and all other sets D↵shortrightarrowβ are chosen as (not necessarily full) sets of functions fromD↵ to Dβ. For all D↵shortrightarrowβ the rule that every term must have a denotation must be obeyed, in particular, it is required that Dunshortrightarrow⌧ , Dishortrightarrow⌧shortrightarrow⌧ and Dishortrightarrowushortrightarrowo contain the elements Ikunshortrightarrow⌧ , Ifishortrightarrow⌧shortrightarrow⌧ and Ieiwishortrightarrowushortrightarrowo as characterized next. Interpretation I is constructed as follows:

• (I kunshortrightarrow⌧ )(bgc(X1 2. I fishortrightarrow⌧shortrightarrow⌧ 2 Dishortrightarrow⌧shortrightarrow⌧ is chosen such that (Ifishortrightarrow⌧shortrightarrow⌧)(s↪ q↪ t) = T for all worlds s↪ t 2 Di and q 2 D⌧ with t 2 f(s↪ ¶x 2 S ♣ q(x) = T♦) in M.
• Otherwise, (I eiwishortrightarrowushortrightarrowo)(s↪ d) = F . 4. For all other constants c↵, choose Ic↵ arbitrary. 3 It is not hard to verify that HM is a Henkin model. 4
• Otherwise, (Ifishortrightarrow⌧shortrightarrow⌧ )(s↪ q↪ t) = F . 3. I eiwishortrightarrowushortrightarrowo 2 Dishortrightarrowushortrightarrowo is chosen such that (I eiwishortrightarrowushortrightarrowo)(s↪ d) = T for individuals d 2 D0 (s) in

2 Sets are identified with their characteristic functions.

3 In fact, it may be safely assumed that there are no other typed constant symbols given, except for the symbols fishortrightarrow⌧shortrightarrow⌧ , eiwishortrightarrowushortrightarrowo,

kunshortrightarrow⌧ , and the logical connectives. 4 In HM we have merely fixed Di = S, Du = D and D⌧ = Q, and the interpretations of kunshortrightarrow⌧ , fishortrightarrow⌧shortrightarrow⌧ and eiwishortrightarrowushortrightarrowo. These choices are not in conflict with any of the requirements regarding frames and interpretations. The existence of a valuation function V for an HOL interpretation crucially depends on how sparse the function spaces have been chosen in frame ¶D↵♦↵2T . [Andrews, 1972a] discusses criteria that are sufficient to ensure the existence of a valuation function; they require that certain λ-abstractions have denotations in frame ¶D↵♦↵2T . Since it is explicitly required that every term denotes and since Q has been appropriately constrained in QCL models (and hence Dishortrightarrowo in HM ) these requirements are met.

LEMMA 5.3 Let HM be a Henkin model for a QCL model M which validates axiom NE. For all quantified conditional logic formulas δ, variable assignments g and worlds s it holds: M↪ g↪ s ♣= δ iff V (bgc[s◁Si]↪ bδc Si) = T .

Proof: The proof is by induction on the structure of δ. The cases for δ = P, δ = k(X1 ↪ ▷ ▷ ▷ ↪Xn ), δ = ≻', δ = ' _ , and δ = ' ) are similar to Benzm¨uller et al. [2012a], Lemma 1.

If δ = 8vaX', by definition, it holds M↪ g↪ s ♣= 8vaX' iff for all d 2 D0 (s) we have M↪ ([d◁Xu]gi ↪ gp )↪ s ♣= '. By induction the latter condition is equivalent to: for all d 2 D0 (s) holds V (b([d◁Xu]gi ↪ gp )c[s◁Si]↪ (b'cSi)) = V (bgc[s◁Si][d◁Xu]↪ b'cSi) = T. Due to the choice of I eiw in HM , the non-emptiness condition NE and Prop. 3.9 this is equivalent to: for all d 2 D it holds V (bgc[s◁Si][d◁Xu]↪ eiwSi Xu ! b'cSi). Hence, by Prop. 3.9 we have that V (bgc[s◁Si]↪ ⇧(ushortrightarrowo)shortrightarrowoλXu(eiwSi Xu ! b'cSi)) =β⌘ V (bgc[s◁Si]↪ (λWi ⇧(ushortrightarrowo)shortrightarrowo λXu(eiwWi Xu ! b'cWi))Si) = T. By def. of ⇧va (ushortrightarrow⌧)shortrightarrow⌧ , def. of b▷c and Prop. 3.9 we get V (bgc[s◁Si]↪ (⇧va (ushortrightarrow⌧)shortrightarrow⌧ λXub'c)Si) = V (bgc[s◁Si]↪ b8vaX'c Si) = T .

The cases for δ = 8coX' and δ = 8P' are similar (actually simpler). 2

THEOREM 5.4 (Soundness and Completeness)

¶NE♦ ♣= vld b'c in HOL iff ♣= ' in QCK

Proof: (Soundness, !) The proof is by contraposition. Assume 6♣= ' in QCK, i.e, there is a QCL model M = hS↪ f↪D↪D0 ↪Q↪ Ii, an assignment g and a world s 2 S, such that M↪ g↪ s 6♣= '. By Lemma 5.3 it holds that V (bgc[s◁Si]↪ b'cSi) = F in Henkin model HM = h¶D↵♦↵2T ↪ Ii for M. Furthermore, HM ♣= ¶NE♦. Thus, by Prop. 3.9, definition of vld and since 8Si(b'cSi) =β⌘ vld b'c it holds that V (bgc↪ 8Si(b'cSi)) = V (bgc↪ vld b'c) = F. Hence, HM 6♣= vld b'c, and thus ¶NE♦ 6♣= vld b'c in HOL.

(Completeness, ) The proof is again by contraposition. Assume ¶NE♦ 6♣= vld b'c in HOL, i.e., there is a Henkin model H = h¶D↵♦↵2T ↪ Ii and an assignment φ such that H ♣= ¶NE♦ and V (φ↪ vld b'c) = F. Without loss of generality it can be assumed that Henkin model H is in fact a Henkin model HM for a corresponding QCL model M and that Φ = bgc for a corresponding QCL variable assignment g. By Prop. 3.9 and since vld b'c =β⌘ 8Si(b'cSi) it holds V (bgc↪ 8Si(b'c Si)) = F , and hence, by def. of vld, V (bgc[s◁Si]↪ b'cSi) = F for some s 2 D. By Lemma 5.3 M↪ g↪ s 6♣= ', and hence 6♣= ' in QCK. 2

This shows that QCL is a natural fragment of HOL.

6 Object- and meta-level automation of QCL

Figure 1 presents the HOL encoding of QCL connectives and axiom NE in THF syntax; THF is a concrete syntax for HOL [Sutcliffe and Benzm¨uller, 2010]. 5

5 Notes on THF: $i and $o represent the HOL base types i and o. $i>$o encodes a function (predicate) type. Function or predi-

%---- file: Axioms.thf ----------------------------------- %--- type mu for individuals thf(mu,type,(mu:$tType)). %--- reserved constant for selection function f thf(f,type,(f:$i>($i>$o)>$i>$o)). %--- 'exists in world' predicate for varying domains; %--- for each v we get a non-empty subdomain eiw@v thf(eiw,type,(eiw:$i>mu>$o)). thf(nonempty,axiom,(![V:$i]:?[X:mu]:(eiw@V@X))). %--- negation, disjunction, material implication thf(not,type,(not:($i>$o)>$i>$o)). thf(or,type,(or:($i>$o)>($i>$o)>$i>$o)). thf(impl,type,(impl:($i>$o)>($i>$o)>$i>$o)). thf(not_def,definition,(not = (ˆ[A:$i>$o,X:$i]:˜(A@X)))). thf(or_def,definition,(or = (ˆ[A:$i>$o,B:$i>$o,X:$i]:((A@X)|(B@X))))). thf(impl_def,definition,(impl = (ˆ[A:$i>$o,B:$i>$o,X:$i]:((A@X)=>(B@X))))). %--- conditionality thf(cond,type,(cond:($i>$o)>($i>$o)>$i>$o)). thf(cond_def,definition,(cond = (ˆ[A:$i>$o,B:$i>$o,X:$i]:![W:$i]:((f@X@A@W)=>(B@W))))). %--- quantification (constant dom., varying dom., prop.) thf(all_co,type,(all_co: (mu>$i>$o)>$i>$o)). thf(all_va,type,(all_va:(mu>$i>$o)>$i>$o)). thf(all,type,(all:(($i>$o)>$i>$o)>$i>$o)). thf(all_co_def,definition,(all_co = (ˆ[A:mu>$i>$o,W:$i]:![X:mu]:(A@X@W)))). thf(all_va_def,definition,(all_va = (ˆ[A:mu>$i>$o,W:$i]:![X:mu]:((eiw@W@X)=>(A@X@W))))). thf(all_def,definition,(all = (ˆ[A:($i>$o)>$i>$o,W:$i]:![P:$i>$o]:(A@P@W)))). %--- box operator based on conditionality thf(box,type,(box:($i>$o)>$i>$o)). thf(box_def,definition,(box = (ˆ[A:$i>$o]:(cond@(not@A)@A)))). %--- notion of validity of a conditional logic formula thf(vld,type,(vld:($i>$o)>$o)). thf(vld_def,definition,(vld = (ˆ[A:$i>$o]:![S:$i]:(A@S)))). %---- end file: Axioms.thf -------------------------------

The content of Fig. 1 is stored in file Axioms.ax and this file is imported in all example problems discussed below. Further definitions, e.g., for the connectives ^ or 9va , can be easily added.

Following Sec. 4 and by employing the QCL connectives defined in Axioms.ax, QCL statements can be directly expressed and automated in HOL. As will be illustrated below, this includes both statements formulated at the QCL object-level and statements at the QCL meta-level, i.e., statements about properties of QCL. In both cases the reasoning is carried out by off-the-shelf automated theorem provers and model finders for HOL. In the experiments discussed below the following systems have been employed: SATALLAX (version 2.6) [Brown, 2012], ISABELLE (version 2012) [Nipkow et al., 2002], LEO-II [Benzm¨uller et al., 2008] (version 1.5.0), NITPICK (version 2012) [Blanchette and Nipkow, 2010] and AGSYHOL (version 1.0) [Lindblad, 2012].

cate application as in (eiwV X) is encoded as ((eiw@V)@X) or simply as (eiw@V@X), i.e., function application is represented by @. Universal quantification and λ-abstraction as in λAishortrightarrowo8Si(AS) and are represented as in ˆ[X:$i>$o]:![S:$i]:(A@S); ? is the existential quantifier, and ≻↪ _↪ ^↪ and ) (mat. impl.) are written as , |, &, and =>. Comments begin with %. Better formatted and easier readable presentations of the THF code in this paper can easily be generated with the TPTP tools of Sutcliffe [2009]; here the minimization of space has been of primary interest.

%--------------------------------------------------------- include('Axioms.ax'). %--- we (falsely) conjecture: ID is implied by Axioms.ax thf(id,conjecture,(vld@(all@ˆ[P:$i>$o]:(cond@P@P)))). %---------------------------------------------------------

In the remainder they will be abbreviated with S, I, L, N and A, respectively. These systems work for Henkin semantics and they support the THF syntax as a common input language. Moreover, the SystemOnTPTP infrastructure [Sutcliffe, 2009] enables remote calls to instances of these provers at the University of Miami. Exploiting these features a simple shell script has been written that bundles these systems into a HOL meta-prover, called H in the remainder. H has been employed in the experiments reported below. Time measurements are given for the subsystems of H, e.g., (HN=5.2, HS=0.0) expresses that Nitpick and Satallax have terminated (with a result as mentioned) within 5.2 seconds, respectively 0.0 seconds, of CPU time. 6 If respective information is not given for a subprover then it produced 'Unknown' or 'Timeout' as a result. In the experiments each subprover of H was given a 20s timeout.

Automation of meta-level reasoning. The HOL approach supports meta-level reasoning for QCL. This includes proving the independence or dependence of QCL axioms, exploring correspondences between axioms and associated properties of the selection function, and showing the admissibility of inference rules. Respective examples for propositional CLs have been carried out by Benzm¨uller et al. [2012a]. Below the focus is on meta-level properties of QCL.

EXAMPLE 1 (Consistency) H quickly proves the satisfiability of Axioms.thf (HL↪S=0.0, HN=6.4). This confirms the consistency of QCL relative to the consistency of metalogic HOL.

EXAMPLE 2 (Axioms and rules) Prominent CL axioms are the law of identity ID: 8P (P ) P) and modus ponens for ) MP: 8P8Q(P ) Q) ! (P ! Q). Further prominent axioms include CS, CEM, AC, RT, CV, CA; cf. Pozzato [2010]). H proves the independence of these axioms by generating countermodels to respective dependence conjectures as exemplified for ID in Fig. 2, which encodes that vld⌧shortrightarrowo8P⌧(P⌧ )⌧shortrightarrow⌧shortrightarrow⌧ P⌧) is implied by the theory in Axioms.thf. When receiving this input file, the subprovers of H expand the definitions contained in Axioms.thf and apply their internal reasoning procedures to search for a solution. Countermodels are generated quickly (ID/MP: HL↪S=0.0, HN=6.4). Similarly, the admissibility of the rules RCEA, RCK and RCEC for QCL can be quickly proved by H. That is, these rules are automatically entailed in the HOL approach and can therefore be omitted without loosing completeness (cf. [Benzm¨uller et al., 2012a], Problem 2).

EXAMPLE 3 (Properties of QCL) Regarding quantifiers properties as given next are of some interest (where

6 Specifications of the SystemOnTPTP computers at Miami: i686 Intel(R) Xeon(R) CPU 5140 @ 2.33GHz, NumberOfCPUs: 4, RAMPerCPU: 1006.25MB, OS: Linux 2.6.32.26.

%--------------------------------------------------------- include('Axioms.ax'). %--- axioms ID and MP thf(id,axiom,(vld@(all@ˆ[P:$i>$o]:(cond@P@P)))). thf(mp,axiom, (vld@(all@ˆ[P:$i>$o]:(all@ˆ[Q:$i>$o]: (impl@(cond@P@Q)@(impl@P@Q)))))). %--- type declarations thf(horse,type,(horse:mu>$i>$o)). thf(wings,type,(wings:mu>$i>$o)). thf(fly,type,(fly:mu>$i>$o)). thf(pegasus,type,(pegasus:mu)). %--- the statements thf(ax1,axiom, (vld@(all_va@ˆ[X:mu]:(impl@(horse@X)@(not@(wings@X)))))). thf(ax2,axiom,(vld@(horse@pegasus))). thf(ax3,axiom,(vld@(wings@pegasus))). %---------------------------------------------------------

⇤ 2 ¶co↪ va♦); P1 and P2 are known as Barcan and converse Barcan formula.

In P1 and P2 it is assumed that X does not occur free in '. Instances of P1 and P2 can be formulated in HOL. E.g., for P1-8va the resulting HOL formula is vld (8vaX(a ) (bX)) ! (a ) 8vaX(bX))), where a and b are constants of types ⌧ and u shortrightarrow ⌧, respectively. Such instances of P18co and P2-8co can be quickly proved by H (P1-8co /P2-8co : HA↪L↪S=0.0,HI=5.8). This is consistent with the assumption of constant domain semantics for 8co . As expected, H reports countersatisfiability for P1-8va and P2-8va (P1-8va /P2-8va : HS=0.0,HL=0.4,HN=6.4). This is illustrated for P1-8va , which expands into HOL formula P1' :=

The countermodel generated by Nitpick is: Let Du = ¶u1 ↪ u2 ♦, Di = ¶i1 ↪ i2 ♦, I(a) = ;, I(b) = ¶(u2 ↪ i2 )♦, I(eiw) = ¶(i1 ↪ u2 )↪ (i2 ↪ u1 )♦, and I(f) = ¶(i1 ↪ ;↪ i2 )♦. Now, choose i1 for S, i2 for W, and u1 for Y . This invalidates P1', and hence P1. Note that the varying domains D0 (i1 ) = ¶u2 ♦ and D0 (i2 ) = ¶u1 ♦ (cf. I(eiw)) play a crucial role.

P3 is a standard property of first-order logic. H proves its validity for 8va and 8co (P3-8va /8co : HA↪L↪S=0.0,HI=5.9).

Automation of object-level reasoning. Automation of object-level reasoning is illustrated by prominent examples from the literature; cf. Delgrande [1998], Sec. 5.1. Following Delgrande, let φ )X be an abbreviation for (9vaXφ) ) 8vaX(φ ! ). Moreover, in all examples below axioms ID and MP are postulated, i.e, the reference logic is QCK+ID+MP.

EXAMPLE 4 (Pegasus, the winged horse) It can be consistently stated that horses (h) contingently do not have wings (w) but Pegasus (p) is a winged horse.

A THF encoding of E1 is presented in Fig. 3. H confirms the satisfiability of E1 (with HN=7.7). The finite model generated by Nitpick tells us that Pegasus is not 'actual', i.e., does not exist (cf. eiw) in any world. As expected, when E1 is formulated with 8co instead of 8va then H reports unsatisfiability (HL↪S=0.0, HI=5.8).

EXAMPLE 5 (Opus, the penguin) Birds (b) normally fly (f), but Opus (o) is a bird that normally does not fly.

This can be consistently stated in QCK+ID+MP and H reports a finite model (HN=8.6). When 8co is used instead of 8va , H reports unsatisfiability for E2 (HS=0.0, HI=7.9).

It can also be consistently asserted that birds normally fly and that necessarily Opus the bird does not fly.

Again, H reports a finite model (HN=8.7). H reports unsatisfiability when 8co is used in E3 (HS=0.0, HI=7.6).

However, it cannot be consistently asserted that birds normally fly and that necessarily there is a non-flying bird.

H reports unsatisfiability (HS=0.0, HI=8.7). H also reports unsatisfiability when 8co is used in E4 (HS=0.0, HI=8.8).

Finally-as desired-it can be consistently stated that birds normally fly, penguins normally do not fly and that all penguins are necessarily birds.

H generates a finite model (E4-8va : HN=8.8; E4-8co : HN=7.9). Moreover, H can conclude from the statements in E5 that birds are normally not penguins (E6-8va : HS=0.9, HL=10.2, HA=9.4; E6-8co : HS=0.8, HL=10.1, HA=0.3).

On the other hand, and in line with Delgrande, H reports a countermodel for the following statement when 8va is used (HN =8.7).

When 8co is used, H reports a theorem (HS=0.8, HA=0.4).

A closer look at the performance of H in this section seems to indicate that Satallax and Nitpick subsume the other subprovers of H. However, experiments in related areas show that there are many counterexamples to this conjecture (cf. the recent case study in first-order modal logics as reported by [Benzm¨uller and Raths, 2013]). The reason is that the search space in HOL is usually highly branching and that the current HOL systems often employ quite orthogonal search strategies and heuristics. In fact, Isabelle, the reigning CASC 7 champion in higher-order automated theorem proving has not been the strongest prover here (e.g. it failed on E6). It is thus recommendable to use the existing HOL provers in combination, just as illustrated in this paper.

7 The results of the 2012 CASC competition are available at http://www.cs.miami.edu/˜tptp/CASC/J6/.

7 Related work

Delgrande [1998] motivates the development of first-order CLs and he points to the problems of naive (constant domain) quantification in this context (a selection of his examples have been replicated with prover H above). The framework developed by Delgrande supports variable and constant domain quantification; it does not address propositional quantification. Regarding the semantics of ), Delgrande [1998] utilizes ternary accessibility relation. Earlier he also worked with selection function semantics [Delgrande, 1987].

First-order quantification in CLs has been studied also by Friedman et al. [2000]. Their focus is on default reasoning and they develop a subjective and statistical first-order logic of conditionals. Their conditional logic semantics is based on plausibility measures. Unfortunately, an implementation of their framework is not available. This also holds for Delgrande's approach.

Further alternative approaches to first-order nonmonotonic reasoning have been presented by Lehman & Magidor [1990] and Schlechta [1995].

The HOL approach supports the automation of arbitrary extensions of normal conditional logics. This is possible by simply postulating respective axioms (cf. ID and MP in Sec. 6). For this, quantification over propositional variables is crucial, which is not supported in any of the above approaches. Alternatively, corresponding semantic conditions on the selection function can be postulated in the HOL approach (if they exist and are known). Moreover, due to the embedding of QCL in the HOL meta-logic, meta-logical reasoning about QCL properties is facilitated. This is not the case for the above approaches.

The HOL approach supports and exploits explicit term representations of possible worlds/states. Hence, it can easily be extended to also cover hybrid CLs and their first-order extensions [Myers et al., 2009].

Even for propositional CLs very few provers currently exist. Some sequent and tableaux calculi are available, e.g., for logics CK+¶ID, MP/CEM, CS♦ and CK+¶CEM, MP♦ [Pozzato, 2010; Schr¨oder et al., 2010]. However, no theorem provers are, e.g., known for CK+¶CS, AC, RT, CV, CA♦ and no model builders for CK+¶ID, CS, AC, RT, CV, CA♦. The work presented here also supports those (and other) combinations and their extension to QCLs.

An embedding of propositional CLs in HOL has been presented by Benzm¨uller et al. [2012a]. First-order constant domain quantification has been studied by Benzm¨uller and Genovese [2011]. However, as Delgrande's examples show, constant domain quantification is counterintuitive in conditional logics. First-order and propositional quantification has also been addressed in a related embedding of quantified multimodal logic in HOL [Benzm¨uller and Paulson, 2013]; again, only constant domain quantification has been considered there. Varying and cumulative domain quantification have subsequently been added and Benzm¨uller et al. [2012b] and Benzm¨uller and Raths [2013] have carried out comparative evaluations of respective provers for quantified monomodal logic with very encouraging results for the HOL approach.

8 Conclusion

First, a notion of quantified conditional logic has been provided that includes first-order and propositional quantification, the former with respect to varying and constant domain semantics. Second, a sound and complete embedding of this logic in classical higher-order logic (w.r.t. Henkin semantics) has been presented. Third, this logic has been automated with off-the-shelf higher-order automated theorem provers and it has been shown that prominent challenges in nonmonotonic reasoning can be adequately addressed this way. The offered automation includes theorem proving and model finding and it is applicable to object-level and meta-level reasoning.

Note the particular relevance of the second point: Since quantified conditional logics are natural fragments of classical higher-order logic important meta-theoretical resp. prooftheoretical results can be obtained for free, including cutelimination and compactness. This is because these results are already known for classical higher-order logic (see e.g. the cut-free sequent calculus of Benzm¨uller et al. [2009]). Consequently, these results also apply to the embedded logics. In fact, my current program to study a wide range of classical and non-classical logics and their combinations as fragments of HOL can be seen as an elegant model theoretic approach to achieve such results.

A comparative evaluation of the presented work has been impossible so far, since there are no other provers for quantified conditional logics practically available to date. However, the results of the experiments so far are promising. Moreover, higher-order automated theorem provers have shown significant improvements over the last years and further improvements are to be expected. The conjecture therefore is that the approach will eventually scale also for more complex examples. An investigation of this conjecture is future work.

Future work will also study combinations of quantified conditional logic with other classical and nonclassical logics. Such combinations are relevant, e.g., for the adequate treatment of nonmonotonic concepts in expressive ontologies such as SUMO [Niles and Pease, 2001; Pease, 2011] or Cyc [Matuszek et al., 2006].

Acknowledgments: I thank the implementors of the HOL reasoning systems employed in this work, in particular, Jasmin Blanchette and Chad Brown. Moreover, I thank Geoff Sutcliffe for providing and maintaining the TPTP infrastructure. His support has been one crucial factor for the good progress of HOL ATP in recent years. I also thank Valerio Genovese, Dov Gabbay and Daniele Rispoli. They have pointed me to conditional logics and we have fruitfully collaborated on the propositional level. Valerio Genovese has also provided some support w.r.t. the extension of this work to constant domain first-order quantification.