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

6 days 2 hours ago

1 week 4 hours ago

1 week 15 hours ago

2 weeks 3 days ago

2 weeks 3 days ago

2 weeks 4 days ago

2 weeks 4 days ago

2 weeks 4 days ago

2 weeks 4 days ago

2 weeks 4 days ago