LK-GL rules

The rules used by the prover are the rules of the Gentzen sequent calculus LK completed by the following rule, which is named necR (necessary right) in the prover
[]Γ, Γ,[]A |-- A
------------------(necR)
[]Γ |-- []A
where A is a formula, Γ is a formula's list, []Γ is the list obtained by adding the sign [] in front of each element of Γ, the sign |-- separates the antecedent list and the succedent list of a sequent.
When we're trying to find a proof, this rule is applied backwards to the critical sequents of the form Λ, []Γ |--Π,[]Δ where Γ and Δ are formula's list, Λ and Π are variables list. This backwards application is actually the below combination of the necR rule and weakening rules
[]Γ, Γ,[]A |-- A
-------------------- where A is member of list Δ
Λ, []Γ |-- Π, []Δ
We give below, as examples, only four of the propositionnal LK rules, implyL, orL with two premisses and implyR, orR with one premisse.
 Γ |-- A, Δ      B, Γ |-- Δ
 ---------------------------(implyL)
 A => B, Γ |-- Δ
A, Γ |-- B, Δ
----------------- (implyR)
Γ |-- A => B, Δ
  A, Γ |-- Δ    B, Γ |-- Δ
  -------------------------(orL)
  A+B, Γ |-- Δ
 Γ |-- A, B, Δ
 --------------(orR)
 Γ |-- A+B, Δ

examples | rules | syntax | info | home | download Last Modified : 17-Dec-2021