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

3 hours 54 min ago

6 hours 38 min ago

6 hours 57 min ago

7 hours 1 min ago

12 hours 50 min ago

2 days 2 hours ago

2 days 6 hours ago

3 days 6 hours ago

3 days 8 hours ago

3 days 14 hours ago