Raul Fervari

Andreas Herzig

Yanjun Li

Yanjing Wang

Strategically Knowing How

In this paper, we propose a single-agent logic of goal-directed knowing how extending the standard epistemic logic of knowing that with a new knowing how operator. The semantics of the new operator is based on the idea that knowing how to achieve ϕ means that there exists a (uniform) strategy such that the agent knows that it can make sure ϕ. We give an intuitive axiomatization of our logic and prove the soundness, completeness and decidability of the logic. The crucial axioms relating knowing that and knowing how illustrate our understanding of knowing how in this setting. This logic can be used in representing and reasoning about both knowledge-that and knowledge-how.

Introduction

Standard epistemic logic focuses on reasoning about propositional knowledge expressed by knowing that ϕ [Hintikka, 1962]. However, in natural language, various other knowledge expressions are also frequently used, such as knowing what, knowing how, knowing why, and so on.

In particular, knowing how receives much attention in both philosophy and AI. Epistemologists debate about whether knowledge-how is also propositional knowledge (cf. the survey [Fantl, 2008]), e.g., whether knowing how to swim can be rephrased using knowing that. In AI, it is crucial to let autonomous agents know how to fulfill certain goals in robotics, game playing, decision making, and multi-agent systems (cf. the surveys [Gochet, 2013;[START_REF] Ågotnes | [END_REF]). In fact, a large body of AI planning can be viewed as finding algorithms to let the autonomous planner know how to achieve some propositional goals, i.e., to obtain goal-directed knowledge-how. Here, both propositional knowledge and knowledge-how matter, especially in the planning problems where initial uncertainty and non-deterministic actions are present. From a logician's point of view, it is interesting to see how knowing how interacts with knowing that, and how they differ in their reasoning patterns. A logic of knowing how also helps us to find a consistency notion regarding knowledge database with knowing how expressions. * corresponding author (email: y.wang@pku.edu.cn) s1 : p, ¬q test q / / s3 : p, ¬q pills / / s5 : ¬p, ¬q s2 : p, q test q / / s4 : p, q surgery , , pills pills 1 1 s6 : ¬p, q Example 1.1. Consider the scenario where a doctor needs a plan to treat a patient and cure his pain (p), under the uncertainty about some possible allergy (q). If there is no allergy (¬q) then simply taking some pills can cure the pain, and the surgery is not an option. On the other hand, in presence of the allergy, the pills may cure the pain or have no effect at all, while the surgery can cure the pain for sure. The model from Figure 1 represents this scenario with an additional action of testing whether q. The dotted line represents the initial uncertainty about q, and the test on q can eliminate this uncertainty (there is no dotted line between s 3 and s 4 ). According to the model, to cure the pain (guarantee ¬p) at the end, it makes sense to take the surgery if the result of the test of whether q is positive and take the pills otherwise. We can say the doctor in this case knows how to cure the pain.

How to formalize the knowledge-how of the agent in such scenarios with uncertainty? Already since the early days of AI, people have been looking at it in the setting of logics of knowledge and action [McCarthy and Hayes, 1969;McCarthy, 1979;Moore, 1985;Lespérance et al., 2000;van der Hoek et al., 2000]. However, there has been no consensus on how to capture the logic of "knowing how" formally (cf. the recent surveys [Gochet, 2013] and [ Ågotnes et al., 2015]). The difficulties are well discussed in [START_REF] Jamroga | Wojciech Jamroga and Thomas Ågotnes. Constructive knowledge: what agents can achieve under imperfect information[END_REF] and [Herzig, 2015]: simply combining the existing modalities for "knowing that" and "ability" in a logical language like ATEL [van der Hoek and Wooldridge, 2003] does not lead to a genuine notion of "knowing how", e.g., knowing how to achieve p is not equivalent to merely knowing that there exists some strategy to make sure p. It does not work even when we replace the strategy by a uniform strategy where the agent has to choose the same action on indistinguishable states [START_REF] Jamroga | Wojciech Jamroga and Thomas Ågotnes. Constructive knowledge: what agents can achieve under imperfect information[END_REF]. Let ϕ(x) express that x is a way to make sure some goal is achieved, and let K be the standard knowledge-that modality. There is a crucial distinction between the de dicto read-ing of knowing how (K∃xϕ(x)) and the desired de re reading (∃xKϕ(x)) endorsed also by linguists and philosophers [START_REF] Stanley | Jason Stanley and Timothy Williamson[END_REF]. The latter intuitively implies the former, but not the other way round. For example, consider a variant of Example 1.1 where no test is available: then the doctor has de dicto knowledge-how to cure, but not de re knowledge. Proposals to capture the de re reading have been discussed in the literature, such as making the knowledge operator more constructive [START_REF] Jamroga | Wojciech Jamroga and Thomas Ågotnes. Constructive knowledge: what agents can achieve under imperfect information[END_REF], making the strategy explicitly specified [START_REF] Herzig | [END_REF]Belardinelli, 2014], or inserting K in-between an existential quantifier and the ability modality in see-to-it-that (STIT) logic [START_REF] Broersen | Using STIT theory to talk about strategies[END_REF].

In [Wang, 2015;2016b], a new approach is proposed by introducing a single new modality Kh of (conditional) goaldirected knowing how, instead of breaking it down into other modalities. This approach is in line with other de re treatments of non-standard epistemic logics of knowing whether, knowing what and so on (cf. [Wang, 2016a] for a survey). The semantics of Kh is inspired by the idea of conformant planning based on linear plans [START_REF] Smith | [END_REF]Yu et al., 2016]. It is shown that Kh is not a normal modality, e.g, knowing how to get drunk and knowing how to drive does not entail knowing how to drive when drunk. The work is generalized further in [Li and Wang, 2017;Li, 2017]. However, in these previous works, there was no explicit knowing that modality K in the language and the semantics of Kh is based on linear plans, which does not capture the broader notion allowing branching plans or strategies that are essential in the scenarios like Example 1.1. In this paper, we extend this line of work in the following aspects:

• Both the knowing how modality Kh and knowing that modality K are in the language, and we capture the interactions of the two explicitly by several axioms. Accordingly, we have both the action transitions and epistemic uncertainty in the models.

• In contrast to the essentially state-independent (global) semantics in [Wang, 2015;2016b], we interpret Kh locally w.r.t. the local uncertainty, in accordance with the standard semantics for the knowing that operator K.

• Instead of linear plans in [Wang, 2015], the semantics of our Kh operator is based on the existence of strategies (branching plans). In this way, the agent can make use of the knowledge learned during the execution of the plan, which helps us to capture situations where the agent intuitively knows how but does not have a linear plan.

The intuitive idea behind our semantics of Khϕ is that the agent knows how to achieve ϕ iff (s)he has an executable uniform strategy σ such that the agent knows that:

• σ guarantees ϕ in the end given the uncertainty;

• σ always terminates after finitely many steps.

Note that for an agent to know how to make sure ϕ, it is not enough to find a plan which works de facto, but the agent should know it works in the end. This is a strong requirement inspired by planning under uncertainty, where the collection of final possible outcomes after executing the plan is required to be a subset of the collection of the goal states [START_REF] Geffner | A concise introduction to models and methods for automated planning[END_REF]. Technically, our contributions are summarized as follows:

• A logical language with both Kh and K operators with a semantics which fleshes out formally the above intuitions about knowing how. • A complete axiomatization with intuitive axioms.

• Decidability of our logic. The paper is organized as follows: Section 2 lays out the language and semantics of our framework; Section 3 proposes the axiomatization and proves its soundness; We prove the completeness of our proof system and show the decidability of the logic in Section 4 before we conclude with future work.

Language and Semantics

Let PROP be a countable set of propositional symbols. Definition 2.1 (Language). The language is defined by the following BNF where p ∈ PROP:

ϕ := p | ¬ϕ | (ϕ ∧ ϕ) | Kϕ | Khϕ.
We use ⊥, ∨, → as usual abbreviations and write K for ¬K¬.

Definition 2.2 (Models). A model M is a quintuple W, ACT, ∼, { a -→| a ∈ ACT}, V where: • W is a non-empty set, • ACT is a set of actions, • ∼ ⊆ W × W is an equivalence relation on W , • a -→ ⊆ W × W is a binary relation for each a ∈ ACT • V : W → 2 PROP is a valuation.
Note that the labels in ACT do not appear in the language but only in the models. The graph in Example 1.1 represents a model with omitted self-loops of ∼ (dotted lines), and the equivalence classes induced by ∼ are {s 1 , s 2 }, {s 3 }, {s 4 }, {s 5 }, {s 6 }. In this paper we do not require any properties between ∼ and a -→ to lay out the most general framework. We will come back to particular assumptions like perfect recall at the end of the paper. Given a model and a state s, if there exists t such that s a -→ t, we say that a is executable at s. Also note that the actions can be nondeterministic as in [Wang, 2015]

′ ∈ [s] and t ′ ∈ [t] such that s ′ a -→ t ′ . If there is t ∈ W such that [s] a -→ [t], we say a is executable at [s]. Definition 2.3 (Strategies). Given a model, a (uniformly ex- ecutable) strategy is a partial function σ : [W ] → ACT such that σ([s]) is executable at all s ′ ∈ [s].
Particularly, the empty function is also a strategy, the empty strategy.

Note that the executability is as crucial as uniformity, without which knowledge-how may be trivialized. We use dom(σ) to denote the domain of σ. Function σ can be seen as a binary relation such that

([s], a), ([s], b) ∈ σ implies a = b. Therefore, if τ is a restriction of σ, i.e. τ ⊆ σ, it follows that dom(τ ) ⊆ dom(σ), and τ ([s]) = σ([s]) for all [s] ∈ dom(τ ). Definition 2.4 (Executions). Given a strategy σ w.r.t a model M, a possible execution of σ is a possibly infinite sequence of equivalence classes δ = [s 0 ][s 1 ] • • • such that [s i ] σ([si]) ----→ [s i+1 ] for all 0 ≤ i < |δ|. Particularly, [s] is a possible execution if [s] ∈ dom(σ). If the execution is a finite sequence [s 0 ] • • • [s n ], we call [s n ] the leaf-node, and [s i ] (0 ≤ i < n) an inner-node w.r.t. this execution. If it is infinite, then all [s i ] (i ∈ N) are inner-nodes. A possible execution of σ is complete if it is infinite or its leaf-node is not in dom(σ). Given δ = [s 0 ] • • • [s n ] and µ = [t 0 ] • • • [t m ], we use δ ⊑ µ to denote that µ extends δ, i.e., n ≤ m and [s i ] = [t i ] for all 0 ≤ i ≤ n. If δ ⊑ µ, we define δ ⊔ µ = µ.
We use CELeaf(σ, s) to denote the set of all leaf-nodes of all the σ's complete executions (can be many due to non-determinism) starting from [s], and CEInner(σ, s) to denote the set of all the inner-nodes of σ's complete executions starting from

[s]. CELeaf(σ, s) ∩ CEInner(σ, s) = ∅ since if [s] is a leaf-node of a complete execution then σ is not defined at [s].
Definition 2.5 (Semantics). Given a pointed model M, s, the satisfaction relation is defined as follows:

