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

13 hours 4 min ago

14 hours 5 min ago

21 hours 45 min ago

1 day 19 hours ago

2 days 30 min ago

2 days 18 hours ago

2 days 19 hours ago

2 days 19 hours ago

2 days 20 hours ago

2 days 20 hours ago