DIPARTIMENTO DI INGEGNERIA E SCIENZA DELL’INFORMAZIONE

UNIVERSITY OF TRENTO

00000 Xxxx – Xxxxxx (Xxxxx), Xxx Xxxxxxxxx 00 xxxx://xxx.xxxx.xxxxx.xx

A LOGIC FOR CONTRACTS

Xxxxxxx Xxxxxxxxxx and Xxxxxxx Xxxxxx

June 2009 (submitted), November 2009 (revised) Technical Report #DISI-09-034

A Logi for Contra ts

Xxxxxxx Xxxxxxxxxx Dipartimento di Matemati a e Informati a

Universit degli Studi di Cagliari, Italy

Xxxxxxx Xxxxxx

Dipartimento di Ingegneria e S ienza dell'Informazione Universit degli Studi di Trento, Italy

Abstra t

We investigate the logi al foundations of ontra ts in distributed ap- pli ations. A ontra t is an agreement stipulated between two or more parties, whi h spe i es the duties and the rights of the parties involved therein. We model ontra ts as formulae in an intuitionisti logi extended with a ontra tual form of impli ation ։. This supports for a variant of Modus Ponens, where from a promise a ։ b to dedu e b, one does not need to know a; yet, it su es to have a dual promise b ։ a. We study the proof theory for our logi . In parti ular, we provide it with a Xxxxxxx- style axiomatisation, whi h is shown onsistent, and with a Xxxxxxx-style sequent al ulus, shown equivalent to the axiomatization. We prove our logi de idable, via a ut elimination property. The rights and the duties deriving from any set of ontra ts an therefore be me hani ally inferred.

1 Introdu tion

Se urity, trustworthiness and reliability of software systems are ru ial issues in the rising Information So iety. As new online servi es (e- ommer e, e-banking, e-government, et .) are made available, the number and the riti ality of the problems related to non-fun tional properties of servi es keeps growing. From the lient point of view, it is important to be sure that, e.g., after a payment has been made, then either the payed goods are made available, or a full refund is issued. From the provider point of view it is important to be sure, e.g., that a

xxxxx will not repudiate a ompleted transa tion, so to obtain for free the goods already delivered. In other words, the intera tion between a lient and a servi e must be regulated by a suitable ontra t, whi h guarantees to both parties the properties on demand. The ru ial problem is then how to de ne the on ept of ontra t, and how to a tually enfor e it, in an environment - the Internet - whi h is by de nition open and unreliable.

Unfortunately, at the present no widespread te hnology seems to give a gen- eral solution to this problem. Typi ally, servi es do not provide the lient with any on rete guarantee about the a tual fun tionality they implement. At best, the servi e provider ommits himself to respe t some servi e level agreement .

In the ase this is not honoured, the only thing the lient an do is to take legal steps against the provider (or vi e versa). Although this is the normal pra ti e nowadays, it is highly desirable to reverse this trend. Indeed, both lients and servi es ould in ur relevant expenses due to the needed legal disputes. This is impra ti al, espe ially for transa tions dealing with small amounts of money.

Contributions. We study the theoreti al foundations upon whi h onstru t- ing a servi e infrastru ture where ontra ts arry, besides the usual legal mean- ing, also a formal one. In other words, our ontra ts will be mathemati al entities, that spe ify exa tly the rights and the duties of lients and servi es. We envisage a world of servi es where lients and servi e providers an have pre ise, mathemati al guarantees about the implemented features, and about the assumed side onditions. In the s enario we aim at, ontesting a ontra t will not ne essarily require to resort to a ourt, yet it will be an event managed automati ally, deterministi ally and inexpensively, by the servi e infrastru ture itself. We all this intera tion paradigm ontra t-based omputing .

