Yannick Forster

Felix Jahn

Constructive and Synthetic Reducibility Degrees Post's Problem for Many-one and Truth-table Reducibility in Coq

Keywords: 2012 ACM Subject Classification Theory of computation → Constructive mathematics; Type theory type theory, computability theory, constructive mathematics, Coq Digital Object Identifier 10.4230/LIPIcs.CSL.2023.16

We present a constructive analysis and machine-checked theory of one-one, many-one, and truth-table reductions based on synthetic computability theory in the Calculus of Inductive Constructions, the type theory underlying the proof assistant Coq. We give elegant, synthetic, and machine-checked proofs of Post's landmark results that a simple predicate exists, is enumerable, undecidable, but many-one incomplete (Post's problem for many-one reducibility), and a hypersimple predicate exists, is enumerable, undecidable, but truth-table incomplete (Post's problem for truth-table reducibility).

In synthetic computability, one assumes axioms allowing to carry out computability theory with all definitions and proofs purely in terms of functions of the type theory with no mention of a model of computation. Proofs can focus on the essence of the argument, without having to sacrifice formality. Synthetic computability also clears the lense for constructivisation.

Our constructively careful definition of simple and hypersimple predicates allows us to not assume classical axioms, not even Markov's principle, still yielding the expected strong results.

Introduction

The founding moment of "computability theory" deserving of the suffix "theory" was maybe Emil L. Post's 1944 paper [START_REF] Post | Recursively enumerable sets of positive integers and their decision problems[END_REF]. Post introduced the concepts of one-one, many-one, and truth-table reducibility and identified and answered important questions on the structure of the reducibility degrees induced by these relations. Centrally, Post was interested in the question whether there are enumerable but undecidable degrees such that an undecidability proof cannot be done by reduction from the halting problem. For many-one and truth-table reducibility, Post was able to construct such degrees by introducing simple and hypersimple sets, which are still taught in modern textbook presentations of the field. The question whether an enumerable, undecidable problem which is not Turing-reducible from the halting problem exists became known as Post's problem, and we reuse the terminology for Post's problem for many-one reducibility (⪯ m ) and Post's problem for truth-table reducibility (⪯ tt ).

Early in his paper, Post remarks 'That mathematicians generally are oblivious to the importance of this work of Gödel, Church, Turing, Kleene, Rosser and others as it affects the subject of their own interest is in part due to the forbidding, diverse and alien formalisms in no reference to any model of computation, 2. uses intuitionistic logic enriched with the assumption of a (parametrically) universal enumerator but no additional axioms, and 3. is fully mechanised in the Coq proof assistant as a further step in the overarching goal of mechanising the pillar-stones of mathematics and computer science. The results of the paper are hyperlinked with Coq code as indicated by the -symbols.

We believe that machine-checked proofs are also on its own a contribution to "classical" computability theory, i.e. without considering synthetic and constructive aspects: It enables the creation of a machine-checked library of the central theorems of computability theory, ensuring that no odd corner cases are left out in proofs or are hidden under uses of the Church Turing thesis. For the present paper, converting the well-known proofs from a set-theoretic foundation present in textbooks to type theory was not problematic, and modelling choices did not play a crucial role. For Post's problem for ⪯ m , i.e. that an enumerable, undecidable, many-one incomplete, simple predicate exists, the definition of simple in the synthetic setting is most interesting. The complement of a simple predicate has to be infinite, but is not allowed to have an infinite, enumerable subpredicate. In classical mathematics, p is infinite if and only if it is Cantor-infinite, i.e. if there is an injective function N → p. However, Cantor-infinite predicates (defined via functions) have a (synthetically) enumerable, infinite subpredicateenumerated by said function. In constructive mathematics, a predicate p is called infinite if for any sequence [x 1 , . . . , x n ] there exists a y different from all x i but s.t. py. However, any fully constructive proof of infinity in this sense can be turned into a proof of Cantor infinity, meaning there can be no such proof for the complement of a simple predicate. It is thus crucial that infinity is defined as non-finiteness free and thereby void of any computational content. The complement of a simple predicate is then non-finite, but not (synthetically) Cantor-infinite. Only with this definition of infinity Post's problem for ⪯ m can be settled constructively.

For Post's problem for ⪯ tt , i.e. that an enumerable, undecidable, truth-table incomplete, hypersimple predicate exists, several interesting aspects appear: First, the definition of hypersimple predicates has to be chosen carefully to ensure that hypersimple predicates are tt-incomplete. The construction of a hypersimple predicate H is then easier. But since conventional proofs of its undecidability factor via simpleness (and since the textbook proofs showing that hypersimple predicates are simple seem to be inherently classical and we only manage to weaken the assumption to MP), we give a direct, fully constructive undecidability proof for H, which however does not generalise to arbitrary hypersimple predicates.

We try to give intuitive conceptual outlines in the paper, but focus on the interesting synthetic and constructive aspects more than the proof ideas. We largely follow the excellent book by Rogers [START_REF] Rogers | Theory of recursive functions and effective computability[END_REF], supplemented by the books by Cutland [START_REF] Cutland | Computability: An introduction to recursive function theory[END_REF], Soare [START_REF] Robert I Soare | Recursively enumerable sets and degrees: A study of computable functions and computably generated sets[END_REF], and Odifreddi [START_REF] Odifreddi | Classical recursion theory: The theory of functions and sets of natural numbers[END_REF]. The Bachelor's thesis of the second author [START_REF] Jahn | Synthetic One-One, Many-One, and Truth-Table Reducibility in Coq[END_REF], containing preliminary results covered in this paper, discusses some aspects in more detail. The PhD thesis of the first author also discusses the material presented in this paper [START_REF] Forster | Computability in Constructive Type Theory[END_REF]. In general, it might be helpful for non-experts in computability theory to consult one of the books in cases where the presented intuition is not sufficient. The Calculus of Inductive Constructions

C S L

We work in the calculus of inductive constructions (CIC) as implemented by the Coq proof assistant [START_REF]The Coq Proof Assistant[END_REF]. The calculus is a constructive type theory with a (cumulative hierarchy of) type universe(s) T and an impredicative universe of propositions P ⊆ T. The universe of propositions P is impredicative, so e.g. (∀X : P. X) : P, and a sub-universe of T, i.e. whenever P : P we also have P : T. Both aspects however only play a minor role in this paper, important is that the universe P is separated from the universe T. That means that in general, computations cannot inspect proofs to return a computational value.

Most instructively, the difference can be explained by looking at dependent pairs Σx. Ax -which we verbalise as "one can construct x s.t. Ax" -and existential quantification ∃x. Ax -"there exists x s.t. Ax". Both are implemented as an inductive type of (dependent) pairs (x, y), with the only difference that (∃x. Ax) : P but (Σx. Ax) : T. Dependent pairs can be eliminated in arbitrary contexts, i.e. there is an elimination function of the following type1 ∀p : (Σx. Ax) → T. (∀xy. p(x, y)) → ∀(s : Σx. Ax). ps.

We call principles eliminating a proposition into types large elimination principles, following the terminology "large elimination" for Coq's case analysis construct match [START_REF] Paulin-Mohring | Inductive definitions in the system Coq rules and properties[END_REF]. Crucially, CIC proves a large elimination principle for the falsity proposition ⊥, i.e. explosion applies to arbitrary types: ∀A : T. ⊥ → A. For existential quantification, a large elimination principle is not provable, the only principle one can obtain is the following, where the return type of p is P:

∀p : (∃x. Ax) → P. (∀xy. p(x, y)) → ∀(s : ∃x. Ax). ps.

There are two exceptions to this observation: First, whenever ∃x. Ax (also in the relational form ∀x 1 .∃x 2 . Rx 1 x 2 ), can be proved without assumptions, one could instead prove the stronger result that Σx. Ax (for the relational form ∀x 1 .Σx 2 . Rx 1 x 2 or equivalently Σf.∀x 1 .Rx 1 (f x 1 )). Secondly, for the case where p has a boolean decision function, an elimination principle is provable, reminiscent of the µ operator of general recursive functions. We mention the following notations here: We use pairing function on natural numbers written as ⟨_ , _⟩: N→N→N and for all f : N→N→X an inverse construction λ⟨n, m⟩. f nm of type N→X s.t. (λ⟨n, m⟩.f nm)⟨n, m⟩ = f nm. We use the list operations map: (X→Y )→LX→LY , _+ +_ : LX→LX→LX, filter: (X→B)→LX→LX, and _[_]: LX→N→OX. We write |l| for the length of l : LX. For p: X→P, we denote the complement as p and the Cartesian product with q: Y →P as p × q. p is called inhabited if ∃x.px. When defining a predicate we identify a type X with λ(x : X).⊤. We write Forall 2 p l 1 l 2 for l 1 : LX, l 2 : LY , and p: X→Y →P if p holds pointwise on the lists l 1 and l 2 , i.e. for the inductive predicate with constructors of type Forall 2 [] [] and ∀x y l 1 l 2 . pxy → Forall 2 l 1 l 2 → Forall 2 (x :: l 1 ) (y :: l 2 ).

Constructive proofs

A proposition P : P is stable if it is unchanged under double negation, i.e. ¬¬P → P . Furthermore, we say that P is logically decidable, if P ∨ ¬P holds.

Fact 2. Logically decidable propositions are stable.

Stability properties are useful if they apply to a goal, whereas logically decidability is also useful to establish assumptions. The law of excluded middle LEM states that every proposition is logically decidable, and thus enables strengthening assumptions. It is folklore that LEM is independent in CIC: It can be consistently assumed, but not proved. However, when the conclusion is stable, LEM is not needed for case analysis: Fact 4. Let Q be stable. We have that

1. P → ¬¬P 2. ¬¬P → (P → Q) → Q 3. (P ∨ ¬P → Q) → Q.
Note that negated propositions are always stable, and in fact the following holds:

Fact 5. P is stable if and only if P is equivalent to ¬Q for some Q.

MP is also independent in CIC [START_REF] Pédrot | Failure is not an option[END_REF][START_REF] Mannaa | The independence of markov's principle in type theory[END_REF]. For classical theorems on enumerable predicates, often full LEM is not needed and MP suffices, see Fact 9 in the next section.

Synthetic Computability Theory

The key ingredients for synthetic computability theory are synthetic definitions of central notions and suitable synthetic axioms. We define synthetic decidability, enumerability, semidecidability, and many-one reducibility [START_REF] Forster | On synthetic undecidability in Coq, with an application to the Entscheidungsproblem[END_REF][START_REF] Forster | Church's Thesis and Related Axioms in Coq's Type Theory[END_REF], mirroring the textbook definitions without the requirement that the witnessing function is computable in a model of computation. We recall the synthetic setting due to Forster [START_REF] Forster | Parametric Church's Thesis: Synthetic computability without choice[END_REF] in which we work. A predicate p: X→P is decidable if there exists a decider: Dp := ∃f : X → B.∀x. px ↔ f x = true semi-decidable if there exists a semi-decider: Sp := ∃f.∀x. px ↔ ∃n.f xn = true enumerable if there exists an enumerator: Ep := ∃f : N → OX.∀x. px ↔ ∃n. f n = Some x strongly enumerable if the following holds:

E + p := ∃f : N→X.∀x. px ↔ ∃n. f n = x
We treat n-ary predicates as unary via (implicit) uncurrying. A type X is discrete if D(λxy: X.x = y) and enumerable if E(λx : X.⊤). We sum up the connections of the notions:

Fact 8. A type is discrete and enumerable if and only if it is a retract of N.

This fact enables most of our results to only mention predicates N→P, and then transport for free to predicates on infinite, enumerable, discrete types (such as LB × ON).

We can characterise MP in terms of enumerable and semi-decidable predicates: The following strengthening of µ N (Fact 1) will be crucial later:

Fact 10.Let p: N→X→P be enumerable and X discrete.Then there is µE : ∀n.(∃x.pnx)→Σx.pnx.

Note that the result of µ E is independent of the proof H: ∃x. pnx, even without assumptions.

In this paper we will define many-one, one-one, and truth-table reducibility (⪯ m , ⪯ 1 , ⪯ tt ). In general, for a reducibility notion ⪯ r we define predicates p: X→P and q: Y →P to be requivalent if p ≡ r q := p ⪯ r q ∧q ⪯ r p. Informally, we might also refer to the class of predicates q s.t. p ≡ r q as the r-degree of p, but will not make degrees formal to avoid extensionality assumptions. A predicate p: N→P is called r-complete if Ep ∧ ∀q: N→P. Eq → q ⪯ r p. We freely use the notion as well for predicates p: X→P if X is in bijection to N.

All notions of reducibility have in common that they form pre-orders (i.e. are reflexive and transitive) and that they transport decidability backwards, i.e. p ⪯ r q → Dq → Dp.

We now start with the first notion of synthetic reducibility: A function f : X → Y is a many-one reduction from p: X→P to q: Y →P if it expresses p in terms of q: p ⪯ m q := ∃f : X → Y.∀x. px ↔ q(f x) Fact 11. 1. Many-one reducibility forms a pre-order. 2. If p ⪯ m q and q is decidable then p is decidable, resp. for semi-decidability and stability.

3. p ⪯ m q → p ⪯ m q.
Regarding the order structure of ⪯ m , one can prove that decidable predicates constitute minima for the class of non-trivial predicates, and that ⪯ m forms an upper semi-lattice:

Fact 12. Let p be decidable. If ∃x 1 x 2 . qx 1 ∧ ¬qx 2 , then p ⪯ m q.
Fact 13. Let p: X→P and q: Y →P. Then there is a lowest upper bound p + q: X + Y →P w.r.t. ⪯ m : If (p + q)(inl x) := px and (p + q)(inr y) := qy, then p + q is the join of p and q w.r.t ⪯ m , i.e. p ⪯ m p + q, q ⪯ m p + q, and for all r if p ⪯ m r and q ⪯ m r then p + q ⪯ m r.

In traditional computability theory, a universal machine for the chosen model of computation is central to almost all interesting results. In a synthetic approach to computability where there is no explicit model of computation and the notion of function and computable function are identified, a universal function cannot be defined. Instead, its existence has to be axiomatically assumed.

To develop synthetic computability theory agnostic towards classical axioms like LEM, we assume the enumerability axiom EA [START_REF] Forster | Parametric Church's Thesis: Synthetic computability without choice[END_REF][START_REF] Forster | Computability in Constructive Type Theory[END_REF]. The axiom EA postulates a parametrically universal enumerator φ: N→(N→ON), i.e. that for all p: N→N→P (∃f : N→(N→ON).∀i. f i enumerates p i ) → ∃γ: N→N.∀i. φ γi enumerates p i .

To ease language, we often refer to just the universal property as EA in this paper. As is common in developments of computability, we start by defining an enumerable, undecidable, m-complete predicate and its diagonal:

W c x := ∃n. φ c n = Some x Kc := W c c
We call W the universal table of enumerable predicates, justified by the following property:

Fact 17. ∀p: N→P. Ep ↔ ∃c. ∀x. W c x ↔ px
The universal table W is enumerable, undecidable and m-complete, i.e. takes the role of the halting problem from textbook computability. K plays a similar role as the self-halting problem, instead of the codes halting on themselves, Kc holds if c is in the range of φ c .

We start by showing that the complement of K is not enumerable. Thus K is undecidable, and undecidability can be transported to W via a many-one reduction. To show the enumerability of both K and W, we show the enumerability of W and again transport via the above many-one reduction, this time positively.

Fact 20. EW and thus EK.

We now turn towards m-completeness of W and K, i.e. that all p: X→P for enumerable, discrete X many-one reduce to W and K. To establish this for K for the first time requires the full strength of EA, whereas before the non-parametric Fact 14 would have sufficed.

Finite predicates

We discuss two notions of finiteness: Finite (often Bishop-or B-finite) and subfinite (also B-finite) predicates. We say that a list l : LX lists a predicate p: X→P if px ↔ x ∈ l. Note that l is not allowed to contain elements not fulfilled by the predicate. A list l : LX exhausts a predicate p: X→P if px → x ∈ l: We write Lp for finite and X p for subfinite predicates p.

Lp := ∃l : LX.∀x : X. px ↔ x ∈ l X p := ∃l : LX. ∀x : X. px → x ∈ l

Clearly, finiteness implies subfiniteness, but the converse is equivalent to LEM:

Pigeonhole principles

Pigeonhole principles are omnipresent in discrete mathematics. We will prove three variants of the pigeonhole principle based on duplicate-free lists: Our formulation of the principle is that for any duplicate-free list l 1 longer than a list l 2 one can obtain an element x which is in l 1 but not in l 2 -for different formalisations of "obtain" in CIC2 : 1.

x is computable (∀l 1 l 2 . • • • → Σx. . . . ), 2.
x constructively exists (∀l 1 l 2 . • • • → ∃x. . . . ), 3. x classically exists (∀l 1 l 2 . • • • → ¬¬∃x. . . . ). These are exactly the three possible formalisations of "obtain" in CIC: A function returning a dependent pair (Σ), a proof of an existential proposition (∃), or of a double-negated existential proposition (¬¬∃, equivalently ¬¬Σ). Formulating existence as Σ inherently means that the result has to be computable, a property unchanged by the assumption of logical axioms like LEM. ∃ has to be proved using a (computable) function, but the function cannot be used computationally after the proof. This means that any constructive proof of ∀x.∃y. . . . not using assumptions could always be turned into a proof of ∀x.Σy and vice versa, but under assumptions and as assumptions the two behave differently, see Section 2 for more details. We now turn towards proving the principles, which will vary in the requirements on the underlying type X. For the formalisation, we define #l : P for a list l : LX inductively in the expected way to state that l does not contain any duplicates.

Given an equality decider for the base type X it is straightforward to prove the ∀Σ-version of the pigeonhole principle: Lemma 29. Let d decide equality on X and l 1 , l 2 : LX.

If #l 1 and |l 1 | > |l 2 |, then Σx. x ∈ l 1 ∧ x ̸ ∈ l 2 .
Proof. By induction on #l 1 , with l 2 generalised. The first case is contradictory, since |[]| = 0 > |l 2 | is impossible. Let x ̸ ∈ l 1 and #l 1 . Using d allows a case analysis whether x ∈ l 2 or x ̸ ∈ l 2 : If x ̸ ∈ l 2 , the claim is immediate. If x ∈ l 2 , the claim follows from the induction hypothesis for l 2 := filter(λy.if dxy then false else true) l 2 (i.e. for l 2 with x removed). ◀ Note how the ∀Σ version depends on computationally removing an element from a list, and thus on an equality decider d. If no such d is available, a removal function is not definable. However, for the ∀∃ and ∀¬¬∃ forms of the pigeonhole principle, a removal function is not needed. Instead, for the ∀∃ version it suffices to prove that for any list l 0 and any element x 0 , there exists (∃) a list with the same elements of l 0 , just x 0 removed. This becomes possible provided x 1 ̸ = x 2 is logically decidable for all x 1 , x 2 .For the ∀¬¬∃ version of the pigeonhole principle, consequently a removal principle of the form ¬¬∃l . . . suffices, which can be proved fully constructively without assumptions.

To prove the two removal principles,we define a generalised filter predicate l 0 ⊇ p l w.r.t. a predicate p: X→P stating that l is exactly the sublist of l 0 with all elements which fulfil p:

[] ⊇ p [] px l 0 ⊇ p l (x :: l 0 ) ⊇ p (x :: l) ¬px l 0 ⊇ p l (x :: l 0 ) ⊇ p l
We can prove two existence principles, one assuming that p is logically decidable, and one proving a double negation:

If ∀x 1 x 2 : X.x 1 ̸ = x 2 ∨ ¬x 1 ̸ = x 2 , #l 1 and |l 1 | > |l 2 |, then ∃x. x ∈ l 1 ∧ x ̸ ∈ l 2 .
Proof. Similar to the last proof, using Fact 30 (2) and the assumption. ◀

Infinite Predicates

The central notions of simple and hypersimple predicates depend on a formalisation of infinity. Similar to finite predicates, there are several classically equivalent but constructively different definitions of infinite predicates. We discuss three possible definitions of infinity, where a predicate p: X→P is non-finite if it is not finite (¬Lp), or equivalently not subfinite (¬X p), both stable propositions, generative (Gp) if for every list there exists a further element fulfilling p not in the list (a ∀∃ proposition), and Cantor-infinite (N → p) if there exists an injection returning only elements in p (equivalent to a ∀Σ proposition). Those three notions of infinite predicates mirror exactly the three different formulations of pigeonhole principles in the previous chapter. We obtain the following graph, where the dashed (dotted) lines are annotated with sufficient (and necessary) conditions:

C S L 2 0 2 3 16:10 Constructive and Synthetic Reducibility Degrees

N → p Gp ¬X p ∀x 1 x 2 . x 1 ̸ =x 2 ∨¬x 1 ̸ =x 2 ∃q⊆p. Gq∧Eq LEM
Formally, a predicate p: X→P is called non-finite if is not finite. A predicate p: X → P is finite (written Lp) if ∃l: LX. ∀x. px ↔ x ∈ l.

Due to the negation, non-finiteness is equivalent to non-sub-finiteness. A predicate p: X → P is subfinite (written X p) if ∃l: LX. ∀x. px → x ∈ l. We discuss more properties on finite predicates in Section 5.

Fact 33. ¬X p ↔ ¬Lp.

A predicate p: X→P is called generative if for every list there exists a further element fulfilling p which is not in the list:

Gp := ∀l : LX.∃x. px ∧ x ̸ ∈ l
Fact 34. Generative predicates are inhabited, and non-finite predicates not not inhabited.

Generative predicates on N can be characterised as follows:

Fact 35. ∀p: N→P. Gp ↔ ∀n.∃m ≥ n. pm

The following characterisation of non-finiteness as ∀¬¬∃-formula connects the two notions: We then can prove the following using Lemmas 31 and 32.

Fact 36. If ∀x 1 x 2 : X. x 1 = x 2 ∨ x 1 ̸ = x 2 , then ¬X p ↔ ∀l : LX.¬¬∃x. px ∧ x ̸ ∈ l.
Fact 42. Unbounded predicates are non-finite, and are generative for types X with ∀x 1 x 2 : X.

x 1 ̸ = x 2 ∨¬x 1 ̸ = x 2 .
LEM is necessary for non-finite predicates to be unbounded: Lemma 43. If all non-finite p: N→P are unbounded, LEM holds.

A function f : X→LY × truthtable is a truth-table reduction from p to q if ∀x.px ↔ l ⊨ π 2 (f x) for all lists l which reflect q pointwise on the query list π 1 (f x). A predicate p: X→P is truth-table reducible to a predicate q: Y →P if there is a truth-table reduction:

p ⪯ tt q := ∃f : X→LY × truthtable.∀x l. Forall 2 (λyb. qy ↔ b = true) (π 1 (f x)) l → px ↔ l ⊨ π 2 (f x)
Lemma 69. 1. Truth-table reducibility forms a pre-order. 2. If p ⪯ tt q and q is decidable then p is decidable.

3. If p ⪯ m q then p ⪯ tt q.
Truth-table reducibility can employ negation and thus does not transport enumerability.

Hypersimple predicates

For settling Post's problem w.r.t. ⪯ tt in our synthetic setting we once more follow Rogers [28, §9.5] and introduce majorising functions: f : N→N majorises a predicate p:

N→P if ∀n.¬¬∃l: LN. #l ∧ |l| = n ∧ ∀m ∈ l.pm ∧ m ≤ f n.
Note that we slightly adapted the definition of majorising in order to be more suitable for constructive proofs. We immediately introduce a strengthening of the notion following Odifreddi [START_REF] Odifreddi | Classical recursion theory: The theory of functions and sets of natural numbers[END_REF]: A function f : N→N exceeds a predicate p:

N→P if ∀n.¬¬∃i. n < i ≤ f n ∧ pi.
Fact 72. If f exceeds p, λn.f n 0 majorises p.

Lemma 73. If ∀x.qx → px and q is Cantor-infinite, there exists f exceeding p.

Proof. Take λn. π 1 (F [0, . . . , n]), where F is obtained from the ∀Σ formula in Lemma 46. ◀ Corollary 74. Given MP, if there is no f majorising p, then p does not have a non-finite, enumerable subpredicate.

Proof. Let no f majorise p and let q be a non-finite, enumerable subpredicate of p. By MP and Lemma 47, q is generative. By Corollary 49, q is Cantor-infinite. By Lemma 73 there is f exceeding p. By Fact 72, p is majorised -contradiction. ◀

The following is an adaption of Th. III. We have to prove falsity. Note that ¬¬∃.i < 2 n . ∀z. z ̸ ∈ gen n [i] ↔ p * z where p * z := (¬¬pz ∧ z ≤ n) ∨ z > n. Since we have to prove falsity, we can assume such an i. Now by ( * ) we have ∀j.n < j ∈ π 1 (ga n,i ) → pj since π 1 (ga n,i ) < max [π 1 (ga n,i ) | i < 2 n ] follows from i < 2 n . Since for x ≤ n, px ↔ p * x by definition, we have ∀x ∈ π 1 (ga n,i ). px ↔ p * x. But now we obtain the following contradiction:

p ⊨ ga n,i ↔ W a n,i a n,i ↔ W (c(gen n [i])) a n,i ↔ ¬(gen n [i] ⊨ ga n,i ) ↔ ¬(p * ⊨ ga n,i ) ↔ ¬(p ⊨ ga n,i ) □
A predicate p is hypersimple if it is enumerable and p is non-finite and not majorised: Proof. EH I follows by ( 6) of Fact 6. ◀

We have not yet proved H I to be undecidable. A proof that H I is simple seems to require MP. We instead constructively prove DH I →DI and thus H I undecidable for undecidable I:

To do so, we define B: N→T describing a certain kind of guardedness with guards in H I :

Bn := Σx.E I x ≥ n ∧ H I x Lemma 81. ∀nx.Σx ′ ≥ x.E I x ′ > n.
Proof. By the injectivity of E I using Lemma 29. ◀ Lemma 82. Let H I be decidable by some f . Then, ∀nx ′ .(Bn) + (Σx > x ′ .E I x < n).

Proof. Let H I be decidable. Given n and x ′ , we show This paper provides formalised, mechanised, constructive, synthetic proofs of major wellknown results in the area of reducibility theory. The synthetic perspective tremendously helped in all three other aspects: Synthetic proofs are easier to formalise, easier to mechanise, and easier to constructivise since it clears the view by avoiding a hard to handle concrete model of computation. We would argue that a synthetic formalisation is an almost necessary pre-requisite for a mechanised proof of advanced computability-theoretic results: working in a model of computation in the phase of mechanisation where details are still unclear seems too tedious, since defining and verifying programs in a model of computation is time-consuming and should be delayed as much as possible. The concretisation of all synthetically developed results to a model of computation in a second step is then routine. Even in the mechanised proofs, no principal obstacles should occur. For Coq specifically, the automatic extraction of functions to a λ-calculus by Forster and Kunze [START_REF] Forster | A Certifying Extraction with Time Bounds from Coq to Call-By-Value Lambda Calculus[END_REF] would simplify the task further.

∀n 0 ≥ x ′ .E I n 0 > n → (Bn) + (Σx > x ′ .E I x < n) by complete induction on E I n 0 : Let n 0 ≥ x ′ with E I n 0 > n. If H I n 0 ,
Choosing CIC rather than other systems is crucial for projects in constructive reverse mathematics concerning synthetic computability theory: the textbook proofs this paper is based on are often heavily classical, not only in the regard that different, constructively non-equivalent definitions of infinity are used interchangeably. It was thus conceivable that some results would depend on a classical logical axiom like LEM or the limited principle of omniscience LPO. Due to the separated universe of propositions CIC features, CT ∧ LEM seems to be consistent, which is however inconsistent in e.g. HoTT [START_REF] Forster | Church's Thesis and Related Axioms in Coq's Type Theory[END_REF]. However, in the end all our results do not require any classical assumptions. This means that the results can be transported to other type theories. Compatibility with classical logic is however still desirable both for possible investigations of classical synthetic computability theory as well as for purposes of constructive reverse mathematics.

As follow-up work to the present paper, Forster, Kunze, and Lauermann [START_REF] Forster | Synthetic Kolmogorov Complexity in Coq[END_REF] prove that nonrandom numbers, defined via Kolmogorov complexity, form a simple predicate. Crucially, they started by working in a classical setting under the assumption of LEM, and gradually constructivise proofs until not even MP is required.

For future work, two questions seem most prominent: First, we would like to analyse whether our assumptions are minimal. It would be interesting to see whether MP is necessary to prove that hypersimple predicates are simple and undecidable. Secondly, Turing reducibility is the next natural step. The first author and Kirst propose a synthetic definition of Turing reducibility in CIC in [START_REF] Forster | Synthetic Turing reducibility in constructive type theory[END_REF], based on an idea by Bauer [2]. Several open questions remain, most prominently how to construct a universal oracle functional. We would like to develop synthetic versions of the Kleene-Post theorem [START_REF] Kleene | The upper semi-lattice of degrees of recursive unsolvability[END_REF], stating that there are incomparable Turing-reducibility degrees, Post's theorem [START_REF] Post | Degrees of recursive unsolvability -preliminary report[END_REF], connecting Turing reducibility via the Turing jump to the arithmetical hierarchy, and directly subsequent to the present paper the Friedberg-Mučnik theorem [START_REF] Richard | Reducibility and completeness for sets of integers[END_REF][START_REF] Abramovich | On strong and weak reducibility of algorithmic problems[END_REF], settling Post's problem by proving that there exists an enumerable, undecidable, but Turing-reducibility incomplete predicate.

The Coq development accompanying the paper is sizeable due to the number of results covered, but due to the synthetic approach it is still concise. It is relatively elementary: No advanced dependent types are needed, we do not rely on complex hand-written automation.

The preparations regarding the axioms for synthetic computability, finiteness, Pigeonhole principles, and infinity, take 900 lines of code (LOC). Defining ⪯ m , ⪯ 1 , and ⪯ tt and proving related facts needs 700 LOC. General results regarding simple and hypersimple predicates take 100 and 230 LOC respectively. The construction of S and S * needs 700 LOC, of H I only 250. The std++ library [START_REF]The Coq std++ Team. An extended "standard library" for Coq[END_REF] is used for several convenient auxiliary functions regarding lists missing in Coq's standard library.

Fact 1 .

 1 There is a guarded minimisation function µ N : ∀f : N → B. (∃n. f n = true) → Σn. f n = true ∧ ∀m. f m = true → m ≥ n. The inductive types of interest in this paper are all standard, but listed for reference: n : N ::= 0 | S n (natural numbers) b : B ::= false | true (booleans) l: LA ::= [] | a :: l with a: A (lists) o: OA ::= None | Some a w/ a: A (options) A + B := inl a | inr b with a: A, b: B (sums) A × B := (a, b) with a: A, b: B (pairs) Σx: X.Ax := (x0, a) with A: X→T, x0: X, a: Ax0 (dependent pairs)

Fact 3 .

 3 Markov's Principle (MP) accepted for instance in Russian constructivism states that satisfiability of a boolean test on natural numbers is stable and is a consequence of LEM: LEM := ∀P : P. P ∨ ¬P MP := ∀f : N → B. ¬¬(∃n. f n = true) → (∃n. f n = true) LEM is routinely used in textbooks, often in the form of double negation elimination: LEM ↔ ∀P : P. ¬¬P → P

Fact 6 . 1 . 3 .

 613 Decidable predicates are semi-decidable. 2. Decidability is closed under (pointwise) ∧, ∨, and ¬. Finite predicates are decidable. 4. Semi-decidable predicates on enumerable types are enumerable. 5. Semi-decidability is closed under (pointwise) ∧ and ∨. 6. The projections λy.∃x. pxy and λx.∃y. pxy of an enumerable predicate p: X→Y →P are enumerable.

Fact 7 .

 7 1. N and B are discrete and enumerable. 2. Both discrete and enumerable types are closed under pairs, sums, options, and lists. A retraction is an injective function with explicit inverse. X is a retract of Y if there are I: X→Y and R : Y → OX s.t. R(Ix) = Some x and ∀xy. Ry = Some x → y = Ix.

Fact 9 (

 9 [START_REF] Forster | On synthetic undecidability in Coq, with an application to the Entscheidungsproblem[END_REF] 2.17,[START_REF] Forster | Church's Thesis and Related Axioms in Coq's Type Theory[END_REF] 41). The following are equivalent: 1. MP 2. ∀p: N→P. Sp → ∀x. ¬¬px → px 3. ∀p: X→P. Ep → ¬¬(∃n. pn) → ∃n. pn

Fact 14 .

 14 ∀p: N→P. Ep → ∃c. φ c enumerates p Fact 15. Let X be enumerable and discrete and p: X × N→P be enumerable. Then ∃γ: X→N.∀x. φ γx enumerates λy.p(x, y). Fact 16. Let I be enumerable and discrete and p: I → N → P. We have (∃f : I→(N→ON).∀i. f i enumerates p i ) → ∃γ: I→N.∀i. φ γi enumerates p i

Fact 18 .

 18 ¬EK and thus ¬DK and ¬DK Fact 19. K ⪯ m W, and thus ¬EW, ¬DW, ¬DW.

Lemma 21 .Fact 23 .Fact 24 .

 212324 W is m-complete. Proof. Let p be enumerable by φ c via Fact 14. Then λx.(c, x) reduces p to W. ◀ Lemma 22. W ⪯ m K Proof. We obtain the reduction function γ from Fact 16 with p(x, y)z := W x y. Since ∀xyz. W γ(x,y) z ↔ W x y we have W x y ↔ W γ(x,y) (γ(x, y)) ↔ K(γ(x, y)). ◀ W ≡ m K and K is m-complete.We can recover the characterisation of MP as stability of halting: MP is equivalent to the stability of 1. W, 2. K, 3. any enumerable, m-complete predicate on N, and 4. every enumerable, m-complete predicate on N.

Fact 25 .Lemma 26 .Corollary 28 .

 252628 Finite predicates are subfinite. Every subfinite predicate is not not finite.Proof. We first prove the lemma that ∀l 0 : LX.∀p: X→P.¬¬∃l ′ .∀x. x ∈ l ′ ↔ x ∈ l 0 ∧ px which follows by induction on l 0 . Now, let l exhaust p and let p be not finite. We have to prove falsity. Using the lemma, we obtain l ′ s.t. ∀x. x ∈ l ′ ↔ x ∈ l ∧ px and still have to prove falsity. Now l ′ lists p. Contradiction. ◀ Lemma 27. If every subfinite predicate is finite, LEM holds. Proof. For P : P we define p(x : B) := P . p is subfinite because it is exhausted by [true, false]. If p is listed by l, case analysis on l allows proving P ∨ ¬P . ◀ LEM holds if and only if every subfinite predicate is finite.

Fact 30 .

 30 Let l 0 : LX. Then (1) ¬¬∃l. l 0 ⊇ p l and (2) (∀x.px ∨ ¬px) → ∃l. l 0 ⊇ p l. The ∀∃ and ∀¬¬∃ forms of the pigeonhole principle follow: Lemma 31. If #l 1 and |l 1 | > |l 2 |, then ¬¬∃x.x ∈ l 1 ∧ x ̸ ∈ l 2 . Proof. By induction on #l 1 , with l 2 generalised. The case l 1 = [] is contradictory since then |[]| = 0 > |l 2 |. Thus let x ̸ ∈ l 1 and #l 1 . Since the claim is negative, we can do a case analysis on x ∈ l 2 by Fact 4 3. If x ̸ ∈ l 2 , the claim is immediate. If x ∈ l 2 , we obtain l s.t. l 2 ⊇ (λy.x̸ =y) l from Fact 30 (1). The claim follows by induction for l. ◀ Lemma 32.

Corollary 37 .

 37 ∀p: N→P. ¬X p ↔ ∀n.¬¬∃m ≥ n.pm Since the proof of the direction from right to left of Fact 36 does not depend on logical decidability of equality we can prove the following: Fact 38. Generative predicates are non-finite. Fact 39. If LEM holds and p is non-finite, p is generative. We introduce a second ∀∃-notion of infinite predicates: p: X→P is called unbounded if there exist duplicate-free lists of arbitrary length containing only elements from p: Up := ∀n : N.∃l. |l| = n ∧ #l ∧ ∀x ∈ l. px Fact 40. ¬X p ↔ ∀n : N.¬¬∃l. |l| = n ∧ #l ∧ ∀x ∈ l. px Lemma 41. Generative predicates are unbounded. Proof. Let p be generative and n : N. We construct l by induction on n. For n = 0 we pick l = []. For n = Sn ′ we use the inductive hypothesis to obtain l, and use generativity to obtain x s.t. px and x ̸ ∈ l. Now x :: l is the wanted list. ◀

Fact 70 .

 70 p ⪯ tt p Fact 71. Truth-table reducibility is an upper semi-lattice.

3 16: 16

 316 3.10 in the book by Odifreddi [22], with p ⊨ (P, T ) := ∀l. Forall 2 (λxb. px ↔ b = true) P l → l ⊨ T. Lemma 75. If K ⪯ tt p there exists a function exceeding p. Proof. Let g be a tt-reduction from K to p. By Fact 16 there is c: LN→N s.t. ∀lx. W(cl)x ↔ ¬((λy.y ̸ ∈ l) ⊨ gx). Let gen n : L(LN) contain exactly all duplicate-free lists l s.t. max l ≤ n. We define a n,i := c(gen n [i]) for i < 2 n and a n,i := c[] otherwise. Then λn. 1 + max [π 1 (ga n,i ) | i < 2 n ] exceeds p. To show this, let n be given and assume ( * ) : ∀j. n < j < max [π 1 (ga n,i ) | i < 2 n ] → pj C S L 2 0 2 Constructive and Synthetic Reducibility Degrees

  hypersimple (p: N→P) := Ep ∧ ¬X p ∧ ¬∃f.f majorises p Fact 76. Hypersimple predicates are not tt-complete. Fact 77. Given MP, hypersimple predicates are simple. 12 Construction of a hypersimple predicate We now construct and verify a hypersimple predicate, a result due to Post [25, §9]. We however follow Rogers [28, §8.1 Th. II], who presents a (more general) construction due to Dekker [5], defining a hypersimple predicate H I for an arbitrary undecidable I: N→P with a strong, injective enumerator E I : N→N. By instantiating with e.g. W ′ := λ⟨c, x⟩.W c x, we obtain that H W ′ is hypersimple, and thus enumerable, undecidable and tt-incomplete. The predicate H I : N→P is defined as the so-called "deficiency predicate" of I: H I x := ∃x 0 > x. E I x 0 < E I x Lemma 78. H I is non-finite. Proof. By Corollary 37 it suffices to prove ∀x.¬¬∃y ≥ x.H I y. We use complete induction on E I x. Given x: N assume ( * ): ¬∃y≥x.H I y. The claim is negative. Case analysis: 1. If H I x, there exists x 0 > x with E I x 0 < E I x. Hence, induction for x 0 yields ¬¬∃y ≥ x 0 .H I y contradicting ( * ). 2. If H I x holds, x is an element as required. ◀ Lemma 79. If f majorises H I , I is decidable. Proof. We prove that g := λx.x ∈ B map E I [0, . . . , f (S x)] decides I if f majorises H I , i.e. ∀x. Ix ↔ gx = true. The direction from right to left is easy, since E I enumerates I. For the converse direction let E I n = x for some n. We show n ∈ [0, . . . , f (S x)], which is stable. Thus let n / ∈ [0, . . . , f (S x)], i.e. n > f (S x). Since f majorises H I and the goal is ⊥, we can assume l with #l, |l| = S x and ∀y ∈ l.H I y ∧ y ≤ f (S x). Let m := max(mapE I l). We have that m ≥ x, since |mapE I l| = |l| > x and #(mapE I l), and that m = E I m 0 for some m 0 ∈ l and therefore m 0 ≤ f (S x) and H I m 0 by the properties of l. We now prove H I m 0 to obtain a contradiction. We have n > f (S x) ≥ m 0 and E I n = x ≤ m = E I m 0 . By the injectivity of E I , E I n = E I m 0 implies n = m 0 (a contradiction), i.e. E I n < E I m 0 as required. ◀ Theorem 80. H I is a hypersimple predicate, and in particular H W ′ is.

C

  Bn holds and we are done. If H I n 0 holds, we have ∃n 1 > n 0 . E I n 1 < E I n 0 . Applying µ N gives the stronger assumption Σn 1 > n 0 . E I n 1 < E I n 0 . Then, induction for E I n 1 implies the claim. Finally, Lemma 81 yields n 0 ≥ x ′ as assumed in the claim. ◀ Lemma 83. Let H I be decidable by some f . Then ∀n.Bn. Proof. Let H I be decidable. Given n, we first show ∀d.(Bn) + (ΣL.#L ∧ |L| = d ∧ ∀x ∈ L.E I x ≤ n) by induction on d: The base case is immediate by picking L := []. In the step case, the inductive hypothesis either yields Bn which shows the claim or a duplicate-free list L with |L| = d and ∀x ∈ L.E I x ≤ n and an element x > max L. Now, Lemma 82 for x ′ := max L yields again either Bn or an element x > max L with E I x ≤ n. Then, (x :: L) is a list as required which. For d := 2 + n however, ΣL.#L ∧ |L| = 2 + n ∧ ∀x ∈ L.E I x ≤ n is contradictory: By the injectivity of E I , map E I L is duplicate-free, |map E I L| = 2 + n > |[0, . . . , n] but ∀x ∈ map E I L.x ∈ [0, . . . , n]. Lemma 29 implies the contradiction. Hence, we have Bn. ◀ Lemma 84. (∀n.Bn) → DI. Proof. ∀n.Bn yields ∀n.Σx.E I x ≥ n ∧ ∀x 0 > x.E I x 0 > E I x which implies H : ∀n.Σx.∀x 0 > x.E I x 0 > n. Then, λn.n ∈ B map E I [0, . . . , π 1 (Hn)] decides I. ◀ Corollary 85. DH I → DI. Proof. Directly by Lemma 83 and Lemma 84. ◀ Corollary 86. H I is undecidable, and in particular H W ′ is.It seems that this fully constructive proof of DH I → DI can be turned into an again fully constructive Turing reduction from I to H I , provided a reasonable notion of synthetic Turing reductions: Instead of applying µ N to the proof of H I n 0 in Lemma 82, partial functions (that must be crucially present in Turing reductions) would allow to find n 1 > n 0 with E I n 1 < E I n 0 via an unbounded search.The above results settle Post's problem for ⪯ tt :Theorem 87. There exists an enumerable, undecidable and tt-incomplete predicate.Proof. By Fact 76, Corollary 86 and Theorem 80. ◀

Note that, as customary in type theory, quantifications range over the rest of the expression, i.e. the above formula is equivalent to ∀(p : (Σx. Ax) → T). ((∀xy. (p(x, y))) → ∀(s : Σx. Ax). (ps)).

Admittedly, this formulation is more a "pigeon-less hole principle", but we use the well-known terminology.

Funding Yannick Forster: received funding from the European Union's Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie grant agreement No. 101024493.

Supplementary Material github.com/uds-psl/coq-synthetic-computability/tree/reddegrees.

16:11

Proof. Let P : P and pn := P ↔ n is even. If p is inhabited, LEM holds: Given pn we can analysing whether n is even. Since unbounded predicates are inhabited, by assumption it suffices to prove that p is non-finite. So let p be exhaustible, we have to prove falsity. We can thus decide P and it suffices to prove that p is generative to obtain a contradiction.

If P holds, pn ↔ n is even and if ¬P , pn ↔ n is odd. Both are generative. ◀ Corollary 44. Non-finite predicates are unbounded or generative if and only if LEM holds.

Lastly, we introduce Cantor infinity, often used in textbooks. A predicate p: X→P is Cantor-infinite if there exists an injection f : N→X only returning elements in p:

whereby we define as also in the remainder of the paper a function f : A → B to be injective if ∀a 1 , a 2 . f (a 1 ) = f (a 2 ) → a 1 = a 2 . Proof. Let p be enumerable and non-finite, and let l be given. We have to prove ∃x. x ̸ ∈ l∧px. Since p is enumerable, so is λx. x ̸ ∈ l ∧ px. Using Fact 9 it suffices to prove ¬¬∃x. x ̸ ∈ l ∧ px, which holds by Fact 36. ◀

We adapt [START_REF] Forster | On synthetic undecidability in Coq, with an application to the Entscheidungsproblem[END_REF]Th. 2.28] to prove that generative enumerable predicates are Cantor-infinite:

Fact 48. Let X be discrete. Generative, enumerable predicates over X have a strong, injective enumerator: ∀p: X→P. Gp → Ep → ∃f. f injective ∧ ∀x. px ↔ ∃n. f n = x.

Corollary 49. Generative, enumerable predicates over discrete types are Cantor-infinite.

In synthetic computability, Cantor-infinite predicates are problematic because the function f : N→X can be turned into an enumerator. From N → p we cannot conclude that p is enumerable, but that p has a Cantor-infinite, enumerable subpredicate:

Proof. Given p and an injection f witnessing N → p, define qx := ∃n. f n = x. Clearly, ∀x. qx → px since ∀n. p(f n), and λn. Some (f n) enumerates q. f still proves N → q. ◀ Recall that a predicate is simple if it is enumerable, and its complement is infinite but does not have an infinite enumerable subpredicate. Given the last lemma, we have that under the assumption of a universal enumerator φ, defining infinity as. . . 1. Cantor infinity proves there is no simple predicate. 2. generativity makes the existence of simple predicates logically independent, since any constructive proof of generativity could be turned into a proof of Cantor-infinity by Lemma 46, but this is not provable, 3. non-finiteness allows to construct a simple predicate. One-one reducibility

We now introduce our second notion of reducibility: One-one reducibility is a special case of many-one reducibility. A function f : X→Y is a one-one reduction from p to q if f is an injective many-one reduction from p to q:

Fact 51. 1. One-one reducibility forms a pre-order, 2. implies many-one reducibility, and 3. transports decidability, semi-decidability, and stability backwards.

It is easy to prove that one-one and many-one reducibility are not equivalent:

Note that the lemma leaves open whether there are two enumerable but undecidable predicates p and q s.t. p ⪯ m q but p ̸ ⪯ 1 q. We settle this more interesting case in Corollary 68 via simple predicates. In Appendix A, we characterise m-reducibility in terms of 1-reducibility via so-called cylindrification, adapting the proof by Rogers [28, §7.6 Th. VIII].

Simple predicates

We We can now show that the complement of m-complete predicates contains an enumerable, Cantor-infinite subpredicate since productiveness transports along many-one reductions: Lemma 57. Let p ⪯ m q. If p is productive, q is productive.

16:13

Proof. Let f many-one reduce p to q, and let g be a productive function for p. Fact 16 yields k s.t. W (kc) x ↔ W c (f x). Then λc. f (g(kc)) is a productive function for q. ◀ Lemma 58. Let p be m-complete. Then p has an enumerable, Cantor-infinite subpredicate.

Proof. Since productiveness of p follows from K ⪯ m p and productiveness of K. ◀

In particular, then the complement of an m-complete predicate has a non-finite, enumerable subpredicate. Post's idea to find an enumerable, but undecidable, many-one incomplete predicate hinges on exactly this observation. We follow Post and define a predicate p: X→P to be simple if it is enumerable, and its complement is both non-finite and does not contain a non-finite, enumerable predicate: We follow the presentation of Rogers [28, §8.1 Th. II] to construct the same simple predicate as Post [25, §5]. The latter two properties of a simple predicate (non-finite complement and may not contain a non-finite, enumerable subpredicate) will drive the construction, since either one is easy to establish on their own, but the combination needs care. Post's idea was to construct a predicate S containing an element from every non-finite (enumerable) predicate W c . Thus, S cannot have a non-finite, enumerable subpredicate. To ensure that S is still non-finite, S contains only a unique x > 2c with W c x for every large enough W c . The condition x > 2c ensures that there are at least n elements less or equal 2n in S, and thus S is non-finite.

The only technical difficulty in the definition of S is to obtain a unique x satisfying x > 2c and W c x for every large enough W c . Post ensures this by choosing the x enumerated first by φ c (i.e. the x with the least index n s.t. φ c n = Some x) satisfying x > 2c. We abstract away from this property, and observe that any function mapping c to an x > 2c does the job.

We fix a function ψ : ∀c. (∃x. W c x ∧ x > 2c) → N s.t. ψcH = x → W c x ∧ x > 2c and ψcH 1 = ψcH 2 , i.e. a proof-irrelevant choice function for the predicate λx. W c x ∧ x > 2c. Such a choice function ψ can be constructed by using for instance µ E (Fact 10).

We then define S as the image of ψ and prove that S is a simple predicate: Proof. Let q be non-finite, contained in S and enumerated by φ c via Fact 10. We derive a contradiction by showing [0, . . . , 2c] to exhaust q: Assume qx. Then W c x since φ c enumerates q. We have to prove x ∈ [0, . . . , 2c], which is stable. So let x / ∈ [0, . . . , 2c] and derive a contradiction. Since W c x ∧ x > 2c holds, there is in particular a proof H : ∃x. W c x ∧ x > 2c. By definition of ψ, we have W c (ψcH). By definition of φ c , q(ψcH), and thus ¬S(ψcH), i.e. ¬∃c ′ H ′ .ψc ′ H ′ = ψcH -contradiction. ◀ Theorem 65. S is a simple predicate.

Proof. Direct by Lemmas 62, 63, and 64. ◀

Based on our definitions and work, Forster, Kunze, and Lauermann [START_REF] Forster | Synthetic Kolmogorov Complexity in Coq[END_REF] prove that nonrandom numbers, defined via Kolmogorov complexity, also are simple. The construction of any of these simple predicates settles Post's problem for ⪯ m : Theorem 66. There exists an enumerable, undecidable and m-incomplete predicate.

Proof. Direct by 60, Lemma 61, and Theorem 65. ◀

In the following we write p × N for the predicate λ(x, n): N × N.px and use the following observation to prove that ⪯ m and ⪯ 1 differ on enumerable, undecidable predicates.

Lemma 67. Given p: N→P and p × N ⪯ 1 p, p is not simple.

Proof. Let p be simple and f a one-one reduction from p × (λx : N.⊤) to p. We have to prove falsity, thus we can assume an element x 0 s.t. px 0 since p is non-finite by Fact 34. Now λx.∃n.f (x 0 , n) = x is a non-finite, enumerable subpredicate of p. ◀ Corollary 68. ⪯ 1 and ⪯ m differ on enumerable, undecidable predicates.

Proof. Let S be a simple predicate. Now S × N ⪯ m S with λ(x, n). x, but S × N ̸ ⪯ 1 S by Lemma 67. ◀

Truth-table reducibility

Recall that p is many-one reducible to q if a decision for px can be computed from one instance of q, namely q(f x). Truth-table reducibility generalises this intuition: A predicate p is truth-table reducible to q if a decision for px can be computed by evaluating a boolean formula with atoms of the form qy i for finitely many queries y i . Equivalently, boolean formulas with n inputs can also be expressed as truth-tables with 2 n rows, explaining the name "truth-table reducibility". We

A Cylindrification proofs

We characterise many-one reducibility and truth-table reducibility in terms of one-one reducibility.

For the former, the proofs by Rogers [28, §7.6 Th. VIII] work via so-called cylindrification and we generalise them slightly to apply to base types other than N. In our setting, a cylindrification of a predicate p : X → P is p × Z for an inhabited type Z, and predicates of the form p × Z in general are called cylinders.

We fix two predicates p: X→P, q: Y →P and z: Z.

Lemma 88. Let f : Y × Z→Z be an injection. Then q ⪯ m p ↔ q × Z ⪯ 1 p × Z.

Proof. We first prove:

The only interesting proof is (3): Let f reduce q to p × Z. Then λy.(π 1 (f y), g(y, π 1 (f y))) is proves q ⪯ 1 p × Z. It is injective since g is injective and correct since f is correct. Now, the direction from left to right follows from (1), (2), and (3). The converse direction from (1) and (2). ◀ Corollary 89. Let f : Y →Z be injective. Then p ⪯ 1 p × Z and for q s.t. q ≡ m p and p ⪯ 1 q, q ⪯ 1 p × Z.

To characterise truth-table reducibility in terms of one-one reduciblity, we introduce so-called truth-table cylinders, following Rogers [28, §8.4 Th. IX]. Given a predicate p: X → P, we define the predicate p tt : LX × truthtable → P:

The characterisation seems to be inherently non-constructive, we thus assume p to be stable. Lemma 90. Let p: X→P, q: Y →P, x 0 : X, y 0 : Y , and g: LX × truthtable→Y be an injection. If p is stable, then p ⪯ tt q ↔ p tt ⪯ 1 q tt . Proof. We loosely follow the proof by Rogers [28, §8.4 Th. IX] and prove the following: (1) If p is stable then p ⪯ 1 p tt . (2) p tt ⪯ tt p. (3) Every reduction p ⪯ tt q can be given via an injective reduction function, provided an injection f : X→Y exists. (4) If p is stable, f : X→Y injective then p ⪯ tt q → p ⪯ 1 q tt .

(1) and (2) are straightforward. For (3) assume p ⪯ tt q via a reduction function g and construct g ′ x := (f x :: π 1 (gx), λ b :: L. π 2 (gx)L). g ′ is injective since f is injective. For (4), let p ⪯ tt q via an injection f by (3). Then f 1-reduces p to q tt . The claim from left to right follows using (1), (2), and (4), the direction from right to left needs (1) and [START_REF] Cutland | Computability: An introduction to recursive function theory[END_REF]. ◀ Corollary 91. If p, q: N→P and p stable, p ⪯ tt q ↔ p tt ⪯ 1 q tt .


Frederic Lachaud
email: frederic.lachaud@isae-supaero.fr

Mathieu Boutin

Christine Espinosa

David Hardy

Failure prediction of a new sandwich panels based on flax fibres reinforced epoxy bio-composites

Keywords: Flax Fibre, Bio-composite, Composite laminate, Woven composite, Stiffness composite panel, Failure model, Damage model, Debonding, Cohesive zone model, 3 point bending, 3PB three points bending

ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

NOMENCLATURE AND UNITS

Introduction

Composites materials using natural fibres such as flax are increasingly studied in the aeronautic area due to their specific properties. Indeed, these fibres present high mechanical properties paired up with a lower density than classical glass fibres [START_REF] Baley | Average tensile properties of French elementary flax fibres[END_REF][START_REF] Lefeuvre | A study of the yearly reproducibility of flax fibre tensile properties[END_REF]. Wambua and al. [START_REF] Wambua | Natural fibres: Can they replace glass in fibre reinforced plastics?[END_REF] compare tensile and impact behaviour of short fibres composite materials (random mat form) realized with five types of natural fibres. It appears that the natural fibre composites tested were found to compare favourably with the corresponding properties of glass mat polypropylene composites. With this mind, such fibres could be beneficial for air transportation as long as their lower mass could allow a reduction in fuel consumption inducing lower costs and environmental impact. Another recent application of natural fibres is also their use for making honeycomb cores and may be replace Nomex ® or Aluminium material. Riccio and al. [START_REF] Riccio | A numerical study on the impact behaviour of natural fibres made honeycomb cores[END_REF] use flax fibres with thermoplastic resin to create honeycomb core for impact applications. Despite of that, flax fibres can be challenging to use as replacement for synthetic fibres in composite materials for different reasons [START_REF] Pickering | A review of recent developments in natural fibre composites and their mechanical performance Compos[END_REF]. First of all, the properties of these fibres strongly depend on the climatic condition of the plant culture and this phenomenon can lead to an important variability over years or geographical production areas which can become an issue in providing a consistent production quality to the industry [START_REF] Baley | Average tensile properties of French elementary flax fibres[END_REF][START_REF] Lefeuvre | A study of the yearly reproducibility of flax fibre tensile properties[END_REF][START_REF] Lefeuvre | Tensile properties of elementary fibres of flax and glass: Analysis of reproducibility and scattering[END_REF]. Then, the adhesion between such fibres and most polymeric matrices is generally poor due to the incompatibility of the hydrophilic characteristic of natural fibres [START_REF] Pucci | Wetting and swelling property modifications of elementary flax fibres and their effects on the Liquid Composite Molding process Compos[END_REF][START_REF] Fuentes | Mechanical behaviour and practical adhesion at a bamboo composite interface: Physical adhesion and mechanical interlocking[END_REF][START_REF] Tran | Understanding the interfacial compatibility and adhesion of natural coir fibre thermoplastic composites[END_REF]. Usually, chemical or physical treatments are used to modify the fibres' surface and improve adhesion between the fibres and the matrix which is a cause of environment or cost effectiveness and competitiveness reduction [START_REF] Faruk | Biocomposites reinforced with natural fibres: 2000-2010[END_REF][START_REF] Kabir | Chemical treatments on plant-based natural fibre reinforced polymer composites: An overview Compos[END_REF][START_REF] Gopalakrishnan | Effect of mercerization of flax fibres on wheat flour/flax fibre biocomposite with respect to thermal and tensile properties Compos[END_REF][START_REF] Balnois | An AFM study of the effect of chemical treatments on the surface microstructure and adhesion properties of flax fibres Compos[END_REF][START_REF] Pizzi | High resin content natural matrix-natural fibre biocomposites[END_REF][START_REF] Gouanve | Unsaturated polyester resin (UPR) reinforced with flax fibres, untreated and cold He plasma-treated: thermal, mechanical and DMA studies Compos[END_REF]. In addition, natural fibres have a complex microstructure compared to synthetic ones [START_REF] Fernández | Role of flax cell wall components on the microstructure and transverse mechanical behaviour of flax fabrics reinforced epoxy biocomposites[END_REF][START_REF] Arnould | Better insight into the nano-mechanical properties of flax fibre cell walls[END_REF][START_REF] Bourmaud | Relationships between micro-fibrillar angle, mechanical properties and biochemical composition of flax fibres[END_REF]. Flax fibres are composed of concentric layers of different structures and compositions of cellulose, hemi-cellulose and lignin, and can be considered as a composite at a lower scale as well. For example At a larger scale, flax fibres are discontinuous and have kink bands that can affect their mechanical response [START_REF] Baley | Influence of kink bands on the tensile strength of flax fibres[END_REF]. From a microscopic point of view, Baley [START_REF] Baley | Analysis of the flax fibres tensile behaviour and analysis of the tensile stiffness increase[END_REF] indicate that an increase of the Young's modulus is due to the reorganisation of the cell structure; especially reorientation of the fibrils toward the load direction. All these characteristics induce a nonlinear mechanical behaviour under loading along the direction of the fibres. Moreover, this nonlinear behaviour is observed in composite materials using this kind of fibres [START_REF] Mahboob | Tensile and compressive damaged response in Flax fibre reinforced epoxy composites Compos[END_REF]. Finally, composite laminates made from flax fibres are subject to complex different damage mechanisms due to their structure and poor adhesion with polymeric matrices [START_REF] Mahi | Damage mechanisms characterization of flax fibres-reinforced composites with interleaved natural viscoelastic layer using acoustic emission analysis[END_REF].

In order to predict the behaviour of composite materials, the Finite Element Method (FEM) is more and more used. FEM is efficient and convenient, compared to experimental methods, to study the behaviour of fibres and their composites or laminates. This method allows studying the influence of several parameters such as layers configuration, fibres volume fraction or mechanical properties of the fibres. Even if flax fibres have been well studied during the past decades, their mechanical characterization is not easy. The main difficulty is that these fibres do not present a linear behaviour even at low charges, in other words, their stiffness matrix is not constant throughout the loading phase. This particular nonlinear mechanical behaviour is challenging when it comes to model the homogenised composite materials compared to synthetic fibres composites such as carbon fibres' ones which exhibit a linear behaviour.

Different FE models have been used to try to model the complex behaviour of natural fibres, or have been built to predict the behaviour of flax fibres at different scales. One of the most popular is going through a Representative Volume Element (RVE) that allows to take into account the microscopic heterogeneities of the fibres [START_REF] Sun | Prediction of composite properties from a representative volume element[END_REF]. Thuault et al. [START_REF] Thuault | Numerical study of the influence of structural and mechanical parameters on the tensile mechanical behaviour of flax fibres[END_REF] have designed another micro-scale FE model which takes into account the chemical components, the cell wall thickness and the micro fibrils angle to model the tensile behaviour. Other models have been created at meso-scale like the one of Beakou and Charlet [START_REF] Beakou | Mechanical properties of interfaces within a flax bundle-Part II: Numerical analysis[END_REF] based on the flax fibres bundles and the cohesive behaviour between fibres. At a larger scale, a FE model has been developed by Tephany et al. [START_REF] Tephany | Influence of the non-linearity of fabric tensile behaviour for preforming modeling of a woven flax fabric Text[END_REF] for woven flax fabrics in 2D to model the influence of nonlinear tensile behaviour of woven fabric. For the behaviour of composites reinforced with natural fibres, Sliseris et al. [START_REF] Sliseris | Numerical modelling of flax short fibre reinforced and flax fibre fabric reinforced polymer composites[END_REF] have established a 3D RVE model for woven fibre fabric reinforced composite for the tensile and shear properties of composites using non-linear plasticity model. Finally, damage and fracture have been modelled for woven fabric reinforced composites in 2D using shell elements by Wang et al. [START_REF] Wang | Establishing a new Forming Limit Curve for a flax fibre reinforced polypropylene composite through stretch forming experiments Compos[END_REF] and in 3D using a mesoscale RVE model by Panamoottil et al. [START_REF] Panamoottil | Anisotropic continuum damage model for prediction of failure in flax/polypropylene fabric composites[END_REF]. But there is not one unique FE model or behaviour law that takes into account all the previously described characteristics.

The main objective of this study is to propose a meso-scale damage behaviour model capable to replicate the non-linear behaviour of flax/epoxy composites and complex structures. It is demonstrated that this model is capable to predict the damage and failure of a flax fibres reinforced composite omega sandwich panels which are complex structures. Omega stiffeners are often used to improve the compressive strength of composite panels [START_REF] Sellitto | Compressive behaviour of a damaged omega stiffened panel: Damage detection and numerical analysis[END_REF]. For our study the Omega stiffeners are used to replace the Nomex® core in our sandwich panels.

To do so, mechanical behaviour of flax fibres composites and associated panels have been experimentally studied. The performance of Flax fibre Omega Sandwich Panels to a three points bending load is compared with classical Nomex® Core sandwich panels. Then, the results of these tests and the damage laws have been identified in order to implement the FE model. Finally, the model has been used to predict the behaviour of the composite panel structure and compared to experimental results.

Materials and Experimental Protocol

Jauges

This part is intended to explain the static analysis that has been carried out in order to derive the model of the behaviour and for the damage. For this late case, a cyclic tensile test is necessary.

First, in order to understand how this damage is acting, a real cyclic tensile test has been conducted in the laboratory on the previously described specimens, so that to create loads in several directions from the fibres' ones. This directions were: the direction taken as reference (0°), also called warp, the direction perpendicular to this one (90°), also called weft, and a (45°) direction for the first one, in order to measure the in-plane/in-ply shear stress.

For the sake of clarity, two of the three stress-strain curves obtained for the [0°]4 configurations are presented on Figure 2. As expected from literature, the mechanical behaviour of flax fibres woven composite coupons is non-linear and exhibits three different stages. This particular behaviour begins with a small linear phase up to 0.2 % of total engineering strain. Then, there is a long non-linear hardening phase up to around 1.2%-1.4 % of total strain. Finally, the failure of the specimens is observed at 1.4 % of total strain. As expected, the mechanical behaviour of the [90°]4 specimens was nearly the one of the [0°]4 ones. The curves are not reported here for the sake of simplicity and because of their similarity with Figure 2.. Resultant mechanical properties are presented in Table 1. This observation is consistent with the fact that in an equilibrated fabric, the behaviour is the same in both in-plane directions. The failure surfaces from a typical (0°) test are shown in Figure 3. The analysis of these pictures shows a clear fracture of the fibres located between two yarns in the direction perpendicular to the direction of loading. Moreover, some fibres seem to have slipped in the composite. The analysis of the curves and of the fracture surfaces shows the appearance of damage during tensile tests responsible for the non-linear behaviour of the composite. Such behaviour is mainly due to flax fibres because of two effects. On the one hand, the particular structure of flax fibres changes during loading. O the other hand the woven pattern is composed of long fibres that are indeed discontinuous and simply stuck together. Therefore they can easily slip and slide on each other. Moreover, the adhesion between the fibres and the matrix may not be perfect.

The curves corresponding to the in plane shear stress as a function of the total engineering strain for the [±45°]4 configurations are shown in Figure 4. In this case, the non-linear mechanical behaviour is slightly different. The first linear phase is longer and goes up to 1 % of deformation. Then, the non-linear part continues up to around 6 % of deformation. The decrease of the stiffness slope in this case is very significant. The different mechanical properties measured with this test are presented in Table 1. The decrease of the slope of the curves for the [±45°]4 configuration can be explained by the fact that in this configuration, the tensile tests do not strain the fibres but rather the matrix that is weaker. Furthermore, the non-perfect adhesion between the fibres and the matrix contributes to the initiation and final shape of the damage.

In the following Table 1, E0 stands for the apparent elastic modulus during the elastic phase;

σmax and εmax are respectively the maximum reached values of engineering axial stress and strain. The Poisson ratio is computed using the ratio of measured lateral to axial strains. Corrugated panels were manufactured using the same products as used for composite laminates. The core and the skins were made separately using only one layer of flax fibres fabric, while the omega stiffeners are made from four layers as for the tensile specimens. The manufacturing process of the skins was the same as the one used for composites laminates (except for the number of layers). The core was manufactured using a special aluminium mould that has been designed and manufactured in purpose so that to obtain the specific required omega shape of the core. The curing pressure and temperature used were the same as previously mentioned. The core and the skins were then assembled using the matrix as the adhesive. Once assembled, the panel was post cured for 1 h at 100 °C in an oven. The rendering aspect of the panels and the 200mmx80mmx10mm specimens that were cut from them and used for flexural tests are shown in Figure 6. The fracture areas of the two fracture modes (M1 and M2) observed are shown in Figure 9. The In order to model this behaviour in 1D, each phase is attributed a specific parameter and so a specific theoretical approach. The stress-strain 1D behaviour can be written as follows:

= 1 - 1 - - Eq. 1
Linear phase:

The first linear phase corresponds to a classic linear elastic behaviour defined by the Young modulus . The hardening behaviour is due to a stable damage development composed of micro-cracks occurring all over the sample volume. This stable damage is named diffuse damage . The softening behaviour is defined by the failure damage variable . Finally, the permanent or residual strain can be computed and subtracted from the total strain value in order to compute the relaxed elastic strain value by the classical sum approach valid

Stress (MPa)
if strains remain relatively small. So the initial stiffness is affected by both diffuse damage and failure damage. The derivation of each damage variable is described hereafter as follows.

Diffuse damage computation: thermodynamic approach:

For the hardening behaviour damages are due to micro-crack of the matrix but also due to micro-structure of flax fibres [START_REF] Mahboob | Fatigue of flax-epoxy and other plant fibre composites: critical review and analysis[END_REF]. Flax fibres are made up of microfibrils which slide relatively to each other during tensile loads. Micro friction arrives between microfibrils that explains residual strains and permanent damages. The multiscale structure (multi cell wall) of these fibres contributes also to create damage.

According to thermodynamic approach [START_REF] Ladeveze | Damage modelling of the elementary ply for laminated composites[END_REF], diffuse damage is written as a function of elastic energy Y: = ( ) Eq. 2

Where :

Y= = = ( ! )
is the elastic energy The function will be determined experimentally.

Failure damage computation: Strain failure criterion approach:

Softening behaviour is modelled with a failure damage variable computes according a strain failure criterion as defined by Linde [START_REF] Linde | Modelling and Simulation of Fibre Metal Laminates[END_REF].

= 1 - "# (( !$). &'() .*+ &'() , -. . ./0) .$

Eq. 3

Where :

-F is a maximum strain criterion 1 =

+ 2 + 3
for a 1D example criterion, -is the total strain at failure determined experimentally is the elastic strain at failure -is the damaged Young's modulus for strain at failure -G is the critical energy release rate (J/m2) determined experimentally -lc is a characteristic length for a non-local approach (m) with FE use.

Lc value is computed by the software. We have modified a user routine in Abaqus in order to compute this length in the perpendicular direction of the yarns direction in order to be coherent with fracture mechanic theory.

Residual strain computation: isotropic work hardening pseudo plasticity approach:

Residual strain is computed according a classical plasticity theory with isotropic hardening hypothesis applied to composite laminates [START_REF] Ladeveze | Damage modelling of the elementary ply for laminated composites[END_REF]. Plasticity is here called pseudo-plasticity because the physical phenomena involved in the generation of irreversible strains are not the same as in metallic materials which suffer from plasticity.

The pseudo plasticity yield surface is defined with a plasticity function Fp given by: 14( 5, 4) = 5 7 -(4) -Eq. 4

The irreversible strain component linked to hardening computation is:

# 8 = 9 8 :$# : = 48 | | Eq. 5
For 1D approach and isotropic hardening 9 8 = 48 , so the only value of residual strain is :

# 8 = 48 | |
Where :

-5 7 is the equivalent effective stress (equal to 5 for 1D formulation), -

) is a function defining the hardening curve, determined experimentally, -4 is the cumulative plastic strain (9 = 4) for isotropic hardening, -is the pseudo-plastic yield stress determined experimentally.

