# Questions tagged [classical-logic]

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

9 questions
Filter by
Sorted by
Tagged with
1 vote
294 views

### 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$...
• 273
213 views

### 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 ...
• 73
1 vote
100 views

### 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 ...
357 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 ...
• 7,240
174 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) ...
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 ...
• 419
205 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 ...
• 419