M, s p ⇐⇒ p ∈ V(s) M, s ¬ϕ ⇐⇒ M, s ϕ M, s ϕ ∧ ψ ⇐⇒ M, s ϕ and M, s ψ M, s Kϕ ⇐⇒ for all s ′ : s∼s ′ implies M, s ′ ϕ M, s Khϕ ⇐⇒ there exists a strategy σ such that 1.[t]⊆ ϕ for all [t]∈CELeaf(σ, s) 2. all its complete executions starting from [s] are finite, where ϕ = {s ∈ W | M, s ϕ}.
Note that the two conditions for σ in the semantics of Kh reflect our two intuitions mentioned in the introduction. The implicit role of K in Kh will become clearer when the axioms are presented. Going back to Example 1.1, we can verify that Kh¬p holds on s 1 and s 2 due to the strategy σ = {{s 1 , s 2 } → test, {s 3 } → pills, {s 4 } → surgery}. Note that CELeaf(σ, s 1 ) = {[s 5 ], [s 6 ]} = {{s 5 }, {s 6 }} and ¬p = {s 5 , s 6 }. On the other hand, Kh¬q is not true on s 1 : although the agent can guarantee ¬q de facto on s 1 by taking a strategy such that {s 1 , s 2 } → test and {s 3 } → pills, he cannot know it beforehand since nothing works at s 2 to make sure ¬q. Readers may also verify that Kh(p ↔ q) holds at s 1 and s 2 (hint: a strategy is a partial function).

Let us compare our work to [Wang, 2015;2016b], where the knowing that operator is not in the language. We include the knowledge operator K to precisely capture the interactions of knowing that and knowing how by the axioms to be introduced in the next section. Although the universal modality definable in the previous work can be viewed as a restricted kind of knowing that operator, it can only express global background knowledge to some extent. Moreover, in our models, both epistemic uncertainty and action transitions are present to model the changes of knowledge after actions, which is essential to facilitate strategies based on local knowledge, compared to the quite restricted linear plans of [Wang, 2015;2016b]. Finally, the Kh(ψ, ϕ) operator there ('the agent knows how to achieve ϕ given ψ') is state-independent. In the present perspective, the condition ψ there exactly defines an initial uncertainty set.

Axiomatization

3.1 The Proof System SKH Axioms TAUT all axioms of propositional logic DISTK Kp ∧ K(p → q) → Kq T Kp → p 4 Kp → KKp 5 ¬Kp → K¬Kp AxKtoKh Kp → Khp AxKhtoKhK Khp → KhKp AxKhtoKKh Khp → KKhp AxKhKh KhKhp → Khp AxKhbot Kh⊥ → ⊥ Rules MP ϕ, ϕ → ψ ψ NECK ϕ Kϕ MONOKh ϕ → ψ Khϕ → Khψ SUB ϕ(p) ϕ[ψ/p]
Note that we have the S5 axioms for K. AxKtoKh says if p is known then you know how to achieve p by doing nothing (we allow the empty strategy). AxKhtoKhK reflects the first condition in the semantics that the goal is known after the executions. We will come back to this axiom at the end of the paper. Note that the termination condition is not fully expressible in our language, but AxKhbot captures part of it by ruling out strategies that have no terminating executions at all. AxKhKh essentially says that strategies can be composed. Its validity proof is quite involved and we devote the next subsection to it. Finally, AxKhtoKKh is the positive introspection axiom for Kh; it is valid due to uniformity of strategies. The corresponding negative introspection can be derived from axioms AxKhtoKKh, 5 and T: Proposition 3.1. ⊢ ¬Khp → K¬Khp.

It is also not hard to show that in SKH, Khp is provably equivalent to KKhp, KhKp, and KhKhp.

Note that we do not have the K axiom for Kh. Instead, we have the monotonicity rule MONOKh. In fact, the logic is not normal, as desired, e.g., Khp ∧ Khq → Kh(p ∧ q) is not valid: the existence of two different strategies for different goals does not imply the existence of a unified strategy to realize both goals.

Validity of AxKhKh

AxKhKh is about the "sequential" compositionality of strategies. Suppose on some pointed model there is a strategy σ to guarantee that we end up with the states where on each s of them we have some other strategy σ s to make sure p (KhKhp). Since the strategies are uniform, we only need to consider some σ [s] for each [s]. Now to validate AxKhKh, we need to design a unified strategy to compose σ and those σ [s] into one strategy to still guarantee p (Khp). The general idea is actually simple: first, order those leaf nodes [s] (using Axiom of Choice); then by transfinite induction adjust σ [s] one by one to make sure these strategies can fit together as a unified strategy θ; finally, merge the relevant part of σ with θ into the desired strategy. We make this idea precise below. First we need an observation:

Proposition 3.2. Given strategies τ and σ with τ ⊆ σ, if [s] ∈ dom(τ ) and dom(σ) ∩ CELeaf(τ, s) = ∅, then a se- quence is σ's complete execution from [s] if and only if it is τ 's complete execution from [s]. Proof. Left to Right: Let [s 0 ] • • • [s n ] • • • be a σ's complete execution from [s] (it also means that [s] = [s 0 ]
, similarly in later proofs). We will show it is also a τ 's complete execution from [s]. Firstly, we show it is a possible execution give τ from [s]. If it is not, there exists [s i ] such that [s i ] is not the leaf-node of this execution and such that [s i ] ∈ dom(τ ). Let [s j ] be the minimal equivalence class in the sequence with such properties. It follows that [s j ] ∈ CELeaf(τ, s) and [s j ] ∈ dom(σ). These are contradictory with dom(σ) ∩ CELeaf(τ, s) = ∅.

Next we will show that

[s 0 ] • • • [s n ] • • • is a τ 's complete execution from [s]. It is obvious if the sequence is infinite. If it is finite, let the leaf-node be [s m ]. It follows that [s m ] ∈ dom(σ). Since τ ⊆ σ, it follows [s m ] ∈ dom(τ ). Therefore, the execution is complete given τ . Right to Left: Let [s 0 ] • • • [s n ] • • • be a τ 's complete exe- cution from [s], we will show it is also a σ's complete ex- ecution from [s]. Since τ ⊆ σ, it is also a possible ex- ecution given σ. If the execution is infinite, it is obvious. If it is finite, let the leaf-node be [s m ]. It follows that [s m ] ∈ CELeaf(τ, s). Since dom(σ) ∩ CELeaf(τ, s) = ∅, it follows that [s m ] ∈ dom(σ).
Therefore, the execution is also complete give σ.

Proposition 3.3. KhKhϕ → Khϕ.

Proof. Supposing M, s KhKhϕ, we will show that M, s Khϕ. It follows by the semantics that there exists a strategy σ such that all σ's complete executions from According to the well-ordering theorem (equivalent to Axiom of Choice), we assume CELeaf(σ, s) = {S i | i < γ} where γ is an ordinal number and γ ≥ 1. Let s i be an element in S i , then [s i ] = S i . Since M, s i Khϕ for each i < γ, it follows that for each [s i ] there exists a strategy σ i such that all σ i 's complete executions from [s i ] are finite and

[v] ⊆ ϕ for all [v] ∈ CELeaf(σ i , s i ) (◭).
Next, in order to show M, s Khϕ, we need to define a strategy τ . The definition consists of the following steps.

Step I. By induction on i, we will define a set of strategies τ i where 0

≤ i < γ. Let f i = β<i τ β and D i = CEInner(σ i , s i ) \ (dom(f i ) ∪ {[v] ∈ CELeaf(f i , t) | [t] ∈ dom(f i )}); we define: • τ 0 = σ 0 | CEInner(σ0,s0) ; • τ i = f i ∪ (σ i | Di ) for i > 0.
Claim 3.3.1. We have the following results:

1. For each 0 ≤ i < γ, τ j ⊆ τ i if j < i; 2. For each 0 ≤ i < γ, τ i is a partial function; 3. For each 0 ≤ i < γ, dom(τ i ) ∩ CELeaf(τ j , t) = ∅ where t ∈ dom(τ j ) if j < i; 4. For each 0 ≤ i < γ, if δ = [t 0 ][t 1 ] • • • is a τ i 's complete execution from [t] ∈ dom(τ i ) then |δ| = n for some n ∈ N and [t n ] ⊆ ϕ ; 5. For each 0 ≤ i < γ, [s i ] ∈ dom(τ i ) or [s i ] ⊆ ϕ .
Proof of Claim 3.3.1:

1. It is obvious.

2. We prove it by induction on i. For the case of i = 0, it is obvious. For the case of i = α > 0, it follows by the IH that τ β is a partial function for each β < α. Furthermore, it follows by (1) that τ β1 ⊆ τ β2 for all β 1 < β 2 < α. Thus, we have f α = β<α τ β is a partial function. Since σ α is a partial function, in order to show τ α is a partial function, we only need to show that dom(f

α )∩D α = ∅. Since D α = CEInner(σ α , s α )\ dom(f α ) \ {[v] ∈ CELeaf(f α , t) | t ∈ dom(f α )}, it is obvious that dom(f α ) ∩ D α = ∅.
3. We prove it by induction on i. It is obvious for the case of i = 0. For the case of i = α > 0, given j < α and t ∈ dom(τ j ), we need to show that dom(τ

α ) ∩ CELeaf(τ j , t) = ∅. Supposing [v] ∈ CELeaf(τ j , t), we will show that [v] ∈ dom(τ α ), namely [v] ∈ dom(f α ) ∪ D α . Since j < α and f α = β<α τ α , it follows t ∈ dom(f α ). Moreover, due to D α = CEInner(σ α , s α ) \ (dom(f α ) ∪ {[v] ∈ CELeaf(f α , t) | t ∈ dom(f α )}), it follows [v] ∈ D α . Next, we only need to show [v] ∈ dom(f α ). Assuming [v] ∈ dom(f α ), it follows that [v] ∈ dom(τ β ) for some β < α. There are two cases: j < β or j ≥ β. If j < β, it follows by the IH that dom(τ β ) ∩ CELeaf(τ j , t) = ∅. Contradiction. If j ≥ β, it follows by (1) that τ β ⊆ τ j . Due to [v] ∈ dom(τ β ), it follows [v] ∈ dom(τ j ). It is contradictory with [v] ∈ CELeaf(τ j , t). Thus, we have [v] ∈ dom(f α ).
4. We prove it by induction on i. For the case of i = 0, due to dom(τ 0 ) = CEInner(σ 0 , s 0 ), it follows that there is a σ 0 's possible execution

[s 0 ] • • • [s m ] such that m ∈ N and [s m ] = [t]. Let µ = [s 0 ] • • • [s m-1 ] • δ. (If m = 0 then µ = δ). Since δ is a τ 0 's complete ex- ecution from [t], it follows that µ is a σ 0 's complete execution from [s 0 ]. It follows by (◭) that µ is finite. Thus, δ = [t 0 ] • • • [t n ] for some n ∈ N. Since [t n ] ∈ CELeaf(σ 0 , s 0 ), it follows by (◭) that [t n ] ⊆ ϕ .
For the case of i = α > 0, there are two situations:

[t] ∈ dom(f α ) or [t] ∈ D α . If [t] ∈ dom(f α ), it follows that [t] ∈ dom(τ β ) for some β < α. By (3), we have dom(τ α )∩CELeaf(τ β , t) = ∅. Since δ is a τ α '
= [t 0 ] • • • is τ α 's complete execution from [t] ∈ dom(τ α )).
-[t k ] ∈ dom(τ β ) for some k < |δ| and some β < α:

It follows that µ = [t k ] • • • is a τ α '
] ∈ dom(τ β ), it follows that δ = [t 0 ] • • • is a σ α 's possible execution from [t]. Since [t] ∈ D α ⊆ CEInner(σ α , s α ), there is a σ α 's possible execu- tion [s 0 ] • • • [s m ] s.t. m ∈ N, [s 0 ] = [s α ] and [s m ] = [t]. Let µ = [s 0 ] • • • [s m-1 ] • δ. (If m = 0 then µ = δ).
It follows that µ is σ α 's possible execution from s α . By (◭), all σ α 's complete executions from s α are finite. Thus, µ is finite. Therefore, δ

