LRC

This is where it all started: the system from the logic class I took at the University of Minnesota in the summer after 9th grade, as I remember it decades later. I believe the system was Pospesel amd will implement that properly at some point. This one does Lemmon derivations as I remember them as well as the Fitch derivation you see here. I worked with this system exclusively from the fall of 2020 until well into the second year of the LRC project. Uses old fashioned Reductio and DNE for negation.

Constants

~&∨⊃≡∀∃=

Example Formula

∀x∀y(x=y⊃(Lx≡Ly))

Term Extensions

F'a''x'''

Allow Open Sentences

No

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 IntroductionRAA: Reductio Ad AbsurdumDNE: Double Negation Elimination≡E: Biconditional Elimination≡I: Biconditional Introduction∃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 IntroductionRAA: Reductio Ad AbsurdumDNE: Double Negation Elimination≡E: Biconditional Elimination≡I: Biconditional Introduction∃E: Existential Elimination∃I: Existential Introduction∀E: Universal Elimination∀I: Universal Introduction=E: Identity Elimination=I: Identity Introduction