✔ Encoding a Prop Inductive in Type · Coq users

bi_rec_enum_t_dec
     : forall (X : Type) (P : X -> Prop),
       rec_enum_t P ->
       rec_enum_t (fun x : X => ~ P x) ->
       forall x : X, P x \/ ~ P x -> {P x} + {~ P x}

from the TRAKHTENBROT part of the Library of Undecidability Proofs to show that a certain axiom system is decidable. In order to do that, I first need to show that this axiom system is enumerable in the sense of rec_enum_t:

rec_enum_t =
fun (X : Type) (P : X -> Prop) =>
{Q : nat -> X -> bool | forall x : X, P x <-> (exists n : nat, Q n x = true)}
     : forall X : Type, (X -> Prop) -> Type

In thinking about how to build Q, I was reminded that we can't eliminate Prop stuff to obtain Type stuff. So I need to translate my Prop axiomatizatization into a Type one. I can just re-define it from scratch, but then I'm not clear on how to relate the two definitions.

I hoped that there would already be something similar somewhere in the Undecidability Library, but my grep/Search-foo is failing to find anything.

Does anyone have any suggestions? I decided to ask before I started digging a redefinition hole. cc. @Yannick Forster, @Dominik Kirst

Yannick Forster (Oct 13 2022 at 17:38):

Can you elaborate why you need to redefine your axiomatisation? The function Q would operate on the underlying type X of your axiomatisation, so something like terms. In the function Q the axiomatisation should not occur at all

Yannick Forster (Oct 13 2022 at 17:40):

Unrelated: I wouldn't use rec_enum_t, but rather the equivalent notion of enumerability from the library for all kinds of logical systems (I don't know why this is called rec_enum in the trakhtenbrot paper, we usually call this semi-decidability to avoid confusion)

Ana de Almeida Borges (Oct 14 2022 at 12:17):

My idea was that Q n A should decode n into a proof of A. What a "proof" is depends on how I decide to implement it. I was hoping I could do something better than "a list of formulas where the last is A and every formula before is either an axiom or follows from a rule applied to previous elements of the list". I mean, I already have a notion of "proof" that is a Prop Inductive, so ideally I would use that.

Ana de Almeida Borges (Oct 14 2022 at 12:20):

I was only using rec_enum_t because it's the requirement for bi_rec_enum_t_dec / Posts_thm. Are you saying there is another version of Post's theorem that uses rec_enum?

Ali Caglayan (Oct 14 2022 at 12:40):

If you have a notion of proof as a Prop inductive you won't be able to get a proof term out of that.

Dominik Kirst (Oct 18 2022 at 12:29):

Hi Ana, are you sure you need to enumerate all proofs, or does it suffice to enumerate all provable formulas? We have several versions of the fact that every complete axiom system is decidable (e.g. Fact 9 in this paper), relying on the enumerability of both the provable and refutable formulas. Would that apply to your situation?

Dominique Larchey-Wendling (Oct 19 2022 at 09:50):

I am positively surprised that you found bi_rec_enum_t_dec in the TRAKHTENBROT/enumerable.v devel because it is used there only as a tool for the exercise showing the equivalence between a statement of Post's theorem and a statement of Markov's principle. So you digged quite deeply into that code ;-)

Concerning rec_enum_t vs rec_enum, you do need computable enumerators, ie rec_enum_t, to get a decider of shape { P ...} + { ~ P ...}. Their mere existence is not enough I think.

There are similar results about enumerability elsewhere in the library that the TRAKHTENBROT part does not use unfortunately. Developments occurred somewhat simultaneously and were not synced afterwards. I think this is what @Yannick Forster is referring too, and indeed the corresponding notion is of semi_decider in Synthetic/Definitions.v. Comparing to that file,opt_enum is the same as enumerable but there is no definition corresponding opt_enum_t in Synthetic/Definitions.v which would however be recoverable as fun P => sig (fun f => enumerator f P).

But please notice the equivalence result between rec_enum_t and opt_enum_t stated as opt_rec_enum_equiv_t which holds over data-types (ie, discrete and enumerable types). When X is not a data-type, these notions differ slightly.

I would agree with @Dominik Kirst that you probably do not need to enumerate proofs but just provable/refutable formulas. Enumerating proofs could be quite tedious if those are dependently typed. If they contain functions, this could even prove not possible. But Hilbert style proofs should be ok if you really need to do that.

