Abdon Atangana
email: atanganaa@ufs.ac.za

Seda Igret Araz
email: sedaaraz@siirt.edu.tr

Deterministic-Stochastic modeling: A new direction in modeling real world problems with crossover effect

Keywords: Stochastic-deterministic models, piecewise existence and uniqueness, piecewise numerical scheme, new classes of chaotic attractors

published or not. The documents may come   L'archive ouverte pluridisciplinaire

Introduction

Indeed these deterministic models have failed to replicate real world problems exhibiting randomness. However they are very useful to depict processes exhibiting power-law, fading memory to power-law, passage from fading memory to power-law [START_REF] Atangana | New fractional derivatives with non-local and non-singular kernel, Theory and Application to Heat Transfer Model[END_REF][START_REF] Caputo | On the notion of fractional derivative and applications to the hysteresis phenomena[END_REF][START_REF] Atangana | Extension of rate of change concept: From local to nonlocal operators with applications[END_REF][START_REF] Atangana | New concept in calculus: Piecewise di¤erential and integral operators[END_REF]. They are also useful to depict memory processes. Stochastic di¤erential equations have been introduced to deal with processes exhibiting randomness. They have been used in many real world problems with great success [START_REF] Ababneh | A new four-dimensional chaotic attractor[END_REF][START_REF] Atangana | Fractional derivatives with no-index law property: application to chaos and statistics[END_REF][START_REF] Faranda | Stochastic chaos in a turbulent swirling ‡ow[END_REF][START_REF] Kosmidis | Stochastic Chaos in a neuronal model[END_REF][START_REF] Canavier | Chaotic versus stochastic dynamics: A critical look at the evidence for nonlinear sequence dependent structure in dopamine neurons[END_REF][START_REF] Toker | A simple method for detecting chaos in nature[END_REF][START_REF] Cunli | Stochastic chaos in a Du¢ ng oscillator and its control[END_REF]. However there exist in nature processes that exhibit passage from power-law to fading memory, or even from memoriless to power-law, indeed such processes cannot be replicated using either stochastic models or deterministic models. Very recently Atangana and Seda introduced new concepts called piecewise di¤erentiation and integration, where a derivative or an integral is de…ned as a piecewise within a given interval [START_REF] Atangana | New concept in calculus: Piecewise di¤erential and integral operators[END_REF]. Such a concept is indeed a new mathematical weapon to model complex real world problems exhibiting complex cross-over behaviors. The new type of modeling will be able to handle many complex problems. For example, we observe a very strange way of spread exhibiting by , where in some cases, the spread shows a sign of deterministic within a given period of time then later 1 it shows sign of stochastic randomness. A clear indication of complex cross-over. In this paper, we aim at modeling behaviors of real world exhibiting cross-over from deterministic to stochastic or vice versa.

2 Modeling cross-over from deterministic to stochastic and vice versa

In this section, we discuss di¤erent possible scenarios that could possibly occur in nature.

Case 1. Assume a real world problem exhibiting cross-over from memoriless process to randomness with no steady state. A general Cauchy problem associated to this is given as 8 > > < > > :

dy(t)
dt = f (t; y (t)) , 0 t t 1 y (0) = y 0 dy (t) = f (t; y (t)) dt + y (t) dB (t) , t 1 t T y (t 1 ) = y 1 [START_REF] Atangana | New fractional derivatives with non-local and non-singular kernel, Theory and Application to Heat Transfer Model[END_REF] where and B (t) ; are density of randomness and environmental noise respectively. Case 2. Assuming that a real world problem exhibits cross-over from power-law to stochastic processes, then the Cauchy problem associated to this problem can be de…ned as 8 > > < > > :

C 0 D t y (t) = f (t; y (t)) , 0 t t 1 y (0) = y 0 dy (t) = f (t; y (t)) dt + y (t) dB (t) , t 1 t T y (t 1 ) = y 1

where 0 < 1: Case 3. Assuming that a real world problem exhibits cross-over from fading memory to stochastic processes, then the general Cauchy problem associated to this real world problem can be de…ned as 8 > > < > > :

CF 0 D t y (t) = f (t; y (t)) , 0 t t 1 y (0) = y 0 dy (t) = f (t; y (t)) dt + y (t) dB (t) , t 1 t T y (t 1 ) = y 1

where 0 < 1: Case 4. Assuming that a complex real world problem is exhibiting cross-over from Mittag-Le-er process to stochastic processes, then the general Cauchy problem associated to such problem is de…ned as 8 > > < > > :

ABC 0 D t y (t) = f (t; y (t)) , 0 t t 1 y (0) = y 0 dy (t) = f (t; y (t)) dt + y (t) dB (t) , t 1 t T y (t 1 ) = y 1

where 0 < 1: In the stochastic part, the classical derivative can be replaced by global derivative to capture more complex behaviors. To accommodate readers that are not use to fractional calculus, we present the following de…nitions

C 0 D t y (t) = 1 (1 ) Z t 0 y0 ( ) (t ) d : (5)
where 0 < 1:

CF 0 D t y (t) = M ( ) 1 Z t 0 y0 ( ) exp 1 (t ) d : (6)
where 0 < 1; M (0) = M (1) and M ( ) is de…ned as normalized function. The space within which such is de…ned is well presented in [??]

ABC 0 D t y (t) = AB ( ) 1
Z t 0 y0 ( ) E 1 (t ) d : (7)
where 0 < 1; AB (0) = AB (1) and AB ( ) = 1 + ( ) : Finally a global derivative of a function f with respect to a function g where g is positive continuously increasing function is de…ned as

D g f (t) = lim t!t1 f (t) f (t 1 ) g (t) g (t 1 ) : (8)
If f and g are di¤erentiable with g0 (t) 6 = 0; then

D g f (t) = f 0 (t) g0 (t) : (9)
Case 5. Assuming that a real world problem exhibits random walk processes from [0; t 1 ], then later the process follows changes within region in [t 1 ; T ]. A mathematical model associate to this will be 8 > > < > > :

dy (t) = f (t; y (t)) dt + y (t) dB (t) , 0 t t 1 y (0) = y 0 D g y (t) = f (t; y (t)) , t 1 t T y (t 1 ) = y 1 : (10)
where D g can be fractional also.

Analysis of deterministic-stochastic models

In this section, we present a discussion regarding numerical solution of each de…ned deterministicstochastic model. For each suggested deterministic-stochastic model, the analysis of existence and uniqueness of solutions can be performed piece-wisely according to each interval. A proper space of the function can be chosen and a suitable methodology for proving existence and uniqueness of such a model can be performed within each interval. This will not be the object of discussion in our paper, however some examples will be considered later and the existence and uniqueness of their solutions will be presented accordingly. In this section, our focus will be to provide a numerical solution to each model using the Newton polynomial interpolation formula [START_REF] Atangana | New numerical scheme with Newton polynomial: Theory, Methods and Applications[END_REF].

Numerical scheme for Case 1

We consider the following problem to present numerical scheme 8 > > < > > :

dy(t) dt = f (t; y (t)) , 0 t t 1 y (0) = y 0 dy (t) = f (t; y (t)) dt + y (t) dB (t) , t 1 t T y (t 1 ) = y 1 : (11)
The above is converted to