= [t 0 ] • • • [t n ] for some n ∈ N. We continue to show that [t n ] ⊆ ϕ . Since δ = [t 0 ] • • • [t n ] is a τ α 's complete execution from [t]
and it is also a σ α 's possible execution from t, there are two cases:

[t n ] ∈ CELeaf(f α , t ′ ) for some t ′ ∈ dom(f α ), or δ is a σ α 's complete execution from t. If [t n ] ∈ CELeaf(f α , t ′ ) for some [t ′ ] ∈ dom(f α ), then there exists β < α s.t. [t] ∈ CELeaf(τ β , t ′ ) and [t ′ ] ∈ dom(β). By IH, [t n ] ⊆ ϕ . If δ is a σ α 's complete execution from [t], it follows that µ is a σ α 's complete execution from [s α ]. Then by (◭), we have [t n ] ⊆ ϕ . 5. If [s i ] ∈ dom(σ i ), it follows by (◭) that [s i ] ⊆ ϕ .
Otherwise, there are two cases: i = 0 or i = α > 0.

If i = 0, it follows by [s 0 ] ∈ dom(σ 0 ) that [s 0 ] ∈ CEInner(σ 0 , s 0 ). Thus, [s 0 ] ∈ dom(τ 0 ). If i = α > 0 and [s α ] ∈ dom(σ α ), we will show that if [s α ] ∈ dom(τ α ) then [s α ] ⊆ ϕ . Firstly, we have that [s i ] ∈ CEInner(σ α , s α ). Since [s α ] ∈ dom(τ α ), it follows that [s α ] ∈ CELeaf(f α , t) for some [t] ∈ dom(f α ).
It follows that there exists β < α such that [s α ] ∈ CELeaf(τ β , t) and t ∈ dom(τ β ). It follows by (4) that [s i ] ⊆ ϕ .

Step II. We define τ γ = i<γ τ i . It follows by ( 1) and ( 2) of Claim 3.3.1 that τ γ is indeed a partial function. Then we prove the following claim.

Claim 3.3.2. If δ = [t 0 ] • • • is a τ γ 's complete execution from [t] ∈ dom(τ γ ) then |δ| = n for some n ∈ N
= µ. If not, then δ = [t 0 ] • • • [t n ][t n+1 ] • • • .
We then have that there exists j < γ such that {t k | 0 ≤ k ≤ n} ⊆ dom(τ j ). It cannot be that j ≤ i. Otherwise, µ is not τ i 's complete execution since τ j ⊆ τ i by (1) of Claim 3.3.1. Thus, we have j > i. Since we also have that [t n ] ∈ dom(τ j ), [t n ] ∈ CELeaf(τ i , t) and t ∈ dom(τ i ), this is in contradiction with (3) of Claim 3.3.1. Therefore, we have δ = µ.

Step III. We define τ as τ = τ γ ∪ (σ|

C ) where C = CEInner(σ, s) \ (dom(τ γ ) ∪ {[v] ∈ CELeaf(τ ′ , t) | [t] ∈ dom(τ γ )})
and σ is the strategy mentioned at ( * ). Since both τ γ and σ| C are partial functions, τ is also a partial function. We then prove the following claim.

Claim 3.3.3. If δ = [t 0 ] • • • is a τ 's complete execution from [t] ∈ dom(τ ) then |δ| = n for some n ∈ N and [t n ] ⊆ ϕ . Proof of Claim 3.3.3: Since dom(τ ) = dom(τ γ ) ∪ C, there are two cases: [t] ∈ dom(τ γ ) or [t] ∈ C. If [t] ∈ dom(τ γ ), it follows that CELeaf(τ γ , t) ∩ C = ∅. Moreover, we have CELeaf(τ γ , t) ∩ dom(τ γ ) = ∅.
δ = [t 0 ] • • • is τ 's com- plete execution from [t] ∈ dom(τ )). • [t k ] ∈ dom(τ γ ) for some k < |δ|: It follows that µ = [t k ] • • • is a τ 's complete execution from [t k ]. Since dom(τ ) ∩ CELeaf(τ γ , t k ) = ∅, it follows by Proposition 3.2 that µ is a τ γ 's complete execution from [t k ]. It fol- lows by Claim 3.3.2 that µ = [t k ] • • • [t k+n ] for some n ∈ N and [t k+n ] ⊆ ϕ . Therefore, |δ| = k + n. • If there does not exist k < |δ| s.t. [t k ] ∈ dom(τ γ ), then δ = [t 0 ] • • • is a σ's possible execution from [t]. Since [t] ∈ C ⊆ CEInner(σ, s), then there is a σ's possible execution [s 0 ] • • • [s m ] s.t. m ∈ N, [s 0 ] = [s] and [s m ] = [t]. Let µ = [s 0 ] • • • [s m-1 ]•δ. (If m = 0 then µ = δ).
It follows that µ is σ's possible execution from s. By ( * ), all σ's complete executions from s are finite. Thus,

µ is finite. Therefore, δ = [t 0 ] • • • [t n ] for some n ∈ N. We continue to show that [t n ] ⊆ ϕ . Since δ = [t 0 ] • • • [t n
] is a τ 's complete execution from t and it is also a σ's possible execution from t, there are two cases:

[t n ] ∈ CELeaf(τ γ , t ′ ) for some t ′ ∈ dom(τ γ ), or δ is a σ's complete execution from t. If [t n ] ∈ CELeaf(τ γ , t ′ ) for some [t ′ ] ∈ dom(τ γ ), it follows by Claim 3.3.2 that [t n ] ⊆ ϕ . If δ is a σ's complete execution from [t], it follows that µ is a σ's complete execution from [s]. It follows that [t n ] = S i for some 0 ≤ i < γ. Since δ = [t 0 ] • • • [t n ] is τ 's complete execution from [t] ∈ dom(τ γ ), it follows [t n ] ∈ dom(τ γ ). We then have [t n ] ∈ dom(τ i ), namely S i ∈ τ i . It follows by (5) of Claim 3.3.1 that S i ⊆ ϕ , namely [t n ] ⊆ ϕ .
Next, we continue to show that M, s Khϕ with the assumption that [s] ∈ dom(σ). Since [s] ∈ dom(σ), we have [s] ∈ CEInner(σ, s). There are two cases:

[s] ∈ dom(τ ) or not. If [s] ∈ dom(τ ), it follows by Claim 3.3.3 that M, s Khϕ. If [s] ∈ dom(τ ), due to [s] ∈ CEInner(σ, s), it follows that [s] ∈ CELeaf(τ γ , t) for some [t] ∈ dom(τ γ ). It follows by Claim 3.3.2 that [s] ⊆ ϕ . It follows that M, s Kϕ. It is obvious that M, s Khϕ.
The validity of the rest of the axioms can be checked (cf. the explanation right after the system SKH), then we have:

Theorem 3.4 (Soundness). If ⊢ ϕ then ϕ.

Completeness and Decidability

Let Φ be a subformula-closed set of formulas. It is obvious that Φ is countable since the whole language itself is countable. Given a set of formulas ∆, let:

∆| K = {Kϕ | Kϕ ∈ ∆}, ∆| ¬K = {¬Kϕ | ¬Kϕ ∈ ∆}, ∆| Kh = {Khϕ | Khϕ ∈ ∆}, ∆| ¬Kh = {¬Khϕ | ¬Khϕ ∈ ∆}.
Below we define the closure of Φ, and use it to build a canonical model w.r.t. Φ. We will show that when Φ is finite then we can build a finite model.

Definition 4.1. The closure cl(Φ) is Φ ∪ {Kϕ | ϕ ∈ Φ}. Definition 4.2 (Atom). We enumerate the formulas in cl(Φ) by {ψ i | i ∈ N}. The formula set ∆ = {Y i | i ∈ N} is an atom of cl(Φ) if • Y i = ψ i or Y i = ¬ψ i for each ψ i ∈ cl(Φ); • ∆ is consistent.
Note that if Φ is the whole language then an atom is simply a maximal consistent set. By a standard inductive construction, we can obtain the Lindenbaum-like result in our setting (which is useful to show the existence lemma for K):

Proposition 4.3. Let ∆ be an atom of cl(Φ), Γ ⊆ ∆ and ϕ ∈ cl(Φ). If Γ ∪ {±ϕ} is consistent then there is an atom ∆ ′ of cl(Φ) such that (Γ ∪ {±ϕ}) ⊆ ∆ ′ , where ±ϕ = ϕ or ±ϕ = ¬ϕ. Definition 4.4. Given a subformula-closed Φ, the canonical model M Φ = W, ACT, ∼, { x -→| x ∈ ACT}, V is defined as: • W = {∆ | ∆ is an atom of cl(Φ)}; • ACT = {ϕ | Khϕ ∈ Φ}; • ∆ ∼ ∆ ′ iff ∆| K = ∆ ′ | K ; • for each ϕ ∈ ACT, ∆ ϕ -→ ∆ ′ iff Khϕ, ¬Kϕ ∈ ∆ and Kϕ ∈ ∆ ′ ; • for each p ∈ Φ, p ∈ V (∆) iff p ∈ ∆.
Note that we use the ϕ in Khϕ formulas as the action labels, and we introduce an action transition if it is necessary, i.e., Khϕ but ¬Kϕ (i.e., empty strategy does not work). Requiring Kϕ ∈ ∆ ′ is to reflect the first condition in the semantics of Kh. Using NECK, DISTK and Proposition 4.3, it is routine to show the existence lemma for K: Proposition 4.5. Let ∆ be a state in M Φ , and Kϕ ∈ cl(Φ). If Kϕ ∈ ∆ then there exists

∆ ′ ∈ [∆] such that ¬ϕ ∈ ∆ ′ . Proof. Let Γ = ∆| K ∪ ∆| ¬K ∪ {¬ϕ}. Γ is consistent. If not, there are Kϕ i , • • • , Kϕ n and ¬Kψ 1 , • • • , ¬Kψ m in ∆: ⊢ Kϕ 1 ∧ • • • ∧ Kϕ n ∧ ¬Kψ 1 ∧ • • • ∧ ¬Kψ m → ϕ.
Following by NECK and DISTK, we have

⊢ K(Kϕ i ∧ • • • ∧ Kϕ n ∧ ¬Kψ 1 ∧ • • • ∧ ¬Kψ m ) → Kϕ.
Since the epistemic operator K is distributive over ∧ and ⊢ KKϕ i ↔ Kϕ i for all 1 ≤ i ≤ n and ⊢ K¬Kψ i ↔ ¬Kψ i for all 1 ≤ i ≤ m, we have

⊢ Kϕ i ∧ • • • ∧ Kϕ n ∧ ¬Kψ 1 ∧ • • • ∧ ¬Kψ m → Kϕ.
Since Kϕ i , • • • , Kϕ n and ¬Kψ 1 , • • • , ¬Kψ m are all in ∆ and Kϕ ∈ cl(Φ), it follows that Kϕ ∈ ∆. It is contradictory with the assumption that Kϕ ∈ ∆. Therefore, Γ is consistent. It follows by Proposition 4.3 that there exists an atom

∆ ′ of cl(Φ) such that Γ ⊆ ∆ ′ . Since (∆| K ∪ ∆| ¬K ) ⊆ ∆ ′ , we have ∆ ′ ∼ ∆, that is, ∆ ′ ∈ [∆].
Proposition 4.6. Let ∆ and ∆ ′ be two states in M Φ such that ∆ ∼ ∆ ′ . We have ∆| Kh = ∆ ′ | Kh .