For the formulation of each phase' behaviour, tests are necessary. The identification of all the parameters will be detailed in the following paragraphs. However, firstly, this model is generalized for a 2D approach for the ply in a 3D modelling purpose.

3D behaviour: 2D in plane damage of the ply

For 3D generalization, the model includes a vector of three diffuse damages and a vector of three failure damages. Pseudo plasticity permits to compute also three in plane residual strains. So the model affects the in plane behaviour of the ply.

The stress-strain behaviour is written in a general form: < = = >? @ A B. < = Eq. 6

Where:

? @ A = C D D D D D E 1 -F (1 -F )? 1 -F 1 -F (1 -F )? 1 -F (1 -F )? G 0 0 0 ? 1 -F (1 -F )? 1 -F G (1 -F )? G 0 0 0 ? G ? G ? GG 0 0 0 0 0 0 1 -F 1 -F 1 -F G (1 -F G )? II 0 0 0 0 0 0 ? JJ 0 0 0 0 0 0 ? KK L M M M M M N
, are the diffuse and failure damages in warp, weft and in plane shear directions respectively for i=1, 2 or 3.

The equivalent thermodynamic force to compute diffuse damages [START_REF] Ladeveze | Damage modelling of the elementary ply for laminated composites[END_REF] is: = OP. ( + ) + Eq. 7