y (t) = ( y (0) + R t1 0 f ( ; y) d y (t 1 ) + R t t1 f ( ; y ( )) d + R t t1 y ( ) dB ( ) (12)
or

y (t n+1 ) = ( y (0) + R t1 0 f ( ; y) d y (t 1 ) + R t t1 f ( ; y ( )) d + R t t1 y ( ) B0 ( ) d : (13)
At t = t n+1 , we write

y (t n+1 ) = ( y (0) + R t1 0 f ( ; y) d y (t 1 ) + R tn+1 t1 f ( ; y ( )) d + R tn+1 t1 y ( ) B0 ( ) d (14)
and

y (t n+1 ) = ( y (0) + P i k=0 R t k+1 t k f ( ; y) d y (t 1 ) + P n k=i+1 R t k+1 t k f ( ; y ( )) d + P n k=i+1 R t k+1 t k y ( ) B0 ( ) d : (15)
We approximate f (t; y) within [t k ; t k+1 ] when 0 t t 1 using the Newton interpolation polynomial

f (t; y) = P k (t) ' f (t k 1 ; y (t k 1 )) + f (t k 1 ; y (t k 1 )) f (t k 2 ; y (t k 2 )) t (t t k 2 ) (16) + f (t k ; y (t k )) 2f (t k 1 ; y (t k 1 )) + f (t k 2 ; y (t k 2 )) 2 ( t)

Numerical scheme for Case 2

We deal with the following problem where …rst part is with Caputo fractional derivative and second part is stochastic. Such model is given by 8 > > < > > :

C 0 D t y (t) = f (t; y (t)) , 0 t t 1 y (0) = y 0 dy (t) = f (t; y (t)) dt + y (t) dB (t) , t 1 t T y (t 1 ) = y 1 : (18)
The above is converted to

y (t) = ( 1 ( ) R t1 0 f ( ; y) (t ) 1 d y (t 1 ) + R t t1 f ( ; y ( )) d + R t t1 y ( ) B0 ( ) d : (19)
At t = t n+1 , we write

y (t n+1 ) = ( 1 ( ) R t1 0 f ( ; y) (t ) 1 d y (t 1 ) + R tn+1 t1 f ( ; y ( )) d + R tn+1 t1 y ( ) B0 ( ) d (20)
and

y (t n+1 ) = ( 1 ( ) P i k=0 R t k+1 t k f ( ; y) (t n+1 ) 1 d y (t 1 ) + P n k=i+1 R t k+1 t k f ( ; y ( )) d + P n k=i+1 R t k+1 t k y ( ) B0 ( ) d : (21)
Replacing f (t; y) by its Newton polynomial , we can approximate f (t; y) within [t k ; t k+1 ] as follows

y (t n+1 ) = 8 > > > > > > > > > > > > > < > > > > > > > > > > > > > : 8 > > > < > > > : ( t) 1 ( +1) P i k=2 f t k 2 ; y k 2 + ( t) 1 ( +2) P i k=2 f t k 1 ; y k 1 f t k 2 ; y k 2 + ( t) 1 2 ( +3) P i k=2 f t k ; y k 2f t k 1 ; y k 1 +f t k 2 ; y k 2 9 > > > = > > > ;
where the …rst part is Caputo-Fabrizio fractional derivative and second part is stochastic. Such problem can be integrated as

y (t) = ( 1 M ( ) f (t; y) + M ( ) R t1 0 f ( ; y) d y (t 1 ) + R t t1 f ( ; y ( )) d + R t t1 y ( ) dB ( ) (24)
or

y (t) = ( 1 M ( ) f (t; y) + M ( ) R t1 0 f ( ; y) d y (t 1 ) + R t t1 f ( ; y ( )) d + R t t1 y ( ) B0 ( ) d (25)
At t = t n+1 , we write

y (t n+1 ) = ( 1 M ( ) f (t; y) + M ( ) R t1 0 f ( ; y) d y (t 1 ) + R tn+1 t1 f ( ; y ( )) d + R tn+1 t1 y ( ) B0 ( ) d (26)
and

y (t n+1 ) = ( 1 M ( ) f (t n ; y n ) + M ( ) P i k=0 R t k+1 t k f ( ; y) d y (t 1 ) + P n k=i+1 R t k+1 t k f ( ; y ( )) d + P n k=i+1 R t k+1 t k y ( ) B0 ( ) d : (27)
We can approximate f (t; y) within [t k ; t k+1 ] as follows

y (t n+1 ) = 8 > > > > > > > > < > > > > > > > > : 1 M ( ) f (t n ; y n ) + M ( ) P i k=2 5 12 f t k 2 ; y k 2 t 4 3 f t k 1 ; y k 1 t + 23 12 f t k ; y k t 2 6 6 6 6 4 y (t 1 ) + P n k=i+3 5 12 f t k 2 ; y k 2 t 4 3 f t k 1 ; y k 1 t + 23 12 f t k ; y k t + P n k=i+3 8 < : 5 12 (B (t k 1 ) B (t k 2 )) y k 2 4 3 (B (t k ) B (t k 1 )) y k 1 + 23 12 (B (t k+1 ) B (t k )) y k 9 = ; : (28)

Numerical scheme for Case 4

To obtain numerical scheme for following problem with piecewise derivative, we consider the following problem 8 > > < > > :

ABC 0 D t y (t) = f (t; y (t)) , 0 t t 1 y (0) = y 0 dy (t) = f (t; y (t)) dt + y (t) dB (t) , t 1 t T y (t 1 ) = y 1 : (29)
The above problem can be converted as

y (t) = ( 1 AB( ) f (t; y) + AB( ) ( ) R t1 0 f ( ; y) (t ) 1 d y (t 1 ) + R t t1 f ( ; y ( )) d + R t t1 y ( ) B0 ( ) d : (30)
At t = t n+1 , we write

y (t n+1 ) = ( 1 AB( ) f (t; y) + AB( ) ( ) R t1 0 f ( ; y) (t ) 1 d y (t 1 ) + R tn+1 t1 f ( ; y ( )) d + R tn+1 t1 y ( ) B0 ( ) d (31)
and

y (t n+1 ) = ( 1 AB( ) f (t n ; y n ) + AB( ) ( ) P i k=0 R t k+1 t k f ( ; y) (t n+1 ) 1 d y (t 1 ) + P n k=i+1 R t k+1 t k f ( ; y ( )) d + P n k=i+1 R t k+1 t k y ( ) B0 ( ) d : (32)
Replacing f (t; y) by its Newton polynomial, we can get the following scheme

y (t n+1 ) = 8 > > > > > > > > > > > > > < > > > > > > > > > > > > > : 8 > > > < > > > : 1 AB( ) f (t n ; y n ) + AB( ) ( t) 1 ( +1) P i k=2 f t k 2 ; y k 2 + AB( ) ( t) 1 ( +2) P i k=2 f t k 1 ; y k 1 f t k 2 ; y k 2 + AB( ) ( t) 1 2 ( +3) P i k=2 f t k ; y k 2f t k 1 ; y k 1 +f t k 2 ; y k 2 9 > > > = > > > ; 2 6 6 6 6 4 y (t 1 ) + P n k=i+3 5 12 f t k 2 ; y k 2 t 4 3 f t k 1 ; y k 1 t + 23 12 f t k ; y k t + P n k=i+3 8 < : 5 12 (B (t k 1 ) B (t k 2 )) y k 2 4 3 (B (t k ) B (t k 1 )) y k 1 + 23 12 (B (t k+1 ) B (t k )) y k 9 = ; : (33)

Numerical scheme for Case 5

In this paper, we consider the following problem with piecewise derivative 8 > > < > > :

dy (t) = f (t; y (t)) dt + y (t) dB (t) , 0 t t 1 y (0) = y 0 D g y (t) = f (t; y (t)) , t 1 t T y (t 1 ) = y 1 (34)
which is transformed into

y (t) = ( y (0) + R t1 0 f ( ; y ( )) d + R t1 0 y ( ) dB ( ) y (t 1 ) + R t t1 f ( ; y ( )) dg ( ) (35)
or

y (t) = ( y (0) + R t1 0 f ( ; y ( )) d + R t1 0 y ( ) B0 ( ) d y (t 1 ) + R t t1 f ( ; y ( )) g0 ( ) d : (36)
At t = t n+1 , we write

y (t n+1 ) = ( y (0) + R t1 0 f ( ; y ( )) d + R t1 0 y ( ) B0 ( ) d y (t 1 ) + R tn+1 t1 f ( ; y) g0 ( ) d (37)
and

y (t n+1 ) = ( y (0) + P i k=0 R t k+1 t k f ( ; y ( )) d + P i k=0 R t k+1 t k y ( ) B0 ( ) d y (t 1 ) + P n k=i+1 R t k+1 t k f ( ; y ( )) g0 ( ) d : (38)
The function f (t; y) can be approximated as follows

y (t n+1 ) = 8 > > > > > > < > > > > > > : 2 4 y (
dx dt = y + (x) z + I dy dt = (x) y dz dt = r [s (x x R ) z] x (0) = x 0 ; y (0) = y 0 ; z (0) = z 0 if 0 t 12 (40) 8 > > < > > : dx = (y + (x) z + I) dt + 1 xdB 1 (t) dy = ( (x) y) dt + 2 ydB 2 (t) dz = (r [s (x x R ) z]) dt + 3 zdB 3 (t) x (12) = x 12 ; y (12) = y 12 ; z (12) = z 12 if 12 t 25: (41)
Here (x) = ax 3 + bx 2 ; (x) = c dx 2 :

We de…ne the norm k'k 1 = sup t2D' j' (t)j, we consider a Banach space. We present here the existence and uniqueness of the solution piecewisely. However to achieve this, we verify the lineargrowth and Lipschitz condition properties. We also assume that 8t 2 [0; 12], there exists 3 positive constant M 1 ; M 2 and M 3 < 1 such that kxk 1 < M 1 ; kyk 1 < M 2 and kzk 1 < M 3 .

> <

> :

x = f 1 (x; y; z; t) y = f 2 (x; y; z; t) z = f 3 (x; y; z; t) if 0 t 12: (42)
8i = 1; 2; 3; we …rst verify that

jf i (x; t)j 2 < k i jx i j 2 + 1 (43)
and

f i x 1 ; t f i x 2 ; t 2 < k i x 1 x 2 2 : (44)
For proof, we consider the function f 1 (x; y; z; t)

jf 1 (x; y; z; t)j 2 = y + bx 2 ax 3 z + I 2 (45) 4 jyj 2 + 4 bx 2 ax 3 2 + 4 jzj 2 + 4I 2 4 sup t2[0;12] y 2 + bx ax 2 2 jxj 2 + sup t2[0;12] z 2 + I 2 ! 4 y 2 1 + bx ax 2 1 jxj 2 + z 2 1 + I 2 (46) 4 y 2 1 + z 2 1 + I 2 1 + bx ax 2 1 ky 2 k 1 + kz 2 k 1 + I 2 jxj 2 ! under the condition that kbx ax 2 k 1 ky 2 k 1 +kz 2 k 1 +I 2 < 1, then jf 1 (x; y; z; t)j 2 k 1 1 + jxj 2 :
Using same routine,

jf 2 (x; y; z; t)j 2 = c dx 2 y 2 (47) 3c 2 + 3d 2 x 2 2 + 3 jyj 2 3 c 2 + d 2 sup t2[0;12] x 4 + y 2 ! 3 c 2 + d 2 x 4 1 + y 2 (48) 3 c 2 + d 2 x 4 1 1 + 1 c 2 + d 2 kx 4 k 1 jyj 2 under the condition that 1 c 2 +d 2 kx 4 k 1 < 1, then jf 2 (x; y; z; t)j 2 k 2 1 + jyj 2 :
For the function F 3 ;

jf 3 (x; y; z; t)j 2 = jr [s (x x R ) z]j 2 2r 2 s 2 jx x R j 2 + 2r 2 jzj 2 2 r 2 s 2 sup t2[0;12] jx x R j 2 + jzj 2 ! 2r 2 s 2 kx x R k 2 1 + jzj 2 (49) 2r 2 s 2 kx x R k 2 1 1 + 1 s 2 kx x R k 2 1 jzj 2 !
under the condition that

1 s 2 k(x x R ) 2 k 1 < 1, then jf 3 (x; y; z; t)j 2 k 3 1 + jzj 2 :
Therefore the condition of linear growth is veri…ed if

max ( bx ax 2 1 ky 2 k 1 + kz 2 k 1 + I 2 ; 1 c 2 + d 2 kx 4 k 1 ; 1
s 2 kx x R k 2 1
)

< 1: (50)
4.1 Numerical scheme for stochastic-deterministic model of Hindmarsh-

Rose model

We consider the Hindmarsh-Rose model in piecewise where the …rst part is classical and the secnd part is stochastic such that the stochastic-deterministic model of Hindmarsh-Rose model [START_REF] Hindmarsh | A model of neuronal bursting using three coupled …rst order di¤erential equations[END_REF] is given as 8 > > < > > :

dx dt = y ax 3 + bx 2 z + I dy dt = c dx 2 y dz dt = rs (x x R ) rz x (0) = x 0 ; y (0) = y 0 ; z (0) = z 0 if 0 t t 1 (51) 8 > > < > > : dx = y ax 3 + bx 2 z + I dt + 1 xdB 1 (t) dy = c dx 2 y dt + 2 ydB 2 (t) dz = (rs (x x R ) rz) dt + 3 zdB 3 (t) x (t 1 ) = x 1 ; y (t 1 ) = y 1 ; z (t 1 ) = z 1 if t 1 t T: (52)
Using the numerical scheme presented in Case1, the numerical solution of the stochastic-deterministic Hindmarsh-rose model is given as follows:

x (t n+1 ) = 8 > > > > > > > > > > > > < > > > > > > > > > > > > : x 0 + P i k=2 8 < : 5 12 y k 2 ax 3k 6 + bx 2k 4 z k 2 + I t 4 3 y k 1 ax 3k 3 + bx 2k 2 z k 1 + I t + 23 12 y k ax 3k + bx 2k z k + I t 9
5 12 (B 1 (t k 1 ) B 1 (t k 2 )) 1 x k 2 4 3 (B 1 (t k ) B 1 (t k 1 )) 1 x k 1 + 23 12 (B 1 (t k+1 ) B 1 (t k )) 1 x k 9 = ; 3 7 7 7 7 7 7 5
, if t 1 t T :

(53)

y (t n+1 ) = 8 > > > > > > > > > > > > < > > > > > > > > > > > > : y 0 + P i k=2 8
z (t n+1 ) = 8 > > > > > > > > > > > > < > > > > > > > > > > > > : z 0 + P i k=2 8 < : 5 12 rs x k 2 x R rz k 2 t 4 3 rs x k 1 x R rz k 1 t + 23 12 rs x k x R rz k t 9 = ; ; if 0 t t 1 2 6 6 6 6 6 6 4
z 1 + P n k=i+3 8 < : 5 12 rs x k 2 x R rz k 2 t 4 3 rs x k 1 x R rz k 1 t + 23 12 rs x k x R rz k t 9 = ; + P n k=i+3 8 < : 5 12 (B 3 (t k 1 ) B 3 (t k 2 )) 3 z k 2 4 3 (B 3 (t k ) B 3 (t k 1 )) 3 z k 1 + 23 12 (B 3 (t k+1 ) B 3 (t k )) 3 z k 9
dx = y ax 3 + bx 2 z + I dt + 1 xdB 1 (t) dy = c dx 2 y dt + 2 ydB 2 (t) dz = (rs (x x R ) rz) dt + 3 zdB 3 (t) x (t 1 ) = x 1 ; y (t 1 ) = y 1 ; z (t 1 ) = z 1 if t 1 t T (57)
where the …rst part is classical and the second part is stochastic.Here initial data is taken as

x (0) = 0:1; y (0) = 0:1; z (0) = 0:1: (58)
In Figure 1, the numerical simulations are depicted with the parameters a = 1; b = 3; c = 1; d = 5; s = 4; x R = 8=5; r = 3 ; I = 6: :

C 0 D t x = y ax 3 + bx 2 z + I C 0 D t y = c dx 2 y C 0 D t z = rs (x x R ) rz if 0 t t 1 (59) 8 <
:

dx = y ax 3 + bx 2 z + I dt + 1 xdB 1 (t) dy = c dx 2 y dt + 2 ydB 2 (t) dz = (rs (x x R ) rz) dt + 3 zdB 3 (t) if t 1 t T:
The numerical solution of such model is given by

x (t n+1 ) = 8 > > > > > > > > > > > > > > > > > > > < > > > > > > > > > > > > > > > > > > > : 8 > > > > > > < > > > > > > : ( t) 1 ( +1) P i k=2 y k 2 ax 3k 6 + bx 2k 4 z k 2 + I + ( t) 1 ( +2) P i k=2 y k 1 ax 3k 3 + bx 2k 2 z k 1 + I y k 2 ax 3k 6 + bx 2k 4 z k 2 + I + ( t) 1 2 ( +3) P i k=2 2 4 y k 2 ax 3k 6 + bx 2k 4 z k 2 + I 2 y k 1 ax 3k 3 + bx 2k 2 z k 1 + I + y k ax 3k + bx 2k z k + I 3 5 9 > > > > > > = > > > > > > ; ; if 0 t
5 12 (B 1 (t k 1 ) B 1 (t k 2 )) 1 x k 2 4 3 (B 1 (t k ) B 1 (t k 1 )) 1 x k 1 + 23 12 (B 1 (t k+1 ) B 1 (t k )) 1 x k 9 = ; , if t 1 t T : (60)
y (t n+1 ) = 8 > > > > > > > > > > > > > > > > > > > < > > > > > > > > > > > > > > > > > > > : 8 > > > > > > < > > > > > > : ( t) 1 ( +1) P i k=2 c dx 2k 4 y k 2 + ( t) 1 ( +2) P i k=2 c dx 2k 2 y k 1 c dx 2k 4 y k 2 + ( t) 1 2 ( +3) P i k=2 2 4 c dx 2k 4 y k 2 2 c dx 2k 2 y k 1 + c dx 2k y k 3 5 9 > > > > > > = > > > > > > ; ; if 0 t
z (t n+1 ) = 8 > > > > > > > > > > > > > > > > > > > < > > > > > > > > > > > > > > > > > > > : 8 > > > > > > < > > > > > > : ( t) 1 ( +1) P i k=2 rs x k 2 x R rz k 2 + ( t) 1 ( +2) P i k=2 rs x k 2 x R rz k 2 rs x k 1 x R rz k 1 + ( t) 1 2 ( +3) P i k=2 2 4 rs x k 2 x R rz k 2 2 rs x k 1 x R rz k 1 + rs x k x R rz k 3 5 9 > > > > > > = > > > > > > ; ; if t t 1 2 6 6 6 6 6 6 4 x 1 + P n k=i+3 8 < : 5 12 rs x k 2 x R rz k 2 t 4 3 rs x k 1 x R rz k 1 t + 23 12 rs x k x R rz k t 9 = ; + P n k=i+3 8 < : 5 12 (B 3 (t k 1 ) B 3 (t k 2 )) 3 z k 2 4 3 (B 3 (t k ) B 3 (t k 1 )) 3 z k 1 + 23 12 (B 3 (t k+1 ) B 3 (t k )) 3 z k 9 = ; 3 7 7 7 7 7 7 (61)
, if t 1 t T : (62) 5

Numerical simulation for stochastic-deterministic model of Hindmarsh-Rose model

We present the numerical simulations for the Hindmarsh-Rose model in piecewise 8 < :

C 0 D t x = y ax 3 + bx 2 z + I C 0 D t y = c dx 2 y C 0 D t z = rs (x x R ) rz if 0 t t 1 (63) 8 <
:

dx = y ax 3 + bx 2 z + I dt + 1 xdB 1 (t) dy = c dx 2 y dt + 2 ydB 2 (t) dz = (rs (x x R ) rz) dt + 3 zdB 3 (t) if t 1 t T:
where initial data is considered as

x (0) = 0:1; y (0) = 0:1; z (0) = 0:1: (64)
In Figure 2 We consider the Hindmarsh-Rose model where the …rst part is Caputo-Fabrizio derivative and the second part is stochastic as follows 8 <

:

CF 0 D t x = y ax 3 + bx 2 z + I CF 0 D t y = c dx 2 y CF 0 D t z = rs (x x R ) rz if 0 t t 1 (65) 8 <
:

dx = y ax 3 + bx 2 z + I dt + 1 xdB 1 (t) dy = c dx 2 y dt + 2 ydB 2 (t) dz = (rs (x x R ) rz) dt + 3 zdB 3 (t) if t 1 t T: (66)
Using the numerical scheme presented in Case 3, the numerical scheme for stochastic-deterministic Hindmarsh-rose model is given as follows: ;

x (t n+1 ) = 8 > > > > > > > > > > > > > > < > > > > > > > > > > > > > > :
+ P n k=i+3 8 < : 5 12 (B 1 (t k 1 ) B 1 (t k 2 )) 1 x k 2 4 3 (B 1 (t k ) B 1 (t k 1 )) 1 x k 1 + 23 12 (B 1 (t k+1 ) B 1 (t k )) 1 x k 9 = ; 3 7 7 7 7 7 7 5
; if t 1 t T :

(67)

y (t n+1 ) = 8 > > > > > > > > > > > > > > < > > > > > > > > > > > > > > : 1 M ( ) c
5 12 (B 2 (t k 1 ) B 2 (t k 2 )) 2 y k 2 4 3 (B 2 (t k ) B 2 (t k 1 )) 2 y k 1 + 23 12 (B 2 (t k+1 ) B 2 (t k )) 2 y k 9 = ; 3 7 7 7 7 7 7 5
; if t 1 t T :

z (t n+1 ) = 8 > > > > > > > > > > > > > > < > > > > > > > > > > > > > > : 1 M ( ) (rs (x n x R ) rz n ) + M ( ) P i k=2 8 < : 5 12 rs x k 2 x R rz k 2 t 4 3 rs x k 1 x R rz k 1 t + 23 12 rs x k x R rz k t 9 = ; ; if 0 t t 1 2 6 6 6 6 6 6 4 z 1 + P n k=i+3 8 < : 5 12 rs x k 2 x R rz k 2 t 4 3 rs x k 1 x R rz k 1 t + 23 12 rs x k x R rz k t 9 = ; + P n k=i+3 8 < : 5 12 (B 3 (t k 1 ) B 3 (t k 2 )) 3 z k 2 4 3 (B 3 (t k ) B 3 (t k 1 )) 3 z k 1 + 23 12 (B 3 (t k+1 ) B 3 (t k )) 3 z k 9 = ; 3 7 7 7 7 7 (68)
; if t 1 t T : (69)

Numerical scheme for stochastic-deterministic model of Hindmarsh-Rose model

In this section, we present the numerical scheme for Hindmarsh-Rose model with piecewise derivative 8 < :

ABC 0 D t x = y ax 3 + bx 2 z + I ABC 0 D t y = c dx 2 y ABC 0 D t z = rs (x x R ) rz if 0 t t 1 (72) 8 <
:

dx = y ax 3 + bx 2 z + I dt + 1 xdB 1 (t) dy = c dx 2 y dt + 2 ydB 2 (t) dz = (rs (x x R ) rz) dt + 3 zdB 3 (t) if t 1 t T:
Stochastic-deterministic Hindmarsh-Rose model can be solved by the following scheme

x (t n+1 ) = 8 > > > > > > > > > > > > > > > > > > > > > < > > > > > > > > > > > > > > > > > > > > > : 8 > > > > > > > > > < > > > > > > > > > : 1 AB( ) y n ax 3n + bx 2n z n + I + AB( ) ( t) 1 ( +1) P i k=2 y k 2 ax 3k 6 + bx 2k 4 z k 2 + I + AB( ) ( t) 1 ( +2) P i k=2 y k 1 ax 3k 3 + bx 2k 2 z k 1 + I y k 2 ax 3k 6 + bx 2k 4 z k 2 + I + AB( ) ( t) 1 2 ( +3) P i k=2 2 4 y k 2 ax 3k 6 + bx 2k 4 z k 2 + I 2 y k 1 ax 3k 3 + bx 2k 2 z k 1 + I + y k ax 3k + bx 2k z k + I 3 5 9 > > > > > > > > > = > > > > > > > > > ; ; if 0 t t 1 2 6 6 6 6 6 6 4
x 1 + P n k=i+3 8 < :

5 12 y k 2 ax 3k 6 + bx 2k 4 z k 2 + I t 4 3 y k 1 ax 3k 3 + bx 2k 2 z k 1 + I t + 23 12 y k ax 3k + bx 2k z k + I t 9 = ; + P n k=i+3 8 < : 5 12 (B 1 (t k 1 ) B 1 (t k 2 )) 1 x k 2 4 3 (B 1 (t k ) B 1 (t k 1 )) 1 x k 1 + 23 12 (B 1 (t k+1 ) B 1 (t k )) 1 x k 9 = ; 3 7 7 7 7 7 7 5
, if t 1 t T :

(73)

y (t n+1 ) = 8 > > > > > > > > > > > > > > > > > > > < > > > > > > > > > > > > > > > > > > > : 8 > > > > > > < > > > > > > : 1 AB( ) c dx 2n y n + AB( ) ( t) 1 ( +1) P i k=2 c dx 2k 4 y k 2 + AB( ) ( t) 1 ( +2) P i k=2 c dx 2k 2 y k 1 c dx 2k 4 y k 2 + AB( ) ( t) 1 2 ( +3) P i k=2 2 4 c dx 2k 4 y k 2 2 c dx 2k 2 y k 1 + c dx 2k y k 3 5 9 > > > > > > = > > > > > > ; ; if 0 t
dx = y ax 3 + bx 2 z + I dt + 1 xdB 1 (t) dy = c dx 2 y dt + 2 ydB 2 (t) dz = (rs (x x R ) rz) dt + 3 zdB 3 (t) x (0) = x 0 ; y (0) = y 0 ; z (0) = z 0 if 0 t t 1 (78) 8 > > < > > : D g x = y ax 3 + bx 2 z + I D g y = c dx 2 y D g z = (rs (x x R ) rz) x (t 1 ) = x 1 ; y (t 1 ) = y 1 ; z (t 1 ) = z 1 if t 1 t T: (79)
Using the numerical scheme presented in Case 5, we can have the following scheme for the stochasticdeterministic Hindmarsh-Rose model

x (t n+1 ) = 8 > > > > > > > > > > > > < > > > > > > > > > > > > :

Numerical simulation for stochastic-deterministic 4D Sinusoidally Driven Lorenz system model

We present the numerical solution for 4D sinusoidally Driven Lorenz model [START_REF] Chunyan | A Sinusoidally Driven Lorenz System and Circuit Implementation[END_REF] in piecewise where the …rst part is considered with classical and the second part is stochastic. Such model is represented by 8 > > < > > :

In Figure 9, the numerical simulations for the considered system are performed with the parameters a = 10; b = 30; d = 8=3; c = 17; w = 0:5: In Figure 14, we present the numerical simulations for stochastic-deterministic Bouali system for the parameters a = 3; = 2:2; b = 1; = 1:51:

where where the …rst part is Caputo and the second part is stochastic. Initial conditions are taken as

x (0) = 1; y (0) = 1; z (0) = 0:02:

In Figure 15, the numerical simulations are depicted for the parameters a = 3; = 2:2; b = 1; = 0:001:

if 0 t t 1 (108) 8 <
:

D g x = ax (1 y) z D g y = y 1 x 2 D g z = x if t 1 t T: (109)
such that g (t) = t: Also initial conditions are as follows

x (0) = 1; y (0) = 1; z (0) = 0:02:

In Figure 18, the numerical simulations are presented for the parameters a = 3; = 2:2; b = 1; = 0:001:

Conclusion

Using the concept of piecewise di¤erentiation and integration suggested by Atangana and Seda recently, we suggested new classes of nonlinear ordinary di¤erential equations. These new classes are called piece-wise deterministic stochastic equations. We suggested …ve classes, of course more classes can be obtained depending on how the piece-wise di¤erential and integral operators are de…ned with given intervals. We informed that, of each class presented, a suitable method to prove existence and uniqueness of piecewise solution can be performed in suitable spaces. However, we also informed that such discussion was not presented in general in our paper. Nevertheless, we considered a few chaotic models and extended each one of the …ve classes suggested, for some we presented conditions under which existence and unique solutions are obtained. General numerical solutions using the Newton polynomial interpolation were obtained. Illustrative examples are presented together with simulations. The obtained solutions leave us no chose to conclude that, this approach is the future of modelling complex real world problems.

4 . 2 = y ax 3 +

 423 Numerical simulation for stochastic-deterministic model of Hindmarsh-Rose model We provide the numerical simulations for the Hindmarsh-Rose model with piecewise derivative 8 bx 2 z + I dy dt = c dx 2 y dz dt = rs (x x R ) rz x (0) = x 0 ; y (0) = y 0 ; z (0) = z 0

Figure 1 .

 1 Figure 1. Numerical visualization of Hindmarsh-Rose model for = 1; 1 = 0:01; 2 = 0:015; 3 = 0:012:

  , the numerical simulations are provided with the parameters a = 1; b = 3; c = 1; d = 5; s = 4; x R = 8=5; r = 10 3 ; I = 6:

Figure 2 .

 2 Figure 2. Numerical visualization of Hindmarsh-Rose model for = 1; 1 = 0:01; 2 = 0:015; 3 = 0:012:

Figure 4 .

 4 Figure 4. Numerical visualization of Hindmarsh-Rose model for = 1; 1 = 0:01; 2 = 0:015; 3 = 0:012:

8 where

 8 g (t) = t and initial data is considered as x (0) = 0:1; y (0) = 0:1; z (0) = 0:1:(85)In Figure5, the numerical simulations are depicted with the parameters a = 1; b = 3; c = 1; d = 5; s = 4; x R = 8=5; r = 10 3 ; I = 6:

Figure 5 .

 5 Figure 5. Numerical visualization of Hindmarsh-Rose model for = 1; 1 = 0:01; 2 = 0:015; 3 = 0:012:

  dx = ( a (x y c sin u)) dt + 1 xdB 1 (t) dy = (bx xz y) dt + 2 ydB 2 (t) dz = (xy dz) dt+ 3 zdB 3 (t) du = wdt + 4 udB 4 (t) if t 1 t Twhere initial data is considered asx (0) = 0:1; y (0) = 0:1; z (0) = 0:1; u (0) = 0:1:(87)For Case 1, the numerical simulations are performed in Figure6. Here the parameters are chosen as a = 10; b = 30; d = 8=3; c = 17; w = 0:5:

Figure 6 .0

 6 Figure 6. Numerical visualization of 4D Sinusoidally Driven Lorenz system for = 1; 1 = 0:012; 2 = 0:013; 3 = 0:015; 4 = 0:014:

Figure 7 .

 7 Figure 7. Numerical visualization of 4D Sinusoidally Driven Lorenz system for = 1; 1 = 0:012; 2 = 0:013; 3 = 0:015; 4 = 0:014:

Figure 8 .D 0 D t y = bx xz y ABC 0 D t z = xy dz ABC 0 D t u = w if 0 t t 1

 80001 Figure 8. Numerical visualization of 4D Sinusoidally Driven Lorenz system for = 1; 1 = 0:012; 2 = 0:013; 3 = 0:015; 4 = 0:014:

Figure 9 .

 9 Figure 9. Numerical visualization of 4D Sinusoidally Driven Lorenz system for = 1; 1 = 0:012; 2 = 0:013; 3 = 0:015; 4 = 0:014:

D

  g x = a (x y c sin u) D g y = bx xz y D g z = xy dz D g u = w if t 1 t T: such that g (t) = t: Here initial conditions are as follows x (0) = 0:1; y (0) = 0:1; z (0) = 0:1; u (0) = 0:1: (95) In Figure 10, the numerical simulations are depicted for the considered problem where the parameters are chosen as a = 10; b = 30; d = 8=3; c = 17; w = 0:5:

Figure 10 .

 10 Figure 10. Numerical visualization of 4D Sinusoidally Driven Lorenz system for = 1; 1 = 0:012; 2 = 0:013; 3 = 0:015; 4 = 0:014:

Figure 12 .

 12 Figure 12. Numerical visualization of Bouali system for = 1; 1 = 0:02; 2 = 0:022; 3 = 0:025:

Figure 13 .

 13 Figure 13. Numerical visualization of Bouali system for = 1; 1 = 0:02; 2 = 0:022; 3 = 0:025:

Figure 14 . 2 C 0 D

 1420 Figure 14. Numerical visualization of Bouali system for = 1; 1 = 0:02; 2 = 0:022; 3 = 0:025:

Figure 17 .

 17 Figure 17. Numerical visualization of Bouali system for = 1; 1 = 0:02; 2 = 0:022; 3 = 0:025:

Figure 18 .

 18 Figure 18. Numerical visualization of Bouali system for = 1; 1 = 0:02; 2 = 0:022; 3 = 0:025:

  (t k ) B 2 (t k 1 )) 2 y k 1 + 23 12 (B 2 (t k+1 ) B 2 (t k )) 2 y k

	< : 8 < : 5 k=i+3 P n k=i+3 y 1 + + P n 8 < : 12 (B 2 (t k 1 ) B 2 (t k 2 )) 2 y k 2 5 t 9 = 12 c dx 2k 4 y k 2 4 3 c dx 2k 2 y k 1 t + 23 12 c dx 2k y k t ; 5 12 c dx 2k 4 y k 2 t 4 3 c dx 2k 2 y k 1 t + 23 12 c dx 2k y k t 9 = ; 4 3 (B 2 9 ; if 0 t t 1 3 = ; 7 7 7 7 5 7 , if t 1 t T 7	:	(54)

  dx 2n y n

	2 6 6 6 6 6 6 4	+ M ( ) y 1 + P n P i k=2 k=i+3 8 8 < : < : 8 < P n + k=i+3 :	5 12 c dx 2k 4 y k 2 4 3 c dx 2k 2 y k 1 + 23 12 c dx 2k y k 5 12 c dx 2k 4 y k 2 4 3 c dx 2k 2 y k 1 + 23 12 c dx 2k y k	t	t t t t t	9 = ; 9 = ;	; if 0 t t 1

  + 1 xdB 1 (t) dy = by 1 x 2 dt + 2 ydB 2 (t) dz = xdt + 3 zdB 3 (t)

				t t 1	(99)
	8 < :	dx = (ax (1 y)	z) dt if t 1	t T:

Numerical simulation for stochastic-deterministic model of Hindmarsh-Rose model

In this subsection, we consider stochastic-deterministic the Hindmarsh-Rose model where initial data is considered as

x (0) = 0:1; y (0) = 0:1; z (0) = 0:1: (71)

In Figure 3

:

where the …rst part is with Mittag-Le-er kernel and the second part is stochastic. Initial data is considered as

In Figure 4, the numerical simulations are depicted with the parameters a = 1; b = 3; c = 1; d = 5; s = 4; x R = 8=5; r = 10 3 ; I = 6:

:

;

,if 0 t t 1

x 1 + P n k=i+3 8 < : ;

; if 0 t t 1

Numerical simulation for stochastic-deterministic model of Hindmarsh-Rose model

In this subsection, we provide the numerical simulations for the following Hindmarsh-Rose model 8 > > < > > :

6 Applications for stochastic-deterministic model of Bouali system In this section, we present applications of stochastic-deterministic Bouali system for all cases.

Numerical simulation for stochastic-deterministic model of Bouali system

We consider the Bouali model [START_REF] Bouali | A 3D Strange Attractor with a Distinctive Silhouette. The Butter ‡y E¤ect Revisited[END_REF] in piecewise where the …rst part is classical and the second part is stochastic as follows 8 <

:

:

where initial conditions are taken as

In Figure 11 and 12, the numerical simulations are depicted for the parameters a = 3; = 2:2; b = 1; = 0:001: We consider the Bouali model with piecewise derivative 8 < :

:

Initial conditions are given by x (0) = 1; y (0) = 1; z (0) = 0:02

In Figure 16, the numerical simulations are provided for Bouali system where the parameters are taken as a = 3; = 2:2; b = 1; = 0:001:

Here the …rst part is Atangana-Baleanu fractional derivative and the second part is stochastic. Also initial conditions are taken as

x (0) = 1; y (0) = 1; z (0) = 0:02:

In Figure 17, we provide simulations for Bouali system with the parameters a = 3; = 2:2; b = 1; = 0:001:


Stéphane Demri
email: demri@imag.fr

Rajeev Goré

Tractable Transformations from Modal Provability Logics into First-Order Logic

We define a class of modal logics LF by uniformly extending a class of modal logics L. Each logic L is characterised by a class of first-order definable frames, but the corresponding logic LF is sometimes characterised by classes of modal frames that are not first-order definable. The class LF includes provability logics with deep arithmetical interpretations. Using Belnap's proof-theoretical framework Display Logic we characterise the "pseudo-displayable" subclass of LF and show how to define polynomial-time transformations from each such LF into the corresponding L, and hence into first-order classical logic. Theorem provers for classical first-order logic can then be used to mechanise deduction in these "psuedo-displayable second order" modal logics.

Introduction

Background. There are two main approaches to modal theorem proving in the literature. The direct approach consists in defining calculi dedicated to modal logics at the cost of modifying existing theorem provers (see e.g. [START_REF] Fitting | Proof methods for modal and intuitionistic logics[END_REF][START_REF] Auffray | Strategies for modal resolution: results and problems[END_REF][START_REF] Massacci | Strongly analytic tableaux for normal modal logics[END_REF]). The translational approach consists in translating modal logics into logics for which theorem provers already exist, typically classical first-order logic (FOL). The relational translation into FOL (see e.g. [START_REF] Ch | Methods for automated theorem proving in non classical logics[END_REF][START_REF] Schmidt | Decidability by resolution for propositional modal logics[END_REF][START_REF] Ganzinger | A resolution-based decision procedure for extensions of K4[END_REF]) is the most common such translation although not the only one (see e.g. [START_REF] Ch | Methods for automated theorem proving in non classical logics[END_REF][START_REF] Ohlbach | A resolution calculus for modal logics[END_REF][START_REF] Herzig | Raisonnement automatique en logique modale et algorithmes d'unification[END_REF][START_REF] Agostino | A set-theoretical translation method for polymodal logics[END_REF][START_REF] Ohlbach | Combining Hilbert style and semantic reasoning in a resolution framework[END_REF]). These two approaches cannot always be applied with equal success (see e.g. [START_REF] Hustadt | On evaluating decision procedures for modal logic[END_REF]). For instance, for the provability logic G which is characterized by a second-order class of modal frames (see e.g. [START_REF] Boolos | The Logic of Provability[END_REF]), the relational translation is not possible unless FOL is augmented with fixedpoint operators (see e.g. [START_REF] Nonnengart | A fixpoint approach to second-order quantifier elimination with applications to correspondence theory[END_REF]). However, dedicated sequent-style calculi do exist for provability logics such as G or Grz (for Grzegorczyk); see e.g. [START_REF] Sambin | A modal sequent calculus for a fragment of arithmetic[END_REF][START_REF] Leivant | On the proof theory of the modal logic for arithmetical provability[END_REF][START_REF] Fitting | Proof methods for modal and intuitionistic logics[END_REF][START_REF] Valentini | The modal logic of provability: cut-elimination[END_REF][START_REF] Avron | On modal systems having arithmetical interpretations[END_REF][START_REF] Boolos | The Logic of Provability[END_REF][START_REF] Goré | Tableaux methods for modal and temporal logics[END_REF]. Display Logic. Display Logic (DL) [START_REF] Belnap | Display logic[END_REF] is a proof-theoretical framework that generalises the structural language of Gentzen's sequents by using multiple complex structural connectives instead of Gentzen's comma. The term "display" comes from the nice property that any occurrence of a structure in a sequent can be displayed either as the entire antecedent or as the entire succedent of some sequent which is structurally equivalent to the initial sequent (see e.g. [START_REF] Belnap | Display logic[END_REF]). Any display calculus satisfying the conditions (C1)-(C8) [START_REF] Belnap | Display logic[END_REF] (see the appendix) enjoys cut-elimination. Kracht's characterisation of properly displayable modal logics [START_REF] Kracht | Power and weakness of the modal display calculus[END_REF] means that any extension of the (poly)modal logic K obtained by the addition of the so-called primitive axioms admits a display calculus that obeys conditions (C1)-(C8) [START_REF] Kracht | Power and weakness of the modal display calculus[END_REF], and therefore enjoys cut-elimination. Since every primitive axiom is a Sahlqvist formula, any such extension is first-order definable [START_REF] Sahlqvist | Completeness and correspondence in the first and second order semantics for modal logics[END_REF].

Our contribution. Let φ be a modal formula and F(φ) be a formula built from {φ} using ¬, ∧, ∨, ⇒, 2 and 3 such that any subformula of the form 2ψ in F(φ) occurs positively (when every φ 1 ⇒ φ 2 is written as ¬φ 1 ∨ φ 2 ). Let L be a properly displayable modal logic and LF be the logic obtained from L by adding the axiom scheme 2(F(φ) ⇒ φ) ⇒ 2φ. Here a logic is understood as a set of formulae and therefore is exactly a (decision) problem in the usual sense in complexity theory. That is, as a language viewed as a set of strings built upon a given alphabet.

By generalising results from [START_REF] Demri | An O((n.log n) 3 )-time transformation from Grz into decidable fragments of classical first-order logic[END_REF], we establish conditions permitting an O(n 3 .log n)-time transformation (also called a "many-one reduction" [START_REF] Ch | Computational Complexity[END_REF]) g from LF into L. If K4 ⊆ L, then g can be in O(n.log n)-time. Now, every primitive modal logic can be translated into FOL in linear-time (using a smart recycling of the variables). So in the general case, we define an O(n 3 .log n)-time transformation from LF into (possibly known) fragments of FOL even though a formula of second-order logic may be essential to describe the class of modal frames characterising LF. This provides an alternative for mechanizing modal provability logics.

Our uniform definition of such mappings shows that DL is ideal for prooftheoretical analyses of calculi for LF and L. In fact, the theoremhood preserving nature of our transformations are a characterisation of (weak) cut-elimination for many of these logics. Plan of the paper. In Section 2, we define the class of modal logics LF studied in the paper. In Section 3, we define display calculi δLF for these logics and show these calculi to be sound and complete. In Section 4, we give necessary and sufficient conditions to establish that the display calculi δLF admit a (weak) cut-elimination theorem, and provide the promised transformations. Section 5 contains a similar analysis for traditional sequent-style calculi. Proofs are omitted because of lack of space and they can be found in [START_REF] Demri | Theoremhood preserving maps as a characterisation of cut elimination for provability logics[END_REF].

Provability Logics

Given a set PRP = {p 1 , p 2 , . . .} of atomic formulae, the formulae φ ∈ FML are inductively defined as follows for p i ∈ PRP:

φ ::= ⊥ | | p i | φ 1 ∧ φ 2 | φ 1 ∨ φ 2 | ¬φ | φ 1 ⇒ φ 2 | 2φ
Standard abbreviations include ⇔, 3: for instance, 3φ def = ¬2¬φ. An occurrence of the subformula ψ in φ is positive [resp. negative] iff it is in the scope of an even [resp. odd] number of negations, where as usual, every occurrence of φ 1 ⇒ φ 2 is treated as an occurence of ¬φ 1 ∨ φ 2 . The standard axiomatic Hilbert system K consists of the axiom schemes 1. the tautologies of the Propositional Calculus (PC) 2. 2(p ⇒ q) ⇒ (2p ⇒ 2q) and the inference rules: modus ponens (from φ and φ ⇒ ψ infer ψ) and necessitation (from φ infer 2φ). When L is an extension of K (including K), we write φ ∈ L to denote that φ is a theorem of L. In the paper, we refer to the following well-known extensions L of K:

T def = K + 2p ⇒ p K4 def = K + 2p ⇒ 22p S4 def = K4 + 2p ⇒ p G def = K4 + 2(2p ⇒ p) ⇒ 2p Grz def = S4 + 2(2(p ⇒ 2p) ⇒ p) ⇒ 2p
Following [START_REF] Kracht | Power and weakness of the modal display calculus[END_REF], a formula is primitive iff it is of the form φ ⇒ ψ where both φ and ψ are built from PRP ∪ { } with the help of ∧, ∨, 3, and where φ contains each atomic proposition at most once.

Example 1. Neither of the formulae 2p ⇒ p and 2p ⇒ 22p are primitive, but their logically equivalent (in K) forms p ⇒ 3p and 33p ⇒ 3p are both primitive.

Definition 1. [START_REF] Kracht | Power and weakness of the modal display calculus[END_REF] A logic (defined via Hilbert system) L is properly displayable iff L is obtained from K by adding primitive formulae as axioms.

By Example 1, the logics T, K4 and S4 are properly displayable. In general, many of the traditional axioms for the most well-known modal logics are not primitive, but most of them have a primitive equivalent [START_REF] Kracht | Power and weakness of the modal display calculus[END_REF]. In [START_REF] Kracht | Power and weakness of the modal display calculus[END_REF], it is shown that every properly displayable logic admits a display calculus satisfying the conditions (C1)-(C8) [START_REF] Belnap | Display logic[END_REF] and therefore enjoys cut-elimination. In what follows, we write δL to denote the display calculus for L defined in [START_REF] Kracht | Power and weakness of the modal display calculus[END_REF].

A formula generation map F : FML → FML is an application such that there is a formula ψ F containing only one atomic proposition, say p, and no logical constants, such that for φ ∈ FML, F(φ) is obtained from ψ F by replacing every occurrence of p by φ. Moreover, we assume that no subformula of the form 2ϕ occurs negatively in ψ F . F is also written λp.ψ F . For any properly displayable logic L and any formula generation map F, we write LF to denote the logic obtained from L by addition of the scheme

2(F(p) ⇒ p) ⇒ 2p (1)
Observe that 2(F(q) ⇒ q) ⇒ 2q is not a Sahlqvist formula. This does not exclude the possibility to find a Sahlqvist formula logically equivalent (in the basic modal logic K) to it. For instance, this is the case when F(q) = ¬q since then, 2(F(q) ⇒ q)) ⇒ 2q is just 2q ⇒ 2q, and this has an equivalent primitive form ⇒ . Moreover, in numerous cases LF is not properly displayable. For instance, let F G and F Grz be λp.2p and λp.2(p ⇒ 2p) respectively. Then, by definition G = K4F G and Grz = S4F Grz . Since F G and F Grz are modal axioms that correspond to essentially second-order conditions on frames, the logics G and Grz are not properly displayable in the sense of Definition 1.

Display calculi

In this section, L is a properly displayable logic, F is a formula generation map and LF is the corresponding extension of L by the axiom scheme (1).

We briefly recall the main features of the calculus δL from [START_REF] Wansing | Sequent calculi for normal modal propositional logics[END_REF][START_REF] Kracht | Power and weakness of the modal display calculus[END_REF]. On the structural side, we have structural connectives * (unary), • (binary), I (nullary) and • (unary). A structure X ∈ struc(δL) is inductively defined as follows for φ ∈ FML:

X ::= φ | * X | X 1 • X 2 | I | •X
We assume that the unary connectives bind tighter than the binary ones. We use formula variables like φ, ψ, ϕ to stand for formulae, and use structure variables like X, Y and Z to stand for arbitrary structures from struc(δL).

A sequent is a pair of structures of the form X Y with X the antecedent and Y the succedent. The rules of δL are presented in Figures 1234. Additional structural rules satisfying conditions (C1)-(C8) are also needed but are omitted here since they depend on the primitive axioms defining L (see [START_REF] Kracht | Power and weakness of the modal display calculus[END_REF] for details).

(Id) p p (cut) X φ φ Y X Y

Fig. 1. Fundamental logical axioms and cut rule

The display postulates (reversible rules) in Figure 2 deal with the manipulation of structural connectives.

In any structure Z, the structure X occurs negatively [resp. positively] iff X occurs in the scope of an odd number [resp. an even number] of occurrences of * [START_REF] Belnap | Display logic[END_REF]. In a sequent Z Z , an occurrence of X is an antecedent part [resp.

succedent part] iff it occurs positively in

Z [resp. negatively in Z ] or it occurs negatively in Z [resp. positively in Z] [Bel82]
. Two sequents X Y and X Y are structurally equivalent iff there is a derivation of the first sequent from the second (and vice-versa) only using display postulates from Figure 2. To define the calculus δLF we need one additional notion. Let m be a map m : FML × {0, 1} → struc(δL) that transforms certain logical connectives into structural connectives, inductively defined as follows (i ∈ {0, 1}):

Theorem 2. ([Bel82]) For every sequent X Y and every antecedent [resp. succedent] part Z of X Y, there is a structurally equivalent sequent Z Y [resp. X Z] that has Z (alone) as its antecedent [resp. succedent]. Z is said to be displayed in Z Y [resp. X Z]. X • Y Z X Z • * Y X • Y Z Y * X • Z X Y • Z X • * Z Y X Y • Z * Y • X Z * X Y * Y X X * Y Y * X * * X Y X Y X * * Y X Y X •Y •X Y Fig. 2. Display postulates I ( ) I X X ( ) X I X ⊥ ( ⊥) ⊥ I (⊥ ) X • φ ψ X φ ⇒ ψ ( ⇒) X φ ψ Y φ ⇒ ψ * X • Y (⇒ ) X * φ X ¬φ ( ¬) * φ X ¬φ X (¬ ) X φ Y ψ X • Y φ ∧ ψ ( ∧) φ • ψ X φ ∧ ψ X (∧ ) X φ • ψ X φ ∨ ψ ( ∨) φ X ψ Y φ ∨ ψ X • Y (∨ ) φ X 2φ •X (2 ) X •φ X 2φ ( 2L)
m(p, i) def = p for any p ∈ PRP m( , i) def = m(⊥, i) def = ⊥ m(φ 1 ∨ φ 2 , 0) def = φ 1 ∨ φ 2 m(φ 1 ∨ φ 2 , 1) def = m(φ 1 , 1) • m(φ 2 , 1) m(φ 1 ∧ φ 2 , 0) def = m(φ 1 , 0) • m(φ 2 , 0) m(φ 1 ∧ φ 2 , 1) def = φ 1 ∧ φ 2 m(φ 1 ⇒ φ 2 , 0) def = φ 1 ⇒ φ 2 m(φ 1 ⇒ φ 2 , 1) def = * m(φ 1 , 0) • m(φ 2 , 1) m(2φ, i) def = 2φ m(¬φ, i) def = * m(φ, 1 -i).
The second argument of m indicates when the first argument is read as an antecedent part (i = 0) or as a succedent part (i = 1). The calculus δLF has the same structures as δL, and is obtained from δL by replacing the ( 2 L )-rule from Figure 3 by the ( 2 LF ) rule: The ( 2 LF )-rules for δGrz and δG are respectively:

X •( * m(F(φ), 0) • φ) X 2φ ( 2 LF ) X Z I • X Z (I l ) X Z X I • Z (Ir) I Y * I Y (Q l ) X I X * I (Qr) X Z Y • X Z (weak l ) X Z X • Y Z (weakr) I X •I X (nec l ) X I X •I (nec r ) X1 • (X2 • X3) Z (X1 • X2) • X3 Z (assoc l ) Z X1 • (X2 • X3) Z (X1 • X2) • X3 (assocr) Y • X Z X • Y Z (com l ) Z Y • X Z X • Y (comr) X • X Y X Y (contr l ) Y X • X Y X (contrr)
X •( * 2(φ ⇒ 2φ) • φ) X 2φ ( 2 Grz ) X •( * 2φ • φ) X 2φ ( 2 G )
The calculus δLF satisfies conditions (C2)-(C7). In particular, δG satisfies the conditions (C1)-(C7). The ( 2 G )-rule in δG is similar to the GLR rule in [START_REF] Sambin | The modal logic of provability . The sequential approach[END_REF] (see also [START_REF] Avron | On modal systems having arithmetical interpretations[END_REF]). Analogously, the ( 2 Grz )-rule in δGrz is similar to the (GRZc) rule in [START_REF] Borga | On the proof theory of the modal logic Grz[END_REF] or to the (⇒ 2) rule in [START_REF] Avron | On modal systems having arithmetical interpretations[END_REF]. An intuitively obvious way to understand the ( 2 LF )-rule is to recall the double nature of the 2-formulae in LF as illustrated by the LF-theorem 2φ ⇔ 2(F(φ) ⇒ φ).

We use the label (dp) as shown below left to denote that the sequent s is obtained from the sequent s by an unspecified finite number (possibly zero) of display postulate applications from Figure 2. The ( 2 L )-rule from δL is derivable in δLF as shown below right:

s s (dp) X •φ •X φ (dp) m(F(φ), 0) • •X φ (weak l ) X •( * m(F(φ), 0) • φ) (dp) X 2φ ( 2 LF )
To prove soundness of δLF with respect to LF-theoremhood, we use the mappings a : struc(δL) → FML and s : struc(δL) → FML recalled below:

a(φ) def = s(φ) def = φ for any φ ∈ FML a(I) def = s(I) def = ⊥ a( * X) def = ¬s(X) s( * X) def = ¬a(X) a(X • Y) def = a(X) ∧ a(Y) s(X • Y) def = s(X) ∨ s(Y) a(•X) def = 3 -a(X) s(•X) def = 2s(X)
The modality 3 -is the backward existential modality associated with 2. That is, as is usual with DL, we extend the language by adding the unary modal operator 2 -. We write L + [resp. L + F] to denote the extension of L [resp. LF] obtained by adding the axiom schemes 2 -p ⇒ (2 -(p ⇒ q) ⇒ 2 -q), q ⇒ 23 -q, q ⇒ 2 -3q and the necessitation rule: from φ infer 2 -φ. The language is extended appropriately by adding 2 -, and 3 -φ is defined as ¬2 -¬φ.

Theorem 4. If X Y is derivable in δLF, then a(X) ⇒ s(Y) ∈ L + F.
The maps a and s can be found for instance in [START_REF] Kracht | Power and weakness of the modal display calculus[END_REF] where they are called τ 1 and τ 2 respectively. The maps a and s give an intuitive way to interpret the meaning of the structural connectives depending on the polarity of their occurrence (either as antecedent part or as succedent part).

Lemma 5. The following rules are admissible in δLF:

X φ 1 ∨ φ 2 X φ 1 • φ 2 ( •) X φ 1 ⇒ φ 2 X * φ 1 • φ 2 (adm1) φ 1 ∧ φ 2 X φ 1 • φ 2 X (• ) X ¬φ X * φ ( * ) F(φ) X m(F(φ), 0) X (adm2) ¬φ X * φ X ( * )
Moreover, for each of these rules, if the premiss has a cut-free proof in δLF, then the conclusion also has a cut-free proof in δLF.

The proof of admissibility of the rules ( •), (adm1), (• ), ( * ) and ( * ) is similar to [Kra96, Lemma 9]. Admissibility of (adm2) is a mere consequence of the admissibility of the above rules. Lemma 6. φ φ is cut-free derivable in δLF for any formula φ.

Lemma 6 requires induction on the formation of φ. Theorem 7 is the DL version of Theorem 1 in [START_REF] Avron | On modal systems having arithmetical interpretations[END_REF] for Gentzen-style calculi.

Theorem 7. A formula φ ∈ LF iff I φ is derivable in δLF.

Proof. The right to left direction is just an instance of Theorem 4. The left to right direction requires uses of the cut rule (to simulate the application of the modus ponens rule) and proceeds by induction on the length of the derivation in LF (viewed as an Hilbert-style system). Most of the cases can be found in [START_REF] Wansing | Sequent calculi for normal modal propositional logics[END_REF][START_REF] Kracht | Power and weakness of the modal display calculus[END_REF][START_REF] Wansing | Displaying Modal Logic, volume 3 of Trends in Logic[END_REF]. It remains to show that I 2(F(φ) ⇒ φ) ⇒ 2φ has a proof in δLF which is done below using the fact that F(φ) F(φ) and φ φ are derivable in δLF by Lemma 6:

φ φ F(φ) F(φ) m(F(φ), 0) F(φ) (adm2)
F(φ) ⇒ φ * m(F(φ), 0) • φ (⇒ ) 2(F(φ) ⇒ φ) •( * m(F(φ), 0) • φ) (2 ) 2(F(φ) ⇒ φ) 2φ ( 2 LF ) I • 2(F(φ) ⇒ φ) 2φ (I l ) I 2(F(φ) ⇒ φ) ⇒ 2φ ( ⇒)
As stated previously, any display calculus satisfying the conditions (C2)-(C8) from [START_REF] Belnap | Display logic[END_REF] admits cut-elimination. Unfortunately δLF does not satisfy (C8) (see the appendix).

Specifically, the cut instance below breaks (C8):

X •( * m(F(φ), 0) • φ) X 2φ ( 2 LF ) φ Y 2φ •Y (2 ) X •Y (cut)
where there is a formula ψ in m(F(φ), 0) that is not a subformula of φ. For instance, such cases are easy to find with the display calculi δG and δGrz. Furthermore, in order to infer X •Y from X •( * m(F(φ), 0) • φ) and φ Y, no cut can be used on ψ if (C8) has to be satisfied. In the display calculus δLF, for all the derivations of the sequent X Y from X •( * m(F(φ), 0) • φ), if a cut with a cut-formula that is not a subformula of φ is forbidden, then either X Y contains ψ as the subformula of some formula/structure (see the introduction rules different from ( 2 LF )), or X Y contains 2φ as the subformula of some formula/structure (see the ( 2 LF )-rule). So, in the general case, there is no way to derive X •Y since neither ψ nor 2φ are guaranteed to occur in it.

We say that LF is pseudo displayable iff for any φ ∈ FML, I φ has a proof in δLF iff I φ has a cut-free proof in δLF. "Pseudo" because strong cut-elimination is couched in terms of arbitrary sequents X Y rather than sequents of the form I φ. For mechanisation "pseudo" is sufficient for our needs since we want to check whether φ ∈ LF. We now provide a characterisation of the class of pseudo displayable logics and show that both G and Grz are pseudo displayable.

Transformations from LF into L

In this section, L is a properly displayable logic and F is a formula generation map. Let f : FML × {0, 1} → FML be the following map for i ∈ {0, 1}:

for any p ∈ PRP, f (p, 0) def = f (p, 1) def = p f ( , i) def = f (⊥, i) def =⊥ f (φ 1 ⊕ φ 2 , i) def = f (φ 1 , i) ⊕ f (φ 2 , i) for ⊕ ∈ {∧, ∨} f (¬φ, 0) def = ¬f (φ, 1) f (¬φ, 1) def = ¬f (φ, 0) f (φ 1 ⇒ φ 2 , 1) def = f (φ 1 , 0) ⇒ f (φ 2 , 1) f (φ 1 ⇒ φ 2 , 0) def = f (φ 1 , 1) ⇒ f (φ 2 , 0) f (2φ, 1) def = 2(f (F(φ), 0) ⇒ f (φ, 1)) f (2φ, 0) def = 2f (φ, 0)
In f (φ, i), the index i carries information about the polarity of φ in the translation process as in [START_REF] Ph | A translation from the modal logic of provability into K4[END_REF]. The map f also generalises one of the maps from G into K4 defined in [START_REF] Ph | A translation from the modal logic of provability into K4[END_REF]. By simultaneous induction one can show that for any φ ∈ FML and for any i ∈ {0, 1}, φ ⇔ f (φ, i) ∈ LF. Moreover, for any φ ∈ FML:

f (φ, 0) ⇒ φ ∈ L, φ ⇒ f (φ, 1) ∈ L and therefore f (φ, 0) ⇒ f (φ, 1) ∈ L. Lemma 8. Every positive [resp. negative] occurrence of 1. 2ψ in f (φ, 1) is of the form 2(f (F(ϕ), 0) ⇒ f (ϕ, 1)) [resp.
2f (ϕ, 0)] for some subformula ϕ of φ;

2. ¬ψ in f (φ, 1) is of the form ¬f (ϕ, 0) [resp. ¬f (ϕ, 1)] for some subformula ϕ of φ; 3.

ψ 1 ⇒ ψ 2 in f (φ, 1) is of the form f (ϕ 1 , 0) ⇒ f (ϕ 2 , 1) [resp. f (ϕ 1 , 1) ⇒ f (ϕ 2 , 0)] for some subformulae ϕ 1 , ϕ 2 of φ; 4. ψ 1 ⊕ ψ 2 (⊕ ∈ {∧, ∨}) in f (φ, 1) is of the form f (ϕ 1 , 1) ⊕ f (ϕ 2 , 1) [resp. f (ϕ 1 , 0) ⊕ f (ϕ 2 , 0)] for some subformulae ϕ 1 , ϕ 2 of φ;
The proof of Lemma 8 is by an easy verification. Lemma 8 is used in the proof of Theorem 9 below. We extend the map f to structures in the following way (i ∈ {0, 1}):

f (I, i) def = I f ( * X, i) def = * f (X, 1 -i) f (X • Y, i) def = f (X, i) • f (Y, i) f (•X, i) def = •f (X, i)
By induction on the structure of φ, the rule below is admissible in δL:

f (m(φ, 0), 0) X f (φ, 0) X (adm3)
Theorem 9 below is the main result of the paper.

Theorem 9. The statements below are equivalent:

1. For all formulae φ, φ

∈ LF iff f (φ, 1) ∈ L. 2. LF is pseudo displayable.
That is, (weak) cut-elimination of δLF is equivalent to the theoremhood preserving nature of f from LF into L. Its proof is purely syntactic and therefore it does not depend on the class of modal frames that possibly characterises LF. Moreover, Theorem 9 goes beyond the mechanisation aspect since it provides a characterisation of the class of pseudo displayable logics which is not directly based on a cut-elimination procedure.

The proof of Theorem 9 is long and tedious. For instance, when (2) holds and φ ∈ LF, to show that f (φ, 1) ∈ L, we show that in any cut-free proof Π of I φ in δLF, for any sequent X Y in Π, f (X, 0) f (Y, 1) has a cut-free proof in δL. By way of example, the proof step (in δLF) shown below left is transformed into the proof steps (in δL) shown below right:

X •( * m(F(ψ), 0) • ψ) X 2ψ ( 2 LF ) f (X, 0) •( * f (m(F(ψ), 0), 0) • f (ψ, 1)) •f (X, 0) * f (m(F(ψ), 0), 0) • f (ψ, 1) (dp) •f (X, 0) f (ψ, 1) • * f (m(F(ψ), 0), 0) (com r ) f (m(F(ψ), 0), 0) * • f (X, 0) • f (ψ, 1) (dp) f (F(ψ), 0) * • f (X, 0) • f (ψ, 1) (adm3) •f (X, 0) • f (F(ψ), 0) f (ψ, 1) (dp) •f (X, 0) f (F(ψ), 0) ⇒ f (ψ, 1) ( ⇒) f (X, 0) •(f (F(ψ), 0) ⇒ f (ψ, 1)) (dp) f (X, 0) 2(f (F(ψ), 0) ⇒ f (ψ, 1)) ( 2 L ) f -1 (I, i) def = I f -1 ( , i) def = f -1 (⊥, i) def =⊥ f -1 (X • Y, i) def = f -1 (X, i) • f -1 (Y, i) or undefined f -1 (•X, i) def = •f -1 (X, i) or undefined f -1 ( * X, 1 -i) def = * f -1 (X, i) or undefined f -1 (p, i) def = p for any p ∈ PRP for ⊕ ∈ {∧, ∨}, f -1 (φ ⊕ ψ, i) def = f -1 (φ, i) ⊕ f -1 (ψ, i) or undefined f -1 (φ ⇒ ψ, 1) def = f -1 (φ, 0) ⇒ f -1 (ψ, 1) or undefined f -1 (φ ⇒ ψ, 0) def = f -1 (φ, 1) ⇒ f -1 (ψ, 0) or undefined f -1 (¬φ, 1 -i) def = ¬f -1 (φ, i) or undefined f -1 (2φ, 0) def = 2f -1 (φ, 0) or undefined f -1 (2φ, 1) def = 2f -1 (φ2, 1) if φ = (φ1 ⇒ φ2) and f -1 (φ2, 1) is defined undefined otherwise
where "x def = y or undefined" means:

x def =
y if all components of y are defined undefined otherwise Fig. 5. Definition of f -1 (.) for i ∈ {0, 1}.

When (1) holds, f (φ, 1) ∈ L implies I f (φ, 1) has a cut-free proof Π in δL, and φ ∈ LF implies I φ is provable in δLF. To show that I φ has a cut-free proof in δLF, we prove that for every sequent X Y in Π, the sequent f -1 (X, 0) f -1 (Y, 1) admits a cut-free proof in δLF with the partial function f -1 defined in Figure 5. Since δL satisfies (C1)-(C8) (see the appendix), for every sequent X Y in Π, both f -1 (X, 0) and f -1 (Y, 1) are defined (Lemma 8 is also used to show this property). Because the map f -1 : struc(δL) × {0, 1} → struc(δL) satisfies f -1 (f (φ, 1), 1) = φ and f -1 (f (φ, 0), 0) = φ, the end-sequent I f (φ, 1) of Π becomes I φ in this procedure, as desired.

The proof of Theorem 9 actually shows that DL is particularly well-designed to reason about polarity, succedent and antecedent parts. One of the translations from G into K4 in [START_REF] Ph | A translation from the modal logic of provability into K4[END_REF] is exactly the map f when L is K4 and F is F G .

Corollary 10. G is pseudo displayable.

Let δ -G be the calculus δG minus the cut-rule. Thus δ -G satisfies all the conditions (C1)-(C8) and for any φ ∈ FML, φ ∈ G iff I φ has a proof in δ -G. At first glance, this seems to contradict the fact that G is not properly displayable in the sense of [START_REF] Kracht | Power and weakness of the modal display calculus[END_REF]. However, in [START_REF] Kracht | Power and weakness of the modal display calculus[END_REF], all the axioms added to K are transformed into structural rules. By contrast, in δ -G, one of the axioms is encoded in the ( 2 G )-rule. This opens an avenue to define display calculi satisfying (C1)-(C8) for modal logics that are not properly displayable.

Theorem 11. For every pseudo displayable logic LF, there is an O(n 3 .log n)time transformation g such that any φ ∈ LF iff g(φ) ∈ L.

Form of φi ψi

( md(φ) i=0 2 i (pi,1 ⇔ ) ∧ 2 i (pi,0 ⇔ )) ⊥ ( md(φ) i=0 2 i (pi,1 ⇔⊥) ∧ 2 i (pi,0 ⇔⊥)) p ( md(φ) i=0 2 i (pi,0 ⇔ pi,1)) ¬φj ( md(φ) i=0 2 i (pi,1 ⇔ ¬pj,0) ∧ 2 i (pi,0 ⇔ ¬pj,1)) φi 1 ∧ φi 2 ( md(φ) i=0 2 i (pi,1 ⇔ (pi 1 ,1 ∧ pi 2 ,1)) ∧ 2 i (pi,0 ⇔ (pi 1 ,0 ∧ pi 2 ,0))) φi 1 ∨ φi 2 ( md(φ) i=0 2 i (pi,1 ⇔ (pi 1 ,1 ∨ pi 2 ,1)) ∧ 2 i (pi,0 ⇔ (pi 1 ,0 ∨ pi 2 ,0))) φi 1 ⇒ φi 2 ( md(φ) i=0 2 i (pi,1 ⇔ (pi 1 ,0 ⇒ pi 2 ,1)) ∧ 2(pi,0 ⇔ (pi 1 ,1 ⇒ pi 2 ,0))) 2φj ( md(φ) i=0 2 i (pi,1 ⇔ 2(F (pj,0, pj,1) ⇒ pj,1)) ∧ 2 i (pi,0 ⇔ 2pj,0)) Fig. 6. Definition of ψi
The right-hand side of the definition of f (2ψ, 1) may require several calls to f (ψ, 0) and f (ψ, 1), so f is not necessarily computable in O(n 3 .log n)-time. However, we can use a variant of f using a standard renaming technique (see e.g. [START_REF] Mints | Gentzen-type and resolution rules part I: propositional logic[END_REF]). Let md(φ) denote the modal depth of φ, let 2 0 ϕ def = ϕ and 2 i+1 ϕ def = 22 i ϕ. Then for any extension

L of K, φ ∈ L iff ( md(φ) i=0 2 i (p new ⇔ ψ)) ⇒ φ ∈ L
where φ is obtained by replacing every occurrence of ψ in φ by p new , a new propositional variable not occurring in φ.

When K4 ⊆ L, φ ∈ L iff (2(p new ⇔ ψ) ∧ (p new ⇔ ψ)) ⇒ φ ∈ L.
Proof. (Theorem 11) The key point to define g is to observe that there is a map F : FML × FML → FML and a formula ψ F containing at most two atomic propositions, say p and q, such that -F (ϕ 1 , ϕ 2 ) is obtained from ψ F by replacing simultaneously every occurrence of p [resp. q] by ϕ 1 [resp. ϕ 2 ]; for any ϕ ∈ FML, f (F(ϕ), 0) = F (f (ϕ, 0), f (ϕ, 1)).

For instance, if F = λp.p ∧ ¬p then F = λpq.p ∧ ¬q.

Let φ be a modal formula we wish to translate from LF into L. Let φ 1 , . . . , φ m be an enumeration (without repetition) of all subformulae of φ, in increasing order of size. We shall build a formula g(φ) using the set {p i,j : 1 ≤ i ≤ m, j ∈ {0, 1}} of atomic propositions such that g(φ) ∈ L iff f (φ, 1) ∈ L. We could also just consider the set {p i : i ∈ ω} of atomic propositions and use a 1-1 mapping from ω 2 → ω, but for simplicity, the present option is the most convenient.

Moreover, g(φ) can be computed in time O(|φ| 3 .log |φ|). For i ∈ {1, . . . , m}, we create a formula ψ i as shown in Figure 6 andlet g

(φ) def = ( m i=1 ψ i ) ⇒ p m,1 . If K4 ⊆ L, the generalised conjunction in Figure 6 is needed only for i ∈ {0, 1}. Each |ψ i | is in O(|φ| 2 ) since Σ md(φ) i=0 i is in O(|φ| 2 ). So |g(φ)| is in O(|φ| × (|φ| 2 × log |φ|)).
As usual in complexity theory, the extra log |φ| factor in the size of φ is because we need an index of size O(log |φ|) for these different atomic propositions. That is, these indices are represented in binary writing.

The map g is a generalisation of the map from Grz into S4 defined in [START_REF] Demri | An O((n.log n) 3 )-time transformation from Grz into decidable fragments of classical first-order logic[END_REF]. One of the maps from G into K4 in [START_REF] Ph | A translation from the modal logic of provability into K4[END_REF] is linear-time and does not use renaming (which allows us to treat the general case). We are currently investigating if their map can be generalised by considering the map f : FML × {0, 1} → FML inductively defined as f except that f (2φ, 1) def = 2(F(φ) ⇒ f (φ, 1)). Another map in P from G into K4 is given in [Fit83, Chapter 5].

Another characterisation

Theorem 9 has a counterpart when LF has a traditional Gentzen system although additional conditions are required. In this section, L is a properly displayable logic and F is a formula generation map.

Definition 12. Assume L, properly displayable by assumption, has a traditional Gentzen system GL in which 1. GL extends a standard Gentzen system for PC containing contraction, weakening, exchange and cut (shown below left), and GL satisfies cut-elimination; 2. any sequent Γ ∆ is derivable in GL iff ( φ∈Γ φ) ⇒ ( φ∈∆ φ) ∈ L; 3. the (2 )-rule (if any) and the ( 2)-rule have the form

Γ, φ ∆ Γ, 2φ ∆ (2 ) Σ φ Σ 2φ ( 2)
where there is a map h : FML → FML such that h(Σ) = Σ , h(f (Σ, 0)) = f (Σ , 0) for any sequence Σ to which the ( 2)-rule is applicable. Both h and f (defined via F) are naturally extended to sequences. Moreover, f (Σ, 0) satisfies any further conditions on the ( 2)-rule iff Σ does too: for example, that Σ must contain only formulae beginning with 2.

These sequents consist of comma-separated lists of formulae. Then, LF is pseudo Gentzenisable iff the Gentzen system GLF obtained from GL by replacing the ( 2)-rule by ( 2 LF ) shown below right enjoys cut-elimination.

Γ φ, ∆ Γ , φ ∆ Γ, Γ ∆, ∆ (cut) F(φ), Σ φ Σ 2φ

( 2 LF ) Definition 12(3.) ensures that (C4) is satisfied when the structures are simply sequences of formulae. Following [Avr84, Theorem 1], we can show that GLF is sound and complete for LF. Here is the Gentzen counterpart of Theorem 9.

Theorem 13. If L satisfies assumptions (1)-(3) from Definition 12 then the statements below are equivalent:

1. For all φ ∈ FML, φ ∈ LF iff f (φ, 1) ∈ L.

2. LF is pseudo Gentzenisable.

By [Avr84, Corollary 3.1], Grz is pseudo Gentzenisable and therefore Grz is pseudo displayable. So by Theorem 13, for any φ ∈ FML, φ ∈ Grz iff f (φ, 1) ∈ S4 where f is defined with F = F Grz . See [START_REF] Demri | An O((n.log n) 3 )-time transformation from Grz into decidable fragments of classical first-order logic[END_REF] for a more detailed case-study showing how to translate Grz into a decidable subset of first-order logic.

Concluding remarks

We can summarise the general situation as follows: an O(n.log n)-time] transformation from LF into L.

Our contribution can be summarised as follows:

1. Automated Reasoning: We gave a uniform framework to translate every pseudo-displayable modal logic LF, which may not be first-order definable, into the first-order definable primitive modal logic L. The transformations are at most in O(n 3 .log n)-time. Since a linear-time transformation from each L into FOL is known, we can use classical theorem provers for any pseudo-displayable logic LF. 2. Cut-elimination: (Often a desirable property for mechanisation) Although the calculi δLF do not satisfy condition (C8), we can nevertheless characterise weak cut-elimination by the theoremhood preserving nature of f . 3. Display Logic: We defined DL calculi for logics that are not properly displayable à la [START_REF] Kracht | Power and weakness of the modal display calculus[END_REF].

Fig. 3 .

 3 Fig. 3. Operational rules

Fig. 4 .

 4 Fig. 4. Other basic structural rules

Theorem 14 .

 14 Assume logic L is properly displayable and F is a formula generation map. Then, (I) (a) LF is pseudo displayable iff (b) for all φ ∈ FML, φ ∈ LF iff f (φ, 1) ∈ L (where f is defined via F). (II) If L satisfies the assumptions (1)-(3) from Definition 12, then (b) holds iff LF is pseudo Gentzenisable. (III) When (a) holds [resp. and when K4 ⊆ L], there is an O(n 3 .log n)-time [resp.

Visit to ARP supported by an Australian Research Council International Fellowship. Supported by an Australian Research Council Queen Elizabeth II Fellowship.

Appendix: Belnap's Conditions.

For every sequent rule Belnap [START_REF] Belnap | Display logic[END_REF]page 388] first defines the following notions: in an application Inf of a sequent rule (ρ), "constituents occurring as part of occurrences of structures assigned to structure-variables are defined to be parameters of Inf ; all other constituents are defined as nonparametric, including those assigned to formula-variables. Constituents occupying similar positions in occurrences of structures assigned to the same structure-variable are defined as congruent in Inf ". The eight (actually seven) conditions shown below are from [START_REF] Kracht | Power and weakness of the modal display calculus[END_REF] and [START_REF] Wansing | Displaying Modal Logic, volume 3 of Trends in Logic[END_REF]: (C1) Each formula which is a constituent of some premiss of a rule ρ is a subformula of some formula in the conclusion of ρ. (C2) Congruent parameters are occurrences of the same structure. (C3) Each parameter is congruent to at most one constituent in the conclusion.

Equivalently, no two constituents of the conclusion are congruent to each other. (C4) Congruent parameters are either all antecedent parts or all succedent parts of their respective sequent. (C5) If a formula is non-parametric in the conclusion of a rule ρ, it is either the entire antecedent, or the entire succedent. Such a formula is called a principal formula. (C6/7) Each rule is closed under simultaneous substitution of arbitrary structures for congruent parameters. (C8) If there are inferences I 1 and I 2 with respective conclusions X ϕ and ϕ Y with ϕ principal in both inferences, and if cut is applied to obtain X Y, then (i) either X Y is identical to one of X ϕ and ϕ Y;

(ii) or there is derivation of X Y from the premisses of I 1 and I 2 in which every cut-formula of any application of cut is a proper subformula of ϕ.

This article was processed using the L A T E X macro package with LLNCS style


Tobias Maletzky
email: t.maletzky@gmx.de

Kazuo Tanaka

Thierry Grosjean
email: thierry.grosjean@univ-fcomte.fr

Ulrich C Fischer
email: fischeu@uni-muenster.de

Leaky waveguide modes along the edge of a dielectric wedge

It is shown experimentally that a Gaussian beam focused from within a finite wedge onto its edge at an angle of total reflection excites a leaky waveguide mode propagating along the edge. This newly described phenomenon is interpreted in terms of waveguide modes of a tapered dielectric slab of a mode index, which is known to decrease with slab thickness. This decrease in the refractive index leads to a gradual refraction of the incident beam parallel to the edge. A numerical simulation of a focused Gaussian beam incident on a finite dielectric wedge gives a full account of this phenomenon.

We consider a beam of light incident on a dielectric wedge structure at an oblique angle with respect to the edge of the wedge as shown schematically in Fig. 1. For a plane wave incident on an infinitely extended wedge at an angle of incidence with respect to the edge, which is larger than the critical angle of total reflection of the dielectric material, the plane wave will be totally reflected in the wedge structure. For a focused Gaussian beam of a finite cross section, a similar phenomenon may be expected as the well known Goos-Hänchen shift [1], which occurs for the total reflection of a Gaussian beam at a dielectric interface. The underlying phenomenon to the Goos-Hänchen shift is the so-called lateral wave, which can be considered as a leaky surface mode at the dielectric-air interface. It is shown here that a focused Gaussian beam incident on a finite dielectric wedge at an angle of total reflection is gradually deflected to be eventually aligned parallel to the edge. This phenomenon can be understood qualitatively in terms of a model of the wedge as a tapered slab with an effective refractive index decreasing with slab thickness [2] as a gradual refraction of the incident beam parallel to the edge. In the experimental part we present evidence for the leaky waveguide modes by observing light emission from the tip of a finite wedge (see Fig. 1) for a condition where a Gaussian beam is focused into the wedge at a location remote from the tip. Finally, numerical calculations simulate a Gaussian beam incident on the wedge.

The experimental configuration is shown in Fig. 2. As a wedge structure with an edge with a radius of curvature of the order of 5 nm [3], we use a glass fragment, which is formed by the cleaving of a piece of cover glass twice at a right angle [4]. The fragment is mounted on a prism serving to couple light into the tip. A twin microscope is used for the excitation and the observation of the leaky waveguide mode. A white-light source illuminates a circular iris dia-phragm. A demagnified image of the diaphragm is projected into the wedge, which is in focus at the edge. The beam, which is reflected from the edge, is reflected from the interface of the glass fragment opposite to the edge, and a magnified image of the edge is formed in the image plane, which is detected by a CCD camera. The NA of the incident beam and the angle of incidence of the beam can be adjusted by an adjustable iris diaphragm in the diffraction plane of the illumination pathway. With the second microscope, an image of the tip or the edge is formed from the outside of the wedge.

The experimental results are shown in Fig. 3. Figure 3(a) shows the reflected image of the edge for conditions of total reflection of the incident beam. The NA of the illuminating beam was adjusted such that the beam was totally reflected in the wedge and no light was emitted from the edge to the outside [Fig. 3(d)]. Figure 3(b) shows the light emitted from the edge as observed with the upper microscope when it is focused on the edge and when the incident beam has a large NA such that parts of the incident beam with a high NA are not totally reflected and lead to radiation from the edge. Light emission from the edge is clearly observed. Adjusting the focus such that the tip is in focus, a blurred image of the emission from the edge is observed and, additionally, somewhat separated from the emission from the edge, a weak emission from the tip is seen [Fig. 3(c)]. The NA was then decreased by reducing the diameter of the iris diaphragm in the illumination pathway until the radiative emission of the edge disappeared, but the emission from the tip still prevails [Fig. 3(d)]. This was also the condition for recording Figs. 3(a) and 3(e). In Fig. 3(e) the structure of the tip is visible by an additional weak delocalized background illumination. The arrangement of the tip is indicated in Fig. 3(f). These results can be interpreted by a leaky waveguide mode propagating parallel to the edge. This leaky waveguide mode is optically excited in the wedge structure by the Gaussian beam incident onto the edge at an angle of total reflection, which is directed into the wedge at a location remote from the tip. At the tip apex the waveguide mode leads to a ray being emitted from the end face of the wedge structure and to a scattering from the tip apex.

Waveguide modes in a dielectric wedge are interpreted in terms of waveguide modes in an adiabatically tapered dielectric slab as a function of its thickness [2]. Figure 4 shows the dispersion relations of slab waveguide modes as a function of slab thickness. For all modes the wavenumber decreases with decreasing thickness of the slab. This property can be described by an effective refractive index of the waveguide mode decreasing with decreasing slab thickness. We assume that in a wedge a waveguide mode exists at a certain height above its edge, which corresponds to the waveguide mode of a slab of a thickness corresponding to the width of the wedge at the given height. For a beam incident at an oblique angle into the wedge, the dispersion relations of Fig. 5 imply that the effective refractive index of the waveguide modes will continuously decrease as the beam penetrates into the wedge. This gradual decrease in the refractive index will lead to a gradual refraction and inclination of the incoming beam parallel to the edge. A similar phenomenon was discussed for an s-polarized surface plasmon mode in a metal-coated dielectric wedge [5]. There the effective refractive index increases with decreasing width within the edge. Fig. 2. Experimental configuration for the observation of a leaky waveguide mode in a wedge structure. A triangular glass fragment serves as a wedge structure. It is attached to a prism such that a focused beam of light can be injected into the edge of the wedge by using a microscope. The beam reflected from the edge is observed by a CCD1 camera. The CCD2 camera attached to a second microscope is used to detect light, which is emitted from the tip of the wedge. Fig. 3. Experimental observations. The white bars correspond to a 10 m (a) image of the reflected beam as recorded by CCD1 (see Fig. 2). To localize the focused spot in the tip structure, the tip was additionally illuminated by a weak nonlocal background illumination. (b) Image of the edge slightly displaced from the tip as recorded with CCD camera 2 (Fig. 2) showing light emission from the edge, which was illuminated by a high NA by adjusting iris diaphragm 2 (Fig. 2). (c) The same as (b) but with the tip in focus such that a blurred image of light emission from the edge and a weak emission from the tip is observed. (d) Image of the tip as in (b) but with a small NA of the illuminating beam such that no emission from the edge occurs. Only the emission from the tip is seen. The same NA of the exciting beam was chosen for image (a) of the reflected beam. (e) The same as (d) but with additional background illumination. (e) Schematic view of the orientation of the tip in the images.

Therefore the incoming beam is refracted toward the normal to the edge just opposite to the case of the dielectric wedge. For a p-polarized surface-plasmon mode, a very similar behavior is however expected as for the case of the purely dielectric wedge [6]. Figure 5 shows the result of numerical calculations by a volume integral equation method [6][7][8]o fx-and y-polarized Gaussian beams incident on a finite wedge at an angle of total reflection of 45°with respect to the edge of the wedge. A standing wave phenomenon is seen parallel to the edge and emission of light at the tip. These numerical results give a detailed description of our experimental results.

Our results may be of interest for the development of sensors based on leaky wedge waveguide modes [9,10]. A wedge configuration would allow for a higher confinement of the sensing area than a planar configuration. The results are also of interest in the process of superfocusing in a metal-coated dielectric wedge by dimensional reduction in surface to edge plasmon modes as discussed recently [6]. Leaky waveguide modes as described here provide an efficient channel for the excitation of surface and edge plasmon modes in a metal-coated wedge as will be described explicitly in a forthcoming publication.

Fig. 1 .

 1 Fig. 1. Schematic view of a beam of light incident at an angle of total reflection onto the edge of a finite wedge, which ends at a tip.

Fig. 4 .

 4 Fig. 4. (Color online) Dispersion relations as a function of the thickness of a dielectric slab for different symmetric and antisymmetric transverse electric (TE) and transverse magnetic (TM) modes for a vacuum wavelength of 630 nm showing a decrease in the wave vector k z with decreasing thickness of the slab in all cases.

Fig. 5 .

 5 Fig. 5. Numerical results of the intensity of the electric field ͉E 2 ͉ in a dielectric tip of / 0 = 2.25 surrounded by vacuum with permittivity 0 and of dimensions B x = 6.1 and B y = 8.15, where is the vacuum wavelength. The spot size is 0.8, the intensity is unity at z = 0, and the beam axis is in the x-z plane parallel to the z axis but displaced from it by a distance d = 1.42. The field intensity is shown for a section at y =0.

This work was supported by the German Science Foundation (DFG) (contract Fi:608/5-1) and by the Network of Excellence Plasmo-Nano-Devices in the FP6 IST program of the European Community.


John M Dudley

Goëry Genty

Frederic Dias

Bertrand Kibler

Nail Akhmediev

Modulation instability

Keywords: Akhmediev breathers, and "rogue waves" in nonlinear fiber optics Solitons, nonlinear optics, supercontinuum generation, photonic crystal fiber, rogue waves

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

INTRODUCTION

There is currently a great deal of interest in the characteristics of extreme-value fluctuations in optical fibre supercontinuum (SC) generation [X1 -3]. In particular, although many aspects of fibre SC generation are now wellunderstood [START_REF]Nonlinear Fiber Optics[END_REF][START_REF] Dudley | Supercontinuum Generation in Photonic Crystal Fiber[END_REF] these recent results have shown how noise-induced fluctuations in the long pulse quasi-CW regime can modify the dynamics so as to lead to very rare cases where high amplitude "optical rogue waves" are generated. A central challenge in understanding these rare events is of course to develop rigorous models linking the complex generation dynamics and the associated statistical behavior. In this regard, although the initial description of optical rogue waves was applied to rare high amplitude soliton pulses generated on the long-wavelength edge of a broadband fibre SC spectrum, there has recently been an improved understanding that a more likely analogy with the oceanic case is to be found in the onset phase of supercontinuum generation when coherent breather structures begin to emerge [START_REF] Akhmediev | Waves that appear from nowhere and disappear without a trace[END_REF][START_REF] Akhmediev | Extreme waves that appear from nowhere: On the nature of rogue waves[END_REF].

Significantly, it has also recently been realised that the spectral characteristics seen in this emergent SC regime can be described using powerful analytic techniques [8]. In fact, despite intensive research over three decades, there are surprisingly-few analytic solutions describing nonlinear pulse evolution in optical fibers. Certainly there are exceptions such as the well-known soliton and self-similar solutions [START_REF] Dudley | Self Similarity in Ultrafast Nonlinear Optics[END_REF], but complex processes such as supercontinuum generation have generally been considered to require numerical approaches. In this paper, however, we summarize recent results that have shown that an analytic theory of "Akhmediev Breather" (AB) propagation [START_REF] Dudley | Modulation instability, Akhmediev Breathers and continuous wave supercontinuum generation[END_REF] can be successfully applied to quantitatively explain the form of the developing SC spectrum under long-pulse excitation conditions. We show that the AB theory provides new insight into the properties of the initial broadening and nonlinear spectral transformation of CW supercontinuum generation seeded by noise. We discuss how the temporal structure that develops from spontaneous modulation instability (MI) can be naturally interpreted in terms of the characteristics of AB evolution, and we show how the frequency-domain properties of the maximally-compressed AB solution reproduce the characteristic triangular shape of the MI spectrum when plotted on a semi-logarithmic scale. Numerical and analytic results are confirmed by experimental studies of quasi-CW spectral broadening induced by nanosecond pulse pumping in the anomalous dispersion regime of a photonic crystal fiber (PCF). Finally, we present simulations that go beyond the initial phase of AB evolution in the presence of symmetry-breaking third-order dispersion. We show that this leads to collisions and interactions between the emergent localized AB structures that may provide a natural link to the instabilities that occur in an oceanographic context.

THEORETICAL SUMMARY

The AB theory we present here was developed in mid-1980s by Akhmediev and co-workers who used an insightful analytical approach to construct novel solutions to the nonlinear Schrodinger equation describing fiber propagation. We first write the NLSE in dimensional form [START_REF]Nonlinear Fiber Optics[END_REF]:

2 2 2 2 || 0 , 2 AA iA A z T β γ ∂∂ + += ∂ ∂ (1)
where |A| 2 has dimensions of instantaneous power in W and the dispersion and nonlinearity coefficients β 2 (< 0) and γ have dimensions of ps 2 km -1 and W -1 km -1 respectively. The AB solution describes the evolution along z of a wave with initial constant amplitude on which is superimposed a small periodic perturbation taking the form of a T-dependent low amplitude modulation. The solution then consists of an evolving train of ultrashort pulses that is periodic in T and that exhibits a recurrence (growth-return) cycle in z.

In contrast to soliton solutions which are localized in T, the ideal breather solution is localised in the z direction. In fact, certain initial conditions can also yield periodic evolution along the z-direction, but even in this case, the pulse train characteristics nonetheless remain well-described by the analytic AB solution. The AB solution to Eq. ( 1) is :

mod , 0 mod (1 4 )cosh( ) sinh( ) 2 cos( ) (, ) 2c o s ( ) c o s h ( ) ab z i b b z a T AzT P aT b z ω ω -+ + = - (2)
which shows growth-return evolution over -∞ < z < ∞. The variable independent parameter ω mod is the (perturbation) frequency of the initial temporal modulation. Coefficients a and b depend on ω mod, defined by: 2a = [1 -( ω mod / ω c ) 2 ] and b = [8a (1-2a)] 1/2 with ω c 2 = 4 γ P 0 / |β 2 | and P 0 the CW power at large |z|. The solution is valid over modulation frequencies that experience MI gain: ω c > ω mod > 0 such that a varies in the interval 0 < a < 1/2 while the parameter b > 0 governs the MI growth. Maximum gain b = 1 occurs for a = 1/4, i.e. ω mod = ω c / 2 . The solution in Eq. ( 2) describes an evolving periodic train of ultrashort pulses with temporal period T mod = 2π/ω mod . The individual temporal sub-pulses have maximum amplitude and minimum temporal width at z = 0. The solution here describes the "maximally-compressed" AB :

mod 0 mod (1 4 ) 2 cos( ) (0 , ) . 2c o s ( )1 aa T Az T P aT ω ω -+ == - (3)
The corresponding spectrum consists of discrete frequency sideband modes with separation ω mod , and intensities that decrease following a geometric progression. For the particular case of the maximally-compressed solution of Eq. ( 3), the mode intensities are: S 0 = P 0 (2 1/2 -1) 2 for the pump, and S n = 2 P 0 (2 1/2 -1) 2|n| (where n = ±1, ±2, ±3, … ) for the sidebands. Thus the pump and sideband intensities follow the relative progression {I 0 , I 1 , I 2 , I 3 , I 4 …} = {1, 2, 0.3431, 0.0589, 0.0101…} so that there is a 3 dB increase from the pump (n=0) to the first sideband (n=±1) and then a constant decrease of 20 log 10 (2 1/2 -1) = -7.66 dB between subsequent sidebands. This geometric progression yields a characteristic triangular shape in the wings of the spectrum when plotted semi-logarithmically.

EXPERIMENTAL RESULTS FOR SUPERCONTINUUM GENERATION

We now present some experimental results: Fig. 1(a) shows spectral measurements at the output of 3.9 m of a highly nonlinear photonic crystal fiber with zero-dispersion wavelength at 780 nm for various peak powers using 1 ns pulses from a passively-modelocked microchip laser operating at 1064 nm. The experiment results in the top panel are compared with generalised nonlinear Schrödinger equation (GNLSE) simulations in the bottom panels. Full simulation details are to be found in Ref. [START_REF] Dudley | Modulation instability, Akhmediev Breathers and continuous wave supercontinuum generation[END_REF] but we note that the major parameters were: β 2 = -75 ps 2 km -1 and γ = 60 W -1 km -1 .

We note immediately that the agreement between experiment and simulation is very good and illustrate the key steps of initial sideband development followed by the merging and formation of a continuous triangular pedestal about the pump. At the lowest power of 26 W, the spectrum consists of small number of distinct sidebands separated by the frequency of peak MI gain. As the power increases to 43 W, we enter an "extended MI" regime where we can still resolve sidebands close to the pump, but we also see the development of continuous low amplitude wings that appear triangular when plotted with a semi-logarithmic y-axis. The spectral width in this regime approaches 60 nm at the -40 dB level, and we note the first sign of a very low amplitude Raman peak around 1120 nm. At higher power levels (not shown), the characteristics of a "fully-developed" supercontinuum are observed [START_REF] Dudley | Supercontinuum Generation in Photonic Crystal Fiber[END_REF]. We focus particular attention on the characteristics of the extended MI spectrum at 43 W peak power. In fact, although we have used GNLSE simulations in Fig. 1(b), this power level actually describes a regime before the onset of higher-order effects become significant and we might expect the AB theory to provide a good description. To examine how the AB theory can be applied to interpret the properties of the broadened spectrum seen at 43 W, Fig. 2 shows in more detail how the temporal properties associated with the extended MI phase develop with distance. The simulations use fiber parameters corresponding to experiment, and assume 43 W peak power CW field with noise.

The grayscale plot shows a single numerical realization illustrating temporal evolution over 3.9 m. At a distance of 3.5 m we extract the temporal profile that shows a high contrast pulse train, but the broadband noise that seeds the MI results in significant variation in the structure of the individual temporal peaks. Nonetheless, the highest amplitude peaks in the temporal profile (shown in the detailed view) are fitted very well by the maximally-compressed AB sub-pulses calculated from Eq. ( 3) using ω mod corresponding to the peak of the MI gain (f mod = 1.32 THz for our parameters.) In fact, analysis of the highest-amplitude peaks at other regions of the profile (not shown) reveals similarly good agreement with the calculated AB solution, and we have confirmed that simulations using different noise seeds reveal the same characteristics.

These results suggest that the extended MI spectrum in Fig. 1(b) in fact contains a dominant contribution from spontaneously-generated AB sub-pulses generated at the peak of the MI gain. Indeed, we can confirm this using experimental spectral measurement by comparing the form of the measured spectrum with the geometric progression predicted for the maximally-compressed AB. Figure 3 compares numerical and analytic results with the experimental results of Fig. 1 for P 0 = 43 W. Specifically, the numerical results show averaged multi-shot simulations using the full GNLSE with a 1 ns pulse input field (blue, short dashes) and using only the NLSE with a CW input field (red, long dashes). It is clear that both GNLSE and NLSE simulations produce similar results in agreement with experiment, with the GNLSE of course also predicting the onset of a small Raman peak on the long wavelength edge around 1120 nm; but this is largely insignificant in the context of the conclusions drawn here relating to AB dynamics. A significant result here is excellent agreement between the experimental decay of the spectral wings and the calculated amplitudes of the discrete frequency modes associated with the analytic form of the maximally-compressed AB. Because spontaneous MI is seeded by broadband noise, the spectral structure is of course not discrete, but rather consists of a continuous span of frequencies. Nonetheless, as with the time domain characteristics, we expect the spectral characteristics to contain a dominant component from the maximally-compressed AB solution calculated at peak MI gain. Thus, normalising to the n = ± 1 sideband amplitudes of experiment, the decay of spectral intensity with frequency in experiment and simulations is reproduced very well by the analytic geometric progression of the maximallycompressed AB breather.

BEYOND BREATHERS

These results have shown that the characteristics of both the modulated temporal profile and the associated spectrum in emergent SC generation can be explained in terms of the development of high amplitude Akhmediev Breather subpulses. This interpretation represents an important step in applying the formalism of breather evolution to the interpretation of supercontinuum generation. But of course this is not a complete explanation of how these sub-pulses subsequently separate from the extended MI spectrum and temporal pulse train and evolve towards higher-amplitude pulses that exhibit rogue wave statistics. In this context, however we note that the extended MI regime where the AB theory works well is essentially described by the integrable NLSE with noise, but any realistic optical fiber system would contain symmetry-breaking physical effects due to odd orders of chromatic dispersion and Raman scattering. In fact, both these effects are important in that they can induce collisions between the emergent breathers, but for illustrative purposes, we consider only the effect of third order dispersion in the results that follow.

In particular, Fig. 4 shows results where we have included the effect of third-order dispersion (TOD) in our simulations and we can see how it modifies the AB dynamics after the initial MI phase. These simulations use parameters different to those described above with a zero dispersion wavelength much closer to the pump. Specifically, we model 100 W, 5 ps FWHM Gaussian pulses at 1060 nm propagating in 20 m of photonic crystal fiber with zero dispersion at 1040 nm. dispersion coefficients at the pump wavelength are: β 2 = -4.10 × 10 -1 ps 2 km -1 , β 3 = 6.87 × 10 -2 ps 3 km -1 and the nonlinearity parameter is: γ = 0.011 W -1 m -1 . The input pulse soliton number for these parameters is N ~ 147, and we see clearly from Fig. 4 how the dynamics are clearly in the long pulse regime. This figure shows a detailed view of the evolution over a portion of the temporal pulse envelope, and we see the clear development of a high contrast modulation as in Fig. 2. However, the modulation is not stationary relative to the reference frame of the pump group velocity, but rather drifts towards larger co-moving time ie: towards the pulse trailing edge. This is a consequence of the TOD. In fact, we see that the combination of the TOD and noise for this case actually results in a non-uniformity in the drift behavior such that collisions can occur between different regions of the modulated field. As a result of these collisions, we see large amplitude localization and the emergence of precursor soliton structures with peak powers ~800 W in comparison with the 200 W peak powers seen for the breathers.

CONCLUSIONS

There are several main conclusions to make based on the results above. Firstly, numerical studies of the temporal and spectral properties of spontaneous MI have shown that the characteristics of both the modulated temporal profile and the associated spectrum can be explained in terms of the development of high amplitude AB sub-pulses. The well-known triangular form of the spontaneous MI spectrum when plotted semi-logarithmically has been explained naturally in terms of the analytic geometric progression describing the frequency dependence of the AB modal amplitudes. The analytic form of the AB spectrum has also been shown to be in very good quantitative agreement with the wings of the spontaneous MI spectrum observed in experiments studying the onset of quasi-CW supercontinuum generation. In addition, other results have shown that SC generation described by an NLSE model perturbed only by TOD can lead to large amplitude localized optical rogue soliton and rogue wave structures. Generally speaking, any single perturbation that destroys the integrability of the NLSE is sufficient to observe "survival of the fittest" soliton amplification as a result of collisions. Our simulations also yield the qualitative observation that collisions between emerging breather structures from an envelope undergoing MI appears to be a precursor to the formation of rogue soliton pulses, and it is possible to conjecture that a difference in relative velocities between breathers formed across an initial wave field is an important (perhaps necessary) condition for rogue soliton emergence. In fact, although the rogue solitons in fibre optics separate distinctly from the initial field because of self-frequency shifting, it is likely that the emergent and colliding breather structures provide a closer analogy with nonlinearity-induced rogue waves on the ocean. This proposal may have wide impact, as it implies that the seeds of rogue wave formation in optics as well as hydrodynamics may be found by identifying particular wave field characteristics (initial conditions, noise frequency content or topography that favor significant breather velocity gradients.

Fig. 1 .

 1 Fig. 1. Experimental results (top) and simulation results (bottom) results at peak powers as shown (see text).

Fig. 2 .

 2 Fig. 2. Single shot temporal evolution. A detail of the extracted temporal trace is shown in the rightmost figure, comparing simulations (solid line) withthe AB solution at a modulation frequency corresponding to peak MI gain (dashed line).

Fig. 3

 3 Fig.3Experiments (black line),simulations using the full GNLSE (blue dashed line), numerical simulations using the NLSE only (red dashed line), and the calculated spectrum of the maximally-compressed AB (green lines from zero).

Fig. 4

 4 Fig.[START_REF]Nonlinear Fiber Optics[END_REF] Detailed view of propagation in the NLSE with noise and TOD. Initially, noise-induced MI generates high-contrast AB-like pulses, but the effect of dispersion induces an additional phase of interactions, collisions and localisation.