Proof. For each Khϕ ∈ ∆, by Definition 4.1, Khϕ ∈ Φ. Then KKhϕ ∈ cl(Φ). For each Khϕ ∈ ∆, by Axiom AxKhtoKKh, we have KKhϕ ∈ ∆. Since ∆ ∼ ∆ ′ , then KKhϕ ∈ ∆ ′ , and by Axiom T, Khϕ ∈ ∆ ′ . Then we showed that Khϕ ∈ ∆ implies Khϕ ∈ ∆ ′ . Similarly we can prove

Khϕ ∈ ∆ ′ implies Khϕ ∈ ∆. Hence, ∆| Kh = ∆ ′ | Kh .
The following is a crucial observation for the later proofs.

Proposition 4.7. Let ∆ be a state in M Φ and ψ ∈ ACT be executable at [∆].

If Khϕ ∈ ∆ ′ for all ∆ ′ with [∆] ψ -→ [∆ ′ ] then Khϕ ∈ ∆.
Proof. First, we show that Kψ is not consistent with ¬Khϕ. Proof. We prove it by induction on ϕ. We only focus on the case of Khϕ ∈ cl(Φ); the other cases are straightforward, e.g., Kϕ case can be proved based on Proposition 4.5. Note that if Khϕ ∈ cl(Φ) then Khϕ ∈ Φ, therefore ϕ ∈ Φ since Φ is subformula-closed. Thus by Definition 4.1, Kϕ ∈ cl(Φ).

Right to Left: If Khϕ ∈ ∆, we will show M Φ , ∆ Khϕ. Firstly, there are two cases:

Kϕ ∈ ∆ or Kϕ ∈ ∆. If Kϕ ∈ ∆, then Kϕ, ϕ ∈ ∆ ′ for all ∆ ′ ∈ [∆]. Since ϕ ∈ Φ, it fol- lows by IH that M Φ , ∆ ′ ϕ for all ∆ ′ ∈ [∆]. Therefore, M Φ , ∆ Kϕ. It
-→ ∆ ′ , then [∆] ϕ -→ [∆ ′ ]. Let [∆ ′′ ] be an equivalence class s.t. [∆] ϕ -→ [∆ ′′ ], which indicates Γ ϕ -→ Γ ′′ for some Γ ∈ [∆] and Γ ′′ ∈ [∆ ′′ ]. By definition of ϕ -→ and ∼ we get Kϕ ∈ Θ for all Θ ∈ [∆ ′′ ]. By IH, M Φ , Θ ϕ for all Θ ∈ [∆ ′′ ], namely [∆ ′′ ] ⊆ ϕ . Moreover, ϕ -→ is not a loop on [∆] because ¬Kϕ ∈ ∆. Thus, the partial function σ = {[∆] → ϕ} is a strategy s.t. all its complete executions starting from [∆] are finite and [∆ ′′ ] ⊆ ϕ for each [∆ ′′ ] ∈ CELeaf(σ, ∆). Then, M Φ , ∆ Khϕ.
Left to Right: Suppose M Φ , ∆ Khϕ, we will show Khϕ ∈ ∆. By the semantics, there exists a strategy σ s.t. all σ's complete executions starting from [∆] are finite and

[Γ] ⊆ ϕ for all [Γ] ∈ CELeaf(σ, ∆). By IH, ϕ ∈ Γ ′ for all Γ ′ ∈ [Γ] and [Γ] ∈ CELeaf(σ, ∆). By Proposition 4.5, we get Kϕ ∈ Γ for all [Γ] ∈ CELeaf(σ, ∆). By Axiom AxKtoKh and Proposition 4.6, Khϕ ∈ Γ for all [Γ] ∈ CELeaf(σ, ∆). If [∆] ∈ dom(σ), it is obvious that Khϕ ∈ ∆ because [∆] ∈ CELeaf(σ, ∆). Next, we consider the case of [∆] ∈ dom(σ), then [∆] ∈ CEInner(σ, ∆).
In order to show Khϕ ∈ ∆, we will show a stronger result that Khϕ ∈ ∆ ′ for all [∆ ′ ] ∈ CEInner(σ, ∆). Firstly, we show the following claim:

Claim 4.8.1. If there exists [∆ ′ ] ∈ CEInner(σ, ∆) such that ¬Khϕ ∈ ∆ ′ then there exists an infinite execution of σ start- ing from [∆]. Proof of Claim 4.8.1: Let X be the set {[Θ] ∈ CEInner(σ, ∆) | ¬Khϕ ∈ Θ}. It follows that [∆ ′ ] ∈ X and X ⊆ dom(σ). We define a binary relation R on X as R = {([Θ], [Θ ′ ]) | [Θ] σ([Θ]) ----→ [Θ ′ ]}. For each [Θ] ∈ X, we have that σ([Θ]) is executable at [Θ].
Since ¬Khϕ ∈ Θ, by Proposition 4.7 there exists an atom Θ

′ s.t. [Θ] σ([Θ]) ----→ [Θ ′ ] and ¬Khϕ ∈ Θ ′ . Since Khϕ ∈ Γ for all [Γ] ∈ CELeaf(σ, ∆) and [Θ] ∈ CEInner(σ, ∆),we have [Θ ′ ] ∈ CEInner(σ, ∆). Then [Θ ′ ] ∈ X. Therefore, R is an entire binary relation on X, namely for each [Θ] ∈ X there is [Θ ′ ] ∈ X such that ([Θ], [Θ ′ ]) ∈ R.
Then by Axiom of Dependent Choice there exists an infinite sequence

[Θ 0 ][Θ 1 ] • • • s.t. ([Θ n ], [Θ n+1 ]) ∈ R for all n ∈ N. From the definition of R, [Θ 0 ][Θ 1 ] • • • is a complete exe- cution of σ starting from [Θ 0 ]. Since [Θ 0 ] ∈ CEInner(σ, ∆) and all complete execution of σ from [∆] are finite, there is a possible execution [∆ 0 ] • • • [∆ j ] for some j ∈ N s.t. [∆ 0 ] = [∆] and [∆ j ] = [Θ 0 ]. Therefore, [∆ 0 ] • • • [∆ j ][Θ 1 ] • • • is an infinite complete execution of σ from [∆].
Therefore, we have Khϕ ∈ ∆ ′ for all [∆ ′ ] ∈ CEInner(σ, s). Otherwise, by Claim 4.8.1 there is an infinite complete execution given σ from [∆]. This is contradictory with all σ's complete execution from [∆] are finite, then Khϕ ∈ ∆ ′ for all [∆ ′ ] ∈ CEInner(σ, s). Since [∆] ∈ dom(σ), we get [∆] ∈ CEInner(σ, ∆). Then Khϕ ∈ ∆. Now let Φ be the set of all formulas, then each maximal consistent set ∆ is actually an atom which satisfies all its formulas in M Φ , according to the above truth lemma. Completeness then follows immediately.

Theorem 4.9. SKH is strongly complete.

Note that if Φ is the set of all subformulas of a given formula ϕ, then cl(Φ) is still finite. Due to the soundness of SKH and Proposition 4.3, a satisfiable formula ϕ must be consistent thus appearing in some atom, and thus ϕ is satisfiable in M Φ . It is not hard to see that |M Φ | ≤ 2 2|ϕ| where 2|ϕ| is the bound on the size of cl(Φ). This gives us a small model property of our logic, then decidability follows.

Theorem 4.10. SKH is decidable.

Conclusion

In this paper, we propose an epistemic logic of both (goaldirected) knowing how and knowing that, and capture their interactions. A sound and complete proof system SKH is obtained, and we prove the decidability of the logic. We hope the axioms are illuminating towards a better understanding of knowing how.

Note that we do not impose any special properties between the interaction of a -→ and ∼ in the models so far. In the future, it would be interesting to see whether assuming properties of perfect recall and/or no learning (cf. e.g., [START_REF] Fagin | [END_REF][START_REF] Wang | Not all those who wander are lost: Dynamic epistemic reasoning in navigation[END_REF]) changes the logic or not.

