Suppose You ask a question beginning from "Why some structure is..." or "Why some object has property..." and several answers arises. Which criteria do You use to qualify which answer is correct? ...
I read about two different versions of the disjunction elimination rule. The first version (http://www.fecundity.com/logic/) says that: if $\Sigma\vdash\phi_0\lor\phi_1$ and ...
I'm looking for a good introductory resource on sequent calculus suitable for someone who has studied natural deduction before. Books and online resources are both OK, as long as each rule of ...
Bourbaki used a very very strange notation for the epsilon-calculus consisting of $\tau$s and $\blacksquare$. In fact, that box should not be filled in, but for some reason, I can't produce a \Box. ...
From time to time, when I write proofs, I'll begin with a claim and then prove the contradiction. However, when I look over the proof afterwards, it appears that my proof was essentially a proof of ...
Strong induction proves a sequence of statements $P(0)$, $P(1)$, $\ldots$ by proving the implication "If $P(m)$ is true for all nonnegative integers $m$ less than $n$, then $P(n)$ is true." for ...
What is the cut rule? I don't mean the rule itself but an explanation of what it means and why are proof theorists always trying to eliminate it? Why is a cut-free system more special than one with ...
Is there a concept of "information" with respect to the axioms of a mathematical system? Suppose we have a universe U of theorems. Suppose an axiom system A=(a1,a2,...) has the universe U as the ...
Are there any good examples of theorems in reasonably expressive theories (like Peano arithmetic) for which it is substantially easier to prove (in a metatheory) that a proof exists than it is ...
I've just been asked for a good example of a situation in maths where using infinity can greatly shorten an argument. The person who wants the example wants it as part of a presentation to the general ...
When constructing proofs using natural deduction what does it mean to say that an assumption or premise is discharged? In what circumstances would I want to, or need to, use such a mechanism? The ...
Many well-known theorems have lots of "different" proofs. Often new proofs of a theorem arise surprisingly from other branches of mathematics than the theorem itself. When are two proofs really the ...