Where:

-UV are the thermodynamic forces in warp, weft and in plane shear directions respectively,

-P = 0 W WW is a coupling parameter.
The failure damage variables' computation needs to introduce a strain criterion. The stressstrain criterion approach was proposed by [START_REF] Linde | Modelling and Simulation of Fibre Metal Laminates[END_REF] for unidirectional laminates. It is proposed here to adapt these criterions to the flax woven ply.

The warp direction failure criterion is computed as follows:

1 1 1 F ε ε ε ε ε ε     = + - >        
Eq. 8

The weft direction failure criterion is expressed by the criterion:

2 22 2 22 Fail_t Fail_c Fail_t Fail_c 22 22 22 22 1 1 1 F ε ε ε ε ε ε     = + - >        
Eq. 9

The in plane shear failure criterion can be written as:

1 F b γ ε ε γ ε ε ε ε         = + + >                
Eq. 10

Where :

Fail_t ii ε is the strain the failure in warp/weft direction in tensile Eq. 11

The equivalent stress introduced in the pseudo-plasticity yield function 14( 5, 4) is:

5 7 = OZ . ( 5 + 5 ) + 5
Eq. 12

Where:

-Z is a coupling parameter between residual strains

Identification of material parameters

The identification of the properties and parameters of the behaviour are done using tests in three steps. The first step permits to identify the Young's modulus, the strain at failure and the diffuse damage evolution. In plane shear stress τ12 (MPa)

