[+] G3cp/G4ip
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 $\Gamma$ is a set of formulas, we use $\Gamma, A$ for $\Gamma \cup \{A\}$, so there is no difference between $\Gamma,A$ and $A , \Gamma$ and also $\Gamma, A, A$)
(Note that $\Gamma$ is a set of formulas, we use $\Gamma, A$ for $\Gamma \cup \{A\}$, so there is no difference between $\Gamma,A$ and $A , \Gamma$ and also $\Gamma, A, A$)
Axioms:
$ \large \frac{}{P, \ \Gamma \hspace{.1cm} \vdash \Delta, \ P } $
$ \large \frac{}{\bot, \ \Gamma \hspace{.1cm} \vdash \Delta } $
Rules:
$ \large \frac{\Gamma \hspace{.1cm} \vdash \Delta, \ A \hspace{.5cm}
\Gamma \hspace{.1cm} \vdash \Delta, \ B}{ \Gamma \hspace{.1cm}
\vdash \Delta, \ A \land B} \small \ L \land$
$ \large \frac{ A, \ B, \ \Gamma \hspace{.1cm} \vdash C } { A \land
B, \ \Gamma \hspace{.1cm} \vdash C} \small \ R \land$
$ \large \frac{A, \ \Gamma \hspace{.1cm} \vdash \Delta \hspace{.5cm}
B, \ \Gamma \hspace{.1cm} \vdash \Delta}{ A \lor B, \ \Gamma
\hspace{.1cm} \vdash \Delta} \small \ L \lor$
$ \large \frac{ \Gamma \hspace{.1cm} \vdash \Delta, \ A, \ B } {
\Gamma \hspace{.1cm} \vdash \Delta, \ A \lor B} \small \ R \lor $
$ \large \frac{ \Gamma \hspace{.1cm} \vdash \Delta, \ A
\hspace{.5cm} B, \ \Gamma \hspace{.1cm} \vdash \Delta}{ A \ \supset
\ B, \ \Gamma \hspace{.1cm} \vdash \Delta} \small \ L \supset$
$ \large \frac{ A, \ \Gamma \hspace{.1cm} \vdash \Delta, \ B } {
\Gamma \hspace{.1cm} \vdash \Delta, \ A \ \supset \ B} \small \ 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 $\bot$, 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):
$\large \frac{\frac{\frac{\frac{A\hspace{.1cm}\vdash A,B,\bot
\hspace{1cm}B,A\hspace{.1cm}\vdash B,\bot }{(A\supset
B),A\hspace{.1cm}\vdash B,\bot }L\supset }{(A\supset
B)\hspace{.1cm}\vdash (A\supset \bot ),B}R\supset }{(A\supset
B)\hspace{.1cm}\vdash ((A\supset \bot )\lor B)}R\lor
}{\hspace{.1cm}\vdash ((A\supset B)\supset ((A\supset \bot )\lor
B))}R\supset $
The law of explosion or Pseudo-Scotus (A&(A>f))>B:
$\large \frac{\frac{\frac{A\hspace{.1cm}\vdash B,A\hspace{1cm}A,\bot
\hspace{.1cm}\vdash B}{A,(A\supset \bot )\hspace{.1cm}\vdash B}L\supset
}{(A\land (A\supset \bot ))\hspace{.1cm}\vdash B}L\land
}{\hspace{.1cm}\vdash ((A\land (A\supset \bot ))\supset B)}R\supset $
Contraposition ((A>f)>(B>f))>(B>A) :
$\large \frac{\frac{\frac{\frac{B,A\hspace{.1cm}\vdash A,\bot
}{B\hspace{.1cm}\vdash (A\supset \bot ),A}R\supset
\hspace{1cm}\frac{B\hspace{.1cm}\vdash A,B\hspace{1cm}B,\bot
\hspace{.1cm}\vdash A}{(B\supset \bot ),B\hspace{.1cm}\vdash A}L\supset
}{((A\supset \bot )\supset (B\supset \bot )),B\hspace{.1cm}\vdash
A}L\supset }{((A\supset \bot )\supset (B\supset \bot
))\hspace{.1cm}\vdash (B\supset A)}R\supset }{\hspace{.1cm}\vdash
(((A\supset \bot )\supset (B\supset \bot ))\supset (B\supset
A))}R\supset$
De Morgan's law ((A&B)>f)>((A>f)|(B>f)):
$\large \frac{\frac{\frac{\frac{\frac{\frac{A,B\hspace{.1cm}\vdash
A,\bot ,\bot \hspace{1cm}A,B\hspace{.1cm}\vdash B,\bot ,\bot
}{A,B\hspace{.1cm}\vdash (A\land B),\bot ,\bot }R\land \hspace{1cm}\bot
,A,B\hspace{.1cm}\vdash \bot ,\bot }{((A\land B)\supset \bot
),A,B\hspace{.1cm}\vdash \bot ,\bot }L\supset }{((A\land B)\supset \bot
),B\hspace{.1cm}\vdash (A\supset \bot ),\bot }R\supset }{((A\land
B)\supset \bot )\hspace{.1cm}\vdash (A\supset \bot ),(B\supset \bot
)}R\supset }{((A\land B)\supset \bot )\hspace{.1cm}\vdash ((A\supset
\bot )\lor (B\supset \bot ))}R\lor }{\hspace{.1cm}\vdash (((A\land
B)\supset \bot )\supset ((A\supset \bot )\lor (B\supset \bot
)))}R\supset $