3
$\begingroup$

Is it possible to construct different systems of logic in Coq or Agda?

I ask because I'm interested in using a proof assistant to construct (and verify) theorems in things like many-valued logics, relevant logics, and conditional logics in Graham Priest's 2nd edition of An Introduction to Non-Classical Logic (I keep going back to over the years in my free time).

It seems like intuitionistic logic is definitely possible in Coq given it was developed alongside the calculus of constructions, but I'm curious if Coq (or Agda) could be used for other logics.

A part of my gut says, "It wouldn't be possible to do logics that use fewer rules of inference or swap out intuitionistic rules for incompatible rules (eg, removing the principle of explosion)." However, another part of my gut says, "Machines using binary gates can still represent & simulate quantum processes, so it may be possible for Coq to represent logics incompatible with it's own implementation."

Any references to good papers/books/lectures/etc. are happily welcome. 🙏

Improve this question
$\endgroup$
6
  • $\begingroup$ (You may have more luck finding information about Agda.) $\endgroup$
    – greybeard
    Mar 12, 2022 at 7:43
  • $\begingroup$ What kind of logic are you aiming for? The "default" logic used in Coq is constructive logic (i.e, to prove existence you have to explicitly show an example). But you can add axioms to Coq using the Axiom keyword. But them again, this is only for things you can represent as statements in the Coq programming language, so you can't really have an impossibly weird logic $\endgroup$
    – nir shahar
    Mar 12, 2022 at 9:48
  • $\begingroup$ @nirshahar All kinds really, but I'm particularly interested in paraconsistent logics (ie, the ones that don't have the principle of explosion by excluding rules of inference like disjunctive syllogism or disjunctive introduction). However, removing rules of inference seems like that might be out of the question, so if Coq or Adga can handle most of the stuff that Priest covers then that'll suffice (eg, normal modal logics, non-normal modal logics, conditional logics, intuitionistic logic, many-valued logics, logics with gaps gluts & worlds, relevant logics, fuzzy logics) $\endgroup$
    – Kevin Flowers Jr
    Mar 14, 2022 at 2:36
  • $\begingroup$ Go take a look at the brand new Proof Assistants Stack Exchange. $\endgroup$
    – Pseudonym ♦
    Mar 18, 2022 at 4:30
  • $\begingroup$ If you are willing to go beyond Coq and Agda, you may want to have a look at Dedukti. $\endgroup$
    – Pierre Jouvelot
    Mar 18, 2022 at 9:29

1 Answer 1

Reset to default
6
$\begingroup$

You can define many non-classical logics in Coq (and I assume Agda too), even if they are incompatible with the logic of your proof assistant, but you need to define the concept of inference yourself. That is, you can't rely on Coq formulas, you need to define your own language. And you can't rely on Coq logic, you need to define what counts as a proof. You still use Coq as a meta-language though.

Here is a silly example in Coq with a very restricted language.

(* well-formed formulas *)
Inductive formula : Set :=
  | T : formula
  | AND : formula -> formula -> formula.

(* axioms and rules of inference *)
Inductive provable : formula -> Prop :=
  | TisProvable : provable T
  | ANDI : forall f1 f2, provable f1 -> provable f2 -> provable (AND f1 f2)
  | ANDEl : forall f1 f2, provable (AND f1 f2) -> provable f1
  | ANDEr : forall f1 f2, provable (AND f1 f2) -> provable f2.

You can now show, using the meta-theory of Coq, that provable f for some specific formulas f, or in other words, you can prove theorems of this logic I just made up.

Lemma ANDTTT : provable (AND (AND T T) T).
Proof.
  apply ANDI.
  - apply ANDI; exact TisProvable.
  - exact TisProvable.
Qed.

You can even make Coq automatically prove such simple lemmas:

#[export] Hint Resolve TisProvable ANDI ANDEl ANDEr : provableHints.

Lemma ANDTTT_auto : provable (AND (AND T T) T).
Proof. eauto with provableHints. Qed.

Some examples of non-classical logics implemented in Coq:

Improve this answer
$\endgroup$
4
  • $\begingroup$ This looks very promising, but I need some clarification if you could be so kind. 🙏 When you write Inductive formula : Set :=, you're simply defining what counts as a well-formed formula after that, correct? And when you use Inductive provable : formula -> Prop := you're then defining the rules of inference, right? $\endgroup$
    – Kevin Flowers Jr
    Mar 14, 2022 at 2:47
  • 1
    $\begingroup$ @KevinFlowersJr Yes, exactly. By the way, I added some examples at the end. $\endgroup$
    – Ana Borges
    Mar 14, 2022 at 10:25
  • $\begingroup$ absolutely phenomenal, thank you. 🙏 Looks like you have quite a bit of experience with programming in Coq, so any recommendations for someone new to the syntax? For context, I've played around a bit with Haskell to get a sense of purely functional languages, took some courses in undergrad that were focused on OOP with C++, and now read about category theory stuff (partially for fun & partially with the vague hope it'll be useful for framing things in logic & programming per the Curry-Howard-Lambek correspondance) $\endgroup$
    – Kevin Flowers Jr
    Mar 15, 2022 at 6:47
  • 1
    $\begingroup$ Software Foundations is a good tutorial. Then, as with any programming language, starting a project of your own, in which you are very interested and invested, is probably the best way to gain some experience. For choosing such a project, I would recommend some piece of mathematics that is very elementary, ie, that does not depend on a lot of other things. Formalizing a logic is usually good in this sense. Finally, the best place for resolving Coq questions and interacting with experienced people is the Coq Zulip chat. $\endgroup$
    – Ana Borges
    Mar 15, 2022 at 9:32

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.