In plane shear strain γ12 (%)

#

And the damage can be expressed as: = 1 -(

Eq. 13

Therefore Y can be expressed too as:

= ( ! )
Eq. 14

The identification method consists in determining the damage in the warp direction, then in in-plane shear direction. In fact, during the shear test, the yarns in the warp direction are stressed and the damage in shear must take this into account. Then the shear diffuse damage is corrected introducing non linear behaviour of the yarns in warp direction. Diffuse damage identification curves are plotted Figure 12. Cumulative plasticity strain is defined by: 4 = (1 -).

Eq. 15

Pseudo plasticity threshold is computed with:

(4) + = 2 ( ! )
Eq. 16

As for damage identification, the methodology for plasticity identification consists in computing the residual strain versus yield stress for a [0°]4 laminate. Then [±45°]4 laminate is used to find the yield stress versus the cumulative residual strain and also the coupling coefficient "a 2 ". 4. Z is equal to 0.075 which means that the ratio between the residual strain in warp direction is about 13 times lower than that in in-plane shear.

For failure damage Eq. 3 needs to identify the critical energy release rate Gf for the fibres (warp and weft yarn direction) and Gm for the matrix. Compact Tension (CT) tests have been realized for yarns (warp and weft direction) Gf identification using the same samples as described by Pinho [START_REF] Pinho | Facture toughness of the tensile and compressive fibre failure modes in laminated composites[END_REF]. A precedent study [START_REF] Médeau | Robust characterization of crack propagation in 3D woven composites and evidences of size dependency[END_REF] concerning 3D woven composites shows us that the area method is the more robust method to determine Gf. We use the same experimental approach to determine Gf in the warp direction of our flax woven composite.

Dimensions of the sample are shown Figure 14a. Loading is shown on Figure 14b. A thick laminate[0]12 is used in order to obtain about 4 mm thickness for the samples. The pre-crack has to be designed in order to be sure that the propagation is stable. A 6mm length has been chosen and is realized with a diamond wire. Eq. 17 5. For the epoxy matrix, the critical energy release rate value is obtained from the literature [START_REF] Lachaud | Experimental and numerical study of delamination caused by local buckling of thermoplastic and thermoset composites[END_REF][START_REF] Lubineau | Construction of a michromechanics-based intralaminar mesomodel, and illustrations in Abaqus/Standard[END_REF][START_REF] Lachaud | Validation of a simplified analysis for the simulation of delamination of CFRP composite laminated materials under pure mode I[END_REF].

Model validation and experimental comparison

Once identified on 2x2 twill flax woven laminates, parameters and properties of the material model are introduced into a developed user material subroutine (UMAT) developed for implicit Abaqus® Software. For the purpose of validation of the model, some preliminary tests have been done with a single fully integrated solid element (8 nodes, 3 degrees of freedom per node and 8 Gauss integration points -C3D8 reference in Abaqus software). The static general solver (Quasi static implicit algorithm, Newton-Rahpson) is used in Abaqus.

Displacements are prescribed at the boundaries for tensile and shear tests.

For the numerical/experimental tensile test comparison, Figure 16 shows the FE model used.

Tabs are not meshed. Solid elements used are the same as prescribed before (C3D8). First section is fixed. Displacement is imposed on a reference point linked to the second section of the sample. Size of brick elements is 1.5mm×1.5mm×1.25mm. Stress-strain curves are saved for some elements situated in the middle of the sample (near strain sensors position).

The FE model results are compared to the experimental ones on Figure 16 for the two staking sequences [0°]4 and [±45°]4. In both cases, the model is in good accordance with the experimental results.

Failure prediction of omega sandwich panels

Objective of this part is to apply the damage/failure model to predict the failure modes of the Omega sandwich panel submitted to 3 points bending tests (section 2).

Mesh, boundary conditions and loading

This subsection is intended to present the model which was realized in ABAQUS in order to simulate the three point bending test. Showing the FEM model will also be a way to introduce the geometry and characteristics of the real model and also some test parameters. The real model was built with some measure specifications, regarding the length, width and the geometry and also measures of the cross section. All the dimensions are resumed in Table 6. with a cross-section "W " shape, which can also be called omega panel (Figure 17). Two models have been created: one with skin tie to the Omega core (same nodes), other with cohesive contact including bilinear cohesive behavior. The rollers fixed use rigid element (R3D4 Abaqus reference). Imposed displacement is done on the central rectangular roller as on the experimental setup. The boundary conditions have been set with a hard contact with friction between the panel and the cylindrical/rectangular rollers.

Computation and input data

The computation uses the Full Newton Raphson solver (ABAQUS General Standard) with nonlinear geometric activation. The full Newton Raphson scheme involved an update of the tangent stiffness matrix at each iteration; this scheme appears to the authors as a suitable approach to support the progressive failure of laminates.

Finally a delayed damage effect [START_REF] Allix | Delayed damage modelling for fracture prediction of laminated composites under dynamic loading[END_REF][START_REF] Montagne | Failure analysis of single lap composite laminate bolted joints : Comparison of experimental and numerical tests[END_REF] is applied to all failure damages in order to limit the localization of the damage in the model and to minimize the mesh dependency. Viscous damage is chosen as follow [START_REF] Chen | A combined elastoplastic damage model for progressive failure analysis of composite materials and structures[END_REF]:

8 r = s ( -r )
Eq. 18

where: d0 is the damage variable without delay damage effect, dv is the regularized viscous damage variable and t is a viscosity constant. τ is equal 0.0025 for all the failure damages. So

r (u + 1) = g svg r (u) + s svg (u)
Eq. 19

Expression of this parameter also facilitates the computation of the tangent matrix [START_REF] Chen | A combined elastoplastic damage model for progressive failure analysis of composite materials and structures[END_REF].

All the model input data are summarized in Table 7 for elastic ply properties, Table 8 for diffuse damage computation and Table 9 for failure characteristics. Pseudo plasticity is not activated for these computations. Model data for cohesive behaviour are given in Table 11. Considering the failure damage, a general view of the damage in the panel at the pic force is presented in Figure 19. These pictures show that failure damage is mainly located in the lower skin in the warp direction (Figure 19-A) and initiated in the free border of the panel. Failure A model integrating classical cohesive damage behaviour [START_REF] Lachaud | Validation of a simplified analysis for the simulation of delamination of CFRP composite laminated materials under pure mode I[END_REF] between the Omega core and the skins was created in order to simulate the failure mode 2 with the buckling of the upper skin. The cohesive zone model (CZM) uses a bi-linear behaviour described by Lachaud [START_REF] Lachaud | Validation of a simplified analysis for the simulation of delamination of CFRP composite laminated materials under pure mode I[END_REF].

Quadratic stress criterion is used of initiation of delamination. A linear propagation energy criterion is defined. Figure 19 shows experimental/numerical global load-displacement behaviours. Specific characteristics values as stiffness values, pic loads and failure displacements are shown in Table 12. It can be seen that in this configuration as well, the FE model is capable to describe the non-linear behaviour of the panel until the failure load is reached. Up to this point, specific values of stiffness and maximum load are very close (Table 12). The general view of the cohesive damage at different relevant steps of the failure is presented in Figure 22. These three steps correspond to the three points showed in Figure 21. We can see that debonding is initiated at each corner of the upper side of the Omega stiffeners, under the central rectangular roller (Figure 23-A). After reaching the full width of the omega top faces, debonding then propagates in the longitudinal direction of the samples (Figure 23-B).

When debonding of the upper skin is sufficiently important, local buckling arises (Figure 22-C). The model is not able to take into account failure mode I while mode I will appear. Local bonding defects or geometric defects during manufacturing can be the initiators of the two observed failure modes.

Conclusion

The main goal of the study was to study multi-scale mechanical behaviour of composite flax fibres reinforced polymer composites, in order to evaluate of this type of material could be used in aeronautical structures. A new manufacturing process of a flax woven ply sandwich panel was developed with Omega stiffeners by hand manufacturing with high pressure curing.

Global behaviour of Flax Omega sandwich panels were compared with some conventional sandwich panels made of a woven glass skin with NOMEX core under static three point bending loading. It appears that the flax fibre sandwich panels have a more marked non-linear behaviour than the Nomex sandwich panels. However, the failure force level of all the panels is similar, with a higher deformation at failure. Moreover, the panels exhibited similar mechanical properties as classical glass fibres reinforced polymer composite panels used in aeronautics.

Two failure modes of the Flax panel have been identified and observed after the tests. The This study could be extended in various ways like using a bio-base matrix that could be modified in order to pass aeronautics norms, especially for fire resistance. It could also be considered to use this model to optimize the structure of the omega or to perform some dynamic analysis such as impact tests or modal analysis.

Acknowledgement

The research leading to these results has received funding from ADEME under the grant agreement n° 1501C0050. Thesis of Mathieu BOUTIN was partially funded by ANRT (National Association of Research and Technology). The authors would like to sincerely thank Robert PIQUET, who died on March 20, 2020 for his initial contribution in this study.

  Eij laminate Young's modulus (MPa) in ij directions εij strain component in ij directions εeij elastic strain component in ij directions εpij residual strain component in ij directions εtij total strain component in ij directions σij stress component in ij directions σeq Von Mises equivalent stress Yij elastic energy in ij directions F maximum strain at failure, failure strain criterion Fp pseudo plasticity yield function Gij laminate shear modulus (MPa) in ij directions Gf critical energy release rate (J/m²) in axial warp/weft direction Gm critical energy release rate in mode II (J/m²) for matrix lc characteristic length (mm) p cumulative plastic strain R experimental hardening curve for isotropic hardening plasticity R0 experimental yield stress

2. 1 .

 1 Flax fabric Composite Laminates behaviour 2.1.1. Manufacturing Composites laminates were manufactured using a twill 2/2 woven flax fibres fabric provided by Groupe Depestele (Le Bocasse, France), having an area weight of 360 g/m 2 . The matrix used was composed of the SR-1126 resin and SD-8202 hardener provided by Sicomin (Châteauneuf les Martigues, France). Sample plates were manufactured by compression moulding with four layers of flax fibres fabrics soaked with a weight mix ratio of resin and hardener of 100:22 for 1h under 10 bars at 100 °C. The measured fibre volume fraction of 40% was estimated from the difference between the weight of the composite and the weight of used fibres. Three specimens for each configuration of 200mmx25mm were cut in the plates and prepared for tensile tests (Figure 1). Thickness of all the samples is 2.5 mm. One mm thick woven fiberglass laminated tabs are bonded to the specimens for introduction of the load by the tensile machine. Specimens were manufactured in order to get different configurations of load to the weft/warp directions, namely [0°]4, [90°]4 and [±45°]4 in order to study the behaviour of the laminate.

Figure 1 :/

 1 Figure 1: Tensile Stress-Strain behaviour of [0]4 samples

Figure 2 :

 2 Figure 2 : Tensile engineering Stress-Strain behaviour of [0°]4 samples

Figure 3 :

 3 Figure 3 : Failure profiles of the [0°]4 samples under cyclic tensile load

Figure 4 :Figure 5 :

 45 Figure 4 : In plane shear Stress-Strain behaviour of [±45°]4 samplesThe pictures of the fracture surfaces of the [±45°]4 configuration are presented in Figure5. Two

Figure 6 :

 6 Figure 6: Flax fibres Omega panels and 3 points bending specimen dimensions

Figure 7 :

 7 Figure 7: 3 points bending test setup A prescribed displacement is applied to the upper roller with a speed of 1 mm/min.

Figure 9 -

 9 Figure 9-A shows the fracture of the specimens with a clear fracture and high load. A lower

Figure 9 :-

 9 Figure 9: Omega sandwich flax panel failure, A) Failure mode 1 M1, B) Failure mode 2 M2

