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

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

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)

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.

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`

?

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

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?

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.

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.

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

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

yes

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?

About `weakPost`

and the FMP, how to you plan to establish `ldecidable`

which corresponds to `P x \/ ~ P x`

above, ie logical decidability?

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

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!

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 ?

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

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

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.

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

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.

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

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.

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

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

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

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

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

Ana de Almeida Borges has marked this topic as resolved.

Last updated: Jun 25 2024 at 15:02 UTC