Our notion of knowing how is relatively strong, particularly evidenced by the axiom AxKhtoKhK : Khϕ → KhKϕ, which is due to the first condition of our semantics for Kh, inspired by planning with uncertainty. We believe it is reasonable for the scenarios where the agent has perfect recall (or, say, never forgets), which is usually assumed implicitly in the discussions on planning (cf. [Li et al., 2017]). However, for a forgetful agent it may not be intuitive anymore, e.g., I know how to get drunk when sober but I may not know how to get to the state that I know I am drunk, assuming drunk people do not know they are drunk. The axiom AxKhKh is also interesting in distinguishing different types of knowing how. We have been focusing on the goaldirected knowing how [Gochet, 2013], but for other types of knowing how such as knowing how to swim, the axiom may not be reasonable anymore, e.g., I know how to let myself to know how to swim (by registering an excellent swimming course) does not mean that I know how to swim right now. We leave the discussion of other types of knowing how in the future. Moreover, by introducing suitable notions of bisimulations we will be able to compare their expressive power. Another obvious next step is to consider knowing how in multi-agent settings, which brings us closer to coalition logics (cf. e.g., [START_REF] Ågotnes | Epistemic coalition logic: completeness and complexity[END_REF][START_REF] Naumov | [END_REF].

Figure 1 :

 1 Figure 1: A scenario representing how to cure the pain.

  [s] are finite and [t] ⊆ Khϕ for all [t] ∈ CELeaf(σ, s) ( * ). If [s] ∈ dom(σ), then CELeaf(σ, s) = {[s]},and then it is trivial that M, s Khϕ. Next we focus on the case of [s] ∈ dom(σ).

ψ

  -→, ∼ and Proposition 4.6, Khψ, ¬Kψ ∈ ∆. It follows that∆ ψ -→ Γ, then [∆] ψ -→ [Γ]. This is in contradiction with the assumption that Khϕ ∈ ∆ ′ for all ∆ ′ with [∆] ψ -→ [∆ ′ ]. Then Kψ is not consistent with ¬Khϕ. Hence, ⊢ Kψ → Khϕ.Since ⊢ Kψ → Khϕ, it follows by Rule MONOKh and Axiom AxKhtoKhK that ⊢ Khψ → KhKhϕ. Moreover, it follows by Axiom AxKhKh that ⊢ Khψ → Khϕ. Since ψ is executable at [∆], it follows by the definition of ψ -→ and Proposition 4.6 that Khψ ∈ ∆. Therefore, we have Khϕ ∈ ∆.Lemma 4.8. For each ϕ ∈ cl(Φ), M Φ , ∆ ϕ iff ϕ ∈ ∆.

. For each s ∈ W , we use [s] to denote the equivalence class {t ∈ W | s ∼ t}, and use [W ] to denote the collection of all the equivalence classes on W w.r.t. ∼. We use [s] a -→ [t] to indicate that there are s

  s complete execution from [t k ]. By (3) and Proposition 3.2, µ is a τ β 's complete execution from [t k ]. By IH, µ = [t k ] • • • [t k+n ] for some n ∈ N and [t k+n ] ⊆ ϕ . Therefore, |δ| = k + n.-If there does not exist k < |δ| and β < α s.t.[t k

  Thus, we have CELeaf(τ γ , t) ∩ dom(τ ) = ∅. It follows by Proposition 3.2 that δ is a τ γ 's complete execution from from [t]. It follows by Claim 3.3.2 |δ| = n for some n ∈ N and [t n ] ⊆ ϕ . If [t] ∈ C, there are two cases: there exists k < |δ| such that [t k ] ∈ dom(τ γ ), or there does not exists such k. (Please note that |δ| > 1 due to the fact that

  It is obvious that Khϕ ∈ cl(Φ). Since ψ is executable at [∆], there are atoms Γ 1 and Γ 2 s.t. Γ 1 ψ -→ Γ 2 . Then Kψ ∈ Γ 2 . Assuming that Kψ is consistent with ¬Khϕ, by Proposition 4.3 there exists an atom Γ of cl(Φ) s.t. {Kψ, ¬Khϕ} ⊆ Γ. Since ψ ∈ ACT is executable at [∆], then by definition of

  follows by Axiom AxKtoKh and the soundness of SKH that M Φ , ∆ Khϕ. If ¬Kϕ ∈ ∆, we first show that Kϕ is consistent. If not, namely ⊢ Kϕ → ⊥, it follows by Rule MONOKh that ⊢ KhKϕ → Kh⊥. It follows by Axiom AxKhbot that ⊢ KhKϕ → ⊥. Since Khϕ ∈ ∆, it follows by Axiom AxKhtoKhK that ∆ ⊢ ⊥, which is in contradiction with the fact that ∆ is consistent. Therefore, Kϕ is consistent.By Proposition 4.3 there exists an atom ∆ ′ s.t. Kϕ ∈ ∆ ′ . Note that ϕ ∈ ACT. Thus, we have ∆

	ϕ

Acknowledgements

Raul Fervari has received funding from the European Union's Horizon 2020 research and innovation programme under the Marie Skodowska-Curie grant agreement No. 690974 for the project MIREL: MIning and REasoning with Legal texts, SeCyT-UNC and ANPCyT-PICT-2013-2011. Yanjun Li thanks the support from China Scholarship Council (CSC). Yanjing Wang acknowledges the support from the National Program for Special Support of Eminent Professionals, and the NSSF key project 12&ZD119.


Tarek A Eimeligy

Enrica Epifano

Maxim Sokot

Gilles Hug

Marcus Hans

Jochen M Schneider

Michel W Barsoum
email: barsoumw@drexel.edu

Tarek A Orcid

G Elmeligy

Isothermal Oxidation of Ti 3 Al 0 . 6 Ga 0 . 4 C 2 MAX Phase Solid Solution in Air at 1000 °C to 1300 °C

The atomically laminated TI 2 AIC, Ti 3 AIC 2 and Cr 2 AIC MAX phases, with A Al, fonn adherent, passivating a alumina, Al 2 O 3 , oxide scales when heated in air. The effect of sol id solutions on the A layers in affecting the oxidation kinetics remains a subject of open research. Herein we synthesize a dense bulk polycrystalline Ti 3 Al 1 .Ga.C 2 (x ::::; 0.4) solid solution and investigate its isothermal oxidation in ambient air, in the 1000 °C 1300 °C temperature range, for limes varying between 15 and 300 h. At 1000 °C, a passivating dense Al 2 O 3 layer (::::; 1 2.6 µ,m thick) with near cubic kinetics and an overall weight gain that is slightly less than either TI 3 AICi or Ti 2 AIC is formed. At 1200 °C, the Al 2 O 3 layer thickens (3.5 12 µ,m thick) with some scale delamination on the corners initiating at 15 h. At 1300 °C, the Al 2 O 3 layer (7.6 20.7 µ,m truck) wrinkles and Al 2 TiO 5 forms. Though the Al 2 O 3 grains coarsen at 1200 °C and 1300 °C, the weight gain is higher than that for Ti 3 AIC 2 or Ti 2 AIC. At around 7 at. %, this is one of the lowest, if not lowest, Al mole fraction in a Ti based alloy/compound that forms an Al 2 O 3 passivating layer. We further provide compelling microstructural evidence, in the form of a duplex oxide, that at 1000 °C, the outward Al flux, J Ah and the inward O flux, J 0 , are related such that 2 J A1 3 Jo-A fraction of these fluxes combine, at the duplex oxide interface, to nucleate small grains [DOi: 10. 1149/1945 7111/ac58c1

suggests that the oxidation behavior in all high perforrning Al 2 0 3 forrning systems is ultimately controlled by the same under lying mechanism, namely, 0 and/or Al diffusion through o Al 2 0 3 grain boundaries, GBs. Essentially, both AFAS and Al 2 0 3 forrning MAX compounds act as Al reservoirs that enable fast diffusion of Al towards the reservoir/Al 2 0 3 interface, where it reacts with oxygen to form the protecti ve Al 2 0 3 layer.

Smialek's work 2() further elucidates the rate controlling me chanism of GB diffusion across the growing Al 2 0 3 grains leading to cubic oxidation kinetics across various Al 2 0 3 forrning alloys and compounds. It is also important to note that Al 2 0 3 has a coefficient of thermal expansion (CTE) close to that of Ti 2 AIC. As a result, the stresses thermally induced in the scales are relatively low [START_REF] Byeon | Microstructure and residual stress of alumina scale formed on Ti 2 AlC at high temperature in air[END_REF] compared to other MAX phases making them resistant to spallation even after 10,000 thermal cycles to 1350 °C. [START_REF] Sundberg | Alumina forming high temperature silicides and carbides[END_REF] Severa! research groups have focused on developing Al based MAX solid solutions. For exam p le, Ti 3 (Ai r -xSix)C 2 , 29 3 t Ti�xSn r -xC/2, [START_REF] Huang | Strengthening and tribological surface self-adaptability of Ti 3 AlC 2 by incorporation of Sn to form Ti 3 Al(Sn)C 2 solid solutions[END_REF] and Ti 2 Al(C r -xNx) [START_REF] Roberis | Structural Materials in Nuclear Power Systems[END_REF] ' [START_REF] Barsoum | Processing and characterization of Ti 2 AlC, Ti 2 AlN, and Ti 2 AlC 0 5 N 0 5[END_REF] show improved mechan ical properties due to a solid solution hardening effect. Others, such as Cr 2 (Air-xSix)C, 36 (Ti,Nb) i AIC [START_REF] Roberis | Structural Materials in Nuclear Power Systems[END_REF] 7 • 38 exhibit solid solution soft ening. The reasons for these observations remain a subject of study, but clearly show that it is possible to tune MAX phase properties by solid solution alloying on the A layers.

The challenge is to enhance the mechanical properties most importantly, creep resistance without sacrifi cing the oxidation resistance. Gao et al. showed that the compressive strength of Ti J CAir-xSix)C 2 solid solutions can be improved by more than 30% compared to their end members, 29 notably without sacrifi cing their oxidation resistance. However, looking for optimal Al MAX solid solutions that could potentially provide both improved mechanical properties in general, and creep properties in particular, as well as, maintaining their excellent oxidation resistance remains uncharted territory.

Herein, we chose to alloy Ga on the Al layers hoping that a mixed Ga 2 0 3 and Al 2 0 3 oxide would form that would have even better oxidation resistance than Al 2 0 3 alone. Ga 2 0 3 and Al 2 0 3 oxide form a complete solid solution over the entire composition range. [START_REF] Hill | The System Alumina-Gallia-Water[END_REF] To that effect, we successfully synthesized a fully dense, bulk Ti 3 Al 1-x Ga x C 2 solid solution with x ≈ 0.4 and studied its iso thermal oxidation in ambient air, in the 1000 °C 1300 °C tempera ture range, for times as long as 300 h. Although we did not obtain a mixed oxide, we did form an Al 2 O 3 scale despite the fact that the Al atomic content was only 10%.

Experimental

Synthesis. To synthesize Ti 3 AlC 2 , Ti, TiC and Al reagents were mixed in molar ratios listed in Table I. The powders were mixed in a polyethylene jar with zirconia milling balls for ∼9 h. The mixed powders were inserted, and hand compacted in a 38.1 mm diameter graphite die coated with boron nitride, BN, release spray and layered with graphite foil. The powder mix was reactively hot pressed (HPed) under a load corresponding to a pressure of ∼12 MPa, applied 15 min after reaching the dwell temperature. The heating rate was 400 °C h -1 , with a dwell time of 5 h at 1500 °C. After furnace cooling, the sample's surfaces were ground using coarse diamond pads (120 grit) to remove residual graphite foil bonded to its surface. The sample was then milled using a TiN coated end mill bit to obtain Ti 3 AlC 2 powder.

To synthesize Ti 3 GaC 2 , Ti, TiC, and Ga reagents listed in Table I were mixed in tabulated molar ratios. In this case, Ga, in the form of a solid rod, was placed in a polyethylene jar together with the other powders. The jar was heated to 50 °C for 0.5 h until Ga melted and wetted the other reactant powders. After cooling to room tempera ture, RT, the mixture was ball mixed for ∼9 h. The powders were then reactively hot pressed at a rate of 400 °C h -1 , up to 1400 °C, and held at that temperature for 3 h at a stress of 12 MPa applied 15 m after reaching the dwell temperature. The HPed samples were then drilled to obtain Ti 3 GaC 2 powders.

To fabricate the solid solution, the Ti 3 AlC 2 and Ti 3 GaC 2 powders were sieved to 325 mesh size, mixed in 3:2 molar ratio and ball milled for ∼9 h. The mixture was HPed at 1500 °C for 5 h at 400 °C h -1 and a load corresponding to a stress of ∼22 MPa.

The HPed Ti 3 Al 0.6 Ga 0.4 C 2 sample of 38.3 mm diameter and 2.5 mm thickness was ground with coarse diamond pads to remove residual graphite bonded to the surface. The sample was then progressively ground and polished using SiC paper in the 400 1200 grit range and cleaned with ethanol and dried.

Oxidation testing. Bulk samples were electrically discharge machined (EDMed) into rectangular slabs (5.8 × 5.8 × 2.3 mm 3 ). Prior to characterization, the samples were re polished with 1200 grit SiC paper and finally down to 3 μm with a diamond suspension. This step is important to remove any residue from the EDM step that can interfere with the formation of the Al 2 O 3 layer.

A Textured Ti 2 AlC rectangular slab (6.4 × 4.8 × 1.8 mm 3 ), used for grain size comparison, was machined out of a bulk sample with a diamond coated saw and polished using SiC paper in the 400 1200 grit range then cleaned with ethanol and dried. The synthesis procedure for the textured Ti 2 AlC is mentioned elsewhere. [START_REF] Shamma | In situ neutron diffraction evidence for fully reversible dislocation motion in highly textured polycrystalline Ti 2 AlC samples[END_REF] The samples were first weighed before placing them in Al 2 O 3 crucibles that were in turn placed in a box furnace and heated under static, ambient air. Experiments were performed at 1000 °C, 1200 °C, and 1300 °C. The samples were placed inside the furnace near the center of the hot zone and heated at 4 °C min -1 up to the target oxidation temperature. Samples were periodically taken out at each oxidation temperature. The oxidized samples were visually inspected, weighed, and checked for macroscopic changes in their dimensions.

Characterization. XRD was performed using a powder dif fractometer (SmartLab, Rigaku Corp., Tokyo, Japan) with Cu Kα radiation in Bragg Brentano scan mode. Drilled powder XRD patterns of Ti 3 AlC 2 , Ti 3 GaC 2 precursors, and the Ti 3 Al 0.6 Ga 0.4 C 2 solid solution were obtained before oxidation. The powder samples were scanned in the 2θ = 5 150°range, with a step size of 0.02°and a dwell time of 4.5 s per step. Lattice parameters of the end members and the reactively HPed solid solution Ti 3 Al 0.6 Ga 0.4 C 2 powders were determined from Rietveld analysis of the XRD patterns, using the Fullprof Suite. [START_REF] Rodríguez-Carvajal | Recent advances in magnetic structure determination by neutron powder diffraction[END_REF] Statistical uncertainties in all subsequent measure ments are included in parentheses after each value. The Rietveld refinements were all performed using the crystal structure of Ti 3 AlC 2 , (P6 3 /mmc space group), where Ti atoms occupy the 2a and 4 f Wyckoff positions, Al atoms are in 2b positions and C atoms are in 4 f positions. Lattice parameters and atomic positions were all refined during the analysis. A Pseudo Voigt function was adopted for the peak shape profile. The XRD patterns were satisfactorily refined, with goodness parameters R p < 13 and R wp < 12.

XRD patterns were acquired from the oxidized surfaces in the 5°100°2θ range with a step size of 0.02°and dwell time of 0.6 s per step. Phase identification of the oxide phases formed on the surface was performed by profile matching of XRD patterns.

Micrographs and relative elemental compositions, phase analysis, and elemental maps were obtained using a scanning electron microscope, SEM (Zeiss Supra 50 VP, Carl Zeiss SMT AG, Oberkochen, Germany), equipped with an energy dispersive X ray spectroscope, EDS, (Oxford EDS, Oxfordshire, United Kingdom). The reported EDS values represent a combination of spot and area scans selected from various regions on samples polished to 1 μm. An accelerating voltage of 20 kV and 15 60 s dwell times were used for the EDS measurement at a 15 mm working distance (WD) and a 60 μm aperture size.

The oxidized samples were also examined in an SEM to view their surface oxide morphologies. Fractured oxidized samples were cold mounted in epoxy and ground first using 240 1200 SiC grit paper and then down to 1 μm with diamond suspension. Oxide scale thicknesses were measured from the SEM micrographs using ImageJ software with each data point being the arithmetic mean of 1024 equally spaced measurements along the scale length with the aid of a slicing addon. The oxide scale grain sizes were estimated from both oxidized sample surfaces and fracture surface micrographs by taking the average measurement of 5 40 grains across the oxide thickness.

In addition, the microstructure of the sample oxidized at 1000 °C for 300 h was characterized by scanning transmission electron microscopy (STEM). A cross sectional thin lamella was prepared by focused ion beam (FIB) techniques in a dual beam microscope (Helios Nanolab 660, FEI, Hillsboro, OR, USA) and Ga ions were used at an acceleration voltage of 30 kV. First, the region of interest from the oxidized sample surface was protected with a 2 μm thick Pt layer. After trench milling, the lamella was extracted with an EasyLift manipulation needle and placed on a Cu omniprobe. Sequential thinning of the lamella to a final thickness of approxi mately 80 nm was done using currents of 0.79, 0.43, 0.23, and 0.08 μA. Bright field images were acquired using a STEM III detector at 30 kV acceleration voltage. EDS line profiles with a step size of 50 nm were performed at 10 kV acceleration voltage using an Octane Elect detector.

Local chemical composition analysis of the interface between oxide scale and MAX phase (1000 °C, 300 h) was carried out by three dimensional atom probe tomography (APT). The local elec trode atom probe (LEAP 4000X HR, Cameca, Madison, WI, USA) was equipped with a reflectron and the flight path length was 382 mm. Field evaporation was employed by thermal pulsing with a UV laser at 50 pJ energy and 125 kHz frequency. The base temperature was 60 K, the detection rate was set at 5 ions out of 1000 pulses and 7 million ions were collected. IVAS 3.8.6 was used for the reconstruction of atomic positions and data analysis. Needle shape atom probe specimens were prepared by FIB according to a standard protocol and the oxide scale was removed close to the oxide MAX phase interface at 5 kV and 40 pA in order to reduce the contamination from Ga ions used for specimen preparation [START_REF] Thompson | In situ site-specific specimen preparation for atom probe tomography[END_REF]

Results

Solid-solution phase structure and composition. Rietveld re finement of XRD patterns was used to estimate phase composition as well as lattice parameters, LPs (Fig. S2 (available online at stacks. iop.org/JES/169/031510/mmedia)). [START_REF] Rietveld | A profile refinement method for nuclear and magnetic structures[END_REF] The fitting was based on a hexagonal crystal structure (space group P 6 3 /mmc), with refined lattice parameters of a = b = 3.083 Å and c = 18.455 Å. EDS spot and area analysis of bulk Ti 3 Al 0.6 Ga 0.4 C 2 cross sections (not shown). shows a Ga:(Ga+Al) ratio of (0.37 ± 0.03):1 which implies x ≈ 0.4. The fracture surface in Figs. S3a S3b demonstrates the typical nano laminated MAX structure with an average grain size of 35 ± 10 μm.

Isothermal Oxidation kinetics and activation energies. The time, t, dependence of the mass gain per unit area, ΔW/A, obtained at 1000 °C, 1200 °C, and 1300 °C is shown in Fig. 1a. Each data point represents a different sample. At 1000 °C, the mass increase is initially rapid with time before slowing down. At this temperature, initially the mass gain for the Ti 3 Al 0.6 Ga 0.4 C 2 sample is 15% less than that reported for either Ti 2 AlC or Ti 3 AlC 2 . 44 46 After 300 h, the Ti 3 Al 0.6 Ga 0.4 C 2 weight gain is about 20% lower than that of Ti 2 AlC 45 and 14% lower than that reported for Ti 3 AlC 2 . [START_REF] Tallman | A critical review of the oxidation of Ti 2 AlC, Ti 3 AlC 2 and Cr 2 AlC in Air[END_REF] After 300 h of oxidation at 1200 °C, the weight gain for the solid solution is greater than that of Ti 2 AlC and Ti 3 AlC 2 by ≈ 57% and ≈ 45%, respectively (Fig. 1a).

At 1300 °C the weight gain after 240 h of oxidation for our solid solution is more than double that of Ti 2 AlC and Ti 3 AlC 2 . At 1300 °C, the Al 2 TiO 5 phase also forms through a reaction between TiO 2 and Al 2 O 3 . Given this poor oxidation resistance, the results at this temperature will only be discussed in a cursory manner.

The ΔW/A results were analyzed assuming cubic, parabolic and power law kinetics, assuming the following relationships were operative, respectively:

⎜ ⎟ ⎛ ⎝ ⎞ ⎠ Δ = [ ] W A k t 1 c w 3 , ⎜ ⎟ ⎛ ⎝ ⎞ ⎠ Δ = [ ] W A k t 2 p w 2 , Δ = ′ [ ] W A k t 3 n where ′ k k and k , c w p w , ,
are the cubic, parabolic, and power law constants, respectively; n is the power law exponent. The estimated rate constants, rate exponents n and corresponding correlation II. An alternative method for estimation of parabolic weight gain rate constants was formu lated by Pieraggi [START_REF] Pieraggi | Calculations of parabolic reaction rate constants[END_REF] by using the slope of the weight gain with the square root of time. These rate constants are summarized in Table S1 and Fig. S1. The results are within the same order of magnitude as the rate constants obtained from weight gain versus time curves.

The temperature and time dependencies of the oxide thickness, x, are plotted in Fig. 1b. A summary of the fits where the k p values in Eqs. 1 to 3 are replaced by k x , and ΔW/A is replaced by x are shown in Table III , values were multiplied by (3950 kg m -3 × 0.47) 3 = (6.4 × 10 9 ), where 0.47 is the mass fraction of O in α Al 2 O 3 . Figure 1c compares both actual measured weight gain with predicted weight gain based on cubic scale thickening kinetics converted to weight gain. At 1000 °C the agreement is excellent. At 1200 °C, the experimental points are higher than those predicted on oxide thickness alone. At 1300 °C the discrepancy is even higher.

The fitted cubic rate constants may be correlated to temperature through an Arrhenius type equation:

⎜ ⎟ ⎛ ⎝ ⎞ ⎠ = - [ ] k k Q RT exp 4 c w , 0
where k 0 is the pre exponential factor, R is the universal gas constant and T is the absolute temperature while Q is the apparent or effective activation energy representing the rate controlling step of the operative diffusion mechanism. Figure 1d plots the best fit line of weight gain rate constant as a function of reciprocal temperature, the slope of the linear fit based on cubic kinetics yields an apparent activation Q app = 191 kJ mol -1 . 1300 °C data point is excluded from activation energy calculation due to the formation of Al 2 TiO 5 at that temperature.

XRD on oxidized samples. XRD patterns before and after oxidation are shown in Figs. 2 4, at 1000 °C, 1200 °C, and 1300 °C, respectively, as a function of time. For all three cases, the appearance of additional peaks is observed in the oxidized samples, as expected. Moreover, a small shift of the Ti 3 Al 0.6 Ga 0.4 C 2 reflections toward higher angles was systematically observed.

At 1000 °C, the MAX peaks in the oxidized sample remain the most intense, even after 300 h of oxidation, implying the scale must be quite thin. Next to the substrate peaks, α Al 2 O 3 peaks are clearly observed in all oxidized samples, at all times. A very low intensity peak around 27.46 °that coincides with the most intense (110) reflection in TiO 2 was observed after 100 h.

After oxidation at 1200 °C, for 24 h, the intensities of the Al 2 O 3 peaks are higher than those of the MAX phase.

After oxidation at 1300 °C, the Al 2 O 3 peak intensities dominate at times as low as 48 h. TiO 2 peaks are visible after 15 h of oxidation. The intensity of these peaks is still quite low in comparison to the other observed phases, but higher than those observed at the lower temperatures. At 1300 °C, an additional phase (marked as * in Fig. 4) can be observed from 48 h onward, corresponding to Al 2 TiO 5 . No pure Ga oxide peaks were observed in any of the oxidized samples.

Scale morphologies, phase compositions, and grain growth. At 1300 °C, localized thick TiO 2 regions form on top of the Al 2 O 3 after 15 h (Fig. 5i), and the Al 2 O 3 layers wrinkle (Fig. 5r). Cracks are observed to propagate through TiO 2 and Al 2 TiO 5 (Fig. 5i).

Surface EDS map after oxidation at 1000 °C for 15 h (Fig. 6a) shows a dense α Al 2 O 3 surface with sparse TiO 2 islands. Polished cross section (Fig. 6b) indicates trace amounts of Ti and Ga in the vicinity of the Al 2 O 3 layer which is most likely originating from the MAX phase. Al rich intermetallic impurities with Ti:Al:Ga molar ratio of 1.00:1.60 ± 0.2:0.21 ± 0.01 are identified along the MAX GBs (Fig. 6b). At 300 h, the surface morphology shows imprinted ridges in the oxide along the substrate GBs (Fig. 6c). Al 2 O 3 extends through surface cracks (Fig. 6d) to form sub surface Al 2 O 3 , this phenomenon may lead to susceptibility to thermal cycling. After 300 h, the Al 2 O 3 layer thickens (Figs. 6b,6d). Interestingly if the TiO 2 islands coarsened (Figs. 6a,6c) it is not very noticeable. Their density increases slightly. No TiC regions are detected.

After oxidation at 1200 °C EDS maps (Fig. S4) show no qualitative differences in the surface morphologies and cross sectional SEM micrographs of the scale. Here again, TiO 2 particles appear on the surface of a dense, adherent Al 2 O 3 layer (Figs. S4a S4h). Not surprisingly, the grain sizes of both phases coarsen. Pores (Fig. S4g) are observed between the TiO 2 and Al 2 O 3 phases.

After oxidation at 1300 °C for 15 h EDS maps (Figs. S5a S5d) shows the formation of ternary Al 2 TiO 5 with visible cracks and erosion (Figs. S5c S5d) at the GBs underneath creating favorable paths for diffusion. Further investigation of the scale surface after 100 h (Fig. S5e S5f) indicates the presence of coarse TiO 2 . Wrinkled Al 2 O 3 with large cavities at the interface (Fig. S5g) are filled with intermetallic impurity of Ti:Al:Ga with molar ratio of 1:2.35 ± 0.05:0.43 ± 0.01 (Fig. S5g).

After 240 h of oxidation at 1300 °C, Al 2 TiO 5 (Figs. S5i S5j) reveals Ga traces (0.15(6) at%) with O:Al:Ti:Ga atomic ratio of 5.5 ± 0.5:1.4 ± 0.3:1:0.2 ± 0.1 and cavities underneath (Figs. S5i S5j).

EDS line profiles through Al 2 O 3 (Figs. S6 7) show a relative increase in the concentration of Al and O content concomitant with a relative decrease in Ti signal as the scan transitions from TiO 2 to Al 2 TiO 5 region. Sample corners at 1000 °C (Fig. 7) demonstrate Table II. Weight gain kinetic parameters and correlation coefficients derived by fitting oxidation experimental results (Fig. 1a). The Al 2 O 3 grains near the substrate are larger than those closer to the surface (Fig. S8d). This variation in grain size across the scale has been observed by Golightly, F. A. et al. [START_REF] Golightly | The influence of yttrium additions on the oxide-scale adhesion to an iron-chromium-aluminum alloy[END_REF] and later by Naumenko et al. [START_REF] Naumenko | Correlation between the microstructure, growth mechanism, and growth kinetics of alumina scales on a FeCrAlY alloy[END_REF] in FeCrAl(Y) alloys, as well as by Kota et al. [START_REF] Kota | Isothermal and Cyclic Oxidation of MoAlB in Air from 1100 °C to 1400 °C[END_REF] for Al 2 O 3 forming MoAlB. Grain growth with oxidation time (Fig. 8a) shows that grain size (∼0.5 0.8 μm) at 1000 °C (see Fig. 8a) after 300 h is in agreement with textured Ti 2 AlC (see Ref. 40

Cubic

for synthesis details).

Conversely, the addition of Ga in Ti 3 Al 0.6 Ga 0.4 C 2 results in Al 2 O 3 grain sizes at 1200 °C (∼1.2 3.7 μm) (Fig. 8a) that are larger than those that form on Ti 2 AlC. [START_REF] Tallman | A critical review of the oxidation of Ti 2 AlC, Ti 3 AlC 2 and Cr 2 AlC in Air[END_REF] Oxygen GB diffusivity (Fig. 8b) for Al forming MAX and MAB phases follow a similar trend on a FeCrAl alloy reference line. Grain growth kinetics as a function of temperature (Fig. 8c) shows the grain size growth for Ti 3 Al 0.6 Ga 0.4 C 2 to be comparable to that of FeCrAl(Zr) alloy studied by Smialek et al. [START_REF] Smialek | Oxygen permeability and grain-boundary diffusion applied to alumina scales, national aeronautics and space administration[END_REF] The activation energy for grain growth for Ti 3 Al 0.6 Ga 0.4 C 2 is estimated to be ≈281 kJ mol -1 .

High-resolution grain imaging and Ga allocation. High resolution STEM imaging (Fig. 9a) at 1000 °C after 300 h of oxidation shows a multi oxide layer of an outer equiaxed grain region (0.9 μm thick), an inner columnar grain region (1.4 μm thick) in contact with the substrate, and interface region (0.4 μm thick). Crucially no Ga is detected in the oxide but only in the MAX phase (Fig. 9a). Ga in the Pt protection layer is from the lamella preparation process and any elemental gradients are attributed to EDX resolution limitations.

ATP of a columnar grain above the substrate (Fig. 9b) shows the elemental distribution across the oxide MAX interface. Mass spec trum data shows no Ti, C, nor Ga within the oxide grain which is thus purely Al 2 O 3 with some H impurities. Even though the atom probe is operated under UHV (< 3 × 10 11 Torr vacuum), the H signal could be from the residual gas in the chamber. The visible gradient in the Al and O composition is an artifact and related to the electric field which changes during the measurement. [START_REF] Hans | Electric field strength-dependent accuracy of TiAlN thin film composition measurements by laser-assisted atom probe tomography[END_REF] Lastly, there is very little O in the bulk. with time (Fig. lOe). More importantly, the ratio of the thicknesses of the outer to inner grains is rwt a function of temperatUTe. Further, a streak of Al rich impurity is detected in the substrate as shown in the EDX line profile of Fig. 10d. There is no Ga or 0 detected through the streak. To the best of OUT knowledge such streaks have never been observed before in any MAX phase and at this time remain a mystery.

Discussion

Based on the totality of OUT results it is reasonable to assume that at T < 1300 °C, the oxidation reaction at short times is

Ti3Alo6Gao4C2 + (x + 3 Y + z)02 ➔ Ti3-x . . 4 X Alo6-y Gao4C2_, + xTi02 + 1'.A[i03 . . • 2
+ zC02(g) [5] After the formation of a passivating Al 2 0 3 layer, TiO 2 formation stops and the reaction is:

Ti3_. ,Alo.6-yGao_4C2-z

+ (3: + s )02 ➔ Ti3-x w X Alo 6-y-wGao 4 C2-•-s + -Ali 03 + sC02 . . - 2
At 1300 °C, a temary oxide is formed accord.ing to

Ti02 + Ali 03 ➔ A/2 Ti0 s [6] [ 7 ]
The formation of CO 2 has been shown experimentally elsewhere, it is suSI)eCted to be a contributing factor to the observed wrinkling of Al 2 O 3 53