Figure 10 :

 10 Figure 10: Example of a typical damage/failure behaviour

Fail_c iiε 12 γ

 12 is the strain the failure in warp/weft direction in compressive fail is the shear strain failure in plane direction, Finally, each failure damage variable can be computed by

  This phase consists in realizing tensile tests for [0°]4, [90°]4 and [±45°]4 with loads-unloads cycles. Diffuse damage identification parameters First we assume that for a 2x2 twill fabric ply, behaviours according to warp or weft directions are the same. So only [0°]4 test samples were used to identify diffuse damage and pseudo-plasticity parameters. The diffuse damage behaviour is identified with load-unload tests by measuring for each cycle, the modulus, the stress and total elastic values and the residual strains as shown Figure 11.

Figure 11 :

 11 Figure 11: Example of damage parameters measurement on a [±45°]4 tensile test

Figure 12 :

 12 Figure 12: Diffuse damage identification curves

Figure 13 : 4

 134 Figure 13: Pseudo-plasticity identification curves

Figure 14 .

 14 Figure 14. CT sample dimensions (a) and tensile test configuration with DIC measurement (b)

Figure 15 .hi

 15 Figure 15. CT sample dimensions (a) and tensile test configuration with DIC measurement (b)

Figure 16 .Figure 17 :

 1617 Figure 16. Mesh and boundary conditions of tensile test.

