LRC_O

Like the base system LRC_F, but allows open sentences

Constants

¬&∨→↔∀∃=⊥

Example Formula

∀x∀y(x=y→(Lx↔Ly))

Term Extensions

F1a2x3

Allow Open Sentences

Yes

Known Issues

None

Problem Types

Typed Forward Strict DerivationPoint And Click DerivationExperimental Point And Click TableauExperimental Free Tableau

Derivation Rules

Typed Forward Strict

A: AssumptionR: Reiteration&E: Conjunction Elimination&I: Conjunction Introduction∨E: Disjunction Elimination∨I: Disjunction Introduction→E: Conditional Elimination→I: Conditional Introduction↔E: Biconditional Elimination↔I: Biconditional Introduction¬I: Negation Introduction⊥I: Falsum Introduction¬E: Negation Elimination⊥E: Falsum Elimination∃E: Existential Elimination∃I: Existential Introduction∀E: Universal Elimination∀I: Universal Introduction=E: Identity Elimination=I: Identity Introduction

Point And Click

A: AssumptionR: Reiteration&E: Conjunction Elimination&I: Conjunction Introduction∨E: Disjunction Elimination∨I: Disjunction Introduction→E: Conditional Elimination→I: Conditional Introduction↔E: Biconditional Elimination↔I: Biconditional Introduction¬I: Negation Introduction⊥I: Falsum Introduction¬E: Negation Elimination⊥E: Falsum Elimination∃E: Existential Elimination∃I: Existential Introduction∀E: Universal Elimination∀I: Universal Introduction=E: Identity Elimination=I: Identity Introduction