The following can also be deduced from our results: i. At 1000 °C and 1200 °C, Ti 3 Alo. 6 Ga 1l.4 C 2 forms a protective adherent o Al 2 0 3 layer. This is quite remarkable since the Al molar ratio in the solid solution is only 10 mol% (~8 wt%). This value is significantly lower than for Ti x Al y allo r s, where the Al content has to be > 50 at. % for Al 2 O 3 to form. 6 58 This is important since we have repeatedly shown that for a given atomic fraction, the activity of Al in the MAX phases is much higher than in most other Ti aluminides. Along the same lines, the end member Ti�C 2 is close to the border of forming Al 2 0 3 ; sometimes it forms alumina while other times it does not. 5 9 61 That Ti 3 A1o. 6 Gao.4C 2 with even less Al, forms a protective Al 2 0 3 layer indicates that somehow the presence of Ga in the A planes may increase the Al activity to the point that a protective Al 2 0 3 film forms even at that low concentration. ii. No trace of Ga was observed in the scale, even at the interface (Fig. 9). This implies that it either somehow escapes through the Al 2 O 3 layer or, more likely, is redistributed into the bulle or GBs. iii. At 1200 °C, the Al 2 O 3 g ain sizes are larger than those reported for Ti 2 AlC (Fig. 8a). 5 Why or how, that results in faster oxidation kinetics is unclear at this time. iv. Based on the lack of delamination of the oxide at the sample corners after oxidation at 1000 °C for 300 h (Fig. 7) and at 1200 °C for the same time (Fig. S7b) one can conclude that the lateral stresses generated in the oxide scale due to the lateral growth of the Al 2 0 3 grains are either small or are relieved by creep. The situation at 1300 °C is quite different since the oxide scale forms what has been referred to as a "dogbone" structure. [START_REF] Golightly | The influence of yttrium additions on the oxide-scale adhesion to an iron-chromium-aluminum alloy[END_REF] In our case, however, the bulk does not deform.