Is your plan to get decidability as a combination of semantic completeness and the finite model property?

PS: sorry to be late to answer, I am not around Zulip so often and I should improve this.

Ana de Almeida Borges (Oct 19 2022 at 11:07):

I just wanted Post's Theorem, or something similar enough! Apparently what I'm looking for is called weakPost in the Undecidability Library Extended Universe, but is it actually in the main repo? So far I could only find it in this fork and a much older repo.

Ana de Almeida Borges (Oct 19 2022 at 11:08):

Ana de Almeida Borges (Oct 19 2022 at 11:16):

Ana de Almeida Borges (Oct 19 2022 at 11:48):

I guess enumerating all provable formulas would suffice, but how is this easier than enumerating all proofs?

Dominique Larchey-Wendling (Oct 19 2022 at 12:47):

About weakPostand the FMP, how to you plan to establish ldecidable which corresponds to P x \/ ~ P x above, ie logical decidability?

Ana de Almeida Borges (Oct 19 2022 at 12:49):

By assuming classical logic. My completeness proof already assumes it (for now, anyway).

Dominique Larchey-Wendling (Oct 19 2022 at 12:50):

Regarding your question wrt enumerating provable formulas, you could for example enumerate formulas provable with a proof of depth n which involves just decorating your proofs with a nat instead of converting them to Type.

Ana de Almeida Borges (Oct 19 2022 at 12:52):

Dominique Larchey-Wendling (Oct 19 2022 at 12:53):

This is a debate among us (I mean @Yannick Forster, @Dominik Kirst etc) but do you think you actually get a decidability proof if you invoque classical logic, even at the propositional level ?

Ana de Almeida Borges (Oct 19 2022 at 12:54):

Ana de Almeida Borges (Oct 19 2022 at 12:57):

You definitely get something extra, since in general logical decidability doesn't imply full decidability.

Dominique Larchey-Wendling (Oct 19 2022 at 13:05):

Indeed. But then if you actually want to establish logical decidability constructively , you are stuck here. I mean unless you get the FMP from failed terminating proof-search, as could be done in LJT/G4ip for instance, you will not be able to get provable A \/ (provable A -> False) constructIvely. And for LJT, you can prove provable A + (provable A -> False) directly.

We could ask @Dominik Kirst but I do not know a constructive way to convert the FMP into a (strong/+) decidability proof.

Ana de Almeida Borges (Oct 19 2022 at 13:30):

Yup! I agree that constructively proving decidability would require a different approach.

Dominik Kirst (Oct 21 2022 at 10:18):

The most up-to-date version of the first-order logic library is here. It is planned to be turned into a more self-contained package soon, orthogonal to the undecidability library.

Dominik Kirst (Oct 21 2022 at 10:19):

It's perhaps easiest to browse the library via my thesis, most links there point towards the current state.

Dominik Kirst (Oct 21 2022 at 10:22):

You can also use our usual technique with cumulative lists, for instance used here.

Dominik Kirst (Oct 21 2022 at 10:27):

Yep, we had the same issue in our constructive treatment of IEL, see this paper. The FMP can only be used for decidability if completeness is proved first, so if completeness relies on classical assumptions, so does the decidability proof. So in the case of IEL we first proved decidability syntactically via cut-elimination and then derived constructive completeness theorems exploiting decidability.

@Ana de Almeida Borges if you think this helps we can have a Zoom chat about these things at some point :)

Ana de Almeida Borges (Oct 21 2022 at 11:44):

Thanks for the links @Dominik Kirst, I hadn't realized I should be looking at your fork, and having your thesis as a guide will be certainly helpful! I look forward to that package :)

Ana de Almeida Borges (Oct 21 2022 at 11:45):

Dominique's tip of decorating proofs with a nat was the insight I was missing, so now I only need to wrap up the model enumerator and my proof that weak decidability implies strong decidability should be done :)

Ana de Almeida Borges (Oct 21 2022 at 11:46):

Dominique Larchey-Wendling (Oct 24 2022 at 10:13):

Btw you may find Coq tools to manipulate bounded-proof and show there are finitely many of these in Constructive Decision via Redundancy Free Proof-Search. Maybe you will find further some ideas for your applications in there?

Stream: Coq users

Topic: ✔ Encoding a Prop Inductive in Type

Ana de Almeida Borges (Oct 13 2022 at 17:14):