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 anat
instead of converting them toType
.
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: Sep 30 2023 at 06:01 UTC