The wrinkling observed can be attributed to the lateral growth of the Al 2 O 3 grains. [START_REF] Wang | Insights into high temperature oxidation of Al 2 O 3 -forming Ti 0 AlC 2[END_REF] The predicted weight gains based on the latter values (Fig. 1c) are less than those measured by 14.4%, 10.8%, and 34.0% at 1000 °C, 1200 °C, and 1300 °C, respectively. There are various reasons that could be contributing to the deviation from predicted and actual weight gains. Primarily due to the internal incorporation of oxygen into the MAX phase. [START_REF] Dahlqvist | Phase stability of Ti 2 AlC upon oxygen incorporation: A first-principles investigation[END_REF][START_REF] Persson | Formation of the MAX -phase oxycarbide Ti 2 AlC 1 x O x studied via electron energy-loss spectroscopy and first-principles calculations[END_REF][START_REF] Lee | High-temperature oxidation of Ti 3 AlC 2 between 1173 and 1473K in air[END_REF][START_REF] Rosen | Oxygen incorporation in Ti 2 AlC thin films[END_REF] However we only see a small oxygen gradient through the substrate (Fig. 9). Other contributing reasons include topmost oxide particles buried underneath polymer mounting; excluded localized regions of TiO 2 and Al 2 TiO 5 both leading to thickness underestimation.

The apparent activation energy for oxidation (191 kJ mol -1 ), assuming cubic kinetics (Fig. 1d) agrees with Wang and Zhou 63 for Ti 3 AlC 2 in 1000 °C 1400 °C range (175 kJ mol -1 ), less than that for Ti 2 AlC (250 kJ mol -1 ) in 1100 °C 1200 °C range, and much lower than Cr 2 AlC in 1100 °C 1200 °C range (507 kJ mol -1 ). [START_REF] Tallman | A critical review of the oxidation of Ti 2 AlC, Ti 3 AlC 2 and Cr 2 AlC in Air[END_REF] To gain further insight into the controlling mechanism for oxidation, we followed the procedure outlined by Smialek et al. [START_REF] Smialek | Oxygen diffusivity in alumina scales grown on Al-MAX phases[END_REF] to analyze the underlying mechanism of The main highlight of the study is the interfacial grain boundary diffusivity of oxygen through Al 2 O 3 in Al 2 O 3 formers follows essentially the same temperature dependence as oxygen diffusion through high [8] where ois the grain boundary width (assumed to be ~1 run), kp,i is the instantaneous parabolic rate constant (see Table m and Ref. 20), and G; is the instantaneous grain size growth constant (see Eq. 9 and Fig. 8a). Using this approach, we estimate interfacial oxygen diffusion product 11; at 1000 °C in 1 300 h range to be 2.9 x 10-25 m 3 s-1 to 2. If the initial §i ain size, G, is small, the grain growth kinetics can be expressed as: [ 9 ] where Kd is a thermally activated coefficient (Fig. 8c) and mi s the grain size exponent. The activation energy for oxide grain growth of Ti�_ 6 GilQ_4C 2 is found to be 136 ± 42 kJ mol-1 . Ti 2 AIC grain growth exponent is consistent with our findings whereas there is some deviation to that of reported Ti 3 AIC 2 • The values are comparable indicating similar underlying growth mechanisms. Though the deviation may elucidate some difference in Al 2 0 3 grains formed in the MAX solid solution, compared to those formed on FeCrAl(Zr) (6 wt% or 11 mol% Al nominal content). [START_REF] Fei | Inhibition of metastable alumina formation on Fe-Cr-Al-Y alloy fibers at high temperature using titania coating[END_REF] This difference could be in the form of different solute atoms dissolved in the GBs or in the grains of respective Al 2 0 3 . If the kinetics are indeed GB controlled then, µ, which is equal 1/ m, is related to n in Eq. 3 by: 66 n ::::i (µ -1)/2µ At 1000 °C, m is 3.02 and thus n should be 0.35. Coincidentally or not, the experimental n value for oxide thickening is 0.32 ± 0.04 (Table ID). This agreement is further evidence that indeed the rate limiting step is GB diffusion. For reasons that are not clear, the agreement is not as good at 1200 °C.

The nature of diffusing species either Al or O can be deduced by investigation of the multi layer oxide regions. The equiaxed grain region (Fig. 9a) occupies around 48% of the total oxide thickness. Fig. S8e indicates that the grain width growth is consistent for both top and bottom regions. Mechanistically the rnicrographs shown in Fig. 10 are significant because if one assumes the inner layer is formed by the inward diffusion of 0, with a flux J 0 , and the outer layer by the outward diffusion of Al, with a flux J Ai , then these results imply that 2 J Ai = 3 J 0 Such dual scales have been observed before and have indeed been explained by the inward diffusion of O thro � h the GBs and the outward diffusion of Al 3 + through the bulk. 68 The presence of small grains in the interface region even after 300 h (Fig. 10c) implies that a fraction of the ionic fluxes combines at the interface to form them.

