Questions tagged [classical-logic]

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

Filter by
Sorted by
Tagged with
1 vote
1 answer

How to write this non-constructive proof in Lean?

There is a theorem which says that there exists two irrationals $x, y$ such that $x^y$ is rational. An interesting proof in classical logic is the following: Consider $u = \sqrt{2}^{\sqrt{2}}$. If $u$...
Weier's user avatar
  • 273
5 votes
0 answers

Mere propositions and Consistency with Impredicativity, Excluded Middle and Large Elimination

Setup Current Understanding I've recently been trying to learn about the interaction of Impredicative Polymorphism, Large Elimination and Excluded Middle (notably, inconsistency). Notably, this is ...
idka's user avatar
  • 73
1 vote
2 answers

Partitioning a list with 2 elements in the middle in coq

I am trying to prove some theorems using sequent calculus, for some parts (e.g. cases with Exchange rule) I need a theorem like below ...
asha soroushpoor's user avatar
6 votes
1 answer

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
  • 7,240
3 votes
2 answers

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) ...
Malcolm Sharpe's user avatar
14 votes
4 answers

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 ( and ...
user695931's user avatar
5 votes
0 answers

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
7 votes
1 answer

Tracing the classical reasoner in Isabelle

Some time ago I asked this question on Stack Overflow but got no answer: Section 9.4 The Classical Reasoner of the Isar ...
Gergely's user avatar
  • 267
16 votes
3 answers

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 ...
Théo Winterhalter's user avatar