Skip to Content
ReferenceAll Available Rules

All Available Rules

x,y,zx, y, z are variables, tt is a term, A,BA, B are formulas, and Ξ“,Ξ”\Gamma, \Delta are sequences of formulas.

For rules with suffix L or R, they will manipulate the left or right side of the sequent, respectively.

I

Syntax: I

A⊒A(I)\frac{}{A \vdash A} \text{(I)}

Closes the current goal.

Cut

Syntax: Cut formula

Ξ“βŠ’A,Ξ”A,Ξ“βŠ’Ξ”Ξ“βŠ’Ξ”(Cut)\frac{\Gamma \vdash A, \Delta \quad A, \Gamma \vdash \Delta}{\Gamma \vdash \Delta} \text{(Cut)}

formula is the intermediate formula AA.

AndL1

Syntax: AndL1

A,Ξ“βŠ’Ξ”A∧B,Ξ“βŠ’Ξ”(AndL1)\frac{A, \Gamma \vdash \Delta}{A \land B, \Gamma \vdash \Delta} \text{(AndL1)}

AndL2

Syntax: AndL2

B,Ξ“βŠ’Ξ”A∧B,Ξ“βŠ’Ξ”(AndL2)\frac{B, \Gamma \vdash \Delta}{A \land B, \Gamma \vdash \Delta} \text{(AndL2)}

AndR

Syntax: AndR

Ξ“βŠ’A,Ξ”Ξ“βŠ’B,Ξ”Ξ“βŠ’A∧B,Ξ”(AndR)\frac{\Gamma \vdash A, \Delta \quad \Gamma \vdash B, \Delta}{\Gamma \vdash A \land B, \Delta} \text{(AndR)}

OrL

Syntax: OrL

A,Ξ“βŠ’Ξ”B,Ξ“βŠ’Ξ”A∨B,Ξ“βŠ’Ξ”(OrL)\frac{A, \Gamma \vdash \Delta \quad B, \Gamma \vdash \Delta}{A \lor B, \Gamma \vdash \Delta} \text{(OrL)}

OrR1

Syntax: OrR1

Ξ“βŠ’A,Ξ”Ξ“βŠ’A∨B,Ξ”(OrR1)\frac{\Gamma \vdash A, \Delta}{\Gamma \vdash A \lor B, \Delta} \text{(OrR1)}

OrR2

Syntax: OrR2

Ξ“βŠ’B,Ξ”Ξ“βŠ’A∨B,Ξ”(OrR2)\frac{\Gamma \vdash B, \Delta}{\Gamma \vdash A \lor B, \Delta} \text{(OrR2)}

ImpL

Syntax: ImpL

Ξ“βŠ’A,Ξ”B,Ξ“βŠ’Ξ”Aβ†’B,Ξ“βŠ’Ξ”(ImpL)\frac{\Gamma \vdash A, \Delta \quad B, \Gamma \vdash \Delta}{A \to B, \Gamma \vdash \Delta} \text{(ImpL)}

ImpR

Syntax: ImpR

A,Ξ“βŠ’B,Ξ”Ξ“βŠ’Aβ†’B,Ξ”(ImpR)\frac{A, \Gamma \vdash B, \Delta}{\Gamma \vdash A \to B, \Delta} \text{(ImpR)}

BottomL

Syntax: BottomL

βŠ₯,Ξ“βŠ’Ξ”(BottomL)\frac{}{\bot, \Gamma \vdash \Delta} \text{(BottomL)}

TopR

Syntax: TopR

Ξ“βŠ’βŠ€,Ξ”(TopR)\frac{}{\Gamma \vdash \top, \Delta} \text{(TopR)}

ForallL

Syntax: ForallL term

A[x≔t],Ξ“βŠ’Ξ”βˆ€x.A,Ξ“βŠ’Ξ”(ForallL)\frac{A[x \coloneqq t], \Gamma \vdash \Delta}{\forall x. A, \Gamma \vdash \Delta} \text{(ForallL)}

ForallR

Syntax: ForallR identifier

Ξ“βŠ’A[x≔z],Ξ”Ξ“βŠ’βˆ€x.A,Ξ”(ForallR)\frac{\Gamma \vdash A[x \coloneqq z], \Delta}{\Gamma \vdash \forall x. A, \Delta} \text{(ForallR)}

The variable zz should not occur free in the conclusion.

ExistsL

Syntax: ExistsL identifier

A[x≔z],Ξ“βŠ’Ξ”Ξ“βŠ’βˆƒx.A,Ξ”(ExistsL)\frac{A[x \coloneqq z], \Gamma \vdash \Delta}{\Gamma \vdash \exists x. A, \Delta} \text{(ExistsL)}

The variable zz should not occur free in the conclusion.

ExistsR

Syntax: ExistsR term

Ξ“βŠ’A[x≔t],Ξ”Ξ“βŠ’βˆƒx.A,Ξ”(ExistsR)\frac{\Gamma \vdash A[x \coloneqq t], \Delta}{\Gamma \vdash \exists x. A, \Delta} \text{(ExistsR)}

WL

Syntax: WL

Ξ“βŠ’Ξ”A,Ξ“βŠ’Ξ”(WL)\frac{\Gamma \vdash \Delta}{A, \Gamma \vdash \Delta} \text{(WL)}

Weakening left. Erases the first formula on the left side.

WR

Syntax: WR

Ξ“βŠ’Ξ”Ξ“βŠ’A,Ξ”(WR)\frac{\Gamma \vdash \Delta}{\Gamma \vdash A, \Delta} \text{(WR)}

Weakening right. Erases the first formula on the right side.

CL

Syntax: CL

A,A,Ξ“βŠ’Ξ”A,Ξ“βŠ’Ξ”(CL)\frac{A, A, \Gamma \vdash \Delta}{A, \Gamma \vdash \Delta} \text{(CL)}

Contraction left. Duplicates the first formula on the left side.

CR

Syntax: CR

Ξ“βŠ’A,A,Ξ”Ξ“βŠ’A,Ξ”(CR)\frac{\Gamma \vdash A, A, \Delta}{\Gamma \vdash A, \Delta} \text{(CR)}

Contraction right. Duplicates the first formula on the right side.

PL

Syntax: PL number

A,Ξ“,Ξ“β€²βŠ’Ξ”Ξ“,A,Ξ“β€²βŠ’Ξ”(PL)\frac{A, \Gamma, \Gamma' \vdash \Delta}{\Gamma, A, \Gamma' \vdash \Delta} \text{(PL)}

Permutation left. Moves the formula at the given index number on the left side to the first position.

PR

Syntax: PR number

Ξ“βŠ’A,Ξ”,Ξ”β€²Ξ“βŠ’Ξ”,A,Ξ”β€²(PR)\frac{\Gamma \vdash A, \Delta, \Delta'}{\Gamma \vdash \Delta, A, \Delta'} \text{(PR)}

Permutation right. Moves the formula at the given index number on the right side to the first position.

Last updated on
Using Lapisla