Figure 18 :

 18 Figure 18: Mesh and boundary conditions of 3 points bending test.

Figure 19 :

 19 Figure 19: Numerical/Experimental load displacement behaviour comparison

  damages in weft direction (Figure19-B) are located in the upper skin of the panel, and on either side of the Omega core (stiffener). In plane shear failure damage initiates only between the lower skin and the Omega core, near the border of the panel (Figure19-C).

Figure 20 :

 20 Figure 20: Position of failure damages at pic force. A) warp direction B) weft direction, C) in plane direction

Figure 21 :

 21 Figure 21: Numerical(B)/Experimental(A) final failure mode comparison (B shows warp damage failure values)

Figure 22 :

 22 Figure 22: Numerical/Experimental load displacement behaviour comparison. Model with cohesive behaviour and ply damage/failure model

Figure 23 :

 23 Figure 23: Cohesive damage parameter during softening part of the 3 points bending behaviour A) pic force, B) longitudinal propagation of debonding and C) local buckling

Figure 24 :

 24 Figure 24: Experimental(A) /numerical(B) final failure mode by Core/Skin debonding (B shows displacement values)

  first one is a tensile failure of the lower skin of the panel. The second one is a debonding and buckling of the upper skin of the panel.The nonlinear behaviour of Omega panels has been attributed to the strong nonlinearity of the flax fibres behaviour in yarn direction, and possible defects in the panel assembly. This is why a ply damage/failure model behaviour has been proposed. This four phase model introduces a linear part followed by non-linear phases: damage model follows a thermodynamic approach; a failure model is based on strain failure criterion coupled with the energy release rate. After presenting the material model, the identification procedure has been detailed. The model has been developed as a user material model subroutine in Abaqus standard software for non-linear static analyses. An experimental versus numerical comparison of the ply behaviour has been presented which show a very good agreement.This model has been used to predict the global and local behaviour including damage failure and debonding of Flax Omega sandwich panels using a 3D FE model. This model has been proved to be able to predict the global non-linear force-displacement behaviour of the Omega Flax Sandwich Panel and also the local failure modes observed experimentally. The first one is due to tensile failure of the lower skin of the panel. The second one is due to debonding of the upper skin probably due to the presence of bonding defects of the skin, observed on some panels.These results are promising for the use of flax fibre composites in aeronautical structures as a replacement solution of glass fibre composite sandwich panels.

