Add relevant parts of mechanisation of Bailitis' Bachelor's thesis #8
Conversation
| Inductive aand (P Q R : Prop) := | ||
| cconj : P -> Q -> R -> aand P Q R. | ||
|
|
||
| Lemma form_inv {Σ_funcs : funcs_signature} {Σ_preds : preds_signature} {ops : operators} {flag : falsity_flag} phi1 phi2 : |
There was a problem hiding this comment.
this is not necessary (see below)
| Existing Instance falsity_on. | ||
|
|
||
| Instance eqdec_funcs : EqDec PA_funcs_signature. | ||
| Proof. intros x y; decide equality. Qed. |
There was a problem hiding this comment.
note to self: we need to organize these instances somewhere. We can't have each file redefine them, that leads to a bunch of duplicated instances in files downstream of both.
JoJoDeveloping
left a comment
JoJoDeveloping
left a comment
There was a problem hiding this comment.
Thanks a lot for your PR, and sorry for not reacting to this earlier. I have some slight nits in some parts of the proof, but overall it looks good enough.
Just to be sure I understand correctly, the Hilbert System definition currently is not used anywhere else, is it?
|
Thank you very much for reviewing the PR, @JoJoDeveloping.
It's not used elsewhere (apart from the proof that the Hilbert System is equivalent to natural deduction). It will come in handy when the mechanisation is extended by internal provability predicates (something we expect to be working on in the future). And also it's nice to have Hilbert Systems in a logic-related library. I will come back to the other points in due course, but I'm quite busy right now. |
|
Apologies for the extremely late reply, but I finally had the time to have a look at your suggestions; see the comments above. |
|
LGTM. Thanks a lot for addressing the reviews 🎉 |
|
Great, thanks for merging and reviewing the code! |
2 participants
As part of this pull request, the Rocq development of Janis Bailitis' Bachelor's thesis at the programming systems lab shall be contributed to the Rocq Library of First-Order Logic. This contribution consists of two parts: Firstly, A mechanisation of Hilbert systems for FO alongside equivalence proof to ND (in$\mathsf{CT}_\mathsf{Q}$ (see
theories/HilbertSystem). Secondly, a mechanisation of Gödel's first incompleteness theorem and Tarski's theorem via Carnap's diagonal lemma (added to previous development intheories/Incompleteness). This part of the mechanisation also contains a generalisation oftheories/Incompleteness/ctq.v) to functions taking multiple arguments, contained in the filetheories/Incompleteness/multivariate_ctq.v.It may be the case that the files do not match guidelines with respect to code formatting. If so, please point this out.