In this paper we begin our investigation on ontra t-based omputing, by studying formalisms to des ribe ontra ts, and to reason about them. A ontra t is a binding agreement between two or more parties, that di tates the duties the involved parties must ful ll, whenever some pre onditions are satis ed. Our theory of ontra ts will be able to infer, in ea h possible ontext, the duties deriving from a given set of ontra ts. To put the developed theory at work, we have implemented a proof sear h tool, whi h de ides whether a given formula is a tautology or not [26℄.

Summary. The paper is organized as follows:

• In Se tion 2 we give, with the help of an example, some motivations about the need for a logi for ontra ts.

• In Se tion 3 we devise a minimal set of properties whi h are desirable in any logi al formalization of ontra ts.

• In Se tion 4 we de ne our logi for ontra ts, through a Xxxxxxx-style axiomatization. Our logi satis es all the properties identi ed above as desirable.

• In Se tion 5 we give further details and examples about using our logi to model a variety of ontra ts.

• In Se tion 6 we provide our logi with a Xxxxxxx-style sequent al ulus, whi h is equivalent to the Xxxxxxx-style axiomatization.

• In Se tion 7 we prove the main te hni al result about our logi , that is its de idability. This is obtained by showing that our sequent al ulus enjoys

ut elimination and the subformula property.

• In Se tion 8 we study relations with other logi s, in parti ular with in- tuitionisti propositional logi IPC, with the modal logi S4, and with propositional lax logi .

• In Se tion 9 we extend our logi with an indexed modality, to model prin ipals. Contra t agreements then ome in a ri her avour, be ause

of the binding between the ontra ting parties and their inferred duties, whi h is now revealed.

• In Se tion 10 we dis uss some related work.

• In Se tion 11 we on lude, by dis xxxxxx some possible future work and extensions to our logi .

2 Motivations

Suppose there are two kids, Xxx e and Xxx, who want to play together. Xxx e has a toy airplane, while Xxx has a bike. Both Xxx e and Xxx wish to play with ea h other's toy: Xxx e wants to ride Xxx'x bike, and Xxx wants to play with Xxx e's airplane. Xxx e and Xxx are very meti ulous kids, so before sharing their toys, they stipulate the following gentlemen's agreement :

Xxx e: I will lend my airplane to you, Xxx, provided that I borrow your bike. Xxx: I will lend my bike to you, Xxx e, provided that I borrow your airplane.

We want to make pre ise the ommitments ex hanged by Xxx e and Xxx, so to be able to formally dedu e that Xxx e and Xxx will indeed share their toys, provided they are real gentlemen who always respe t their promises.

Let us write a for the atomi proposition Xxx e lends her airplane and b for

Xxx lends his bike . Using lassi al propositional logi , a straightforward yet na ve formalization of the above ommitments ould be the following. Ali e's

ommitment A is represented as the formula b → a (if Xxx lends his bike, then Xxx e lends her airplane) and Xxx'x ommitment as the formula a → b (if Xxx e lends her airplane, then Xxx lends his bike):

A = b → a B = a → b

where the symbol → denotes lassi al impli ation. Under the hypothesis that Xxx e and Xxx always respe t their promises, both formulas A and B are sound with respe t to our s enario. For the formula A, it is true that whenever b holds (Xxx lends his bike), then a will also hold (Xxx e lends her airplane). For the

formula B, it is true that whenever a holds (Xxx e lends her airplane), then b

will also hold (Xxx lends his bike).

So, why are we unhappy with the above formalization? The problem is that, in lassi al propositional logi , the above ommitments are not enough to dedu e that Xxx e will lend her airplane and Xxx will lend his bike. Formally, it is possible to make true the formula A∧B by assigning false to both propositions

a and b. So, Xxx e and Xxx will not be able to play together, despite of their

gentlemen's agreement, and of the hypothesis that they always respe t promises. The failure to represent s enarios like the one above seems related to the

standard interpretation of the Modus Ponens. In both lassi al and intuition- isti proof theories, the Modus Ponens rule allows to dedu e b whenever a → b and a are true. Ba k to our s enario, we ould dedu e that Xxx lends his bike, but only after Xxx e has xxxx Xxx her airplane. One of the two parties must

take the rst step in order to make the agreement be ome e e tive, that is to imply the promised duties. In a logi for mutual agreements, we would like instead to make an agreement be ome e e tive also without the need of some party taking the rst step (as we shall see in a while, su h party might not even exists in more omplex s enarios). That is, A and B are ontra ts, that on e stipulated imply the duties promised by all the involved parties.

Te hni ally, we would like our logi able to dedu e a ∧ b whenever A ∧ B

is true. As we have noti ed above, this does not hold neither in lassi al nor

in intuitionisti propositional logi , where the behaviour of impli ation stri tly adheres to Modus Ponens.

To model ontra ts, we extend the intuitionisti propositional logi IPC [30℄ with a new form of impli ation, that we denote with the symbol ։. The re- sulting logi is alled PCL, for Propositional Contra t Logi . For instan e, the

ontra t de lared by Xxx e, I will lend my airplane to Xxx provided that Xxx

lends his bike to me , will be written b ։ a. This form of, say, ontra tual im- pli ation, is stronger than the standard impli ation → of IPC. A tually, b ։ a implies a not only when b is true, like IPC impli ation, but also in the ase that a ompatible ontra t, e.g. a ։ b, holds. In our s enario, this means

that Xxx e will lend her airplane to Xxx, provided that Xxx agrees to lend his bike to Xxx e whenever he borrows Xxx e's airplane, and vi e versa. A tually, the following formula is a theorem of our logi :

(b ։ a) ∧ (a ։ b) → a ∧ b

In other words, from the gentlemen's agreement stipulated by Xxx e and Xxx, we an dedu e that the two kids will indeed share their toys.

To make our s enario a bit more interesting, suppose now that a third kid, Xxxx, joins Xxx e and Xxx. Xxxx has a omi book, whi h he would share with Xxx e and Xxx, provided that he an play with the other kids' toys. To a -

ommodate their ommitments to the new s enario, the three kids de ide to stipulate the following gentlemen's agreement (whi h supersedes the old one):

Xxx e: I will share my airplane, provided that I an play with Xxx'x bike and read Xxxx'x omi book.

Xxx: I will share my bike, provided that I an play with Xxx e's airplane and read Xxxx'x omi book.

Xxxx: I will share my omi book, provided that I an play with Xxx e's airplane and ride Xxx'x bike.

Let us write a for Xxx e shares her airplane , b for Xxx shares his bike , and c for Xxxx shares his omi book . Then, the above ommitments an be rephrased as: Xxx e promises a provided that b and c, Xxx promises b provided that a and c, and Xxxx promises c provided that a and b. In our ontra t logi ,

we model the above agreement as the formula A ∧ B ∧ C, where:

A = (b ∧ c) ։ a B = (a ∧ c) ։ b C = (a ∧ b) ։ c

The proof system of our logi will be able to dedu e that the three kids will indeed share their toys, that is, the following is theorem of the logi :

A ∧ B ∧ C → a ∧ b ∧ c

It it interesting to ompare the spe i ation above, whi h uses ontra tual im- pli ation, with a spe i ation whi h uses, instead, standard impli ation. Let:

A′ = (b ∧ c) → a B′ = (a ∧ c) → b C′ = (a ∧ b) → c

Clearly, in this ase we annot dedu e A′ ∧ B′ ∧ C′ → a ∧ b ∧ c. This s enario provide us with a further insight about ontra tual impli ation. Re onsider for a moment the s enario with only two ontra ting parties, modelled with standard

impli ation: (a → b) ∧ (b → a). We have shown above that, in su h a situation, a single party an make the agreement e e tive, e.g. Ali e an take the rst step,

and lend her airplane to Xxx (then, by Xxxxx Xxxxxx, Xxx will lend his bike to Xxx e). Instead, in the extended s enario (modelled with standard impli ation), it is no longer the ase that a single party an take the rst step and a hieve the same goal. For instan e, assume that Xxx e de ides unilaterally to share her airplane. Even by doing that, Xxx e will have no guarantee that, eventually, she will be able to play with the other kids' toys. This is be ause, with standard

impli ation, setting a to true would transform A′ ∧B′ ∧C′ into (c → b)∧(b → c),

whi x xxxxxx implies neither b nor c. To make their agreement e e tive, at least

two of the three parties must use ontra tual impli ation in their ommitments (while the other one an use standard impli ation).

This observation an be generalised to a s enario with n ontra ting parties, where one an show that at least n−1 parties must use ontra tual impli ation.

3 Desirable properties

We now dis uss some desirable properties of a logi for ontra ts, as well as some other properties that instead are undesirable. In the next se tion, we will show an axiomatisation that enjoys all the properties marked here as desired.

As shown in the previous se tion, a hara terizing property of ontra tual impli ation is that of allowing two ontra ting parties to handshake , so to make their agreement e e tive. This is resumed by the following handshaking property, whi h we expe t to hold for any logi for ontra ts:

(p ։ q) ∧ (q ։ p) → p ∧ q (1)

A generalisation of the above property to the ase of n ontra ting parties is also desirable. It is a sort of ir ular handshaking, where the (i + 1)-th party, in order to promise some duty pi+1, relies on a promise pi made by the i-th party. In the ase of n parties, we would expe t the following:

(p1 ։ p2) ∧ · · · ∧ (pn−1 ։ pn) ∧ (pn ։ p1) → p1 ∧ · · · ∧ pn (2)

As a on rete example, onsider an e- ommer e s enario where a Buyer an buy items from a Seller, and pay them through a redit ard. To mediate the intera tion between the Buyer and the Seller, there is a Bank whi h manages payments. The ontra ts issued by the three parties ould then be:

Buyer: I will li k pay provided that the Seller will ship my item Seller: I will ship your item provided that I get the money

Bank: I will transfer money to the Seller provided that the Buyer li ks pay .

Let the atomi propositions ship, clickpay, and pay denote respe tively the fa ts Seller ships item , Buyer li ks pay , and Bank transfers money . Then, the three ontra ts above an be modelled as follows:

Buyer = ship ։ clickpay Bank = clickpay ։ pay Seller = pay ։ ship

Then, by the handshaking property (2), we obtain a su essful transa tion:

Buyer ∧ Bank ∧ Seller → pay ∧ ship

Note that, in the spe ial ase that n equals 1, the above ir ular handshak- ing property turns into a parti ularly simple form:

(p ։ p) → p (3)

Intuitively, (3) an be interpreted as the fa t that promising p provided that p, implies p (a tually, also the onverse holds, so that promise is equivalent to p).

A generalisation of the s enario of the previous se tion to the ase of n kids

is also desirable. It is a sort of greedy handshaking property, be ause now a party promises pi only provided that all the other parties promise their duties,

i.e. p1, . . . , pi−1, pi+1, . . . , pn. The greedy handshaking an then be stated as:

i∈1..n

(p1 ∧ . . . ∧ pi−1 ∧ pi+1 ∧ . . . ∧ pn) ։ pi

→ p1 ∧ · · · ∧ pn (4)

As shown by (1), a ontra t p ։ q be omes e e tive, i.e. implies the promise q, when it is mat hed by a dual ontra t q ։ p. Even more dire tly, p ։ q should be e e tive also in the ase that the premise p is already true:

p ∧ (p ։ q) → q (5)

In other words, ontra tual impli ation should be stronger than standard impli-

xxxxx, x.x. we expe t that the following is a theorem of any logi for ontra ts:

(p ։ q) → (p → q) (6)

On the other hand, we do not want that also the onverse holds, sin e this would equate the two forms of impli ation:

(p → q) → (p ։ q) NOT A TAUTOLOGY

We want ontra tual impli ation to share with standard impli ation a num- ber properties. We dis uss some of them below. First, a ontra t that promises true (written ⊤) is always satis ed, regardless of the pre ondition. Then, we expe t the following tautology:

p ։ ⊤ (7)

However, di erently from standard impli ation, we do not want that a on- tra t with a false pre ondition (written ⊥) always holds.

⊥ ։ p NOT A TAUTOLOGY

So see why, assume that we have ⊥ ։ p as a tautology, for all p. Then, it would also be the ase for p = ⊥, and so by the binary handshaking property we would dedu e a ontradi tion: (⊥ ։ ⊥) ∧ (⊥ ։ ⊥) → ⊥.

Another property of impli ation that we want to preserve is transitivity:

(p ։ q) ∧ (q ։ r) → (p ։ r) (8)

Ba k to our previous example, transitivity would allow the promise of the Buyer (ship ։ clickpay) and the promise of the Bank (clickpay ։ pay) to be

ombined in the promise ship ։ pay.

Contra tual impli ation should also enjoy a stronger form of transitivity. We illustrate it with the help of an example. Suppose an air- ight ustomer wants to book a ight. To do that, he issues the following ontra t:

Customer : bookFlight ։ pay

The ontra t states that the ustomer promises to pay the required amount, provided that he obtains a ight reservation. Suppose now that an airline om- pany starts a spe ial o er, in the form of a free drink for ea h ustomer that makes a reservation:

AirLine : pay ։ bookFlight ∧ freeDrink

Of ourse, the two ontra ts should give rise to an agreement, be ause the airline

ompany is promising a better servi e than the one required be the ustomer

ontra t. To a hieve that, we expe t to be able to weaken the ontra t of the airline ompany, to make it mat h the ontra t issued by the ustomer:

AirLine → (pay ։ bookFlight)

Alternatively, one ould make the two ontra ts mat h by making stronger the pre ondition required by the ustomer, that is:

Customer → (bookFlight ∧ freeDrink ։ pay)

More in general, we want the following two properties hold for any logi for

ontra ts. They say that the promise in a ontra t an be arbitrarily weak- ened (9), while the pre ondition an be arbitrarily strengthened (10).

(p ։ q) ∧ (q → q′) → (p ։ q′) (9)

(p′ → p) ∧ (p ։ q) → (p′ ։ q) (10) Note that the properties (8), (9) and (10) over three of the four possible

ases of transitivity properties whi h mix standard and ontra tual impli ation.

Observe, instead, that ombining two impli ations into a ontra t is not a de- sirable property of any logi for ontra ts, for the same reason for whi h we do not want standard and ontra tual impli ations be equivalent.

(p → q) ∧ (q → r) → (p ։ r) NOT A TAUTOLOGY Another property that should hold is that, if a promise q is already true,

then it is also true any ontra t whi h promises q:

q → (p ։ q) (11)

Of ourse, we do not want the onverse to hold: it is not always the ase that a ontra t implies its promise.

(p ։ q) → q NOT A TAUTOLOGY

4 A Logi for Contra ts

In this se tion we give the basi ingredients of our logi for ontra ts PCL. In Se t. 4.1 we present the syntax of PCL; in Se t. 4.2 we provide it with an Xxxxxxx-style axiomatization. Finally, in Se t. 4.3 we study some interesting properties of PCL that follow from the given axioms.

4.1 Syntax

The syntax of PCL is a simple extension of IPC. It in ludes the standard logi

onne tives ¬, ∧, ∨, → and the ontra tual impli ation onne tive ։. We as- sume a denumerable set {p, q, r, s, . . .} of prime (atomi ) formulae. Arbitrary PCL formulae are denoted with the letters p, q, r, s, . . . (note that the font dif-

fers from that used for prime formulae). The pre eden e of IPC operators is the following, from highest to lowest: ¬, ∧, ∨, →. We stipulate that ։ has the same pre eden e as →.

De nition 4.1. The formulae of PCL are indu tively de ned by the following grammar.

p ::=	⊥	false
\|	⊤	true
\|	p	prime
\|	¬p	negation
\|	p ∨ p	disjun tion
\|	p ∧ p	onjun tion
\|	p → p	impli ation
\|	p ։ p	ontra tual impli ation

We let p ↔ q be synta ti sugar for (p → q) ∧ (q → p). If a formula is ։-free, we say it is an IPC formula. We use the symbol =⇒ to denote impli ation in the meta-theory, so to avoid onfusion with →.

4.2 Proof Theory: Xxxxxxx-style Axiomatization

We now de ne a Xxxxxxx-style proof system for PCL. The axioms in lude all the standard axioms for IPC (see e.g. [24℄). Like in IPC, we have a single inferen e rule, i.e. Modus Ponens. The hara terising axioms for PCL are alled Zero, Fix and PrePost.

De nition 4.2. The axioms of PCL are presented below.

• Core IPC axioms.

p ∧ q → p ∧1

p ∧ q → q ∧2

p → q → p ∧ q ∧3

p → p ∨ q ∨1

q → p ∨ q ∨2

(p → r) → (q → r) → (p ∨ q) → r ∨3

p → q → p → 1

(p → q → r) → (p → q) → p → r → 2

⊥ → p ⊥

⊤ ⊤

¬p → p → q ¬1

(p → q) → (p → ¬q) → ¬p ¬2

• Contra tual impli ation axioms.

⊤ ։ ⊤ Zero

(p ։ p) → p Fix

(p′ → p) → (p ։ q) → (q → q′) → (p′ ։ q′) PrePost

• Modus ponens ( ut).

p p → q Cut

We write ⊢ p when p is derivable from the axioms and inferen e rules above.

The ontra tual impli ation axioms are a tually spe ial ases of the desired

properties of ontra ts seen in Se t. 3. For instan e, the axiom Zero is a spe ial

ase of (7). The axiom Fix is exa tly the property (3). The axiom PrePost plays the role of both the properties (10) and (9).

4.3 Fundamental Consequen es

We present below some signi ant onsequen es of the axioms in Def. 4.2. Note that these onsequen es over all the properties marked in Se t. 3 as desirable. To shorten our notation, when speaking about non-provability, we write /⊢ p

when the formula p is not a theorem of PCL (i.e. p is not true for all the

instantiations of the metavariables). For instan e, we write/⊢ p → p ∧ q to mean that ¬∀p, q. ⊢ p → p ∧ q.

Lemma 4.3. Contra tual impli ation is stri tly stronger than impli ation.

⊢ (p ։ q) → (p → q) (12)

/⊢ (p → q) → (p ։ q) (13)

Proof. For (12), assume that p ։ q and p hold. Hen e, q → p trivially holds. By using PrePost on q → p,p ։ q, and q → q, we get q ։ q. We then on lude q by Fix. We anti ipate in (13) a negative result that an be me hani ally veri ed

using the de ision pro edure of Lemma 6.14.

Below, we establish some further onne tions between ։ and →, whi h generalize the transitivity of ։.

Lemma 4.4. Contra tual impli ation is transitive. More in detail, we have the following intera tions between ։ and →.

⊢ (p ։ q) → (q ։ r) → (p ։ r) (14)

⊢ (p → q) → (q ։ r) → (p ։ r) (15)

⊢ (p ։ q) → (q → r) → (p ։ r) (16)

/⊢ (p → q) → (q → r) → (p ։ r) (17)

Proof. Properties (15,16) are dire t onsequen es of PrePost, and the trivial

r → r and p → p.

For (14), we apply Lemma 4.3(12) to p ։ q, so obtaining p → q. Then we

an apply (15) to on lude.

We anti ipate in (17) a negative result that an be me hani ally veri ed using the de ision pro edure of Lemma 6.14.

The distributivity laws of ։ are quite pe uliar. As for standard impli a- tion in IPC, ∨-distributivity holds in only one dire tion (18,19). Instead, while

∧-distributivity holds in both dire tions in IPC for standard impli ation, on-

tra tual impli ation only satis es one dire tion (20,21). property holds (22). Lemma 4.5. Distributivity laws.	However, a related
⊢ (p ։ q) ∨ (p ։ r) → (p ։ (q ∨ r))	(18)
/⊢ (p ։ (q ∨ r)) → (p ։ q) ∨ (p ։ r)	(19)
⊢ (p ։ (q ∧ r)) → (p ։ q) ∧ (p ։ r)	(20)
/⊢ (p ։ q) ∧ (p ։ r) → (p ։ (q ∧ r))	(21)
⊢ (p ։ q) ∧ (q ։ r) → (p ։ (q ∧ r))	(22)

Proof. For (18), assume (p ։ q) ∨ (p ։ r). If p ։ q holds, we apply PrePost to weaken q to q ∨ r. The p ։ r ase is similar.

For (20), assume p ։ (q ∧ r). By PrePost, it is then easy to obtain both

p ։ q and p ։ r.

We anti ipate in (19,21) some negative results that an be me hani ally veri ed using the de ision pro edure of Lemma 6.14.

For (22), assume the hypotheses. We apply Lemma 4.3 to q ։ r and obtain

q → r, hen e q → (q ∧ r). By PrePost on p ։ q, we obtain the thesis.

Lemma 4.6. Substitution of equivalent formulae.

⊢ (p ↔ p′) → (q ↔ q′) → (p ։ q) → (p′ ։ q′)

Proof. Apply PrePost to p′ → p, p ։ q, and q → q′.

The following lemma states a su ient ondition and a ne essary ondition for p ։ q to hold. These onditions are expressed in IPC, i.e. they make no use of ։. We will return on these in Def. 8.6, 8.8 and related results, where we will prove that, when p, q are IPC formulae, these onditions are a tually the weakest su ient ondition and the strongest ne essary ondition that an be expressed within IPC (Lemma 8.10).

Lemma 4.7. Contra tual impli xxxxx admits the following su ient ondition and ne essary ondition.

⊢ q → (p ։ q) (23)

⊢ (p ։ q) → ((q → p) → q) (24)

Proof. For (23), assume q. We on lude by PrePost on p → ⊤ (trivial), ⊤ ։ ⊤

(by Zero), ⊤ → q (by q).

For (24), assume p ։ q and q → p. By PrePost, we have q ։ q, so we

on lude by Fix.

The following lemma justi es our hoi e of IPC, rather than lassi al logi CPC, as the basis for our logi : indeed, hoosing CPC would make our ontra - tual impli ation mu h less interesting.

Lemma 4.8. Denote with ⊢C p the provability of p in the system of Def. 4.2 augmented with the axiom of ex luded middle (p ∨ ¬p). Then, we have:

⊢C (p ։ q) ↔ q

Proof. Dire t onsequen e of Lemma 4.7, sin e ((q → p) → q) → q is a tautology of CPC (a tually, it is the well-known Peir e's law).

The following two lemmata are about handshaking of n ontra ting parties. Lemma 4.9 speaks about ir ular handshaking where the i-th party relies on the promise made by the i − 1-th party, as in (2). Lemma 4.10 is a stronger version of this, be ause it allows ea h party to rely on the promises made by all the other parties, as in (4).

Lemma 4.9. (Handshaking) For all n ≥ 0 and for all p0, . . . , pn:

⊢ (p0 ։ p1) → · · · → (pn—1 ։ pn) → (pn ։ p0) → (p0 ∧ . . . ∧ pn)

Proof. Assume all the hypotheses. By repeated appli ation of Lemma 4.4, we have pi ։ pi for all i ∈ 0..n. We then on lude by Fix.

Lemma 4.10. (Greedy handshaking) For all n ≥ 0, for all p0, . . . , pn, and for all i, j ∈ 0..n:

^ ^

⊢ pj

։ pi

→ pi (25)

i j i i

Proof. By indu tion on n. The base ase n = 0 is simple: (⊤ ։ p0) → p0 is proved by applying PrePost to ⊤ ։ p0, hen e obtaining p0 ։ p0 and on luding by Fix.

In the indu tive ase, assume that (25) holds fo r n − 1. We then prove it

for n. To do that, we assume that the hypothesis

j i pj

։ pi is true for

ea h i = 0..n, and then we pro eed to prove the thesis

the following auxiliary result:

i pi. First, we prove

pn →

j/=n

pj (26)

To prove (26), assume pn. Then, we have j

i pj

↔ j i,j/=n pj

, so

by Lemma 4.6 we get j

i,j

n pj

։ pi for i = 0..n − 1. We an apply the

indu tive hypothesis (25), and have j

n pj. V

Ba k to the indu tive ase, note that sin e i an be n, we have

pn. We then on lude by (26,24).

j n pj ։

5 Examples

Example 5.1. The toy ex hange s enario from Se t. 2 is modelled as:

⊢ (airplane ։ bike) ∧ (bike ։ airplane) → (airplane ∧ bike)

Indeed, this is a onsequen e of our axioms, and a spe ial ase of Lemma 4.9.

Example 5.2. We now exploit our logi to model a typi al preliminary ontra t for a real estate sale in Italy.

Assume a buyer who is interested in buying a new house from a given seller. Before stipulating the a tual pur hase ontra t, the buyer and the seller meet to stipulate a preliminary sale ontra t, that xes the terms and onditions of the pur hase. Typi ally, this ontra t will indi ate the pri e and the date when the deed of sale will take pla e, and it will outline the obligations for the buyer and the seller. When the preliminary ontra t is signed by both parties, the buyer will typi ally pay a part of the sale pri e. By the italian laws, if the seller de ides not to sell the house after having signed the preliminary ontra t and xxxx xxx the deposit, she must pay the buyer ba k twi e the sum re eived. Similarly, if the buyer hanges his mind and de ides not to buy the house, he loses the whole deposited amount.

We model the preliminary sale ontra t as two PCL formulae, one for the

xxxxx and the other for the seller. The buyer will sign the preliminary ontra t (signB), provided that the seller will a tually sell her house (sellS), or she refunds twi e the sum re eived (refundS). Also, the buyer promises that if he signs the preliminary ontra t, than either he will pay the stipulated pri e (payB), or he will not pay and lose the deposit (refundB)

Buyer : ((sellS ∨ refundS) ։ signB) ∧ (signB ։ (payB ∨ (¬payB ∧ refundB)))

The seller promises that she will sign the preliminary ontra t (signS), pro- vided that either the buyer promises to pay the stipulated amount, or he promises to lose the deposit. Also, the seller promises that is she signs the preliminary ontra t, then she will either sell her house, or will not sell and refund twi e the sum re eived.

Seller : ((payB ∨ refundB) ։ signS) ∧ (signS ։ (sellS ∨ (¬sellS ∧ refundS)))

A rst onsequen e is that the two ontra ts lead to an agreement between the buyer and the seller, that is both parties will sign the preliminary ontra t:

Buyer ∧ Seller → signB ∧ signS (27)

As a se ond onsequen e, if one of the parties does not nalize the nal deed of sale, than that party will refund the other:

Buyer ∧ Seller ∧ ¬payB → refundB (28)

Buyer ∧ Seller ∧ ¬sellS → refundS (29)

To prove the above, we pro eed as follows. First, we apply transitivity (14) to Buyer and Seller:

(sellS ∨ refundS) ։ (payB ∨ (¬payB ∧ refundB)) (payB ∨ refundB) ։ (sellS ∨ (¬sellS ∧ refundS))

Then, we use PrePost:

(sellS ∨ (¬sellS ∧ refundS)) ։ (payB ∨ (¬payB ∧ refundB)) (payB ∨ (¬payB ∧ refundB)) ։ (sellS ∨ (¬sellS ∧ refundS))

So, by Xxxxx 4.9, we have that Buyer ∧ Seller implies

(sellS ∨ (¬sellS ∧ refundS)) ∧ (payB ∨ (¬payB ∧ refundB))

By (12) the above and Buyer ∧ Seller imply signB∧ signS. This proves (27). Also, the above and ¬payB learly imply refundB. The same holds for sellS and refundS. Hen e, we establish (28,29).

Example 5.3. We now des ribe a possible online sale between two parties. In order to buy an item, rst the buyer has to onta t the bank and reserve from his a ount a spe i amount of money for the transa tion. When this happens, that amount is no longer available for anything else. We model this reservation with the formula lock. Then, the buyer has to make an o er to the seller: this is modelled with offer. The seller, when provided with an o er, evaluates it. If she thinks the o er is good, and the money has been reserved, then she will send the item (send). Otherwise, she an els the transa tion (abort). When the transa tion is aborted, the bank an els the money reservation, so that the buyer an use the amount for other transa tions (unlock).

We now formalize the s enario. The buyer agrees to lock ∧ offer, provided

that either the item is sent, or the money reservation is an elled. The seller

agrees to evaluate the o er. The bank agrees to an el the reservation when the transa tion is aborted.

Buyer : (send ∨ unlock) ։ (lock ∧ offer) Seller : offer ։ ((lock → send) ∨ abort) Bank : (lock ∧ abort) ։ unlock

Under these assumptions, we an see that either the item is sent, or the transa tion is aborted and the reservation an elled.

⊢ (Buyer ∧ Seller ∧ Bank) → (send ∨ (abort ∧ unlock))

To prove this, rst we apply PrePost to Seller and obtain (lock ∧ offer) ։

((lock → send)∨abort). By property (22) and Buyer, we have (send∨unlock) ։

(lock ∧ offer ∧ ((lock → send) ∨ abort)). By PrePost, we weaken it, obtaining (send ∨ unblock) ։ (send ∨ (lock ∧ abort)). By Bank and 4.3, we have (lock ∧ abort) → unlock, as well as (lock ∧ abort) → (abort ∧ unlock). Therefore, by PrePost we have (send ∨ unlock) ։ (send ∨ (abort ∧ unlock)). We on lude by PrePost and Fix.

Example 5.4. (Dining retailers) Around a round table, a group of n utlery retailers is about to have dinner. In the enter of the table, there is a large dish of food. Despite the food being deli ious, the retailers annot start eating right now. To do that, and follow the proper etiquette, ea h retailer needs to have a omplete utlery set, onsisting of n pie es, ea h of a di erent kind. Ea h one of the n retailers owns a distin t set of n pie e of utlery, all of the same kind. The retailers start dis xxxxxx about trading their utlery, so that they an

nally eat. Sin e everyone wants to get a fair deal, they want to formalize their

ommittments.

We formalize the s enario as follows. Number the retailers r1, . . . , rn together with the kinds of pie es of utlery, so that ri initially owns n pie es of kind number i. Then, write gi,j for ri gives a pie e (of kind i) to rj . Sin e retailers

an use their owVn utlery, we assume gi,i to be true. Retailer ri an start eating

whenever ei =

x xx,x .

Suppose that r1 ommits to a simple ex hange with r2: they ommit to g2,1 ։ g1,2 and g1,2 ։ g2,1, and the ex hange takes pla e sin e g2,1 ∧ g1,2 an be derived. While this seems a fair deal, it a tually exposes r1 to a risk: if r3, . . . , rn perform a similar ex hange with r2, then we have g2,i ∧ gi,2 for all

i. In parti ular, gi,2 holds for all i, so r2 an start eating. This is however not

ne essarily the ase for r1, sin e r3 has not ommitted to any ex hange with r1. A wise retailer would then never agree to a simple ex hange g2,1 ։ g1,2.

Instead, the retailer r1 ould ommit to a safer ontra t1:

g1,1 ∧ g2,1 ∧ · · · ∧ gn,1 ։ g1,1 ∧ g1,2 ∧ · · · ∧ g1,n

The idea is simple: r1 requires ea h pie e of utlery, that is, r1 requires to be able to start eating (e1). When this happens, r1 agrees to provide ea h other retailer with a pie e of his utlery. Now, assume e h retailer ri ommits to the analogous ontra t:

ci = ei ։

gi,j

V V

We an now verify that i ci → i ei, that is, the above oVntra ts a tually

allow everyone to eat. Assume ci for all i, and de ne pi =

ci = ei ։ pi. Note that

x xx,x. Clearly,

pj =

^ ^

gj,k →

gj,i = ei (30)

j i j i k j

sin e we an hoose k = i and gi,i is true. Therefore, by PrePost,

ci = ei ։ pi →

j/=i

։ pi

By Lemma 4.10, sin e Vi ci, we have Vi pi. By (30) we then on lude Vi ei.

1 We in lude g1,1 = ⊤ to make it more homogeneous.

Example 5.5. In Se t. 3 we listed several requirements for the notion of on- tra tual impli ation. A small set of these was then pi ked as our axiomatization: Zero, Fixand PrePost. However, we have not yet he ked that this is indeed om- plete with respe t to the other requirements. That is, we have to he k that all the requirements are theorems of PCL. We now qui kly re all the list of all these requirements and provide a support for ea h one.

The handshaking properties (1,2) have been established in Lemma 4.9. Prop- erty (3) is the axiom Fix. The greedy handshaking (4) was established in Lemma 4.10. Property (6) was proved in Lemma 4.3. Property (7) is a dire t

onsequen e of Zero. Property (8) is proved in Lemma 4.4. Properties (9,10) are dire t onsequen es of PrePost. Property (11) is a onsequen e of axioms

Zero and PrePost.

6 Proof Theory: Sequent Cal ulus

In this se tion we provide an alternative formalization of PCL, through a sequent

al ulus la Xxxxxxx. Our sequents have the form Γ ⊢ p, where Γ is a nite set of formulae. Below, we write Γ, p for Γ ∪ {p}.

Most of the rules for the IPC fragment have been taken from [27℄, whi h fea-

tures a rule set for IPC without stru tural rules. This fa t turns out to be quite useful when reasoning about the rule system. Indeed, as in [27℄, we are able to establish ut-elimination by applying a reasonably simple stru tural indu tion; we refer to Se t. 7 for the detailed proof. In the IPC fragment of our rule system

below, only rules ¬R and weakR diverge from [27℄. This hange was required to establish the subformula property (Lemma 6.13). Another minor di eren e

from [27℄ arises from our Γ's being sets rather than multisets; this is however immaterial, be ause of the absen e of stru tural rules, and the admissibility of

ontra tion in [27℄.

De nition 6.1. The Xxxxxxx-style rule system for PCL omprises the following rules.

IPC ore rules

Γ, p ⊢ p

Γ, p ∧ q, p ⊢ r

Γ, p ∧ q ⊢ r

∧ L1

Γ, p ∧ q, q ⊢ r

Γ, p ∧ q ⊢ r

∧ L2

Γ ⊢ p Γ ⊢ q

Γ ⊢ p ∧ q ∧ R

Γ, p ∨ q, p ⊢ r Γ, p ∨ q, q ⊢ r ∨ L Γ ⊢ p

∨ R1 Γ ⊢ q

∨ R2

Γ, p ∨ q ⊢ r

Γ ⊢ p ∨ q

Γ, p → q ⊢ p Γ, p → q, q ⊢ r

Γ, p → q ⊢ r → L

Γ, p ⊢ q

Γ ⊢ p → q → R

Γ, ¬p ⊢ p ¬L Γ, p ⊢ ⊥¬R

Γ, ¬p ⊢ r Γ ⊢ ¬p

Γ, ⊥ ⊢ p ⊥L

Γ ⊢ ⊤ ⊤R

Γ ⊢ ⊥

Γ ⊢ p

weakR

Γ ⊢ p Γ, p ⊢ q cut

Γ ⊢ q

Contra tual impli ation rules

Γ ⊢ q

Γ ⊢ p ։ q

Zero

Γ, p ։ q, r ⊢ p Γ, p ։ q, q ⊢ r

Γ, p ։ q ⊢ r Fix

Γ, p ։ q, a ⊢ p Γ, p ։ q, q ⊢ b

Γ, p ։ q ⊢ a ։ b PrePost

Note that IPC rules have left and right rules for ea h IPC onne tive. Roughly, ea h onne tive has right rules for introdu tion, and left rules for elimination. Contra tual impli ation instead has a di erent avor. Rule Zero is e e tively an introdu tion rule, and has a similar fun tion to the Xxxxxxx axiom Zero. Similarly, rule Fix is an elimination rule; its fun tion is related to the Xxxxxxx axiom Fix. Indeed, these rules ould be named ։ R and ։ L, respe - tively. The left/right rule dualism however is broken by rule PrePost. Of ourse, its fun tion is that of the Xxxxxxx axiom PrePost. This rule behaves both as an introdu tion and an elimination, so is both a right and left rule, in a sense.

In the rest of this se tion we study the sequent rule system above. First, we prove it equivalent to our Xxxxxxx axioms (Th. 6.4). Then we prove the redundan y of the weakR rule, i.e. that weakR is admissible in the proof sys- tem omposed of all the other rules. More importantly, we also prove the cut rule redundant, i.e. we prove ut-elimination for our sequent rule system. As a

onsequen e of ut-elimination, we are able to establish the onsisten y of the

logi (Th. 6.11), the subformula property (Lemma 6.13), and the de idability

of ⊢(Lemma 6.14). We also prove that the rules Zero, PrePost, Fix are not re- dundant, as one might expe t (Lemma 6.15). Finally we prove that PCL is a

onservative extension of IPC (Lemma 6.16).

6.1 Equivalen e of the Xxxxxxx and Xxxxxxx Systems

In this se tion, we establish the equivalen e between the two di erent logi al systems we introdu ed. We denote with ⊢H p the fa t that p is provable from the Xxxxxxx-style axioms of Def. 4.2. Similarly, by ⊢G p we denote that ∅ ⊢ p is a derivable sequent from the Xxxxxxx-style rules of Def. 6.1. We will then prove ⊢H =⊢G .

Lemma 6.2. ⊢H p =⇒ ⊢G p

Proof. It is su ient to show that ⊢G holds for all the Xxxxxxx-style axioms, and that it is losed under modus ponens. The latter is trivially done by cut and

→ R. For the former, we he k the ։-related axioms, only, sin e the others are standard.

• Zero

⊤R

⊢ ⊤ Zero

⊢ ⊤ ։ ⊤

• PrePost

∆, p′ ⊢ p′ id ∆, p′, p ⊢ pid

∆, p′ ⊢ p → L

∆, q ⊢ q′ id ∆, q, q′ ⊢ q′ id

∆, q ⊢ q′ → L

∆ = p′ → p, p ։ q, q → q′ ⊢ p′ ։ q′ PrePost

p′ → p, p ։ q ⊢ (q → q′) → (p′ ։ q′) → R

p′ → p ⊢ (p ։ q) → (q → q′) → (p′ ։ q′) → R

⊢ (p′ → p) → (p ։ q) → (q → q′) → (p′ ։ q′) → R

• Fix

p ։ p, p ⊢ pid p ։ p, p ⊢ pid

p ։ p ⊢ p Fix

⊢ (p ։ p) → p → R

Lemma 6.3. ⊢G p =⇒ ⊢H p

Proof. It is su ient to prove the following statement for ea h rule:

Γ0 ⊢G p0 · · · Γn ⊢G pn

V V

=⇒ ⊢

→ p ] → Γ → p

Γ ⊢G p

H i [ Γi i

Then, the lemma follows by indu tion on the derivation of ⊢G p. Most ases

are standard, so we he k only the ։-related rules.

• Rule Zero: (V Γ → q) → V Γ → (p ։ q).

Assume the hypotheses. By modus ponens, we get q, hen e ⊤ → q. We have ⊤ ։ ⊤ by Zero. The formula p → ⊤ trivially holds. We then apply PrePost to rea h p ։ q:

(p → ⊤) → (⊤ ։ ⊤) → (⊤ → q) → (p ։ q)

V V V

• Rule PrePost:[( Γ ∧ (p ։ q) ∧ a) → p]∧[( Γ ∧ (p ։ q) ∧ b) → q] → ( Γ∧ (p ։ q)) → (a ։ b).

Assume all the hypotheses. We easily get a → p, p ։ q, q → b. By

PrePost, we get a ։ b.

V V V

• Rule Fix: [( Γ ∧ (p ։ q) ∧ r) → p] ∧ [( Γ ∧ (p ։ q) ∧ q) → r] → ( Γ ∧ (p ։ q)) → r.

Assume all the hypotheses. We get r → p, q → r, hen e q → p. Using

q → p (dedu ed), p ։ q (hypothesis), q → q (trivial), we apply PrePost

and get q ։ q. By Fix, q, hen e r.

Theorem 6.4. ⊢G=⊢H

Proof. Immediate from lemmas 6.2 and 6.3.

6.2 Properties of the Xxxxxxx System

A rst basi result of our system is that the left-weakening of a sequent, i.e. augmenting the Γ, is strongly admissible. That is, whenever we have a derivation for a sequent, we an produ e a derivation for the augmented sequent having the same height.

D D′ ′

Lemma 6.5. If Γ ⊢ p then Γ, Γ′ ⊢ p where D

has the same height of D.

Proof. It is su ient to augment ea h sequent in D with Γ′. It is straightforward to he k that no rule is invalidated by this.

Convention. The above lemma is very frequently used in our proofs. To avoid ontinuously referring to it, we adopt the following notation: when we

D D+

have Γ ⊢ p , we simply write Γ, Γ′ ⊢ p for the augmented derivation.

The next result is dual to Lemma 6.5. It states that the right-weakening of a sequent, i.e. repla ing a ⊥ on the right of the turnstile ⊢ with some other formula , an be performed without using the weakR rule. In other words, rule weakR is redundant in our system. To prove this, we rst introdu e an auxiliary

lemma.

Lemma 6.6. If

Γ ⊢ ⊥

where D is a weakR-free derivation, then we also have

Γ ⊢ p with a weakR-free derivation, for any p.

Proof. By indu tion on the height of the derivation D. The last step of D must be one of id, cut, Fix or a left rule. If a left rule or a cut has been used, the thesis is either trivial (¬L, ⊥L) or immediately follows by the indu tion hypothesis. If

id has been used, then ⊥ ∈ Γ, and ⊥L su es. If Fix has been used, we rewrite

the derivation in the following way:

D0 D1

Γ, a ։ b, ⊥ ⊢ a Γ, a ։ b, b ⊢ ⊥ Fix =⇒

Γ, a ։ b ⊢ ⊥

Γ, a ։ b, p, a ⊢ aid

D1′′+

Γ, a ։ b, p, b ⊢ a

D1′

Γ, a ։ b, p ⊢ a Fix Γ, a ։ b, b ⊢ p

Γ, a ։ b ⊢ p Fix

where D1′ and D1′′ are obtained from the indu tion hypothesis on D1, and the formulae p, a respe tively.

Note that the transformation above does not introdu e new cuts in the derivation. So, on e the ut has been eliminated, the same pro edure an elim- inate weakR, too.

Lemma 6.7. The weakR rule is redundant. Proof. It is su ient to iterate Lemma 6.6.

Another fundamental result enjoyed by our Xxxxxxx-style rules, is the re- dundan y of the cut rule. This is a lassi ut-elimination result, or Haupsatz, whi h is the basis for many of the results in this se tion.

Theorem 6.8. (Cut-elimination)The cut rule is redundant. Proof. See Se t. 7 for the detailed proof.

It is possible to remove both the rules cut and weakR from our system without a e ting the generated ⊢ relation.

Theorem 6.9. The rule set {cut, weakR} is redundant.

Proof. This is not an immediate orollary of the previous results, sin e removing a cut from a derivation ould for e us to in lude weakR in the new derivation, and, vi e versa, removing a weakR ould for e us to introdu e a cut. However, by inspe ting the proof for Lemma 6.7, we an see that the weakR-elimination pro edure does not introdu e new cuts. So, given an arbitrary derivation D for

a sequent, by Th. 6.8 we also have a ut-free derivation D′ for the same sequent.

Then, we an apply the pro edure of Lemma 6.7 to on lude.

In our logi , as for IPC, every negation-free theory Γ is onsistent.

Lemma 6.10. Let Γ be free from ¬, ⊥. Then Γ /⊢ ⊥.

Proof. By ontradi tion, assume

Γ ⊢ ⊥

to be a ut-free derivation. We pro eed

by xxxx xxxx on the derivation D, and then by ase analysis. The last step of

D an not be id, ¬L, ⊥L, otherwise Γ is not free from ¬, ⊥. If the last step is another left rule, we have Γ′ ⊢ ⊥ as a premise for some Γ′ free from ¬, ⊥ so the indu tive hypothesis su es. The same applies to Fix. No right rule

an introdu e ⊥, so the last step is not a right rule. The same applies to

Zero, PrePost. No other rule exists.

Theorem 6.11. (Consisten y)The logi is onsistent, i.e. ∅ /⊢ ⊥. Proof. Dire t onsequen e of Lemma 6.10.

Cut-free derivations enjoy the subformula property, stating that all the for- mulae o urring su h a derivation for a sequent appear as subformulae in the sequent as well. Equivalently, it states that a ut-free derivation of a sequent an only involve subformulae of that sequent. As a single ex eption, the derivation

might mention ⊥ while the sequent does not, be ause of the weakR rule.

De nition 6.12. The subformulae sub(p) of a formula p are indu tively de ned as follows

sub(p) = {p}

sub(⊥) = {⊥}

sub(⊤) = {⊤}

sub(¬p) = {¬p} ∪ sub(p)

sub(p ∨ q) = {p ∨ q} ∪ sub(p) ∪ sub(q) sub(p ∧ q) = {p ∧ q} ∪ sub(p) ∪ sub(q) sub(p → q) = {p → q} ∪ sub(p) ∪ sub(q) sub(p ։ q) = {p ։ q} ∪ sub(p) ∪ sub(q)

The subformulae of a set of formulae Γ is sub(Γ) = p∈Γ sub(p).

Lemma 6.13. (Subformula Property)If

Γ ⊢ p

and D is ut-free, then the

formulae o urring in D belong to sub(Γ, p, ⊥).

Proof. By a simple indu tion on D. The property is preserved by every rule.

Note that a {cut, weakR}-free derivation would instead have a more tight

sub(Γ, p) bound.

We an now establish de idability for PCL. Lemma 6.14. (De idability)Γ ⊢ p is de idable.

Proof. We have Γ ⊢ p i it an be derived without cuts. We an de ide the

latter by xxxx xxxx for a shortest derivation bottom-up, exploring the whole

proof spa e non-deterministi ally. By the subformula property, ut-free proofs

an only ontain sequents having formulae in sub(Γ, p, ⊥). This is a nite set of sequents: let k be its ardinality. The depth of the sear h in the proof spa e an be limited to k: if there is a taller derivation, it has a sequent o urring twi e in some path, so the proof an be made shorter. This ensures the termination

of the algorithm.

We have implemented the above na ve de ision pro edure for PCL, develop- ing a prototype tool, whi h we used for experimenting with our logi . Sin e the proof spa e is huge, the tool was very helpful in establishing the negative results

for our logi , i.e. /⊢ p from some given p. We give more information about it in Se t. A.2.

We an now prove the non redundan y of the ։-related rules.

Lemma 6.15. None of the Zero, PrePost, Fix Xxxxxxx rules is redundant.

Proof. First, we arefully examine the proof of the ut-elimination theorem, and he k that the same proof a tually establish ut-elimination event in the rule system without any of the rules Zero, PrePost, Fix. This is be ause the

ut-elimination pro edure never introdu es a new appli ation of, say, a Fix rule unless Fix was already present in the original derivation. Similarly, we an restate the subformula property in these restri ted rule systems, as well as de-

idability. We therefore have de ision pro edures for both the full rule system and ea h restri tion of it, so we an he k that indeed some formula is provable in the full system, but not in the restri tion. As it might be expe ted, it turns out that to prove the Xxxxxxx axioms Zero, PrePost, Fix in the Xxxxxxx system, the related rule is ne essary. This was he ked by a simple modi ation of our tool, des ribed in Se t. A.2.

As a ni e result of the subformula property, we get that PCL is a onservative extension of IPC.

Lemma 6.16. PCL is a onservative extension of IPC, that is ⊢IPC p ⇐⇒ ⊢ p

for all IPC formulae p.

Proof. The ⇒ part is Lemma 8.4. For the ⇐ part, if ⊢ p, by Lemma 6.2 we

have ⊢G p. By ut-elimination and the subformula property, we have ⊢ p where

D make no use of rules Zero, Fix, and PrePost. Sin e all the other rules are in luded in the Xxxxxxx system of IPC, we an state ⊢IPC p.

7 Cut-elimination

In this se tion we prove ut elimination for the Xxxxxxx system of Def. 6.1. In order to do this, we borrow a fairly simple stru tural indu tion te hnique from [27℄.2 The whole te hnique an be des ribed as a re ursive algorithm, transforming a generi derivation into a ut-free one. The algorithm is made of two re ursive routines: a ore routine ( ut-redu e) and a driver ( ut-elim). The ore routine deals with the spe ial ase of a derivation ending with a cut between two ut-free subderivations. We name derivations of this spe ial form redu ible derivations. When provided with a redu ible derivation, ut-redu e produ es a ut-free derivation for the same sequent. Exploiting ut-redu e, the driver ut-elim handles the general ase. The a tual pro edure is shown in Alg. 1.

2 Here, stru tural means that it pro eeds indu tively on the stru ture of a derivation in the Xxxxxxx system.

Algorithm 1 Main driver for ut-elimination.

D1 !

D′

D′ !

ut-elim

Γ0 ⊢ p0 Γ1 ⊢ p1 cut

Γ ⊢ p

= ut-redu e

Γ0 ⊢ p0 Γ1 ⊢ p1 cut

Γ ⊢ p

· · · Di · · · !

′

· · · i · · ·

ut-elim

Γi ⊢ pi r

Γ ⊢ p

= Γi ⊢ pi r (r /= cut)

Γ ⊢ p

D′ Di

where i = ut-elim

Γi ⊢ pi

The ut-elim driver takes as input a derivation D. First, it applies itself re ursively on the derivations of the premises Di so onverting them to the ut- free ones D′. Then, if the last rule r used in D is not a cut, we an apply the same rule to D′ to onstru t a ut-free derivation. Otherwise, r is a cut,

and we are in the spe ial ase handled by ut-redu e, so we just invoke it.

The ut-elim driver always terminates sin e ea h re ursive all is made on a subderivation.

In the rest of this se tion, we de ne the ore routine ut-redu e. This routine makes use of a sophisti ated re ursion s heme. When invoked as

D0 D1 !

ut-redu e

Γ ⊢ p Γ, p ⊢ q cut

Γ ⊢ q

with ut-free D0, D1

the routine makes several re ursive alls, all of them for redu ible derivations.

Assume a re ursive all is made on a ut having p′ as the ut formula, and D′ , D′

0 1

as the subderivations. Then, one of the following onditions holds:

De nition 7.1. Constraints on the re ursive alls to ut-redu e:3

1. p′ is a proper subformula of p, or

2. p′ = p and h(D′ ) < h(D0), or

3. p′ = p, h(D′ ) ≤ h(D0), and h(D′ ) < h(D1).

0 1

We an state the onditions above as follows: the triple (p′, h(D′ ), h(D′ )) is

0 1

lexi ographi ally smaller than (p, h(D0), h(D1)). It is easy to see that this or-

xxxxxx for triples is a well-founded ordering relation, and therefore the re ursion must eventually terminate.

We now pro eed to de ne the ut-redu e routine. This is done by ex- amining the last rules used in D0 and D1, and overing all the possible ases. To simplify the presentation, we adopt a ompa t notation, writing =⇒ for our redu tion, as seen in Alg. 2. The rest of this se tion will pre isely de ne the

=⇒ relation.

3 We let onditions 2 and 3 to overlap, sin e we use ≤ instead of =. This is done to follow our a tual redu tion pro edure more losely, as we will see.

Algorithm 2 Core routine for ut-elimination.

D0 D1 !

ut-redu e

Γ ⊢ p Γ, p ⊢ q cut

Γ ⊢ q

=D¯

D0 D1

where

Γ ⊢ p Γ, p ⊢ q cut =⇒ D'

Γ ⊢ q

and D¯ is obtained by re ursively applying ut-redu e to all the cuts in D′.

When we write D =⇒ D′, D is a redu ible derivation, and D′ is the result of the redu tion. When we use cuts in D′, they are to be interpreted as re ursive

alls to the ut-redu e routine. Of ourse, we shall take are these uts

agree with the well-founded ordering dis ussed above. We do ument this in the derivation D′, by writing cutp when we are in ase 1 of the enumeration above, cut0 when we are in ase 2, or cut1 when we are in ase 3.

7.1 Summary of Cases

To lassify all possible ases, we rst introdu e some terminology. Ea x Xxxxxxx rule is related to some logi al onne tive. A rule for a generi onne tive ⊙ has as its prin ipal formulae the formulae o urring in that rule that involve ⊙. Rules id, weakR and cut have no prin ipal formulae. Both left and right

rules in the IPC fragment have exa tly one prin ipal formula. Rules Zero and Fix have one prin ipal formula as well. When a prin ipal formula o urs in the left (resp. right) hand side of the turnstile ⊢we all it a left (resp. right) prin ipal formula. Rule PrePost has two prin ipal formulae, named left prin ipal

and right prin ipal formulae.

In order to redu e:

D0 D1

Γ ⊢ a Γ, a ⊢ b cut

Γ ⊢ b

we pro eed by ase analysis on the last rule used in D0, D1. The derivation D0 an end with a Zero rule, a PrePost rule, a Fix rule, or an IPC rule. Similarly for D1. These 42 ases are further split, a ording to whether

• the ut formula is the left prin ipal formula of D0 and the right prin ipal formula of D1 (the essential ase),

• is not the right prin ipal formula of D0 (the left ommutation ase), or

• is not the left prin ipal formula of D1 (the right ommutation ase).

This lassi ation is rather standard in ut-elimination results, and is used in [27℄ as well. Note that the two ommutation ases an overlap when the ut formula is not right/left prin ipal in both D0, D1, respe tively. In Table 1, we

over all the possible ases, and group them whenever the handling is similar.

We now provide a reading key for Table 1. The rst row des ribes the ase where D0 ends with Zero. In this ase, the ut formula is the right prin ipal for- mula of D0, and so there is no left ommutation ase, denoted by ∄(l). The rst

D0 \ D1

Zero

PrePost

Fix

IPC

Zero

∄ (l)

∄ (e)

*/Zero (r)

Zero/PrePos

*/PrePost

t (e)

(r)

Zero/Fix (e)

*/Fix (r)

∄ (e) standard (r)

PrePost

∄ (l)

∄ (e)

*/Zero (r)

PrePost/PreP

*/PrePost

ost (e)

(r)

PrePost/Fix (e)

*/Fix (r)

∄ (e) standard (r)

Fix

∄ (e)

[Fix/* (l)℄

*/Zero (r)

Fix/* (l)

[*/PrePost (r)℄

Fix/* (l)

[*/Fix (r)℄

Fix/* (l)

[standard (r)℄

IPC

∄ (e) [standard (l)℄

*/Zero (r)

∄ (e) standard (l)

[*/PrePost (r)℄

∄ (e) standard (l)

[*/Fix (r)℄

standard (e,l,r)

(e) essential, (l) left ommutation, (r) right ommutation, [subsumed℄

Table 1: Summary of ases for ut-elimination

ell is for the ase where D1 ends with Zero as well: this is a right ommutation

ase whi h is handled in the same way as PrePost/Zero, Fix/Zero, et . so we will have a single ase ∗/Zero ase for the whole olumn. The Zero/PrePost ase

an be an essential ase or a right ommutation depending on whether the ut

formula is the left prin ipal formula of PrePost, so we split in two sub ases. The right ommutation ase ∗/PrePost is also reused in other points in the same ol- umn. The same applies to Zero/Fix. The Zero/IPC ase an not be an essential

xxx, sin e ։ never o urs in an IPC rule; so this is a right ommutation.

The se ond row des ribes the ase where D0 ends with PrePost, and is similar to the rst row.

The third row des ribes the ase where D0 ends with Fix. Sin e Fix has no right prin ipal formula, there is no essential ase in this row, denoted by

∄(e). The ase Fix/Zero is both a left and right ommutation ase, whi h we arbitrarily hose to handle as a right ommutation ase. The remaining ases might be right ommutations, but are surely left ommutations Fix/∗, so we handle them in that way.

The fourth row des ribes the ase where D0 ends with an IPC rule. The ase IPC/Zero might be a left ommutation (depending on the a tual IPC rule), but is surely a right ommutation as well, so we handle it in that way. The ase IPC/PrePost an not be an essential ase, sin e ։ o urs in no IPC rule; it might be a right ommutation, but is surely a left ommutation (no IPC rules involves ։), so we handle it in that way. The ase IPC/Fix is similar. The ase IPC/IPC an be either essential, a left ommutation, or a right ommutation. We invite the reader to he k that Table 1 indeed enumerates all the possible

ases, whi h an therefore be grouped as follows:

• essential: Zero/PrePost (e), Zero/Fix (e), PrePost/PrePost (e), PrePost/Fix

(e), standard (e)

• left ommutations: Fix/∗ (l), standard (l)

• right ommutations: ∗/Zero (r), ∗/PrePost (r), ∗/Fix (r), standard (r)

Most ases of the standard group are well-known ases for IPC, and are overed in [27℄, Appendix 1. This in ludes, for instan e, the essential ase ∧R/ ∧ L1, the left ommutation ∧L1/∗, and the right ommutation ∗/ ∧ R. Handling these

ases here would essentially amount to opying the whole Appendix 1 of [27℄

here, and perform some minor notation hange, only. Sin e this would provide no a tual ontribution, we will refer to [27℄ when these ases arise, and omit them. For ompleteness, we do ument in Se t. A.1 how to rephrase [27℄ in our notation. Finally, re all that in Def. 6.1 we diverge from [27℄ in a few IPC rules,

namely ¬R and weakR. Of ourse, these rules are involved in standard ases whi h are not overed in [27℄, so we shall provide a redu tion for these ases.

The ase ¬R/∗ an not be a left ommutation, but it an be essential (¬R/¬L); the ase ∗/¬R is instead a right ommutation. The ase ∗/weakR is a right

ommutation, while weakR/∗ is a left ommutation.

We now pro eed by handling all the ases mentioned above. We sometimes write Γ(p) instead of Γ to stress that p ∈ Γ.

7.2 The Essential Cases

In these ases the ut formula is (right/left) prin ipal in both the premises of the ut.

• Case Zero/PrePost

D0 D1 D2

Γ ⊢ q Zero Γ, p ։ q, a ⊢ p Γ, p ։ q, q ⊢ b PrePost

Γ ⊢ p ։ q Γ, p ։ q ⊢ a ։ b cut =⇒

Γ ⊢ a ։ b

Γ, q ⊢ q Zero

D0 Γ, q ⊢ p ։ q

Γ, q, p ։ q ⊢ b

Γ ⊢ q

Γ, q ⊢ b cut1

Γ ⊢ b cutp

Γ ⊢ a ։ b

Zero

• Case Zero/Fix

D0 D1 D2

Γ ⊢ q Zero Γ, p ։ q, a ⊢ p Γ, p ։ q, q ⊢ a Fix

Γ ⊢ p ։ q Γ, p ։ q ⊢ a cut =⇒

Γ ⊢ a

Γ, q ⊢ q Zero

D0 Γ, q ⊢ p ։ q

Γ, q, p ։ q ⊢ a

Γ ⊢ q

Γ, q ⊢ a cut1

Γ ⊢ a cutp

• Case PrePost/PrePost. We an assume (p ։ q) ∈ Γ.

D0 D1 D2 D3

Γ, a ⊢ p Γ, q ⊢ b PrePost Γ, a ։ b, x ⊢ a Γ, a ։ b, b ⊢ y PrePost

Γ ⊢ a ։ b Γ, a ։ b ⊢ x ։ y cut =⇒

Γ(p ։ q) ⊢ x ։ y

Dˆ0 Dˆ1

Γ, x ⊢ p Γ, q ⊢ y PrePost

Γ(p ։ q) ⊢ r

D0+ D1+

Γ, x, a ⊢ p Γ, x, q ⊢ b PrePost D2

Γ, x ⊢ a ։ b Γ, x, a ։ b ⊢ a cut

ˆ Γ, x ⊢ a

D0+

Γ, x, a ⊢ p

D0 =

D0+

Γ, x ⊢ p cutp

D1+

Γ, q, b, a ⊢ p Γ, q, b, q ⊢ b PrePost D3+

ˆ Γ, q ⊢ b

Γ, q, b ⊢ a ։ b

Γ, q, b ⊢ y

Γ, q, b, a ։ b ⊢ y cut

D1 =

Γ, q ⊢ y cutp

• Case PrePost/Fix. We an assume (p ։ q) ∈ Γ.

D0 D1 D2 D3

Γ, a ⊢ p Γ, q ⊢ b PrePost Γ, a ։ b, r ⊢ a Γ, a ։ b, b ⊢ r Fix

Γ ⊢ a ։ b Γ, a ։ b ⊢ r cut =⇒

Γ(p ։ q) ⊢ r

Dˆ0 Dˆ1

Γ, r ⊢ p Γ, q ⊢ r Fix

Γ ⊢ r

D0+ D1+

Γ, r, a ⊢ p Γ, r, q ⊢ b PrePost D2

Γ, r ⊢ a ։ b Γ, r, a ։ b ⊢ a cut

ˆ Γ, r ⊢ a

D0+

Γ, r, a ⊢ p

D0 =

D0+

Γ, r ⊢ p cutp

D1+

Γ, q, b, a ⊢ p Γ, q, b, q ⊢ b PrePost D3+

ˆ Γ, q ⊢ b

Γ, q, b ⊢ a ։ b

Γ, q, b ⊢ r

Γ, q, b, a ։ b ⊢ r cut

D1 =

Γ, q ⊢ r cutp

• standard. As anti ipated, we refer to [27℄ here, but for the ase ¬R/¬L, shown below.

• Case ¬R/¬L

Γ, p ⊢ ⊥ ¬R

Γ, ¬p ⊢ p ¬L

Γ ⊢ ¬p Γ, ¬p ⊢ q cut =⇒

Γ ⊢ q

Γ, p ⊢ ⊥ ¬R D1

Γ ⊢ ¬p Γ, ¬p ⊢ p cut1

Γ ⊢ p

Γ, p ⊢ ⊥

Γ ⊢ ⊥ cutp

Γ ⊢ q

7.3 The Left Commutation Cases

weakR

In these ases the ut formula is not a right prin ipal formula in the left premise of the ut.

• Case Fix/∗.We an assume (p ։ q) ∈ Γ.

D0 D1

Γ, a ⊢ p Γ, q ⊢ a Fix D2 ∗

Γ ⊢ a Γ, a ⊢ b cut =⇒

Γ(p ։ q) ⊢ b

D1+ D0+

id Γ, b, q ⊢ a Γ, b, q, a ⊢ p cut

D1 D2+

Γ, b, p ⊢ p

Γ, b, q ⊢ p

0 Γ, q ⊢ a Γ, q, a ⊢ b

Fix

Γ, b ⊢ p

Γ ⊢ b

Γ, q ⊢ b cut0

Fix

• standard. As anti ipated, we refer to [27℄ here, but for the ase weakR/∗, shown below.

• Case weakR/∗

Γ ⊢ ⊥ weakR D1 ∗ D0

Γ ⊢ p Γ, p ⊢ q cut =⇒ Γ ⊢ ⊥ weakR

Γ ⊢ q Γ ⊢ q

7.4 The Right Commutation Cases

In these ases the ut formula is not a left prin ipal formula in the right premise of the ut.

• Case ∗/Zero

D0 ∗

Γ, a ⊢ q

Zero

Γ ⊢ a Γ, a ⊢ p ։ q cut =⇒

Γ ⊢ p ։ q

D0 D1

Γ ⊢ a Γ, a ⊢ q cut1

Γ ⊢ q Zero

Γ ⊢ p ։ q

• Case ∗/PrePost. We an assume (p ։ q) ∈ Γ.

D1 D2

D0 ∗ Γ, a, x ⊢ p Γ, a, q ⊢ y PrePost

Γ ⊢ a Γ, a ⊢ x ։ y cut =⇒

Γ(p ։ q) ⊢ x ։ y

D0+ D1 D0+ D2

Γ, x ⊢ a Γ, x, a ⊢ p cut1 Γ, q ⊢ a Γ, q, a ⊢ y cut1

Γ, x ⊢ p Γ, q ⊢ y PrePost

Γ ⊢ x ։ y

• Case ∗/Fix. We an assume (p ։ q) ∈ Γ.

D1 D2

D0 ∗ Γ, a, r ⊢ p Γ, a, q ⊢ r Fix

Γ ⊢ a Γ, a ⊢ r cut =⇒

Γ(p ։ q) ⊢ r

D0+ D1 D0+ D2

Γ, r ⊢ a Γ, r, a ⊢ p cut1 Γ, q ⊢ a Γ, q, a ⊢ r cut1

Γ, r ⊢ p Γ, q ⊢ r Fix

Γ ⊢ r

• standard. As anti ipated, we refer to [27℄ here, but for the ases ∗/weakR

and ∗/¬R, shown below.

• Case ∗/weakR

D0 ∗ Γ, p ⊢ ⊥ weakR

D0 D1

Γ ⊢ p Γ, p ⊢ ⊥ cut

Γ ⊢ p Γ, p ⊢ q

Γ ⊢ q

cut =⇒

Γ ⊢ ⊥

Γ ⊢ q

weakR

• Case ∗/¬R

D0 Γ, p, q ⊢ ⊥ ¬R

D0+ D1

Γ, q ⊢ p Γ, q, p ⊢ ⊥ cut

Γ ⊢ p Γ, p ⊢ ¬q

Γ ⊢ ¬q

cut =⇒

Γ, q ⊢ ⊥ 1

¬R

Γ ⊢ ¬q

8 Relations with Other Logi s

In this se tion we explore the relationships between PCL and other logi s. We are interested in possible mappings, to see if there is some way to en ode PCL in some other pre-existing logi . For instan e, sin e PCL is a dire t extension of IPC, one might wonder whether the newly introdu ed onne tive for ontra tual impli ation ։ an be expressed using IPC onne tives. We answer negatively to this question in Se t. 8.1. In Se t. 8.2 we explore some mappings to the modal logi S4, by extending a well-known mapping from IPC to S4.

In this se tion, when we need to prove tautologies of IPC or S4, we will

sometimes resort to an automati theorem prover. To this purpose, we use the Logi s WorkBen h (LWB) [22℄. The interested reader will nd in Se t. A.3 how to obtain the a tual proofs generated by LWB.

8.1 Mappings to IPC

As shown by Xxxxx 4.8, the prin iple of ex luded middle trivializes ontra tual impli ation. This supports for the use of IPC, rather then e.g. CPC and S4, as the basis for our logi . We study here the mappings that a t homomorphi ally with respe t to ea h IPC onne tive.

De nition 8.1. A homomorphi mapping (from PCL to IPC) is a fun tion

m(•) su h that:

m(p) = p (p prime)

m(p ∧ q) = m(p) ∧ m(q)

m(p ∨ q) = m(p) ∨ m(q)

m(p → q) = m(p) → m(q) m(¬p) = ¬m(p)

m(⊤) = ⊤

m(⊥) = ⊥

A homomorphi mapping m(•) is omplete if and only if ⊢ p implies ⊢IPC m(p), and it is sound if and only if ⊢IPC m(p) implies ⊢ p. Note that m(p ։ q) is not onstrained by the above de nition.

We rst state some basi properties of homomorphi mappings.

Lemma 8.2. Let m(•) be a homomorphi mapping. Then:

m(p ↔ q) = m(p) ↔ m(q)

Proof. Trivial expansion of the synta ti sugar for ↔.

Lemma 8.3. For all homomorphi mappings m(•) and for all IPC formulae p, we have m(p) = p.

Proof. Trivial stru tural indu tion.

The identity is a sound and omplete partial mapping for IPC formulae.

Lemma 8.4. ⊢IPC p =⇒ ⊢ p.

Proof. Trivial, sin e the Xxxxxxx axioms of PCL in lude those of IPC.

We anti ipate here a result whi h will be formally proved in Se t. 6, namely the partial ompleteness of the identity mapping. Note that this a tually makes PCL a onservative extension of IPC.

Lemma 8.5. For all IPC formulae p, we have ⊢ p =⇒ ⊢IPC p. Proof. See Lemma 6.16.

We are aware of several omplete but unsound mappings from PCL to IPC. Among these, two are pe uliar, in that they provide the strongest and weakest interpretations of the onne tive։ in IPC. The formal justi ation for this terminology will be xxxx after Lemma 8.11.

De nition 8.6. The strongest interpretation of ։ in IPC, alled s(•), is de ned as the homomorphi mapping su h that:

s(p ։ q) = s(q)

We now prove the ompleteness of s, as well as its unsoundness.

Lemma 8.7. For all PCL formulae p, we have that ⊢ p =⇒ ⊢IPC s(p). The

onverse is false, in general.

Proof. Easy indu tion on the derivation of ⊢ p.

• If ⊢ p was derived through an IPC axiom, then we use the same axiom to derive ⊢IPC s(p), sin e s is an homomorphism.

• If ⊢ p was derived through a ։ axiom, we have the following sub ases.

Zero: p = ⊤ ։ ⊤. Trivially, ⊢IPC s(p) = ⊤.

Fix: p = (r ։ r) → r. Trivially, ⊢IPC s(p) = s(r) → s(r).

PrePost: p = (r′ → r) → (r ։ q) → (q → q′) → (r′ ։ q′). Then,

⊢IPC s(p) = (s(r′) → s(r)) → s(q) → (s(q) → s(q′)) → s(q′)

is easy. Indeed, if we generalize the above by repla ing s(r), s(r′), s(q), s(q′)

with distin t prime formulae, the formula still holds, as it an be triv-

ially veri ed either by hand or through an IPC theorem prover. We used LWB for this: see Se t. A.3 for more details.

• If ⊢ p was derived through a ut p p → q , then by indu tive hypothesis

we have ⊢IPC s(p) and ⊢IPC s(p → q), the latter being ⊢IPC s(p) → s(q).

s(p) s(p) → s(q)

We an then on lude by the ut

s(q)

The onverse does not hold in general, e.g. for p = (r ։ q) → q.

Below, we introdu e the weakest interpretation w for ontra tual impli a- tion. This is somehow dual with respe t to s, as we will see in Lemma 8.10.

De nition 8.8. The weakest interpretation of ։ in IPC, alled w(•), is de ned as the homomorphi mapping su h that:

w(p ։ q) = (w(q) → w(p)) → w(q)

We now prove the ompleteness of w, as well as its unsoundness.

Lemma 8.9. For all PCL formulae p, we have that ⊢ p =⇒ ⊢IPC w(p). The

onverse is false, in general.

Proof. Easy indu tion on the derivation of ⊢ p.

• If ⊢ p was derived through an IPC axiom, then we use the same axiom to derive ⊢IPC w(p), sin e w is an homomorphism.

• If ⊢ p was derived through a ։ axiom, we have the following sub ases.

Zero: p = ⊤ ։ ⊤. Trivially, ⊢IPC w(p) = (⊤ → ⊤) → ⊤.

Fix: p = (r ։ r) → r. Then, ⊢IPC w(p) = ((w(r) → w(r)) →

w(r)) → w(r) is simple to prove.

PrePost: p = (r′ → r) → (r ։ q) → (q → q′) → (r′ ։ q′). Then,

⊢IPC w(p) = (w(r′) → w(r)) → ((w(q) → w(r)) → w(q)) → A

where A = (w(q) → w(q′)) → ((w(q′) → w(r′)) → w(q′))

an be proved in IPC. Indeed, if we generalize the above by repla ing w(r), w(r′), w(q), w(q′) with distin t prime formulae, the formula still holds, as it an be trivially veri ed by an IPC theorem prover. We used LWB for this: see Se t. A.3 for more details.

• If ⊢ p was derived through a ut p p → q , then by indu tive hypothesis we

have ⊢IPC w(p) and ⊢IPC w(p → q), the latter being ⊢IPC w(p) → w(q).

w(p) w(p) → w(q)

We an then on lude by the ut

w(q)

The onverse does not hold in general, e.g. for p = ((q → r) → q) → (r ։ q).

Below, we relate the mappings s and w, by examining their behaviour on p ։ q, where p, q are IPC formulae. In Lemma 4.7 we proved that these mappings give su ient and ne essary onditions for p ։ q, i.e.:

⊢ s(p ։ q) → (p ։ q) (31)

⊢ (p ։ q) → w(p ։ q) (32)

We now establish that s and w are, respe tively, the weakest su ient on- dition and the strongest ne essary ondition for p ։ q that an be expressed in IPC. Note that Lemma 8.10 below does not apply when p, q ontain ontra tual impli ations.

Lemma 8.10. Let p, q be IPC formulae. That is,

1. If for an IPC formula c we have ⊢ c → (p ։ q), then ⊢ c → q.

2. If for an IPC formula c we have ⊢ (p ։ q) → c, then ⊢ ((q → p) → q) → c.

Proof. For (1), by Lemma 8.7, we have ⊢IPC s(c → (p ։ q)). That is ⊢IPC

s(c) → s(q), hen e by Lemma 8.3 ⊢IPC c → q. We on lude by Lemma 8.4.

For (2), by Lemma 8.9, we have ⊢IPC w((p ։ q) → c). That is ⊢IPC

((w(q) → w(p)) → w(q)) → w(c), hen e by Lemma 8.3 ⊢IPC ((q → p) → q) →

c. We on lude by Lemma 8.4.

Here we justify the terms strongest and weakest for s and w.

Lemma 8.11. Let m ≤ n be the preorder over omplete homomorphi mappings

m, n given by

⊢IPC n(p ։ q) → m(p ։ q) for all IPC formulas p, q

Then, s(•) is a maximum and w(•) is a minimum. That is, w ≤ m ≤ s for any omplete m.

Proof. For s, we need to show that ⊢IPC s(p ։ q) → m(p ։ q). By Lemma 8.3,

m(s(p ։ q)) = s(p ։ q), so we need to show ⊢IPC m(s(p ։ q)) → m(p ։ q),

whi h is ⊢IPC m(s(p ։ q) → (p ։ q)). By ompleteness, it is enough to show

⊢ s(p ։ q) → (p ։ q), whi h is (31).

Similarly, for w we need to show that ⊢IPC m(p ։ q) → w(p ։ q). By Lemma 8.3, m(w(p ։ q)) = w(p ։ q), so we need to show ⊢IPC m(p ։ q) → m(w(p ։ q)), whi h is ⊢IPC m((p ։ q) → w(p ։ q)). By ompleteness, it is enough to show ⊢ (p ։ q) → w(p ։ q), whi h is (32).

We proved that s and w are omplete homomorphi mappings. Several others do exist, however. Below, we provide a short table of those known to us at the time of writing.

m(p ։ q) = m(q) (s)

m(p ։ q) = (m(q) → m(p)) → m(q) (w)

m(p ։ q) = ¬¬(m(q) → m(p)) → m(q)

m(p ։ q) = ¬(m(q) → m(p)) ∨ m(q)

m(p ։ q) = ((m(q) → m(p)) ∨ a) → m(q) for any prime a

The ompleteness proofs for these mappings are similar to those of Lemma

8.7 and 8.9, so we omit them. However no mapping an be sound, as we show below.

Theorem 8.12. There is no sound homomorphi mapping from PCL to IPC. Proof. By ontradi tion, suppose there exists an homomorphi mapping m(•)

su h that ⊢IPC m(p) =⇒ ⊢ p for all p. Take p = m(q ։ r) ↔ (q ։ r) for some

prime q, r. Then m(p) = m(m(q ։ r)) ↔ m(q ։ r) = m(q ։ r) ↔ m(q ։ r)

by Lemma 8.2. The last form is trivially provable in IPC, so we an state

⊢IPC m(p). By the soundness of m(•), we have ⊢ p. Hen e

⊢ m(q ։ r) → (q ։ r)

⊢ (q ։ r) → m(q ։ r)

By Lemma 8.10, we have

⊢ m(q ։ r) → r

⊢ ((r → q) → r) → m(q ։ r)

hen e, ⊢ ((r → q) → r) → r. By Lemma 8.5 we have ⊢IPC ((r → q) → r) → r. This is however false, sin e IPC an not prove Peir e's law (not even on prime formulae).

8.2 Mappings to S4

We shall onsider the extensions of a standard IPC mapping to S4 [20, 17℄.

De nition 8.13. An extended mapping to S4 is a fun tion m(•) from PCL to S4 su h that

m(p) = p

m(p ∧ q) = m(p) ∧ m(q)

m(p ∨ q) = m(p) ∨ m(q)

m(p → q) = (m(p) → m(q)) m(⊤) = ⊤

m(⊥) = ⊥

m(¬p) = ¬m(p)

m(p ։ q) = C[m(p), m(q)]

for some xed S4 formula ontext C.

We now introdu e some te hni al lemmas.

De nition 8.14. A formula p is -invariant i ⊢S4 p ↔ p.

Note that the ← dire tion is a tually true for all p.

Lemma 8.15. If p, q are -invariant, then m(p∧q), m(p∨q), m(p → q), m(¬p), m(⊤), m(⊥), m(a)

(with a prime) are su h.

Proof. The ases ⊤, ⊥ are trivial. For the others, we pro eed as follows. For

∧, we simply apply ⊢S4 a ∧ b → (a ∧ b). Similarly, for ∨, we apply ⊢S4

a ∨ b → (a ∨ b). For ¬, →, a, we apply ⊢S4 a → a.

Lemma 8.16. Assume that, for all -invariant p, q, m(p ։ q) is -invariant. Then, for any p, m(p) is -invariant.

Proof. By stru tural indu tion on p. Indeed, all the indu tive steps are overed by either the hypothesis or Lemma 8.15.

Lemma 8.17. If a is prime, m(q) is -invariant, and ⊢S4 m(p), then we have

⊢S4 m(p{q/a}).

Proof. Clearly, m(p) = C[m(a)] = C[ a] for some ontext C. So, for the same

ontext, m(p{q/a}) = C[m(q)]. Sin e m(q) is -invariant, the latter is equivalent in S4 to C[ m(q)] = C[ a]{m(q)/a} = m(p){m(q)/a}. The last formula holds in S4, by substituting a in ⊢S4 m(p).

We are aware of several omplete but unsound mappings to S4.

De nition 8.18. The extended mappings e1, . . . , e4 to S4 are de ned as follows:

e1(p ։ q) = (e1(q) → e1(p)) → e1(q)

e2(p ։ q) = ♦(♦e2(q) → e2(p)) → e2(q)

e3(p ։ q) = ( (e3(q) → e3(p)) → e3(q))

e4(p ։ q) = ( (e4(q) → ♦e4(p)) → e4(q))

Lemma 8.19. ei(p) is -invariant.

Proof. By Lemma 8.16, we only need to he k that ei(p ։ q) is -invariant whenever p, q are su h. If we write Ci for the ontexts su h that ei(p ։ q) = Ci[ei(p), ei(q)], then it is su ient to verify that

⊢S4 (a ↔ a) ∧ (b ↔ b) → (Ci[a, b] ↔ Ci[ a, b]) (33)

and then on lude by substituting the prime formulae a, b. Formula (33), for ea h i, an be easily veri ed. A simple way to do it is to use a S4 theorem prover. We used LWB for this: see Se t. A.3 for more details.

Lemma 8.20. ⊢S4 ei(p ։ q) ↔ ej(p ։ q) i i = j .

Proof. This is an easy, albeit long, exer ise. See Se t. A.3 for more details.

Lemma 8.21. The mappings ei(•) are omplete, i.e.⊢ p =⇒ ⊢S4 ei(p), for

i ∈ [1..4]. The onverse is false, in general, so they are unsound.

Proof. We pro eed by indu tion on the derivation of ⊢ p.

If p is an instan e of a PCL axiom, by Xxxxx 8.16 and 8.17 it is su ient to

onsider the ase of the axiom being applied to prime distin t formulae, sin e we an then substitute them to obtain p. Therefore, we he k whether ⊢ ei(q) for ea h prime instan e of ea h PCL axiom q. This generates a nite number of spe i formulae to verify in S4. Sin e this is rather long, we resort to LWB

for this task. See Se t. A.3 for more details.

If instead ⊢ p was derived through a ut rule, say

a a → p p

, then, by the

indu tive hypothesis, we have ⊢S4 m(a) and ⊢S4 m(a → p) = (m(a) → m(p)).

Sin e q → q is a tautology of S4, we an have ⊢S4 m(a) → m(p). By the ut rule of S4, we on lude ⊢S4 m(p).

For the unsoundness result, it is enough to he k that ⊢S4 ei(pi) for some pi

su h that /⊢ pi. This was he ked using the LWB theorem prover: we refer to

Se t. A.3 for more details.

8.3 Lax PCL

Propositional lax logi (PLL) [15℄ is an extension of IPC with a single modality

◯, alled lax modality, hara terized by the following axioms:

p → ◯p ◯R

◯ ◯ p → ◯p ◯M

(p → q) → (◯p → ◯q) ◯F

These axioms appear to be relevant for ontra ts. Suppose we have a on- tra t at hand, and reason about its impli ations. If we read ◯p as p is ensured by the ontra t , then the axioms agree with our intuition. Axiom ◯R states that true propositions are always guaranteed. Axiom ◯M states that ommit- ting to a promise is a tually a promise itself. Axiom ◯F is simple: if p is ensured, and implies q, learly q must be ensured as well.

One might expe t that, if we take a xed formula c expressing the require- ments of a ontra t, and we interpret ◯q as c ։ q, then this should satisfy the axioms above. In other words, we expe t ◯ = c ։ • to be a lax modality (for any xed c). However, it turns out that this is not the ase in PCL.

Lemma 8.22. PCL proves ◯R and ◯F, but not ◯M.

Proof. Under the above de nition of ◯, Axiom ◯R holds, as one an derive it using PrePost and Zero. Axiom ◯F is also a spe ial ase of PrePost. Axiom ◯M does not hold, that is /⊢ (c ։ (c ։ p)) → (c ։ p): this an be veri ed through the de ision pro edure of Lemma 6.14.

Quite interestingly, sometimes PLL is axiomatized in an alternative equiva- lent way. Instead of in luding ◯F as an axiom, a related inferen e rule is used, together with another axiom:

p → q ◯F

◯p → ◯q

(◯q ∧ ◯r) → ◯(q ∧ r) ◯S

Axiom ◯S does not hold either in PCL under our interpretation for ◯. We a tually already stated this when we dis ussed property (21). We will not use this alternative axiomatization, sin e it uses another inferen e rule, and we nd this in onvenient.

We now dis uss how to extend PCL so that the indexed modality ◯p, de ned as ◯pq = p ։ q, is a lax modality. We need to adapt both our Xxxxxxx- style axiomatization and our sequent al ulus rules. For the Xxxxxxx-style proof system, we simply augment the axioms of Def. 4.2 with the ◯M axiom, following Lemma 8.22. We all PCLLax the logi extended as su h.

De nition 8.23. The Xxxxxxx-style axiomatisation of PCLLax extends that of PCL (Def. 4.2) with the following axiom:

(p ։ (p ։ q)) → (p ։ q) Lax

In this se tion we rede ne ⊢ to stand for provability in PCLLax.

We now adapt the sequent al ulus of Def. 6.1.

De nition 8.24. The sequent al ulus for PCLLax extends that of PCL (Def. 6.1) with the rule:

Γ, p ։ q, a ⊢ p Γ, p ։ q, q ⊢ a ։ b

Γ, p ։ q ⊢ a ։ b Lax

The above rule is best understood when ompared with PrePost:

Γ, p ։ q, a ⊢ p Γ, p ։ q, q ⊢ b

Γ, p ։ q ⊢ a ։ b PrePost

The single di eren e between PrePost and Lax is the use of b instead of a ։ b in the se ond premise. Indeed, be ause of this, rule Lax is more general, in that it subsumes rule PrePost.

Lemma 8.25. The PrePost rule is redundant in the PCLLax sequent al ulus.

Proof. Indeed, we an repla e ea h use of PrePost in a derivation using Lax as follows:

D0 D1

Γ, p ։ q, a ⊢ p Γ, p ։ q, q ⊢ b PrePost =⇒

Γ, p ։ q ⊢ a ։ b

D0 Γ, p ։ q, q ⊢ b

Zero

Γ, p ։ q, a ⊢ p Γ, p ։ q, q ⊢ a ։ b Lax

Γ, p ։ q ⊢ a ։ b

Consequently, we will negle t rule PrePost from now on. We an now restate a number of fundamental results, starting from the Xxxxxxx-Xxxxxxx equivalen e.

Theorem 8.26. ⊢H p ⇐⇒ ⊢G p

Proof. We adapt the proof of Th.6.4. To prove ⊢H p =⇒ ⊢G p, we just need to derive the Lax axiom in the sequent al ulus.

p ։ (p ։ q), p ⊢ p id p ։ (p ։ q), p ։ q ⊢ p ։ q id

p ։ (p ։ q) ⊢ p ։ q Lax

⊢ (p ։ (p ։ q)) → (p ։ q) → R

For the other dire tion, ⊢G p =⇒ ⊢H p, we provide the missing ase:

• RVule Lax: [(

Γ ∧ (p ։ q) ∧ a) → p] ∧ [(

Γ ∧ (p ։ q) ∧ q) → (a ։ b)] →

( Γ ∧ (p ։ q)) → (a ։ b).

Assume all the hypotheses. We get Γ, p ։ q, hen e a → p, q → (a ։ b).

By PrePost, we get p ։ (a ։ b). Again by PrePost, we get a ։ (a ։ b).

We apply Lax to on lude a ։ b.

Lemma 8.27. The Lax rule is not redundant.

Proof. Otherwise, the PrePost rule would be redundant in plain PCL, so we

on lude by Xxxxx 6.15 and Lemma 8.25.

Theorem 8.28. (Cut-elimination) The cut rule is redundant in PCLLax.

Proof. We pro eed as in Se t.7, repla ing the PrePost rule with the Lax one. Cases not involving PrePost are thus una e ted. A ording to Table 1, we need to he k four new ases: three essential (Zero/Lax, Lax/Lax, Lax/Fix), and one right ommutation (*/Lax). We now de ne the redu tion relation =⇒ for these

ases.

• Case Zero/Lax (essential)

D0 D1 D2

Γ ⊢ q Zero Γ, p ։ q, a ⊢ p Γ, p ։ q, q ⊢ a ։ b Lax

Γ ⊢ p ։ q Γ, p ։ q ⊢ a ։ b cut =⇒

Γ ⊢ a ։ b

Γ, q ⊢ q Zero

D0 Γ, q ⊢ p ։ q

Γ, p ։ q, q ⊢ a ։ b

Γ ⊢ q

Γ, q ⊢ a ։ b cut1

Γ ⊢ a ։ b cutp

• Case Lax/Lax (essential)

D0 D1 D2 D3

Γ, p0 ⊢ p Γ, q ⊢ p0 ։ q0 Lax ∆, a0 ⊢ p0 ∆, q0 ⊢ a0 ։ b0 Lax

Γ ⊢ p0 ։ q0 ∆ = Γ, p0 ։ q0 ⊢ a0 ։ b0 cut =⇒

Γ(p ։ q) ⊢ a0 ։ b0

Da Db

Γ(p ։ q) ⊢ a0 ։ b0

D0+

Lax

D1+

Γ, a0, p0 ⊢ p Γ, a0, q ⊢ p0 ։ q0 Lax D2+

Γ, a0 ⊢ p0 ։ q0 Γ, a0, p0 ։ q0 ⊢ p0 cut

Γ, a0 ⊢ p0 1

D0+

Γ, a0, p0 ⊢ p

Da =

D2+

Γ, a0 ⊢ p cutp

D3+

D1 Γ, q, p0 ։ q0, a0 ⊢ p0

Γ, q, p0 ։ q0, q0 ⊢ a0 ։ b0 Lax

Db =

Γ, q ⊢ p0 ։ q0

Γ, q, p0 ։ q0 ⊢ a0 ։ b0 Γ, q ⊢ a0 ։ b0

cut0

• Case Lax/Fix (essential)

D0 D1 D2 D3

Γ, p0 ⊢ p Γ, q ⊢ p0 ։ q0 Lax

Γ ⊢ p0 ։ q0

Γ, r, p0 ։ q0 ⊢ p0 Γ, q0, p0 ։ q0 ⊢ r Fix

Γ, p0 ։ q0 ⊢ r

Γ(p ։ q) ⊢ r

cut =⇒

Da Db

Γ(p ։ q) ⊢ r

Fix

D1+

D2+

Γ, r, q ⊢ p0 ։ q0 Γ, r, q, p0 ։ q0 ⊢ p0 cut

Γ, r, q ⊢ p0 0

D0+

Γ, r, q, p0 ⊢ p

Da =

X, r, p ⊢ p

D2+

Γ, r, q ⊢ p cutp

Γ, r ⊢ p

D3+

Fix

D1 Γ, q, p0 ։ q0, r ⊢ p0 Γ, q, p0 ։ q0, q0 ⊢ r Fix

Db = Γ, q ⊢ p0 ։ q0 Γ, q, p0 ։ q0 ⊢ r cut

Γ, q ⊢ r 0

• Case */Lax (right ommutation)

D1 D2

D0 Γ, r, a ⊢ p Γ, r, q ⊢ a ։ b Lax

Γ ⊢ r Γ, r ⊢ a ։ b cut =⇒

Γ(p ։ q) ⊢ a ։ b

D0+ D1 D0+ D2

Γ, a ⊢ r Γ, a, r ⊢ p cut1

Γ, a ⊢ p

Γ, q ⊢ r Γ, r, q ⊢ a ։ b cut

Γ, q ⊢ a ։ b 1

Γ(p ։ q) ⊢ a ։ b Lax

Of ourse, we are able to restate de idability.

Lemma 8.29. The sequent al ulus of PCLLax satis es the subformula prop- erty.

Proof. Trivial inspe tion of the rule Lax.

Theorem 8.30. (De idability) The logi PCLLax is de idable.

Proof. Immediate by Lemma 8.29 and Th.8.28. See Th.6.14 for more details.

9 Prin ipals

As illustrated by the examples in Se t. 5, PCL allows for inferring whether some promise is implied by a set of ontra ts. In real-world s enarios, ea h ontra t will be issued by a given prin ipal. It would then be useful to represent the binding between prin ipals and ontra ts within the logi . This would allow, for instan e, to single out the prin ipal who is responsible for a violation, and possibly take ountermeasures against him.

To this aim, we extend our logi with a says modality, similarly to [17℄.

De nition 9.1. The syntax of PCLsays extends that of PCL (Def. 4.1) as follows:

p ::= · · · | A says p

where we assume a set of (atomi ) prin ipals, ranged over by A, B, . . ..

We an then rephrase Xxx e's ontra t from the toy ex hange example in Se t. 1 as Xxxxx says (b ։ a). This represents the fa t that the prin ipal named Xxx e has issued a ontra t, where she promises to lend her airplane, provided that she borrows a bike.

We now develop the proof theory of PCLsays . Essentially, we extend the PCL axioms with those of the logi ICL [17℄. This is an indexed lax logi , where the lax modality orresponds to our says . The interesting ontribution is that this extension preserves all the main results of PCL, in parti ular its de idability.

De nition 9.2. The Xxxxxxx-style axiomatisation of PCLsays extends that of PCL (Def. 4.2) with the following axioms:

p → (A says p) SaysR

(A says A says p) → A says p SaysM

(p → q) → (A says p) → (A says q) SaysF

Ba k to our toy ex hange example of Se t. 1, one would expe t to dedu e an agreement between Xxx e and Xxx, that ommits Xxx e to lend her airplane (i.e., Xxxxx says a), and ommits Xxx to lend his bike (i.e., Xxx says b). A

areful spe i ation of the kids ontra ts is however needed, in order to obtain

the expe ted result. As a rst attempt, onsider the following spe i ation:

ptoy = Xxxxx says (b ։ a) ∧ Xxx says (a ։ b)

While, at rst sight, this spe i ation seems enough to dedu e the desired result, it turns out that a di erent (and quite weaker) handshaking is rea hed, i.e.:

ptoy → Xxxxx says Xxx says (a ∧ b)

That is, Xxx e and Xxx together promise to ex hange their toys. However, this only tells half of the story: a tually, it does not distinguish the duties of Xxx e from those of Xxx. A tually, the onditions required by Xxx e and Xxx (respe tively, b and a) do not pre isely apture our intuition. In the ontra t Xxxxx says (b ։ a), a promise of b from Xxx is not enough to ommit Xxx e to lend her airplane: requiring b means that Xxx e wants indeed to have the bike. As a result, in the spe i ation ptoy we an dedu e that a and b hold only under the responsibility of both Xxx e and Xxx.

The spe i ation an be made more pre ise as follows. Xxx e promises to lend her airplane, provided that Xxx promises to lend his bike (and vi e versa). The overall ontra t an then be rephrased as:

′

toy

= Xxxxx says ((Xxx says b) ։ a) ∧ Xxx says ((Xxxxx says a) ։ b)

The new ontra t reveals the whole story, that is, the duty of Xxx e is that of lending her airplane, and the duty of Xxx is that of lending his bike.

′

toy

→ Xxxxx says a ∧ Xxx says b

The above obligations an be exploited by a third party (a sort of au- tomated judge) whi h has to investigate the responsibilities of the involved parties, in the unfortunate ase that the ontra t is not respe xxx. For instan e, if our judge is given the eviden e that Xxx e's airplane has never been lent to Xxx, then he will be able to infer that Xxx e has not respe xxx her ontra t (and possibly punish her), that is:

′

toy

∧ ¬a → (Xxxxx says a ∧ ¬a) → Xxxxx says ⊥

Expli itly representing prin ipals has some additional bene ts, espe ially when putting our logi at work in inse ure environments populated by atta kers. A tually, an atta ker ould mali iously issue a fake ontra t, where he makes a promise that he annot a tually implement, e.g. be ause the promised duty an

only be performed by another party. By binding ea h ontra t with its prin ipal, it is easy to realize when someone has attempted su h a fraud, be ause the prin ipal who has signed the ontra t is di erent from who is due to implement the promised behaviour.

Ba k to our te hni al development, the main results of PCL are also enjoyed by its extension PCLsays .

De nition 9.3. The sequent al lus of PCLsays in ludes all the rules for PCL, and the following additional rules:

Γ ⊢ p

Γ ⊢ A says p

SaysR

Γ, A says p, p ⊢ A says q SaysL

Γ, A says p ⊢ A says q

Theorem 9.4. (Cut Elimination) If p is provable in PCLsays , then there exists a proof of p whi h does not use the Cut rule.

Proof. We use the stru tural approa h of [27℄, similarly to Se t. 7. The ases involving only PCL rules have been already dealt with in Se t. 7. The ases involving only says are dealt with in [17℄. The other ases are ommutations, and so they are dealt with either as in Se t. 7 or as in [17℄.

Lemma 9.5. The sequent al ulus of PCLsays satis es the subformula property. Proof. Trivial inspe tion of rules XxxxX and SaysL.

Theorem 9.6. (De idability) The logi PCLsays is de idable. Proof. Dire t from Th.9.4 and Lemma 9.5.

10 Related Work

Various approa hes to the problem of providing both lients and servi es with provable guarantees about ea h other's fun tional behaviour have been studied over the last few years. Yet, at the present no widespread te hnology seems to give a general solution to this problem.

The motivations underlying our ontra t logi seem somewhat related to those for the logi s introdu ed in [3℄ to study how to ompose assume-guarantee spe i ations of on urrent systems [2℄. The idea is that a system will give some guarantee M1 about its behaviour, provided that also the environment it

operates within will behave a ording to some assumption M2, and vi e versa. This is rendered in [3℄ as the intuitionisti formula (M1 → M2) ∧ (M2 → M1). However, the te hni al development of the two approa hes is quite di erent. In our approa h, we use ontra tual impli ation ։, rather than impli ation →, in order to obtain M1 ∧ M2 from (M1 ։ M2) ∧ (M2 ։ M1). In [3℄, instead, the

onne tive → is the usual impli ation of intuitionisti logi . Therefore, simply adding the axiom (M1 → M2) ∧ (M2 → M1) ⊢ M1 ∧ M2 would make the

logi in onsistent. To over ome this problem, in [3℄ the above judgement only

holds in parti ular models, whi h are subje t to several onstraints (e.g., the propositions M1, M2 must be interpreted as safety properties). While this allows for exploring these models at some depth, our approa h appears more general, sin e it develops a proof theory of ontra ts while abstra ting from the spe i models of the logi .

The omplexity of real-world s enarios, where several on epts like prin i-

pals, ontra ts, authorizations, duties, delegation, mandates, regulations, et . are inextri ably intermingled, have led to a steady ourishing of new logi s over the years. The logi s proposed to model su h s enarios take inspiration and extend e.g. lassi al [12℄, modal [11℄, deonti [28, 18℄, default [19℄ and defeasible logi s [21℄. We think none of these logi s, in luding our PCL, aptures all the fa ets of ontra ts. Ea h of these logi s is designed to represent some parti ular aspe t of ontra ts, e.g. obligations, permissions and prohibitions in deonti log- i s, violation of ontra ts in default and defeasible logi s, and agreement in our

ontra t logi . We argue that, sin e these aspe ts are orthogonal, it is possible to extend PCL with features from some of these logi s.

Our resear h seems also related to foundational resear h on authorization logi s for distributed systems [1, 17, 23℄. There, the problem is that of de id- ing whether, given a bun h of authorization assertions modelled in the logi (possibly involving omplex on epts like roles, groups, delegations), we an dedu e that a prin ipal has the right to a ess a given resour e. While many of these on epts are ommon with ontra ts, there is a fundamental di eren e between the two worlds. While authorizations logi s are fo ussed on de iding if a prin ipal is allowed to perform some a tion, in our ontra t logi we are also

on erned with dis overing what that prin ipal has to promise in return.

Re ent resear h papers address the problem of de ning ontra ts that spe ify the intera tion patterns among ( lients and) servi es [8, 9, 25℄. For instan e, in [9℄ a ontra t is a pro ess in a pro ess algebra featuring only pre xing, internal and external hoi e. A lient ontra t is ompliant with a servi e ontra t if any possible intera tion between the lient and the servi e will always su eed. There, a main problem is how to de ne (and de ide) a sub ontra t relation, that allows for safely substituting servi es without a e ting the omplian e with their lients. Even assuming that servi es are trusted and respe t the published

ontra t, this approa h provides the lient with no provable guarantees, ex ept that the intera tion with the servi e will su eed , that is all the expe xxx syn hronizations will take pla e. For instan e, onsider a simple buyer-seller s enario. In our vision, it is important to provide the buyer with the guarantee that, e.g., after the payment has been made, then either the payed goods are made available, or a full refund is issued. For the seller, it is important to be sure that, e.g., a buyer will not repudiate a ompleted transa tion, so to obtain for free the goods already delivered. This ould be modelled by the following

ontra ts, assuming a perfe t duality between buyer and seller:

Buyer = (ship ∨ refund) ։ pay Seller = pay ։ (ship ∨ refund)

The above two ontra ts lead to an agreement, whi h allows the buyer for pay- ing, and the seller for shipping or issuing a refund. Instead, in [9℄ the ontra ts of the buyer and of the seller would take a very di erent form, e.g.:

Buyer = pay. (ship + refund) Seller = pay. (ship ⊕ refund)

Intuitively, this means that the lient will rst output a payment, and then either re eive the item, or re eive a refund (at servi e dis retion). Dually, the servi e will rst input a payment, and then opt for shipping the item or issuing a refund. However, this is very distant from our notion of ontra ts.

First, su h ontra ts are quite rigid, in that they pre isely x the order in whi h the a tions must be performed. Even though in some ases this may be desirable, many real-world ontra ts seem to allow for a more liberal way of

onstraining the involved parties (e.g., I will pay before the deadline ).

Se ond, while the ru ial notion if the ontra ts in [9℄ is ompatibility, in our model we fo us on the inferring the obligations that arise from a set of ontra ts. The key di eren e between the two notions is that, given a set of ontra ts, a

ompatibility he k results in a yes/no output, while inferring the obligations provides a ne-grained quanti ation of the rea hed agreement. For instan e, the obligations may identify who is responsible of ea h a tion mentioned in the

ontra t. We an then exploit this information to take some re xxxxx a tion against lients and servi es whi h do not respe t their promises.

A lot of work addresses the problem of managing servi e failures in long- running business transa tions, see e.g. [10, 5, 7, 6℄. Sin e, in a long-lived trans- a tion, the standard rollba k me hanism of database systems does not s ale, the idea is to partition the long transa tion into a sequen e of smaller transa tions, ea h of whi h is asso iated with a given ompensation [16℄. Compensations are re xxxxx a tions spe i ed by the servi e designer, that will be run upon failures of the standard exe ution. For instan e, we an model our buyer-seller s enario as follows in Compensating CSP [7℄. The seller xxxxxx the buyer redit ard, and then pro eeds by shipping the ordered item. Simultaneously, the seller performs an availability he k, to see whether the ordered item is in sto k. If the item is not available, the servi e throws an ex eption, whi h triggers the

ompensation refundAmount. This ompensation restores the original state of the buyer a ount, so it will a tually perform a transa tion rollba k:

Seller = [ availCheck; (ok; SKIPP notOk; THROWW )

|| (debitAmount ÷ refundAmount) ]; ship

Noti e that the hoi e of the ompensation is ru ial; while refundAmount may be a eptable by any lient, if the ompensation was instead just a 15%Discount on the next order, then not all the lients would have been perfe tly happy. A tually, our main riti ism to long-running transa tions is that lients have absolutely no ontrol on the ompensations provided by servi es.

In our vision, instead, lients have the right to sele t those servi es that o er the desired ompensations. For instan e, we may exploit our logi to model the

ontra t of a buyer that will pay provided that, if the ordered item is unavailable, then she will obtain a full refund, as well as a 15% dis ount on the next order:

Buyer =

unavailable → (refund ∧ 15%discount)

։ pay

11 Con lusions and Future Work

We have investigated the notion of ontra t from a logi al perspe tive. To do that, we have extended intuitionisti propositional logi with a new onne tive, that models ontra tual impli ation. We have provided the new onne tive with

an Xxxxxxx-style axiomatisation, whi h have allowed us to dedu e, for instan e, that n ontra ting parties, ea h requiring a promise from the other n − 1 parties in order to make its own promise, eventually rea h an agreement. Further interesting properties and appli ation s enarios for our logi have been explored, in parti ular in Se t. 3 and 5.

The main result about our logi is its de idability. To prove that, we have devised a Xxxxxxx-style sequent al ulus for the logi , whi h is equivalent to the Xxxxxxx-style axiomatisation. De idability then follows from the subformula property, whi h is enjoyed by our Xxxxxxx rules, and by a ut elimination theo- rem, whi h we have proved in full details in this paper. As a further support to our logi , we have implemented a proof sear h algorithm, whi h de ides if any given formula is a tautology or not.

Our logi for ontra ts has served as a basi building blo k for designing a

al ulus of ontra ting pro esses [4℄. This is an extension of Con urrent Con- straints, featuring a pe uliar me hanism for the fusion of variables, whi h well suites to formalise ontra t agreements. Our al ulus is expressive enough to model a variety of typi al s enarios, and to en ode some ommon idioms for

on urren y, among whi h the π- al ulus and graph rewriting.

11.1 Future Work

While designing the logi for ontra ts proposed in this paper, our main on-

xxxx were to give a minimal set of rules for apturing the notion of ontra t agreement, and at the same time preserving the de idability of IPC.

We expe t that many useful features an be added to our logi , to make it suitable for modelling omplex s enarios, whi h are not dire tly manageable with the basi primitives presented here. Of ourse, preserving the de idability of the logi will be a major on ern, while onsidering these extensions. We dis uss below some of the additional features whi h we think to be more useful in the future developments of our logi .

First order features. A signi ant extension to our logi would be that of extending it with predi ates and quanti ers. This will allow us to model more a urately several s enarios, where a party issues a generi ontra t that an be mat hed by many parties. While this rst order extension shall for e us to drop the de idability result, we expe t to nd interesting de idable fragments of the logi , through whi h modelling many relevant situations.

For instan e, onsider an e- ommer e s enario, where a seller promises to ship the pur hased item to a given address, provided that the ustomer will pay for that item. Aiming at generality, we make the seller ontra t parametri with respe t to the item, ustomer and address. This ould be modelled using a universal quanti ation over these three formal parameters:

Seller = ∀item, customer, address :

pay(item, customer, address ) ։ ship(item, address )

(34)

Now, assume that a ustomer (say, Xxx) promises that he will pay for a drill, provided that the seller will ship the item to his address. This is modelled by the following ontra t issued by Xxx, where the a tual parameters remark that

the a tual payment is made by Xxx, and that the destination address is Xxx'x.

Bob = ship(drill, bobAddress) ։ pay(drill, Xxx, bobAddress)

Joining the two two ontra ts above will yield the intended agreement, that is:

Seller ∧ Bob → pay(drill, Xxx, bobAddress) ∧ ship(drill, bobAddress)

Consider now an atta ker wanting to mali iously exploit the seller ontra t, in order to re eive a free item, and to make the unaware ustomer Bob pay for it. To do that, the atta ker issues the following ontra t:

FakeBob = ship(10Kdiamond, fakeAddress)

։ pay(10Kdiamond, Xxx, fakeAddress)

Joining the seller and the atta ker ontra ts will then ause an unwel ome sit- uation for Xxx, who is due to pay for a 10K diamond, whi h will be shipped to the atta ker's address:

Seller ∧ FakeBob → pay(10Kdiamond, Xxx, fakeAddress) ∧

ship(10Kdiamond, fakeAddress)

To ope with this situation, we ould require that ea h ontra t p is signed by the prin ipal A who issues it, i.e. it has the form A says p. Revisiting our example with this tri k, in the safe ase that Xxx himself has ordered the item, we would expe t to dedu e:

Seller ∧ Xxx → Xxx says pay(drill, Xxx, bobAddress)

In this ase, we have a su essful transa tion, be ause Xxx is stating that he will pay for his drill. Instead, joining the seller and the atta ker ontra ts produ es:

Seller ∧ FakeBob →

FakeBob says pay(10Kdiamond, Xxx, fakeAddress)

Now, it is easy to realize that someone has attempted a fraud, be ause the prin ipal who has signed the ontra t (FakeBob) is di erent from that who is due to pay (Xxx).

Expli it time. Time is another useful feature that may arise while modelling real-world s enarios. For instan e, in an e- ommer e transa tion, a ontra t may state that if the ustomer returns the pur hased item within 10 days from the pur hase date, then she will have a full refund within 21 days from then.

We would like to model su h a ontra t in a temporal extension of our logi , so to reason about the obligations that arise when the deadlines expire. Ba k to our e- ommer e example, we ould imagine to express the seller's ontra t as the following formula, where the parameter t in p(t) tells the point in time where the event p o urs:

Seller (t) : ∀t′ : (pay(t) ∧ return(t′) ∧ t′ < t + 10) ։ ∃t′′ < t′ + 21 : refund(t′′)

From the point of view of the buyer, the ontra t says that the buyer is willing to pay, provided that she an obtain a full refund (within 21 days from the

date of payment), whenever she returns the item within 7 days from the date of payment:

Buyer (t) : ∀t′ : (return(t′) ∧ t′ < t+10 → ∃t′′ < t′ +21 : refund(t′′)) ։ pay(t)

We expe t our extended logi able to dedu e that, in the presen e of an agreement (i.e. a ompleted e- ommer e transa tion) between the ustomer and the seller on (say) January the 1st, 2009, if the ustomer has returned the pur hased item on January the 5th, then the seller is required to issue a full refund to the ustomer within January, the 26th. This ould be modelled by the formula:

Buyer (1.1.09) ∧ Seller (1.1.09) ∧ return(5.1.09) → refund(26.1.09)

There are a number of te hniques aimed at the expli it representation of time in logi al systems, so we expe t to be able to reuse some of them for extending PCL. These te hniques range from Temporal Logi [14℄, to more re ent approa hes on temporal extensions of authorization logi s like [13℄.

Pro ess al uli and ontra ts. In this paper we have fo ussed our attention on logi s-based formalisms for modelling ontra ts, and for de iding when they lead to an agreement among the involved parties. However, our investigation on ontra ts is still at its beginnings, and in future work we plan to study, along with logi s for ontra ts, programming languages that exploit their features. As a rst attempt towards this dire tion, we have designed in [4℄ a ore al ulus for ontra t-based omputing.

In the future, we will ontinue to develop pro ess al uli for ontra ts, in parti ular to des ribe the behaviour of pro esses in the presen e of atta kers. All the extensions we shall onsider will have to preserve some hara terizing features, e.g. the ability of publishing and stipulating ontra ts, that of de iding whether a given formula is on duty, and that of taking re xxxxx a tions in the

ase a ontra t is not respe xxx.

We plan to develop analysis te hniques to formally and automati ally prove the orre tness of the servi e infrastru ture, e.g. that the ontra ts are always respe ted, without the need for resorting to third parties (e.g. legal o es) external to the model.

A knowledgements

This work has been partially supported by EU-FETPI Global Computing Proje t IST-2005-16004 SENSORIA (Software Engineering for Servi e-Oriented Over- lay Computers) and by the MIUR-PRIN proje t SOFT (Te ni he Formali Ori- entate alla Si urezza).

Referen es

[1℄ Mart n Abadi, Mi hael Xxxxxxx, Xxxxxx Xxxxxxx, and Xxxxxx Xxxxxxx. A

al ulus for a ess ontrol in distributed systems. ACM Transa tions on Programming Languages and Systems, 4(15):706 734, 1993.

[2℄ Mart n Abadi and Xxxxxx Xxxxxxx. Composing spe i ations. ACM Trans- a tions on Programming Languages and Systems, 15(1):73 132, 1993.

[3℄ Mart n Abadi and Xxxxxx X. Xxxxxxx. A logi al view of omposition. The- oreti al Computer S ien e, 114(1):3 30, 1993.

[4℄ Xxxxxxx Xxxxxxxxxx and Xxxxxxx Xxxxxx. A al ulus of ontra ting pro-

esses. Te hni al Report DISI-09-056, DISI - Universit di Trento, 2009.

[5℄ Xxxxx Xx hi, Xxxxxx Xxxxxx, and Xxxxxxxxx Xxxxxxxxx. A al ulus for long running transa tions. In Pro . FMOODS, 2003.

[6℄ Xxxxxxx Xxxxx, Hern n C. Xxxxxxxxx, and Xxx Xxxxxxxxx. Theoreti al foundations for ompensations in ow omposition languages. In Pro . POPL, 2005.

[7℄ Mi xxxx X. Xxxxxx, X. X. X. Xxxxx, and Xxxxx Xxxxxxxx. A tra e seman- ti s for long-running transa tions. In 25 Years Communi ating Sequential Pro esses, 2004.

[8℄ Xxxxxxx Xxxxxxxxx and Xxxxxx Xxxxxx. A basi ontra t language for web servi es. In Pro . ESOP, 2006.

[9℄ Xxxxxxxx Xxxxxxxx, Xxxx Xxxxxxx, and Xx x Xxxxxxxx. A theory of on- tra ts for web servi es. ACM Transa tions on Programming Languages and Systems, 31(5), 2009.

[10℄ Xxxxx Xxxxxxxx, Xxxxxxxxx Xxx n, Xxxxx Xxxxx, Xx xxxx X. Xxxxxx, Xxxxx Xxxxxxxx, and Xxxxx Xxxxxxxxx. Extending the on ept of transa tion om- pensation. IBM Systems Journal, 41(4):743 758, 2002.

[11℄ Aspassia Daskalopulu and Xxx Xxxxxxx. Towards ele troni ontra t performan e. In Pro . 12th International Workshop on Database and Expert Systems Appli ations, 2001.

[12℄ Xxxxx Xxxxx u, Mi hael Xxxxx, and I.V. Xxxxxxxxxxxx. CTR-S: A logi for spe ifying ontra ts in semanti web servi es. In Pro . WWW04, 2004.

[13℄ Xxxxx XxXxxxx, Xxxxxx Xxxx, and Xxxxx Xxxxxxxx. An authorization logi with expli it time. In Pro . CSF, 2008.

[14℄ E. Xxxxx Xxxxxxx. Temporal and modal logi . In Handbook of Theoreti al Computer S ien e, Volume B: Formal Models and Xxxxxx s (B), pages 995 1072. North-Xxxxxxx Pub. Co./MIT Press, 1990.

[15℄ Xxxx Xxxxxxxxxx and Xx xxxx Xxxxxxx. Propositional lax logi . Information and Computation, 137(1):1 33, 1997.

[16℄ He xxx Xxx xx-Xxxxxx and Xxxxxxx Xxxxx. Sagas. In SIGMOD Conferen e, 1987.

[17℄ Xxxxxx Xxxx and Mart n Abadi. A modal de onstru tion of a ess ontrol logi s. In Pro . FoSSaCS, pages 216 230, 2008.

[18℄ Xxxxxxxx Xxxxxx, Xxxxxxxx Xxxxxx, Xxxxxxxx Xxxxxx, and Xxxxx Xxxxxxx- xxxx. Normative autonomy and normative o-ordination: De larative power, representation, and mandate. Arti ial Intelligen e and Law, 12(1-2):53 81, 2004.

[19℄ Xxxxxxxx X. Xxxxxxxxx and Aspassia Daskalopulu. The representation of e- ontra ts as default theories. In New Trends in Applied Arti ial Intelli- gen e, 2007.

[20℄ Xxxx X del. Eine interpretation des intuitionistis hen aussagenkalkuls.

Ergebnisse eines mathematis hen Kolloquiums, 8:39 40, 1933.

[21℄ Xxxxx Xxxxxxxxxxx. Representing business ontra ts in RuleML. Interna- tional Journal of Cooperative Information Systems, 14(2-3), 2005.

[22℄ Xxxxx Xxxxxxxxx, Xxxxxxx X xxx, Xxxxxx X xxxxxxxxxx, and Xx xxxx Xxxxxxxx. A logi s workben h. AI Communi ations, 9(2):53 58, 1996.

[23℄ Xxxxxxx Xx, Xxxxxxxx X. Xxxxxx, and Xxxx Xxxxxxxxxx. Delegation logi : A logi -based approa h to distributed authorization. ACM Transa tions on Information Systems Se urity, 6(1):128 171, 2003.

[24℄ Xxxx Xxx xxxxxxx. Intuitionisti logi . In Xxxxxx X. Xxxxx, editor, The Stanford En y lopedia of Philosophy. 2008.

[25℄ Lu a Padovani. Contra t-based dis xxxxx and adaptation of web servi es.

In SFM, 2009.

[26℄ The PCL web site. xxxx://xxx.xxxx.xxxxx.xx/∼zunino/PCL.

[27℄ Xxxxx Xxxxxxxx. Stru tural ut elimination - I. intuitionisti and lassi al logi . Information and Computation, 157(1/2):84 141, 2000.

[28℄ Xxxxxxxx Xxxxx xxxx and Xxxxxxx X xxxxxxx. A formal language for ele troni

ontra ts. In Pro . FMOODS, 2007.

[29℄ Ri hard Xxxxxxx. Intuitionisti propositional logi is polynomial-spa e

omplete. Theoreti al Computer S ien e, 9:67 72, 1979.

[30℄ Xxxx Xxxxxxxxx and Xxxx xxx Xxxxx. Constru tivism in Mathemati s, vol.

1. North-Xxxxxxx, 1988.

A Appendix

A.1 Adapting Pfenning's Notation

For ompleteness, we show here how to adapt the notation of [27℄, Appendix 1, to ours. As an example, we adapt the essential ase ∧R/ ∧ L1. All the other

ases are similarly dealt with. In [27℄ we nd the redu tion

N N3 N4

Γ→A1 Γ→A2 ∧ R ⊗

Γ → (A1 ∧ A2)

Γ,(A1 ∧A2 ),A1 →A

Γ, (A1 ∧ A2) → A

∧ L1 ⇒ N2

Γ → A

N N3

Γ,A1 →A1 Γ,A1 →A2

Γ, A1 → (A1 ∧ A2)

∧ R ⊗ N4

Γ, (A1 ∧ A2), A1 → A

⇒ N1

Γ, A1 → A

Γ → A1

⊗ N1

Γ, A1 → A

⇒ N2

Γ → A

whi h we an read as follows. The sign ⊗ in the rst line is the redu ible

ut, the sign → is our ⊢, while N, N3, N4 are the subderivations from whi h we want to onstru t N2. This is done in the next lines. First, a re ursive all

is made in the se ond line using N, N3, N4 in order to obtain N1. Note that the rightmost derivation w.r.t. ⊗ is smaller now. Then, N1 is used in another re ursive all in the third line, together with N, to onstru t N2. Here instead the ut formula A1 is smaller than (A1 ∧ A2).

In our notation, we rephrase the above as:

N N3 N4

Γ ⊢ A1 Γ ⊢ A2 ∧ R Γ, A1 ∧ A2, A1 ⊢ A ∧ L1

Γ ⊢ A1 ∧ A2 Γ, A1 ∧ A2 ⊢ A cut =⇒

Γ ⊢ A

N + N3+

Γ, A1 ⊢ A1 Γ, A1 ⊢ A2 ∧ R N4

Γ ⊢ A1

Γ, A1 ⊢ A1 ∧ A2

Γ, A1 ⊢ A

Γ, A1, A1 ∧ A2 ⊢ A cut1

Γ ⊢ A cutp

A.2 The PCL Tool

To experiment with our logi , we developed a theorem prover for PCL. To prove (or refute) a formula p, it tries to onstru t a derivation of ∅ ⊢ p using the rules of the sequent al ulus. The derivation is onstru ted in a bottom-up fashion, through an exhaustive sear h of the proof spa e. We avoid potential loops (e.g. repeating weakL forever) by pruning the bran hes whi h would lead

to a derivation having a double o urren e of the same sequent in a root-to-leaf path. In other words, we look for minimal proofs. Lemma 6.14 ensures this is a sound and omplete pro edure to he k for validity in PCL. When a derivation is found, it is provided as output. When the whole proof spa e is exhausted unsu essfully, a no derivation message is printed.

This simple proof-sear h te hnique is ine ient in the worst ase. Indeed, PCL is a onservative extension of IPC (Lemma 6.16), so the problem is no easier than he king validity in IPC, whi h is known to be PSPACE-hard [29℄. In all our examples, however, we were able to apply the tool, whi h required only a few se onds to omplete. In our experiments, a depth- rst proof sear h performed worse than a depth- rst sear h, so we adopted the latter in our tool. The urrent prototype onsists of about 600 lines of Xxxxxxx sour e ode.

The tool is made available as free software from [26℄. Below we show a simple session with the PCL tool:

> P l '(((a ->> b) /\ (b ->> a)) -> (a /\ b))'

Formula: (((a ->> b) /\ (b ->> a)) -> (a /\ b)) Result

> P l '(((p ->> q) /\ (p ->> r)) -> (p ->> (q /\ r)))'

Formula: (((p ->> q) /\ (p ->> r)) -> (p ->> (q /\ r))) NoResult

> # High verbosity prints sear h progress and LaTeX derivation

> P l --verbosity=4 '((p ->> q) -> ((q -> p) -> q))'

Formula: ((p ->> q) -> ((q -> p) -> q)) 1

Result (LaTeX follows):

\dfra {\dfra {\dfra {\dfra {\dfra {}{q, (q \imp p), (p \ oimp q) \vdash q} id...

The last derivation renders as

q, (q → p), (p ։ q) ⊢ q id p, q, (q → p), (p ։ q) ⊢ p id

q, (q → p), (p ։ q) ⊢ p → L q, (q → p), (p ։ q) ⊢ q id

(q → p), (p ։ q) ⊢ q Fix

(p ։ q) ⊢ ((q → p) → q) → R

⊢ ((p ։ q) → ((q → p) → q)) → R

A.2.1 Auxiliary Results for PCL

Here is the input le we used to prove the negative results in the paper with our PCL tool.

#!/bin/sh

P l '((p -> q) -> (p ->> q))'

P l '((p -> q) -> ((q -> r) -> (p ->> r)))'

P l '((p ->> (q \/ r)) -> ((p ->> q) \/ (p ->> r)))'

P l '(((p ->> q) /\ (p ->> r)) -> (p ->> (q /\ r)))'

P l '(( ->> ( ->> p)) -> ( ->> p))'

A.3 Formal Proofs in LWB

Sometimes in our proofs we rely on a theorem prover for he king IPC or S4 tautologies. To this purpose we used the Logi s WorkBen h tool (LWB) [22℄. We provide here the sour e ode we used to perform these he ks. The output of the tool, whi h in ludes the long, detailed, formal proofs is also available online [26℄.

A.3.1 Auxiliary Results in IPC

# For proof generation, un omment this. # generateDetailedProof :== true;

load(ip );

if generateDetailedProof then set("infolevel", 4); # Debug.

pro : tra e(x) begin #print(x); return x;

end;

# translate a formula pro : transl(A, phi) begin

if (phi[0℄ = AND) then

return (transl(A, phi[1℄) & transl(A, phi[2℄)); if (phi[0℄ = OR) then

return (transl(A, phi[1℄) | transl(A, phi[2℄)); if (phi[0℄ = IMP) then

return (transl(A, phi[1℄) -> transl(A, phi[2℄));

if (phi[0℄ = EQ) then

return transl(A, (phi[1℄ -> phi[2℄) & (phi[2℄ -> phi[1℄) ); if (phi[0℄ = SYMBOL) then

return phi;

if (phi[0℄ = imp) then begin

lo al a, b;

a := transl(A, phi[1℄); b := transl(A, phi[2℄); return A{a/p}{b/q}; end;

print("ERROR transl!!!!");

print(phi[0℄); return phi[0℄; end;

# Test whether A is sound pro : test(A)

begin

# axioms: Zero, Fix, PrePost

if not provable(tra e(transl(A, imp(true,true)))) then return false;

if not provable(tra e(transl(A, imp(p,p) -> p))) then return false;

if not provable(transl(A, (p1 -> p) -> imp(p,q) -> (q -> q1) -> imp(p1,q1)))

then return false; return true;

end; #########################################################

# Known mappings interp :==

[ q

, (q->p) -> q

, ((q->p) v r) -> q

, ~~(q->p) -> q

, ~(q->p) v q

℄ ;

sound :== true;

forea h A in interp do begin print("Proving soundness for ",A); if not test(A) then begin

print("unsound: ", A);

sound :== false; end;

end;

if sound then

print("#### All mappings are sound.");

print("Proving independen e"); interp2 :== interp;

indep := true;

while not (interp2 = [℄) do begin A :== pop(interp2);

forea h B in interp2 do

if provable(transl(A, imp(p,q)) <-> transl(B, imp(p,q))) then begin indep :== false;

print("NOT independent: ", A, " AND ", B);

end;

if indep then

print("#### All mappings are independent."); quit;

A.3.2 Auxiliary Results in S4

# Sear h for all the sound S4 mappings of ontra tual impli ations # of the form

# qs[1℄ ( qs[2℄ ( qs[3℄ q -> qs[4℄ p ) -> qs[5℄ q )

# where qs are modalities among identity, box, and diamond.

# The mapping is an extension of the standard IPC-to-S4 mapping. #

# For proof generation, un omment this. # generateDetailedProof :== true;

load(s4);

if generateDetailedProof then set("infolevel", 4);

# apply a modality q (one of i,b,d) to a formula pro : appMod(q, phi)

begin

if q = i then return phi;

if q = b then return box phi; if q = d then return dia phi; print("ERROR appMod"); print(q);

end;

# translate a imp using the modalities in qs pro : translCoimpl(qs,p,q)

begin

return appMod(qs[1℄,

( appMod(qs[2℄, (appMod(qs[3℄, q) -> appMod(qs[4℄, p)))

appMod(qs[5℄, q)

));

end;

# translate a formula using the modalities in qs pro : transl(qs, phi)

begin

if (phi[0℄ = AND) then

return (transl(qs, phi[1℄) & transl(qs, phi[2℄)); if (phi[0℄ = OR) then

return (transl(qs, phi[1℄) or transl(qs, phi[2℄)); if (phi[0℄ = IMP) then

return box (transl(qs, phi[1℄) -> transl(qs, phi[2℄)); if (phi[0℄ = EQ) then

return transl(qs, (phi[1℄ -> phi[2℄) & (phi[2℄ -> phi[1℄) ); if (phi[0℄ = NOT) then

return box ~ transl(qs, phi[1℄);

if (phi[0℄ = SYMBOL) then return box phi;

if (phi[0℄ = imp) then

begin

lo al p, q;

p := transl(qs, phi[1℄);

q := transl(qs, phi[2℄); return translCoimpl(qs,p,q); end;

print("ERROR transl!!!!");

print(phi[0℄); return phi[0℄; end;

# Test whether the modalities qs give rise to a sound imp pro : test(qs)

begin

# axioms: Zero, Fix, PrePost

if not provable(transl(qs, imp(true,true))) then return false;

if not provable(transl(qs, imp(p,p) -> p)) then return false;

if not provable(transl(qs, (p1 -> p) -> imp(p,q) -> (q -> q1) -> imp(p1,q1)))

then return false; return true;

end;

###########################################

# main loop

mods :== [ i , b , d ℄ ; # modalities: identity, box, dia sound :== 0 ;

tot :== 0 ;

sol :== [℄;

forea h q0 in mods do forea h q1 in mods do

forea h q2 in mods do forea h q3 in mods do

forea h q4 in mods do begin

lo al x;

x :== [q0,q1,q2,q3,q4℄; tot :== tot + 1;

if test(x) then

begin

sound :== sound + 1;

sol :== on at(sol,[x℄); end;

end;

print("Total formulas: ", tot); print("Sound formulas: ", num); #print(sol);

# remove redundant solutions (quotient up to <->)

sol2 :== [℄;

forea h s in sol do begin

found :== false;

forea h s2 in sol2 do

if provable(transl(s, imp(p,q)) <-> transl(s2, imp(p,q))) then found :== true;

if not found then

sol2 :== on at(sol2, [s℄); end;

print("Sound formulas up to <->: ", nops(sol2)); print(sol2);

forea h s in sol2 do

print(transl(s, imp(p,q)));

print("Completeness he k"); xxxxx h s in sol2 do begin

omplete :== true;

# we try several formulas that are not PCL theorems if provable(transl(s, imp(a,b) <-> b )) then # 1

omplete :== false;

if provable(transl(s, imp(a,b) <-> (~(b->a) or b) )) then # 2

omplete :== false;

if provable(transl(s, imp(a,b) <-> ((b->a)->b) )) then # 3

omplete :== false;

if provable(transl(s, imp(a,b) <-> (~~(b->a)->b) )) then # 4

omplete :== false; if not omplete then

print("Formula ", s, " is not omplete."); else

print("Formula ", s, " MIGHT be omplete.");

end; quit;

Document Metadata

Table of Contents

DIPARTIMENTO DI INGEGNERIA E SCIENZA DELL’INFORMAZIONE

Document Metadata