leanlogic

A Lean 4 layer for symbolic logic.

The idea:

• Lean still checks every proof
• users get a much smaller proof vocabulary at the start
• the proof scripts can look closer to natural deduction
• the first few Logic 2010 moves now map to explicit Lean tactics

in here so far

• Leanlogic/ND.lean classroom style helper lemmas such as mp, adj, sl, sr, bc_left, and bc_right
• Leanlogic/Tactics.lean custom tactics like ASS_CD, EI, UI, MP, ADJ, EG, DM, QN, and LL
• Leanlogic/Examples.lean compiled examples showing the layer in use
• Leanlogic/Workbook/Chapter1.lean sentential logic examples keyed to the basic and derived rule handouts
• Leanlogic/Workbook/Chapter2.lean quantifier examples keyed to the quantifier handout and strategy notes
• Leanlogic/Workbook/Chapter3.lean identity examples keyed to the identity handout
• Leanlogic/Workbook.lean one import for the workbook modules
• Leanlogic/Exercises/Week06.lean basic rule exercises based on Logic 2010 and the sample test sheet
• Leanlogic/Exercises/Week07.lean derived rule exercises based on Logic 2010 chapter two style problems
• Leanlogic/Exercises/Week09.lean quantifier exercises based on Logic 2010 chapter three problems
• Leanlogic/Exercises/Week10.lean later quantifier and identity exercises
• Leanlogic/Exercises.lean one import for the week based exercise modules
• Leanlogic/Theorems/Chapter2.lean numbered sentential theorems like T33, T45, T66, and T90
• Leanlogic/Theorems/Chapter3.lean numbered quantifier theorems like T201 to T206 and T231 to T232
• Leanlogic/Theorems.lean one import for the theorem bank
• Leanlogic/TheoremTactics.lean theorem number commands like T 45
• Leanlogic/TheoremDrills.lean compiled examples using numbered theorems
• Leanlogic/Symbolization/Syntax.lean a small symbolic formula language for english to symbols and back
• Leanlogic/Symbolization/Patterns.lean course style builders like unless, only if, all are, and every loves some
• Leanlogic/Symbolization/Examples.lean checked example cards pulled from the local symbolization material
• Leanlogic/Symbolization/Tutorial.lean follow along symbolization examples followed by exercises with sorry
• Leanlogic/Symbolization/Workflow.lean a direct write inspect and check workflow with evals
• Leanlogic/Symbolization/Practice/Easy.lean a logic2010 style easy practice sheet with legends and answer cards
• Leanlogic/Symbolization/Practice.lean one import for the practice sheets
• Leanlogic/Symbolization/Questions/Chapter1Sentential.lean chapter one sentential logic symbolization questions with sorry slots and checks
• Leanlogic/Symbolization/Questions.lean one import for the question banks
• Leanlogic/Symbolization.lean one import for the symbolization layer
• Leanlogic.lean one import that pulls the whole layer in

quick start

From the repo root:

lake +leanprover-community/mathlib4:lean-toolchain build

Then in a Lean file:

import Leanlogic

the tactics

The main tactics currently implemented:

• ASS_CD h introduces an assumption like intro h
• ASS_ID h starts an indirect derivation by assuming the negation of the goal
• UD y introduces a universally quantified variable like intro y
• R h as h3 repetition
• DN h as h3 query style double negation that can introduce or eliminate
• S h as h3 query style simplification that can pick either conjunct
• SHOW φ writes the current goal explicitly as φ
• SHOW_CONC φ a Logic 2010 flavored alias for SHOW
• SHOW_CONS h a Logic 2010 flavored alias for assuming the antecedent of a conditional goal
• DD h direct derivation close step
• CD h conditional derivation close step
• ID h1, h2 closes from an explicit contradiction in either order
• EI h as u, hu opens an existential witness and its fact
• UI hu with t as h5 instantiates a universal statement at t
• SID t proves t = t
• SM h as h5 symmetry of identity
• BC_LEFT h as h5 from P ↔ Q gets P → Q
• BC_RIGHT h as h5 from P ↔ Q gets Q → P
• BC h as h5 query style biconditional conditional step
• BP h1, h2 as h3 biconditional ponens in either direction
• BT h1, h2 as h3 biconditional tollens in either direction
• SL h as h5 gets the left half of a conjunction
• SR h as h5 gets the right half of a conjunction
• MP h1, h2 as h3 modus ponens
• ADJ h1, h2 as h3 conjunction introduction
• CB h1, h2 as h3 biconditional introduction
• DNI h as h3 double negation introduction
• DNE h as h3 double negation elimination
• MT h1, h2 as h3 modus tollens
• HS h1, h2 as h3 hypothetical syllogism
• ADDL h as h3 addition on the left
• ADDR h as h3 addition on the right
• ADDL h with φ as h3 left addition with an explicit parameter like Logic 2010 command mode
• ADDR h with φ as h3 right addition with an explicit parameter like Logic 2010 command mode
• DS_LEFT h1, h2 as h3 disjunctive syllogism using ¬P
• DS_RIGHT h1, h2 as h3 disjunctive syllogism using ¬Q
• MTP h1, h2 as h3 Logic 2010 style modus tollendo ponens in either direction
• NC h as h3 negated conditional in or out
• NB h as h3 negated biconditional in or out
• DM h as h3 demorgan in or out
• CDJ h as h3 corresponding conditional in or out
• SC h1, h2, h3 as h4 separation of cases from a disjunction and two conditionals
• SC h1, h2 as h3 separation of cases from a conditional and its negated antecedent version
• AV h as h3 alphabetical variance for quantifiers
• QN h as h3 quantifier negation in or out
• LL h1, h2 as h3 leibniz for unary predicates
• LL_WITH h1, h2 using (fun z => ...) as h3 leibniz with an explicit abstraction for a chosen argument slot
• EG t starts an existential proof with witness t