Table 1 :

 1 Young's moduli and failure characteristics of flax fabric ply

	Laminate	E0 (GPa)	σmax (MPa)	εmax (%)	ν
	[0°]	13.9 ± 0.5	122 ± 0.2	1,37 ± 0,21	0,13
	[90°]	14.0 ± 1.2	121 ± 6.0	1,45 ± 0,01	0,10
	±[45°]	2.1 ± 0.2	36 ± 0.3	6,48 ± 0,39

-2.2. 3 points bending Omega Sandwich Panels behaviour 2.2.1. Manufacturing

Table 2 .

 2 Figure

	Panel type	Thickness (mm)	Surface weight (kg/m 2 )	Force at Failure (N)	Stiffness (N/mm)	failure Force per surface weight (N/kg.m 2 )
	Glass fibres / NOMEX	12.70	2.9	2353	562	811
	Flax fibres OMEGA M1 (mean)	11.27	3.1	2250	577	658
	Flax fibres OMEGA M2 (mean)	11.27	3.1	1845	577	658

8: Load displacement behaviour comparison of omega sandwich panels and a commercial Glass fibres/Nomex® sandwich panels Table 2: Comparison of characteristic behaviour of Flax Omega panels and Glass Nomex Panels(M1: failure mode 1, M2 failure mode II)

