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

10 hours 26 min ago

12 hours 40 min ago

19 hours 14 min ago

1 day 4 hours ago

1 day 6 hours ago

1 day 7 hours ago

1 day 8 hours ago

1 day 9 hours ago

1 day 12 hours ago

1 day 13 hours ago