logic2010 style show steps

The Logic 2010 help text leans hard on Show lines and commands like Show Conj, Show Cond, and Show Conclusion.

leanlogic has:

• SHOW_CONJ_LEFT starts the left conjunct of a conjunction goal
• SHOW_CONJ_RIGHT starts the right conjunct of a conjunction goal
• SHOW_COND_LEFT starts the left conditional of a biconditional goal
• SHOW_COND_RIGHT starts the right conditional of a biconditional goal
• SHOW_ALT_LEFT picks the left side of a disjunction goal
• SHOW_ALT_RIGHT picks the right side of a disjunction goal
• SHOW_CORR turns a disjunction goal into its corresponding conditional
• SHOW_ANT h turns a matching conditional or biconditional line into an antecedent goal
• SHOW_ANT_LEFT h left branch of the biconditional antecedent query
• SHOW_ANT_RIGHT h right branch of the biconditional antecedent query
• SHOW_NEGCONS h turns a matching conditional or biconditional line into a negated consequent goal
• SHOW_NEGCONS_LEFT h left branch of the biconditional negated consequent query
• SHOW_NEGCONS_RIGHT h right branch of the biconditional negated consequent query
• SHOW_UNNEG turns a negated compound goal into the positive rule shape that proves it
• SHOW_NEGDISJ h turns a matching disjunction line into a negated disjunct goal
• SHOW_NEGDISJ_LEFT h as h2 proves the negation of the left disjunct and then gives the right disjunct a name
• SHOW_NEGDISJ_RIGHT h as h2 proves the negation of the right disjunct and then gives the left disjunct a name
• SHOW_INST y does the universal derivation move with a chosen fresh variable name
• UD_CLOSE h closes the instance step of a universal derivation

theorem bank

leanlogic also has a numbered theorem layer closer to Logic 2010:

• chapter 2 theorem numbers such as T33, T42, T45, T49, T50, T63, T64, T65, T66, T74, T75, T76, T77, and T90
• chapter 3 theorem numbers such as T201, T202, T203, T204, T205, T206, T231, and T232

There is also a theorem command:

have h : (P ∨ Q) ↔ (¬P → Q) := by
  T 45

and a shorter context-sensitive form:

T 45 as h

when the local names line up with the theorem statement.

These tactics throw friendlier errors when the current goal has the wrong shape.

workbook

leanlogic has a chapter style workbook:

• Leanlogic.Workbook.Chapter1 sentential rules and strategy moves like SHOW_CORR, DM, NC, and SC
• Leanlogic.Workbook.Chapter2 quantifier rules and strategy moves like SHOW_INST, QN, AV, EI, UI, and EG
• Leanlogic.Workbook.Chapter3 identity rules like SID, SM, and LL

If you just want everything loaded:

import Leanlogic.Workbook

exercises

There is also a week based exercises layer built from the local Logic 2010 problem database and some common symbolic logic problems:

• Leanlogic.Exercises.Week06 basic rules and early strategy moves
• Leanlogic.Exercises.Week07 derived rules and show command style problems
• Leanlogic.Exercises.Week09 quantifier exercises
• Leanlogic.Exercises.Week10 identity and later quantified exercises

If you want those loaded too:

import Leanlogic.Exercises

about discharge

