Questions tagged [classical-logic]

The tag has no usage guidance, but it has a tag wiki.

Filter by
Sorted by
Tagged with
14 votes
4 answers
1k views

Open source proof assistants for first order logic with equality and set theory

I have been trying to find open source proof assistants for first order logic with equality and set theory. To date, the closest that I have found is Metamath (http://us.metamath.org/index.html) and ...
user695931's user avatar
6 votes
1 answer
421 views

How important is global choice (a la Lean, HOL Light, Isabelle/HOL) practically?

Choice is indispensable for much of modern classical mathematics. Therefore, most proof assistants offer it as part of their standard library. The most powerful version is sometimes called global ...
Jason Rute's user avatar
  • 8,145
5 votes
0 answers
211 views

An algorithm for the substitution of formulas for predicates in first order logic

I am trying to find a detailed description of the definition of substitution of formulas for predicates in first order logic and an implementation of this as a function in Lean or Haskell. The aim is ...
user695931's user avatar