Articles of proof theory

Proof negation in Gentzen system

I am provided with the L¬ and R¬ Gentzen rules for negation (besides “Cut” rule and some rules for ⋀ and →): $${\Gamma\vdash\Delta,\varphi\over \Gamma,\lnot\varphi\vdash \Delta}\ L\lnot \\[4ex] {\Gamma,\varphi\vdash\Delta\over \Gamma\vdash\Delta\lnot\varphi}\ R\lnot $$ I’m trying to proof: $${\Gamma,\lnot\lnot q\vdash\Delta\over \Gamma,q\vdash \Delta}$$ However, I did not manage to this with the provided rules. Does anyone have an idea […]

Complexity of verifying proofs

My question can be read on many levels and so I welcome answers to any reading. The general question is: What is the computational complexity of verifying a proof? One way of looking at a computational complexity class (for decision problems) is that is is a set of theories (a theory being a set of […]

Quasi-interactive proof on real numbers

[This is a cleaner and simpler restatement of a question I asked earlier on Theoretical CS forum. Please re-tag as appropriate.] Suppose you have two oracles (black boxes) that represent real numbers. Each oracle works like this: you give it integer $n$ and it returns integer $k$ such that $k/n \leq r < (k+1)/n$, where […]

Proof that SAT is NPC

I am not really sure I understand the idea behind Cook theorem (it says that SAT is a NP-complete problem). I read the proof with all its parts corresponding to the Turing machine TM solving it (TM is in a single state at any given time, only single cell is read by the head of […]

Entailment relations that are not partial orders

The derivability relation of classical logic is a partial order, for which: \begin{align} &(i) &&a \vdash a \\ &(ii) &&\text{If} \hspace{0.2cm} a \vdash b \hspace{0.2cm} \text{and} \hspace{0.2cm} b \vdash a, \hspace{0.2cm} \text{then} \hspace{0.2cm} a = b \\ &(iii) &&\text{If} \hspace{0.2cm} a \vdash b \hspace{0.2cm} \text{and} \hspace{0.2cm} b \vdash c, \hspace{0.2cm} \text{then} \hspace{0.2cm} a \vdash c […]

Double Negation is sequent calculus systems LK and LJ

In sequent calculus LK (see Gaisi Takeuti, Proof Theory (2nd ed – 1987)) we have a “standard” derivation of Double Negation in the form $\rightarrow \lnot \lnot A \supset A$. We have to start from an Axiom : $$\frac{A \rightarrow A}{\rightarrow \lnot A, A}$$ by $\lnot$-right; then : $$\frac{\rightarrow \lnot A, A}{\lnot \lnot A \rightarrow […]

Learning how to prove that a function can't proved total?

In proof-theory one can prove that in, say, Peano Arithmetic one can’t prove a function $f$ total. Often this seems to mean $f$ is growing too fast to be provably total. I have some background in logic and know the very basics about formal proofs in FO, but overall I’m more familiar with finite model […]

Ideas about Proofs

If there are two different proofs for one theorem, at some level are the two proofs the same, or can they be fundamentally different? In other words, if you have two proofs of a theorem, can one show that the two proofs are expressing the same thing in different ways, and then remove the redundancies […]

What is this property relating to logical systems called?

See the revised version of this question here. The following property exhibited by some logical systems has captured my attention: $$x_1 \vdash x_2 \text{ if and only if } \vdash (x_1 \rightarrow x_2)$$ for any well-formed formulas $x_1$ and $x_2$. My question is 3-fold: Does this property have a name? If so, what is it […]

What does “rigorous proof” mean?

I have heard several times that some mathematician has given another and more rigorous for an established theorem, but I don’t know what does it really mean and what differences makes it to be more ‘rigorous’. My understanding of a proof is that a proof is some explanation to convincing others that a statement is […]