Conclusions

In this work, the isothermal oxidation behavior of bulk hot pressed Ti�_ 6 Gao.4C 2 has been investigated, in natural air, from 1000 °C to 1300 °C, for durations up to 300 h. The solid solution exhibited a good oxidation resistance at 1000 °C, with slow, cubic oxidation kinetics due to the formation of a dense, adherent Al 2 0 3 protective layer. At 1000 °C, the low weight gain observed indicates that the oxidation resistance of Ti 3 Aio. 6 Gao. 4 C 2 is slightly better than those previously reported for both Ti 3 AIC 2 and Ti 2 AIC. The rate limiting step in the oxidation is grain boundary diffusion of Al and/ or O through the Al 2 O 3 protective layer.

At 1200 °C, with time, the wrinkling of the Al 2 0 3 layer results in poor oxidation protection.

At 1300 °C, contrary to the lower temperatures, the weight gain due to oxidation is considerably larger and faster than the values reported for Ti�C 2 and Ti 2 AIC. SEM characterization revealed that the oxidized samples were highly inhomogeneous, with some localized but extended regions of Ti 0 2 , likely responsible for the big mass intake observed at this temperature. In addition, in these regions, TiO 2 and Al 2 0 3 react to form the temary Al 2 TiO 5 oxide. Even in the areas of the samples where TiO 2 was not observed, the Al 2 O 3 was wrinkled and sometimes delarninated. At around 8 at. %, the Al concentration is one of the lowest, if not the lowest, in Ti based alloys/compounds that still form an Al 2 O 3 passivating layer.

In conclusion, the maximum use temperature of this solid solution is about 1000 °C. lnterestingly, at 1200 °C and 1300 °C, the presence of Ga enhances the grain size of the Al 2 0 3 layer. Why that does not lead to better oxidation resistance is not entirely clear at this time. These comments notwithstanding, Ga seems a promising dopant for Al based MAX phases and can probably be used to tune other properties of interest, such as creep, which we are currently exploring.

Figure 1 .

 1 Figure 1. (a) Temperature dependence of weight gain per unit surface area, and (b) scale thickness, as a function of time for Ti 3 Al 0.6 Ga 0.4 C 2 . Note that 1 kg/m 2 10 2 mg/cm 2 . Thicknesses and error bars in (b) represent the mean of 1024 automatic scale thickness measurements across polished mounted cross section samples. Markers represent experimental points. Dashed lines represent power law fits of kinetics. (c) Weight gains predicted from scale thickening kinetics assuming cubic rate constants listed in Table III, compared to experimental weight gain measurements. (d) Arrhenian plot for cubic rate constant k c,w . Other results are taken from Refs. 24, 45, 47

Figure 5

 5 shows surface and cross sectional fractured and polished SEM micrographs of most of the samples tested herein. At 1000 °C, Figs. 5d, 5g show the presence of a dense adherent Al 2 O 3 scale, with a grain size <1 μm (∼0.1 0.5 μm). After 300 h, the Al 2 O 3 layer is thicker but still adherent (Figs. 5m, 5p). At 1200 °C, the Al 2 O 3 layer is dense (Figs. 5e, 5h, 5n, 5q) with larger grains (∼1.67 4.05 μm) than at 1000 °C (Figs. 5b, 5k).

Figure 2 .

 2 Figure 2. XRD patterns from surfaces of samples oxidized at 1000 °C. M MAX phase Ti 3 AlC 2 type, A Al 2 O 3 ,T TiO 2 .

Figure 4 .

 4 Figure 4. XRD patterns acquired on the samples after iso thermal oxidation at 1300 °C. M MAX phase Ti 3 AlC 2 type, A Al 2 O 3 , T TiO 2 , * Al 2 TiO 5 .

Figure 3 .Figure 6 .Figure 7 .

 367 Figure 3. XRD patterns from surfaces of samples oxidized at 1200 °C. M MAX phase Ti 3 AlC 2 type, A Al 2 O 3 , T TiO 2 .

8 15 - 3 ëii 5 •

 1535 -��-------��----� --1200-C-Tl,AIC (T allman et. al, 2013) -1 0 b 10 •20 ---------�---�------. ■ 1 OOO-C-Tl,AI ._. G3o.,C, a, ◄ --Fr tCurveof1000-C-Tl,AI ._. G3o.,c, . §. • □ e 1200-C-Tl,AI._.G3o.,C 2 d(µm)=1.51xt 0 • 35 i ê;5 0 . 9 ü 10•21 ,. .,. .,. .,. .,.. d(µm)=0. 4 3xt 0 • 38 § q_10•2 o 10•2 4 -■-FeCrAl(Zr) (Smialek et. al) e MoAIB (Kota et. al) C: n1 ....

À 26 ◄ 6 ■

 266 Cr,AIC (Hajas et. al) 'f' Cr, AIC (Lee and Nguyen) ♦ Ti,AIC (Tallman et. al) ' ' / � I, -.,_ --200 :C r;.AtC (Tallman et. al, Ti,AIC (Song et. al) ► Ti,AIC 2 (Wang and Zhou) ■ Ti,A� .• Ga..,c (This Work) ' ' ' ' ■ --Ti,A� . • Ga._.c (This Work) (Fit) 10 • 2 7 _______________ ...., ____ _ Ti3Al 0 _6G8<, .4 C 2 (This wor1<) Exp. À Ti 3AIC2 (Wang et. al) Exp. ♦ TiiAIC (Tallman et. al) Exp.

2 MFigure 8 .

 28 Figure 8. (a) Alumina grain sire dependence on oxidation lime at 1000 °C 1300 °C, respectively, 1200 °C Ti�IC (blue) taken from Ref. 45. Inset compares grain sire for solid solution to ternary textured Ti�IC. Grain sire at 1000 °C was estimated from STFM images of individual grains. (b) oxygen diffusion product ofTiJAlo. 6Gao. 4C 2 compared to alumina forming FeCrAl(Zr) al loy, MoAIB and select MAX phases extracted from Refs. 20,45,47,48,52 . (c) Arrhenian type plot for grain growth kinetics in the 1200 °C 1300 °C range. Data extracted from Refs. 45,53.

Figure 9 .

 9 Figure 9. Microstructure and nanometer scale chemical composition analysis of sample oxidized at 1000 °C for 300 h by STEM and APT. (a) Bright field micrograph and EDS line scan from the region indicated in the micrograph by a dashed vertical line. (b) Reconstruction of Ti, Al, Ga, C and O atomic positions and chemical composition profile by APT. The extraction region of atom probe specimen is indicated in (a).

Figure 10 .

 10 Figure 10. Microstructural comparison of samples oxidized at 1000 °C for (a) 15 h, (b) 48 h, and (c) 300 h by STEM. Higher magnification micrographs are shown in the right panel and the region is indicated by a box in the left panel. (d) EDS linescan from the sample oxidized at 1000 °C for 15 h and the region is indicated in (a). (e) Grain width analysis of the upper and lower oxide scale as well as the interface between two scales.

  purity, bulk poly crystalline Al 2 0 3 . Smialek defines a nearly time invariant constant 11; proportional to the interfacial oxygen grain boundary diffusivity, Dgb,O,int as 11; = kp,;Gi = 12oDgb,O,int

  8 x 10-25 m 3 s-1 with a median value of 2.8 x 10-25 m 3 s-1 at 150 h as shown in Fig. 8b. At 1200 °C, in the 1 300 h range, 11; ranges from 9.7 x 10-24 m 3 s-1 to 3.4 x 10-23 m 3 s-1 • The median value is 2.9 x 10-23 m 3 s-1 at 150 h as shown in Fig. 8b. At 1300 °C, in the 1 240 h range, 11; ranges from 1.5 x 10-22 m 3 s-1 to 3.1 x 10-22 m 3 s-1, with a median value of 2.9 x 10-22 m 3 s-1 at 120 h. When these median values are plotted on an Arrhenian plot (Fig. 8b) they are consistent with other Al 2 0 3 forming MAX phases, MoAIB and FeCrAl(Zr) alloys, 20 • 45 , s1,63 •64 confinning the common undeclying rate controlling mechanism of oxidation, namely the growth of the oxide scale through grain boundary, GB, diffusion.

  Figure S8 demonstrates counter current diffusing fluxes of Al and O with inward diffusion of O leading to columnar region. Further, Al and O species meet and nucleate Al 2 O 3 at the interface region. This phenomenon was observed in other Al 2 O 3 forming compounds such as Cr 2 AIC 63 and FeCrAI. 66 It was also shown by 18 O/SIMS that the dual oxide region forms by countercurrent diffusion of Al and O in NiAl and MCrAl alloys. 6 7 , 68

Table I .

 I Specifications of powders and processing parameters used for the synthesis of Ti 3 Al 0.6 Ga 0.4 C 2 .

			Molar					Pressure
	Phase	Reagent	ratio	Supplier	Purity (metal basis)	Particle Size (μm)	Temp. (°C)	(MPa)	Dwell time (h)
	Ti 3 AlC 2	Ti	1	Alfa Aesar	99.5%	⩽ 44 ( 325 mesh)	1500	12	5
		TiC	2	H.C. Starck	98%	Between 5.6 and 22.5
		Al	1.05	Alfa Aesar	99.5	⩽ 44 ( 325 mesh)
	Ti 3 GaC 2	Ti	1	Alfa Aesar	99.5%	⩽ 44 ( 325 mesh)	1400		3
		TiC	2	H.C. Starck	98%	Between 5.6 and 22.5
		Ga	1.15	Gallant	99.99%	Rod
				Metals
	SS			Ti 3 Al 0.6 Ga 0.4 C 2		1500	22

  . The weight gain and scale thickening results reveal that: i. At all temperatures in Table II, the highest R 2 values are for the cubic fits for weight gain. Henceforth when discussing the weight gain kinetics, cubic kinetics, viz. n = 3, will be assumed. ii. At 1200 °C scale thickening is sub parabolic (n = 0.42), while weight gain kinetics are closer to cubic (n = 0.32). As a check for the correctness of the kinetics fit assumed, the k c x , values in Table III were converted to k c w , by assuming the formation of fully dense α Al 2 O 3 with a density of 3950 kg m -3 . k c x

Table III .

 III Scale thickness kinetic parameters and correlation coefficients derived by fitting experimental results (Fig.1b).

		Cubic		Parabolic			Power Law
	T (°C)	k c,x (m 3 s 1 )	R 2	k p,x (m 2 s 1 )	R 2	k′ (ms 1 )	n	R 2
	1300	8 ± 1 × 10 21	0.9766	5.4 ± 0.5 × 10 16	0.9592	10 ± 5 × 10 8	0.39 ± 0.04	0.9730
	1200	1.2 ± 0.2 × 10 21	0.9732	1.5 ± 0.5 × 10 16	0.9814	3.5 ± 0.5 × 10 8	0.42 ± 0.02	0.9948
	1000	1.7 ± 0.1 × 10 23	0.9933	8 ± 2 × 10 18	0.9127	3 ± 2 × 10 8	0.32 ± 0.04	0.9847

Acknowledgments

The research was supported by National Science Foundation (1729335).

Higher magnification images (Fig. 10) of oxide layers at 1000 °C as a function of time clearly show three regions; outer, inner, and interfacial regions at two magnifications. The left column compares the layers at the same magnification; the right column shows the same but at higher magnifications (Fig. 10). The inner layer is more columnar than the outer layer which is more equiaxed. The interfacial regions contain grains that are quite small even after