Questions tagged [classical-logic]

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

Filter by
Sorted by
Tagged with
4 votes
1 answer
144 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 ...
  • 4,690
3 votes
2 answers
106 views

Coq: can `tauto` be used to prove classical tautologies?

When I experiment, I get inconsistent results. Running the following code (with a proof included to double-check that it's provable) ...
12 votes
3 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 ...
5 votes
0 answers
191 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 ...
7 votes
1 answer
221 views

Tracing the classical reasoner in Isabelle

Some time ago I asked this question on Stack Overflow but got no answer: https://stackoverflow.com/questions/60521384/tracing-tactics-in-isabelle Section 9.4 The Classical Reasoner of the Isar ...
  • 173
16 votes
3 answers
851 views

Well-foundedness: classical equivalence of no infinite descent and accessibility

I have often seen the claim that in a classical setting, well-foundedness of a relation > defined as the absence of an infinite descent ...