As of now, there is no separate DD tactic in this repo and that is intentional. This is because Lean already handles discharge through proof block structure so the leanlogic pattern is:

theorem tiny {P Q : Prop} : P → Q → P := by
  ASS_CD h
  ASS_CD h2
  exact h

When the block closes, the assumptions are discharged!

example

This proof from Leanlogic/Examples.lean is fully checked by Lean:

theorem warmup_swap {P Q : Prop} : P ∧ Q → Q ∧ P := by
  ASS_CD h
  SL h as h5
  SR h as h6
  ADJ h6, h5 as h7
  exact h7

There is also a larger quantifier example in Leanlogic/Examples.lean:

• warmup_show_conj
• warmup_show_cond
• warmup_mt
• warmup_ass_id
• demo_forward
• demo_backward
• demo_full

And there are chapter-based examples such as:

• Leanlogic.Workbook.Chapter1.c1_show_corr
• Leanlogic.Workbook.Chapter2.c2_ei_before_ui
• Leanlogic.Workbook.Chapter3.c3_identity_quantifier

And there are exercise style problems such as:

• Leanlogic.Exercises.Week06.sample_test_basic
• Leanlogic.Exercises.Week06.deriv_1_015
• Leanlogic.Exercises.Week06.koo_t2_q5
• Leanlogic.Exercises.Week07.deriv_2_00g
• Leanlogic.Exercises.Week07.deriv_2_009
• Leanlogic.Exercises.Week07.deriv_2_019_show_negdisj
• Leanlogic.Exercises.Week09.deriv_3_010
• Leanlogic.Exercises.Week09.deriv_3_033
• Leanlogic.Exercises.Week10.deriv_4_010
• Leanlogic.Exercises.Week10.deriv_4_020

And there are theorem-number drills such as:

• Leanlogic.TheoremDrills.use_t45
• Leanlogic.TheoremDrills.use_t203
• Leanlogic.TheoremDrills.use_t231

symbolization

leanlogic has a first symbolization layer too.

NOTE: As of now this is not a full free form natural language parser yet.

It is a structured layer with:

• a formula and term syntax
• ascii and unicode renderers
• a plain english readback
• course style pattern builders for common english forms
• curated english to symbol example cards

If you want it directly:

import Leanlogic.Symbolization

Some useful entry points are:

• Leanlogic.Symbolization.inspect
• Leanlogic.Symbolization.checkAgainst
• Leanlogic.Symbolization.exerciseReport
• Leanlogic.Symbolization.Patterns.unless5
• Leanlogic.Symbolization.Patterns.onlyIf
• Leanlogic.Symbolization.Patterns.allAre
• Leanlogic.Symbolization.Patterns.someAre
• Leanlogic.Symbolization.Patterns.noAre
• Leanlogic.Symbolization.Patterns.everyLovesSome
• Leanlogic.Symbolization.Examples.cards
• Leanlogic.Symbolization.Tutorial.Examples
• Leanlogic.Symbolization.Tutorial.Exercises
• Leanlogic.Symbolization.Workflow.Examples
• Leanlogic.Symbolization.Workflow.Exercises
• Leanlogic.Symbolization.Practice.Easy
• Leanlogic.Symbolization.Questions.Chapter1Sentential

Examples from the symbolization bank include:

• P unless Q
• P only if Q
• P is necessary for Q
• neither P nor Q
• all dogs are mammals
• some dogs are brown
• every giraffe frolics only if it is happy
• every giraffe loves some monkey

If you want a follow along file with finished examples first and then exercises to fill in yourself, start in:

• Leanlogic/Symbolization/Tutorial.lean

That file intentionally includes sorry in the exercise section.

If you want the most direct workflow for writing your own symbolization and checking it against an answer, start in:

• Leanlogic/Symbolization/Workflow.lean

That file shows the pattern:

def p : Formula := "P"
def q : Formula := "Q"

def mine : Formula :=
  symb% p ∧ ¬ q

#eval inspect mine
#eval checkAgainst mine (symb% p ∧ ¬ q)

If you want a sheet that feels more like the Logic 2010 symbolization screen with letter legends and ready made prompts, open:

• Leanlogic/Symbolization/Practice/Easy.lean

If you want a real chapter one sentential logic question bank with sorry attempts and ready made check commands, open:

• Leanlogic/Symbolization/Questions/Chapter1Sentential.lean

There are also explicit close-step demos in Leanlogic.Examples:

• warmup_dd
• warmup_ass_id
• warmup_ud_close

extensions

If you find leanlogic useful, feel free to reach out or open an issue if you have any extension suggestions (or if you encounter any bugs, of course). Thanks!