Questions tagged [classical-logic]
The classical-logic tag has no usage guidance, but it has a tag wiki.
9
questions
1
vote
1
answer
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
5
votes
0
answers
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
2
answers
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
...
6
votes
1
answer
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
3
votes
2
answers
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)
...
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 ...
- 419
5
votes
0
answers
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
7
votes
1
answer
244
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 ...
- 267
16
votes
3
answers
959
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 ...
