Stream: Coq users

Topic: ✔ Encoding a Prop Inductive in Type


view this post on Zulip Ana de Almeida Borges (Oct 13 2022 at 17:14):

I'm trying to use

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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip Ana de Almeida Borges (Oct 14 2022 at 12:20):

Re: rec_enum_t vs rec_enum

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?

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Dominique Larchey-Wendling (Oct 19 2022 at 09:50):

Hi @Ana de Almeida Borges ,

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?

Best,

Dominique

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

view this post on Zulip Ana de Almeida Borges (Oct 19 2022 at 11:07):

I am positively surprised that you found bi_rec_enum_t_dec in the TRAKHTENBROT/enumerable.v

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.

view this post on Zulip Ana de Almeida Borges (Oct 19 2022 at 11:08):

(and I only found it by following links in the papers you helpfully cited)

view this post on Zulip Ana de Almeida Borges (Oct 19 2022 at 11:16):

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

yes

view this post on Zulip Ana de Almeida Borges (Oct 19 2022 at 11:48):

are you sure you need to enumerate all proofs, or does it suffice to enumerate all provable formulas?

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

view this post on Zulip 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?

view this post on Zulip Ana de Almeida Borges (Oct 19 2022 at 12:49):

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

view this post on Zulip 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.

view this post on Zulip Ana de Almeida Borges (Oct 19 2022 at 12:52):

I see!

view this post on Zulip Dominique Larchey-Wendling (Oct 19 2022 at 12:53):

By assuming classical logic

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 ?

view this post on Zulip Ana de Almeida Borges (Oct 19 2022 at 12:54):

I've gone back and forth on that many times. :)

view this post on Zulip 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.

view this post on Zulip Dominique Larchey-Wendling (Oct 19 2022 at 13:05):

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

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.

view this post on Zulip Ana de Almeida Borges (Oct 19 2022 at 13:30):

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

view this post on Zulip Dominik Kirst (Oct 21 2022 at 10:18):

Ana de Almeida Borges said:

I am positively surprised that you found bi_rec_enum_t_dec in the TRAKHTENBROT/enumerable.v

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.

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.

view this post on Zulip 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.

view this post on Zulip Dominik Kirst (Oct 21 2022 at 10:22):

Dominique Larchey-Wendling said:

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.

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

view this post on Zulip Dominik Kirst (Oct 21 2022 at 10:27):

Dominique Larchey-Wendling said:

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

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 :)

view this post on Zulip 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 :)

view this post on Zulip 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 :)

view this post on Zulip Ana de Almeida Borges (Oct 21 2022 at 11:46):

Dominik Kirst said:

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

Thanks a lot! I will keep it in mind. For now I'm set. :)

view this post on Zulip Dominique Larchey-Wendling (Oct 24 2022 at 10:13):

Ana de Almeida Borges said:

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 :)

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?

view this post on Zulip Ana de Almeida Borges (Oct 24 2022 at 10:47):

Thank you!!

view this post on Zulip Notification Bot (Oct 24 2022 at 13:40):

Ana de Almeida Borges has marked this topic as resolved.


Last updated: Jun 25 2024 at 15:02 UTC