G3cp/G4ip

[+] G3cp/G4ip

It is a proof-search tool for classical and intuitionistic propositional logic which provides proof in sequent style for theorems of these logics. Sequent calculus was invented by brilliant logician Gerhard Genzen in 1934, here you can find an implementation of two cut-free sequent systems G3cp & G4ip, which are different from Gentzen's original systems LK and LJ. Gentzen used sequent calculus to prove the relative consistency of Peano arithmetic (PA).
Dirk van Dalen describes Gentzen with the following words:

"Gentzen was an exponent of the new generation in every regard. A generation which had begun to understand that Gödel wasn’t the end of logic but meant the beginning of a new and rich life of the subject. Gentzen found himself at the summit of the discipline as he brilliantly created methods to put into practice in logic, namely those of natural deduction and sequent calculi. With the help of these methods he saw chances to do what was still to be done after Gödel. He thoroughly investigated the problem of excluding contradictions from arithmetic. The adjective “brilliant” is correct here . . . Gentzen, who without fuss had relegated Hilbert’s age to the museum, was immature in his socio-political development"

Here is a brief presentation of G3cp:
(Note that

Γ

is a set of formulas, we use

Γ, A

for

Γ \cup {A}

, so there is no difference between

Γ, A

and

A, Γ

and also

Γ, A, A

)

Axioms:

\frac{}{P, Γ ⊢ Δ, P}

\frac{}{⊥, Γ ⊢ Δ}

Rules:

\frac{Γ ⊢ Δ, A Γ ⊢ Δ, B}{Γ ⊢ Δ, A \land B} L \land

\frac{A, B, Γ ⊢ C}{A \land B, Γ ⊢ C} R \land

\frac{A, Γ ⊢ Δ B, Γ ⊢ Δ}{A \lor B, Γ ⊢ Δ} L \lor

\frac{Γ ⊢ Δ, A, B}{Γ ⊢ Δ, A \lor B} R \lor

\frac{Γ ⊢ Δ, A B, Γ ⊢ Δ}{A \supset B, Γ ⊢ Δ} L \supset

\frac{A, Γ ⊢ Δ, B}{Γ ⊢ Δ, A \supset B} R \supset

For more informations about the system and also G4ip, see "Structural Proof Theory" by Sara Negri.

How to search a proof

Type a well-formed formula in the input field above and then press the "Search" button, please use | for

\lor

, & for

\land

and > for

\supset

, f for

⊥

, the language has not primitive negation, so for the negation of "A" use

A > f

Make sure the input formula is well-formed, wrap parentheses around each complex sentence.

If your formula is a theorem the leaves of the proof tree must be just axioms, otherwise it is not a provable formula.

Here are some examples, the well-known definition of material implication (A>B)>((A>f)|B):

\frac{\frac{\frac{\frac{A ⊢ A, B, ⊥ B, A ⊢ B, ⊥}{(A \supset B), A ⊢ B, ⊥} L \supset}{(A \supset B) ⊢ (A \supset ⊥), B} R \supset}{(A \supset B) ⊢ ((A \supset ⊥) \lor B)} R \lor}{⊢ ((A \supset B) \supset ((A \supset ⊥) \lor B))} R \supset

The law of explosion or Pseudo-Scotus (A&(A>f))>B:

\frac{\frac{\frac{A ⊢ B, A A, ⊥ ⊢ B}{A, (A \supset ⊥) ⊢ B} L \supset}{(A \land (A \supset ⊥)) ⊢ B} L \land}{⊢ ((A \land (A \supset ⊥)) \supset B)} R \supset

Contraposition ((A>f)>(B>f))>(B>A) :

\frac{\frac{\frac{\frac{B, A ⊢ A, ⊥}{B ⊢ (A \supset ⊥), A} R \supset \frac{B ⊢ A, B B, ⊥ ⊢ A}{(B \supset ⊥), B ⊢ A} L \supset}{((A \supset ⊥) \supset (B \supset ⊥)), B ⊢ A} L \supset}{((A \supset ⊥) \supset (B \supset ⊥)) ⊢ (B \supset A)} R \supset}{⊢ (((A \supset ⊥) \supset (B \supset ⊥)) \supset (B \supset A))} R \supset

De Morgan's law ((A&B)>f)>((A>f)|(B>f)):

\frac{\frac{\frac{\frac{\frac{\frac{A, B ⊢ A, ⊥, ⊥ A, B ⊢ B, ⊥, ⊥}{A, B ⊢ (A \land B), ⊥, ⊥} R \land ⊥, A, B ⊢ ⊥, ⊥}{((A \land B) \supset ⊥), A, B ⊢ ⊥, ⊥} L \supset}{((A \land B) \supset ⊥), B ⊢ (A \supset ⊥), ⊥} R \supset}{((A \land B) \supset ⊥) ⊢ (A \supset ⊥), (B \supset ⊥)} R \supset}{((A \land B) \supset ⊥) ⊢ ((A \supset ⊥) \lor (B \supset ⊥))} R \lor}{⊢ (((A \land B) \supset ⊥) \supset ((A \supset ⊥) \lor (B \supset ⊥)))} R \supset