Table 3 .

 3 Identified values of diffuse damage

		A	B
	±[45°]	0.3708	0.4427
	[0°] & [90°]	0.2083	0.3503

Table 4 .

 4 Identified values for pseudo plasticity

		A	B
	±[45°]	97.6	0.471
	[0°] & [90°]	428.3	0.554

Table 5 .

 5 Failure energy of Flax/epoxy woven 2x2 twill ply

	Gf (0° warp)	Gf (90° weft)	Gm (Matrix)
	J/m2	J/m2	J/m2
	5.0 ±0.23	4.86 ±0.32	0.125

Table 6 :

 6 Dimension of the Omega Sandwich

	Measures	lenght	width	height Thickness of the skins Thickness of the core
	Value (mm)	200	80	11.27	0.5	0.6
	This model Figure 17 has been meshed with C3D8 brick elements (Mesh obtains with a
	global convergence normal stress due to bending). Size of elements in skin and core part is
	near 1.0mm×1.0mm×0.25mm. Some elements are smaller in refined part close to rounded
	corners (about 0.25mm×0.25mm×0.25mm). The model tested consist on a corrugated panel,

Table 7

 7

			: woven ply characteristics
	E11=E22 (MPa)	E33 (MPa)	G12 (MPa)	G13=G23 (MPa)	ν12	ν13=ν23
	17500±42	7500±62	1900±20	1600±30	0.06±0,005 0.06±0.007

Table 8 :

 8 Initial values for diffuse damage computation

	ε11=ε22 init	ε33 init	γ12 init	γ13=γ23	Yf init	Ym init
	(%)	(%)	(%)	(%)	(J/m 3 )	(J/m 3 )
	0.23±0.05	0.52±0.025	0.63±0.035 0.85±0.045	0.5,e,E,e	0.5.g.G12.g

Table 9 :

 9 Failure values for failure damage computation

	ε11=ε22 fail	ε33fail	γ12fail	γ13=γ23 fail	Gf fail	Gm fail
	(%)	(%)	(%)	(%)	(J/m 2 )	(J/m 2 )
	1.45±0.12	3.45±0,.6	7.2±0.43	8.3±0.8	5000 ±163	125 ±15

Table 10 :

 10 Cohesive values for cohesive behaviourWe observed during the experimental study, two modes of failure of the panels; one by failure of the lower skin in tension, the other by debonding of the upper skin in compression (see section 2). According to these results, two types of models were analysed in a global way but also in terms of local damages. , or forces and displacements at failure, are reported in Table11. As can be seen, the FE model simulates accurately the behaviour of the flax fibres omega panel in three point bending. The behaviour is globally nonlinear as observed experimentally and specific values in Table11are also very close.

	Κnn = Κnn = Κnn	σ33 init	σ13= σ23	GIc	GIIc = GIIc
		(N/mm 3 )	(MPa)	(MPa)	(J/m 2 )	(J/m 2 )
		100 000	50	70	125 ±15	350 ±36
	4.3.	Test and numerical behaviour comparison
	4.3.1. Ply damage model results
	The first experimental/numerical comparison uses a pure damage/failure model without
	cohesive behaviour. Figure 18 shows numerical/experimental comparison of load-
	displacement behaviours. Characteristic values as stiffness values (measured between 100N
	and 500N)

Table 11 :

 11 Global numerical/experimental values results comparison

		Stiffness K	Failure force	Displacement at failure
		(N/mm)	(N)	(mm)
	Exp.	577	2250	7.0
	FE model	528	2090	6.6
	Difference	9.3 (%)	7.6 (%)	6.0(%)

Table 12 :

 12 Global numerical/experimental values results comparison

		Stiffness K	Failure force	Displacement at failure
		(N/mm)	(N)	(mm)
	Exp.	577	1845	6,3
	FE model	533	1820	5.6
	Difference	8.2 (%)	5.6 (%)	12.5 (%)