Lengrand & Miquel (2008). Classical FÏ‰, orthogonality and symmetric candidates. Annals of Pure and Applied Logic 153:3-20.

We present a version of system FÏ‰, called FÏ‰^C, in which the layer of type

constructors is essentially the traditional one of FÏ‰, whereas provability

of types is classical. The proof-term calculus accounting for the classical

reasoning is a variant of Barbanera and Berardiâ€™s symmetric Î»-calculus.

We prove that the whole calculus is strongly normalising. For the

layer of type constructors, we use Tait and Girardâ€™s reducibility method

combined with orthogonality techniques. For the (classical) layer of terms,

we use Barbanera and Berardiâ€™s method based on a symmetric notion of

reducibility candidate. We prove that orthogonality does not capture the

fixpoint construction of symmetric candidates.

We establish the consistency of FÏ‰^C, and relate the calculus to the

traditional system FÏ‰, also when the latter is extended with axioms for

classical logic.

## Recent comments

25 min 58 sec ago

1 hour 14 min ago

7 hours 48 min ago

9 hours 33 min ago

17 hours 50 min ago

17 hours 50 min ago

18 hours 25 min ago

20 hours 30 sec ago

22 hours 18 min ago

1 day 1 hour ago