0

I have entered the following code in CoqIde:

Require Export Classical. 
Require Export Description. 

Inductive pbool : Type :=
    T : pbool
    | F : pbool
    | U : pbool.

Variables s p e t f: Type. 

Axiom classical_definite_description :
forall (A : Type) (P : A->pbool), inhabited A ->
{ x : A | (exists! x : A, P x) -> P x }.

I am working in a type theory with three truth values: true, false and undefined. Hence I created a type pbool as above. However I also require a definite description (Hilbert's iota) operator that returns exactly one element from a set of objects.

In the axioms above I initially had Prop and changed it to pbool. I then receive the error that The term "P x0" has type "pbool" while it is expected to have type "Prop". How can I change the definition of the description operator so that it works with pbool?

2
  • The only sorts in Coq are Prop, Set, and the Type hierarchy (and also SProp if experimental strict propositions are enabled). If you want to shallow-embed a logic into Coq, you have to add axioms such that one of these existing sorts acts like your desired notion of proposition. I don't know whether this can be done in your case; you might have to tell us more about the logic you have in mind.
    – mudri
    Mar 11 at 19:05
  • @mudri Thanks. The logic I am trying to model is described here: projecteuclid.org/journals/notre-dame-journal-of-formal-logic/… It
    – user65526
    Mar 12 at 8:57

0

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.