# Questions tagged [classical-logic]

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

9 questions
Filter by
Sorted by
Tagged with
1k 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 ...
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 ...
• 429
245 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 ...
• 299
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 ...
• 8,135
227 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
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 ...
• 429
202 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) ...
1 vote
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$...