## Stream: Coq users

### Topic: ✔ Encoding a Prop Inductive in Type

#### 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

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

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`?

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

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.

#### 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.

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

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

#### 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

#### 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?

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

About `weakPost`and 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`.

I see!

#### 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 ?

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

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

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

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.

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

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.

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

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.

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

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

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

#### 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?

Thank you!!

#### Notification Bot (Oct 24 2022 at 13:40):

Ana de Almeida Borges has marked this topic as resolved.

Last updated: Sep 30 2023 at 06:01 UTC