Add some documentation comments in files

[Gbury]

I'm currently trying to consider using dk_logic.dk as axiomatisation of first-order for proof generated by archsat, and the file seems to be lacking any comment explaining things.

While some constants are pretty intuitive, others are much less so and would greatly benefit from some explanations. Until standard documentation practices emerge from dedukti, it seems that adding some comments would be a good first step, particularly if these files are meant to be used by people who didn't write them, ^^

While I'm there, and since it isn't really mentionned, what logic exactly is encoded in dk_logic ? For instance does it also encode polymorphism ?

[rafoo]

I am not sure that dklib is currently a good target for the following reasons:

• it is a higher-order logic so you do not get the guarantee that the proof does not use higher-order features,
• I am not sure it is consistent; it might be too polymorphic and be subject to Girard paradox.

The second point is not hard to fix, actually it has already been fixed recently in the context of FoCaLiZe.

However, I do not know of an encoding of polymorphic first-order logic in Dedukti that comes with enough formalisation of arithmetics to check SMT proofs. We have either libraries from proof assistants (based on rich logics) or encodings of FOL without arithmetics.

I am interested in the standardisation of the Dedukti encoding of first-order logic so I would be happy to work on adapting dklib to meet your goals. Which first-order theories do you need?

[rafoo]

While I'm there, and since it isn't really mentionned, what logic exactly is encoded in dk_logic ? For instance does it also encode polymorphism ?

The encoded logic is the Calculus of Constructions. The file cc.dk is the standard encoding of the PTS presentation of CoC. In particular, it is a polymorphic logic.

[Gbury]

So I currently have a working axiomatisation (taken mostly from zenon, available here), in which all my proofs can be expressed and typechecked in dedukti (the axiomatisation may be incoherent though, :p ), and in Coq.

Basically, I need:

• logical connectives (negation, implication, conjunction, disjunction, equivalence)
• equality and uninterpreted functions and predicates (equality symmetry, reflexivity, transitivity, and substitution, and function equality to keep small proof simple)
• first-order term quantification and Hilbert's epsilons
• type quantification and Hilbert's epsilons for types
• classic axioms (particularly nnpp, and de Morgan's law for quantifiers).

It is not a problem for the proof to use higher-order, all that matters is that all first-order reasoning can be expressed and checked.

[Gbury]

Arithmetic is not necessary right now. To make proof readable, I guess it would probably need something like AC rewriting, or a way to encode equality modulo normalization of first-degree polynoms.

[Gbury]

So have you had time to read the axiomatisation, and what do you think of it ? (In particular, does it seem consistent ?)

I actually have a question about this encoding: do you think it would be inconsistent to add a function of type : "(a : type): term a", i.e a function which gives a term of any first-order type. Such a function is consistent with usual first-order logic, but in coq without encoding, it is inconsistent I think.

[rafoo]

So have you had time to read the axiomatisation, and what do you think of it ? (In particular, does it seem consistent ?)

Yes, I was afraid I encoded a stronger, inconsistent, PTS in cc.dk but the current version is just good old Calculus of Constructions.

I actually have a question about this encoding: do you think it would be inconsistent to add a function of type : "(a : type): term a", i.e a function which gives a term of any first-order type. Such a function is consistent with usual first-order logic, but in coq without encoding, it is inconsistent I think.

It wouldn't for the same reason than Coq: the type "dk_logic.eeP dk_logic.False" is empty.

Since you do not need arithmetic yet, you might consider the encoding of multisorted FOL that is used in dktactic (https://gitlab.math.univ-paris-diderot.fr/cauderlier/dktactics/tree/master/fol). It does not feature type quantification but I think it should not be hard to add. The axiom you want to add is assumed in file https://gitlab.math.univ-paris-diderot.fr/cauderlier/dktactics/blob/master/fol/inhabited_sorts.dk.

[rafoo]

Another possibility is to target the signature of Holide. Hilbert's choice operator is exactly hol.select.