The practical employment of automated deduction systems requires the user to input problem statements in a well-formed string representation. While this presentation is usually fixed by the respective system, the various language dialects of the TPTP library are meanwhile accepted as a de-facto standard for all current automated theorem provers based on classical logics. In the context of reasoning in non-classical logics, however, only a few limited standardization approaches exist, with QMLTP being the most notable exception. To move standardization forward, we outline conservative extensions to the TPTP language that allow systematic syntax definitions for various expressive, non-classical logics. These logics include higher-order versions of modal logics, conditional logics, hybrid logics, free logics, and many-valued logics. We are convinced that a standard syntax for prominent non-classical logics will not only facilitate their deployment but also support the development and comparability of corresponding theorem proving systems.
Computer-assisted reasoning in non-classical logics is of increasing interest to enable and support applications in e.g. computer science, mathematics and philosophy. Several powerful automated and interactive theorem proving systems have been developed over the past decades. However, when it comes to quantified logics, most of the available systems focus on classical logic only. Amongst the notable exceptions is MleanCoP [26] which automates first-order modal logic.
Orthogonal to the development of specialized provers, the semantical embedding approach [7] allows for a quick adaptation of existing higher-order reasoning systems to a broad variety of expressive, non-classical logics. In fact, for each logic discussed in this paper, we already have a new theorem provers in place [7,5,9,8,32]. These reasoners have been implemented by utilizing the embeddings approach on top of systems such as Leo-II [4] or Isabelle/HOL [22]. Recent experiments show that this approach indeed offers a surprisingly effective automation of the embedded non-classical logics. However, from the users perspective the utilization of the embeddings approach can become rather involved and distracting. Hence, system users may eventually not want to be exposed to the embeddings at all. Moreover, a comprehensive evaluation of systems based on the embeddings approach against systems based on the direct approach is currently hardly feasible. One reason, in addition to the fact the very few systems in the direct approach are available to date, is the lack of commonly agreed input formats.
In order to amplify the practical development, deployment and comparison of automated reasoning in quantified non-classical logics, we therefore outline problem representation formats for various (quantified) non-classical logics, primarily for use in automated theorem proving (ATP) systems. More specifically, we present conservative extensions to the well-known TPTP [34] syntax representations. We display proposals on how to represent logical problems in quantified versions of multi-modal logics, hybrid logics, conditional logics, free logics and some propositional many-valued logics. Additionally, we include means of adding meta-logical information to the problem statement that specifies details regarding the assumed semantics of the respective problem and logic. We briefly introduce each of the mentioned logics and describe the necessary modifications of the already existing languages.
TPTP and QMLTP. The Thousands of Problems for Theorem Provers problem library (TPTP) [34] provides a coherent environment for testing automated theorem provers for their correctness and performance. To that end, it postulates a standardized and stable formula representation syntax for most classical logic languages (e.g. FOF for first-order formulas or THF [35] for typed higher-order formulas). We will base our problem representation format on the THF dialect and moderately extend the existing syntax definitions to match the requirements of the particular non-classical logic in question.
A closely related project is QMLTP [27] which provides a syntax and a collection of problems for first-order modal logic. The QMLTP syntax is designed as an extension of the TPTP FOF language, introducing special symbols for the box and the diamond operators of modal logic (cf. §3.1). Regarding modal logics (or logics based on modal logic), we will also re-use existing syntax representations of the QMLTP project. Moreover, we adopt and extend the QMLTP approach for the specification of meta-logical information.
We primarily address quantified versions of non-classical logics in this paper. Since we do not intend to (artificially) restrict these logics to be first-order only, their representation formats will quite naturally be given as extensions of (classical) higher-order logic (HOL) [13]. The syntax and semantics of HOL is now briefly introduced as it serves as a basis for later, when logic-specific definitions of the syntax and semantics of non-classical higher-order logics are depicted. The brief introduction to HOL is mainly borrowed from [33] which, in turn, adapts the simplified notation of [21] for HOL.
HOL is a typed logic. The set of simple types T contains all types that are freely generated using the binary function type constructor → and a set of base types, usually chosen to be {o, ι} for Booleans and individuals, respectively. Terms of HOL are given by the following grammar:
where cτ ∈ Στ is a constant symbol from the (typed) signature Σ := τ Στ and Xτ is a variable. The type of a term is explicitly stated as subscript but may be dropped for legibility reasons if obvious from the context. Terms so of type o are formulas.
In general, we require Σ to contain a complete logical signature. To that end, we choose Σ to consist at least of the primitive logical connectives for disjunction, negation, and, for each type, equality and universal quantification. Hence, we have {∨o→o→o, ¬o→o, = τ τ →τ →o Π τ (τ →o)→o } ⊆ Σ for all τ ∈ T . 1 Optionally, we add choice operators and definite description operators ι for all types. Depending on the logics we are addressing in the following, the concrete set of constants (hence also connectives, quantifiers, etc.) Σ will actually vary. Often, we will only add further constants to the above ones. In all other cases, we will specify Σ explicitly.
thf(1, type, (p: ($i > $i) > $o)). thf(2, conjecture, (? [F: $i > $i]:
(p @ F = p @ (^[X: $i]: X)))).
Figure 1: A small HOL problem in THF representation.
The semantics of HOL is now briefly addressed. A frame {Dτ }τ∈T is a collection of non-empty sets Dτ such that Do = {T, F } (for truth and falsehood, respectively) and Dτ→ν ⊆ Dν Dτ is a collection of functions from Dτ to Dν . An interpretation is a pair M = ({Dτ }τ∈T , I) where {Dτ }τ∈T is a frame and I is a function mapping each constant cτ to some denotation in Dτ . We assume that the primitive logical connectives are assigned their usual denotation. Given a variable assignment g we can define a valuation . M,g by
where g[z/Xτ ] denotes the variable assignment that maps Xτ to z and every other variable Yν to σ(Yν ), where Yν = Xτ . A formula so is called valid, iff so M,g = T for every variable assignment g and every interpretation M. We call M a standard model iff Dτ→ν is the complete set of total functions, i.e. Dτ→ν = D Dτ ν . As a consequence of Gödel's Incompleteness Theorem [17], HOL with standard semantics is necessarily incomplete. However, if we allow Dτ→ν to be a proper subset of D Dτ ν with the constraint that . remains total, a meaningful notion of completeness can be achieved [19]. We assume this so-called Henkin semantics in the following.
A de-facto standard representation of HOL problems for automated theorem provers is given by the THF dialect [35] of the TPTP syntax [34]. This representation syntax is supported by most current HOL ATP, including Satallax [11], LEO-II [4], agsyHOL [20], Isabelle/HOL [22] and many others. A small example problem encoded in THF is displayed in Fig. 1. The circumflex ^and the @ denote λ-abstraction and function application, respectively. Types can be stated explicitly (cf. first line of Fig. 1), where > denotes the function type constructor →. Most remaining operations are standard TPTP syntax as used in first-order syntax.
We will use the THF dialect as a starting point for the development of specific representations of quantified non-classical logics in the following section.
In this section, we outline possible conservative extensions to the TPTP THF dialect in order to capture various quantified non-classical logics, to be used as input language of suitable ATP systems. The here discussed logics are modal logics, hybrid logics, conditional logics and free logics, each of them in a higher-order quantified version. Also, we briefly discuss means of representation for many-valued logics.
"Modal logic" refers to a family of non-classical logics that are used to express and reason about modal qualities of truth. To that end, the operators and are added to the usual classical logic language and characterized by appropriate rules and axiomatizations. Notions of necessity and possibility are probably the most prominent of such modal concepts represented by the new operators, but many further related systems and interpretations (e.g. focusing on temporal or deontic aspects) exist. Modal logics are not only of strong interest for the interpretation of philosophical arguments, but have also become increasingly important to mathematics and computer science [18].
Syntax and semantics. We now briefly sketch the syntax and semantics of higherorder modal logics (HOML) [21] by augmenting the appropriate definitions of HOL as given in §2. We here assume a multi-modal logic, that is a modal logic consisting of multiple, different box operators i , i ∈ I (and corresponding diamond operators), for some index set I.
The syntax definition is nearly identical to that of HOL. We merely add the box operators i o→o (for all i ∈ I) to the set of constants Σ. Their duals, the diamond operators i , can be defined by i o→o := λΦo. ¬( i (¬Φ)). For the semantics of HOML, we augment the concept of a HOL model with Kripke (possible world) semantics, yielding a HOML model structure M:
where W is a set of worlds, the R i ⊆ W × W are accessibility relations between the worlds of W , and each Iw is an interpretation function (similar to I of §2) for world w. We assume that connectives are always given the standard interpretation by Iw in each world w ∈ W .
In a final step, we augment the valuation function . M,g for HOL models to a valuation function . M,g,w for HOML models M, a variable assignment g and a world w ∈ W by i so M,g,w = T iff for all v ∈ W such that wR i v it holds that so M,g,v = T The semantics definition stated here are only adequate for constant domain semantics in which we assume the domains Dτ to be the same for all worlds w ∈ W . However, if we assume varying domain semantics (or their restricted forms of cumulative or decreasing domains), we need to further augment the above model. Instead of a single frame D := {Dτ }τ∈T we employ a family of frames {Dw}w∈W , one for each world. Additionally, the valuation of universal quantification is appropriately adjusted. We refer to the literature for details (cf. e.g. [15]). Regarding the quantification constants Π τ , τ ∈ T , we might want to allow mixed-semantics quantification statements, i.e. formulas where multiple quantifications are contained, each possibly with different semantics. 2 This can simply be done by adding different quantification constants for the respective different quantification semantics to the signature, yielding Σ = {. . . , Π τ,co , Π τ,va , Π τ,inc , Π τ,dec } for each type τ ∈ T for constant, varying, cumulative and decreasing domain quantification semantics, respectively.
We are in a higher-order setting. Hence, bridge rules (e.g. i φ =⇒ j φ) can simply be postulated as axioms (e.g. ∀φ( i φ =⇒ j φ)). Consequently, we can avoid a specific representation for bridge rules below. However, such axioms should possibly be marked specifically so that provers can easily recognize them (similar to TPTP definitions) and apply special techniques where possible.
The above definitions give us modalities with logic K properties. In order to obtain stronger logics, such as KB, KD, S4 and S5, we e.g. could, analogous to the above bridge rules, postulate respective axioms. However, it seems to us that this approach would be impractical and too verbose. Hence, we include a special syntax for postulating frame conditions to the modalities below.
Representation. We adopt the representation of QMLTP for representing the box and diamond operators, i.e. by writing #box for and #dia for . Since we are in a multi-modal setting, we qualify these connectives with an appropriate identifier, called index: #box(i) for i and #dia(i) for i . The modal operators are then used similar to quantifiers in TPTP: #box(a): t represents the formula a to. The remaining syntax is standard THF. A short example (where a and b are identifiers from I) is given by:
The ! quantifier respects some quantification semantics that is chosen by the user. Additionally, we add four new quantifiers !=, !~, !+, !-that always denote constant, varying, cumulative and decreasing domain quantification semantics, respectively, regardless of the default setting for !. Existential variants are added analogously.
Global parameters. These parameters need to be included in the problem description using the TPTP process instruction language (TPI) 3 Here, three different indexed modalities a, b and c are introduced with the given axiomatizations S5, KB and K, respectively. Valid axiomatization schemes for modalities include k, kb, k4, k5, d, m, b, s4 and s5. There have been more systems presented in the literature. Hence, this list could/should be appropriately extended.
Per-Symbol Options. As a convenience feature, we allow per-symbol specification of rigidity, allowing some symbols to be rigid and some symbols to be world-dependent. More specifically, all symbols introduced using type statements have the default rigidity as stated by the constants option of the set_logic statement, unless overridden by another set_logic statement specifically for that new constant. In the following example, the constant symbol q is a rigid symbol while p is world-dependent as stated by statement 4:
tpi(1, set_logic, modal(['quantification' = 'cumulative', 'constants' = 'rigid', 'modalities' = [(a, s5), (b, kb), (c, k)]])). hmf(2, type, (q: $i)). hmf(3, type, (p: $i)). tpi(4, set_logic, hmf(p, 'dependent')).
Hybrid logic [10] is a general term for extensions of ordinary modal logics that introduce a new sort of atomic formulas -the so-called nominals. Nominals introduce one convenient feature to modal logic, that is referencing and arguing about worlds. In natural language it is a common construct to refer to a specific point in time or the knowledge of one particular person. Although modal logic is used to model these problem domains, it is not possible to reference to the underlying world structure. Hybrid logic allows to evaluate a formula in a specific world -with the satisfaction operator @ -and to bind the current world to a variable -with the shift operator ↓.
Syntax and semantics. Classically, nominals are introduced in propositional and first-order logic by introducing new cases into the syntax BNF and adjusting the models accordingly. Additional to HOML we need to introduce the nominals, the satisfaction operator @, and the shifter ↓ to the BNF over a set N OM . 4s, t ::= ...|no|@(no)so| ↓ so→o|... n ∈ N OM
The semantics is build on the same model as ordinary modal logic.
The variable assignment g = (g i , g n ) is adorned with an extra variable assignment g n , that maps nominals to worlds. The assignment g i is the variable assignment from standard higher-order modal logic. The valuation . is then augmented for formulas containing nominals, given by n M,g,w = g n (n) ≡ w. n ∈ N OM @nϕ M,g,w = ϕ M,g,g n (n) ↓ ϕo→o M,g,w = ϕn M,g,w where n is free in ϕ and g n (n) = w
Since hybrid logic is an extension of ordinary modal logic, we can still obtain the stronger logics stated by the frame conditions K B, K D, S4, S5 as usual. On the other hand, nominals allow the formulation of frame conditions, that were not previously expressible in ordinary modal logic. For example, the condition n ⇒ ¬n for n ∈ N OM , for instance, corresponds to an irreflexivity condition. As in the last section we allow to name the new frame conditions explicitly.
Representation. We extend the hmf syntax for ordinary modal logic described before and add the two new syntax features described above. To distinguish nominals from ordinary Boolean constants, we introduce a new type, called $nominalType. In a formula the nominal is grounded to Boolean type, by introducing a new predicate #nom. A nominal n has then to be written as #nom(n) inside a formula. We propose to adopt the satisfaction and shifter operator with an explicit binding mechanism: #at(n) : p for @n p, and #shift [n] : p for ↓ (λX . p). Thereby, in both cases, the operator takes as first argument only nominals. The remaining syntax containing modal operators and higher-order features are the above described hmf based on the standard THF. A short example (where n1 is a nominal) is given by:
Global parameters. Hybrid logic is an extension to ordinary modal logic, with the same parameters. The same options for quantification, constants, and consequence can be given, as well as giving each symbol a rigid or dependent. In theory a range of additional frame conditions can be given for the modalities, but in practice hybrid logic is used in common frame settings. Hence we suggest to use the exact same (resp. suitably adapted) notation as for ordinary higher-order modal logic.
Conditional logics [24] have many applications including action planning, counter-factual reasoning, default reasoning, deontic reasoning, metaphysical modeling and reasoning about knowledge. A new operator for so-called conditionality, denoted −→, is added to the basic logical language which is not to be confused with material implication ( =⇒ ). 5First-order conditional logics have been studied in [14,16] and extended (to include propositional quantification) and embedded in HOL in [3]. We here consider a higher-order quantified version of conditional logic (HCL). 6Syntax and semantics. Terms of HCL are defined as ordinary HOL terms, except that we add a new constant symbol for conditionality to the signature, i.e. Σ = {. . . , −→o→o→o}. As for modal logics above, we may add quantifiers for different domain conditions. Monomodal logics are subsumed by HCL since 2so can be introduced as an abbreviation for ¬so −→ so. Syntactically, HCL can be seen as a generalization of HOML where the index of modality −→ is a formula of the same language. For instance, in (so −→ to) −→ uo the subformula s −→ t is the index of the second occurrence of −→.
An adequate semantics is achieved by adapting selection function semantics [31,12]. We modify the HOL model structure by adding possible worlds (similar to HOML) and a selection function
where W is a set of worlds, {Dτ }τ∈T is a frame and {Iw}w∈W a collection of interpretation functions.
Together with a variable assignment g and a world w ∈ W we can then refine the valuation function . M,g,s (only the valuation of conditionality is shown, the remaining cases are straight-forward adaptions of the HOL case):
where [so] := {u | so M,g,u = T } is the so-called proof set of s.
Like in the case of modal logics, where we distinguish between logics such as K, B, D, S4, S5, there are many different conditional logics, which differ regarding the particular axioms/conditions associated with the conditionality operator −→. These logics are based on the axioms ID, MP, CS, CEM, AC, RT, CV, CA; see Fig. 2.
Representation. Representation of HCL is straight-forward: The syntax is exactly the same as for ordinary HOL problems. We merely add a new implication -> which denotes the conditional implication whereas the included implication of THF, =>, still denotes material implication (for the sake of consistency). Also, we add the different new quantification symbols !=, !~, !+ and !-for the respective quantification semantics and denote by ! the default quantification semantics as chosen by the user. The following example presents a formula that is valid in MP but not in ID:
Parameters. The global parameters quantification and constants are the same as for in HOML. We also allow per-symbol rigidity specification as done for HOML. We do not need the specification of modalities here, instead we only need to specify the logic (axiomatization) under consideration. In contrast to modal logic where there exist mostly standardized naming conventions for important logical systems, this is not as evident for conditional logic. However, the axiom names themselves seem standard enough, hence we can describe the logical system by enumerating the included axioms. This is done by the parameter logic Sets the semantics for the conditional logic under consideration. More precisely, collects a list of axioms that is to be considered. If omitted, a base conditional logic with none additional axioms is assumed.
Valid values: All of the axiom names of Fig. 2.
In the following example the logical axioms ID, MP and CEM (cf. Analogous to HOML, the above representations could be extended to support multiconditional logics, i.e. indexed operators ->. We do not pursue this further here, since were are not aware yet of applications.
Classical logic is only mildly suited for handling undefinedness and partiality in an appropriate way. There are two related reasons: (i) terms denote, without exemptions (e.g. for undefined terms), entities in a non-empty domain of "existing" objects D, and (ii) the quantifiers range over this entire set D.
An elegant alternative to remedy these shortcomings is free logic [23,28], which distinguishes between a raw domain of possibly non-existing objects D and a particular subdomain E of D, containing only the "existing" entities. Free variables range over D and quantified variables only over E. Each term denotes in D, but not necessarily in E. This is the case, for example, for improper definite descriptions which can now be mapped to a distinguished non-existing object, denoted * ∈ D.
Moreover, the domain E may be empty (this special case is called inclusive logic). Unfortunately, no theorem provers have been available so far for free logic. Nevertheless, free logic can be embedded in HOL [8], allowing indirect automation via HOL ATP systems.
Syntax and semantics. The syntax of free higher-order logic is the same as for ordinary HOL. The non-trivial semantics definitions concern universal quantification and definite description (denoted by ι). A model M in this context distinguishes (for all types τ ) between a raw domain Dτ and a set Eτ ⊆ Dτ of existing objects. A valuation function for these cases can be formulated as Where the ti are the truth-values of the logic, c ∈ Σ is a constant symbol and C is a symbol of the set of binary connectives, containing at least {&, ∨, ∧, →}. Depending on the selected logic, additional symbols can be added, and the number of ti is fixed.
The semantics here is highly dependent on the chosen logic. As usual the semantics of the connectives can be given in a truth-table. In Fig. 3 the semantics of → for three different three-valued logics is given as an example.
Representation. Since we are only considering propositional many-valued logic at this point, it does not fit well into the quantified fragment of the TPTP. But since there exist quantified versions of many-valued logics, we base the propositional case on the FOF fragment of the TPTP. This way, the proposal can be extended towards a first-order version.
In addition to FOF, we first introduce a term for truth degrees #t(i) for ti with i = 1, . . . , n, where n is the number of truth constants for the selected logic. To distinguish between weak and strong conjunction, we introduce a new symbol /\ for the standard weak conjunction ∧. The standard AND-symbol & is defined to be the strong conjunction to avoid confusion. The following is an example for axioms of a many-valued logic, relating ∧ and ∨ to the minimal signature of Lukasiewicz or Gödel logics. Global Parameters. There are two parameters we can provide to adjust the semantics. The first fixes the exact logic. As described, there are many possible many-valued logics, that fix an interpretation for the logical symbols. The second parameter sets the cardinality of the set of truth values. This parameter is only important for the logics with an adjustable amount of truth values. The exact parameters are: semantics Sets the exact logic and fixes the interpretation for the logical symbols.
Valid values: kleene-weak, kleene-strong, post, lukasiewicz, goedel, bocvar.
card Sets the size of the truth values. Has only an effect on lukasiewicz and goedel.
The parameters can be set as in the previous cases in the instruction language TPI. For example, a Lukasiewicz logic with {0, In theory the cardinality cases ℵ0 and ℵ1 were possible, but this would require a different mechanism to name truth values.
There are several sixteen-valued logics based on a lattice denoted SIXTEEN. These logical systems have been developed by Shramko and Wansing as a generalization of the fourvalued system of Dunn/Belnap [2] to knowledge bases in computer networks [29] and was subsequently further investigated in various contexts (e.g. [25,30]). In SIXTEEN, the truth-degrees are given by the power set of Belnap's truth values, i.e. V = 2 {N,T,F,B} = {∅, N, T, F, B, . . . , {N, T, F, B}} where N, T, F and B are the respective singleton sets containing N, T, F and B. The remaining truth-degrees are named using a combination of the letters N, T, F and B, representing the truth-degree that contains the respective elements when regarded as a set (e.g. NT for the set {N, T}). This generalization is essentially motivated by the observation that a four-valued system cannot express certain phenomena that arise in knowledge bases in computer networks. Further applications in linguistics and philosophy are discussed in the monograph by Shramko and Wansing [30], to which we refer to for a thorough investigation of SIXTEEN, the definitions of logical connectives and their semantics. Briefly speaking, there exists a set of connectives ∨ , ∧ , ¬ for two distinct logics L with ∈ {t, f } and a logic given by their union, denoted L tf . Additionally, multiple different entailment relations |= for ∈ {t, f, tf } can be considered. An embedding of logics based on SIXTEEN into HOL for use in ATP systems is sketched in [32].
Representation. The representation of the L is more involved as we need a nonquantified language with different infix operators denoting the different logical connectives. The following syntax representation could be seen as a generalization and restriction of FOF, where we add new infix connectives but restrict the problem not to contain firstorder ingredients (such as quantifiers). Consequently, we add infix operators &t, |t, ~t, =>t, &f, |f, ~f and =>f to the language. The problem statements are then straight-forward, an example is given by where a, b are ad-hoc introduced individuals symbols as supported by FOF.
In this paper, we discussed means of representing both problems and meta-logical specification for quantified non-classical logics. To that end we adapt and extend TPTP-THF and QMLTP syntax for problems and the TPI language proposal for fixing semantic parameters. We have outlined specialized syntaxes for higher-order modal logic, hybrid logic, conditional logic, and free logic to be used as input languages of ATP systems. Additionally, we sketched ideas for representing many-valued logics. Further logics can easily be added and addressed along the same lines. For example, due to space restrictions we have omitted the inclusion of (quantified) intuitionistic logic [6].
The suggestions in this paper are, at this stage, not meant to be conclusive. Instead, we want to stimulate discussions, e.g. at the ARQNL event, about further requirements and extensions. Moreover, we envision a close collaboration with the QMLTP and TPTP projects. A concluding, motivating example is displayed in Appendix A where an encoding of Gödel's Ontological argument is given in hmf syntax.
We thank Harold Boley for his comments and for proofreading this document. We also thank the reviewers for the very valuable feedback they provided.
This work has been supported by the DFG under grant BE 2501/11-1 (Leo-III) and grant BE 2501/9-2 (Computational Metaphysics).
The following example is an encoding of Gödel's ontological argument in hmf syntax as described in this work (cf. §3.1). More precisely, we present here Dana Scott's variant as a one step proof in which intermediate argumentation steps are omitted. HOL provers such as Leo-II are capable of automating this example in a few seconds (however, not yet for the syntax representation below). Details about the ontological argument, its formalization and its automation can be found in the literature (e.g. in [5]). ((p @ (^[X:$i]: ~(Phi @ X)) <=> ~(P @ Phi))))). hmf(A2,axiom,(![Phi: $i>$o,Psi: $i>$o]:
(((p @ Phi) & #box(a): (![X:$i]: ((Phi @ X) => (Psi @ X)))) => (p @ Psi)))). hmf(god_const,type,(g: $i>$o)). hmf(god,definition,(g = (^[X:$i]: (![Phi: $i>$o]: ((p @ Phi) => (Phi @ X)))))). hmf(A3,axiom,(p @ g)). hmf(A4,axiom,(![Phi: $i>$o]: ((p @ Phi) => #box(a): (p @ Phi)))). hmf(essence_const,type,(ess: (Phi @ Y))))))). hmf(A5,axiom,(p @ ne)). hmf(T3,conjecture,(#box(a): (?[X:$i]: (g @ X)))).