Skip to content

Commit 6083b4c

Browse files
benbrastmckiebenbrastmckie
committed
feat(Logics/Propositional): add Bool semantics and minor attribution fixes
Adds two new semantics files in response to Zulip discussion on PR 648: - Cslib/Logics/Propositional/Semantics/Basic.lean: Valuation type, Evaluate function, Tautology predicate (bivalent truth-value semantics) - Cslib/Logics/Propositional/Semantics/Bool.lean: BoolValuation, BoolEvaluate, bridge lemma BoolEvaluate_eq_iff, decidability instance; responds to Zulip question from Matthew Doty about Atom → Bool valuations for DPLL Also applies minor attribution fixes to existing PR files: - Defs.lean: copyright year extended to 2026, Chagrov reference added - NaturalDeduction/Basic.lean: copyright year extended to 2026 Task 202 originally implemented Bool.lean as a direct response to the Zulip conversation. The Atom → Prop valuation is structurally required for canonical model construction; BoolEvaluate is the correct additional layer for DPLL/SAT.
1 parent b041ae7 commit 6083b4c

5 files changed

Lines changed: 179 additions & 2 deletions

File tree

‎Cslib.lean‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -148,6 +148,8 @@ public import Cslib.Logics.Modal.Denotation
148148
public import Cslib.Logics.Modal.LogicalEquivalence
149149
public import Cslib.Logics.Propositional.Defs
150150
public import Cslib.Logics.Propositional.NaturalDeduction.Basic
151+
public import Cslib.Logics.Propositional.Semantics.Basic
152+
public import Cslib.Logics.Propositional.Semantics.Bool
151153
public import Cslib.MachineLearning.PACLearning.Defs
152154
public import Cslib.MachineLearning.PACLearning.VCDimension
153155
public import Cslib.MachineLearning.PACLearning.VersionSpace

‎Cslib/Logics/Propositional/Defs.lean‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
/-
2-
Copyright (c) 2025 Thomas Waring, Benjamin Brast-McKie. All rights reserved.
2+
Copyright (c) 2025 Thomas Waring, 2026 Benjamin Brast-McKie. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Thomas Waring, Benjamin Brast-McKie
55
-/
@@ -46,6 +46,7 @@ conjunction, disjunction, implication and negation.
4646
* [A. S. Troelstra, D. van Dalen,
4747
*Constructivism in Mathematics: An Introduction*][TroelstraVanDalen1988]
4848
* [A. Church, *Introduction to Mathematical Logic*][Church1956]
49+
* [A. Chagrov, M. Zakharyaschev, *Modal Logic*][ChagrovZakharyaschev1997], Chapter 1
4950
-/
5051

5152
@[expose] public section

‎Cslib/Logics/Propositional/NaturalDeduction/Basic.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
/-
2-
Copyright (c) 2025 Thomas Waring, Benjamin Brast-McKie. All rights reserved.
2+
Copyright (c) 2025 Thomas Waring, 2026 Benjamin Brast-McKie. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Thomas Waring, Benjamin Brast-McKie
55
-/

‎Cslib/Logics/Propositional/Semantics/Basic.lean‎

Lines changed: 64 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,64 @@
1+
/-
2+
Copyright (c) 2026 Benjamin Brast-McKie. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Benjamin Brast-McKie
5+
-/
6+
7+
module
8+
9+
public import Cslib.Logics.Propositional.Defs
10+
11+
/-! # Bivalent Truth-Value Semantics for Propositional Logic
12+
13+
This module defines bivalent truth-value semantics for classical propositional logic.
14+
15+
## Main Definitions
16+
17+
- `Valuation`: A (bivalent) propositional valuation assigns a truth value to each atom.
18+
- `Evaluate`: Evaluate a proposition under a valuation (recursive, 3 cases: atom/bot/imp).
19+
- `Tautology`: A proposition is a tautology iff it is true under every valuation.
20+
21+
## References
22+
23+
* [A. Chagrov, M. Zakharyaschev, *Modal Logic*][ChagrovZakharyaschev1997], Section 1.2
24+
-/
25+
26+
@[expose] public section
27+
28+
namespace Cslib.Logic.PL
29+
30+
variable {Atom : Type*}
31+
32+
/-- A (bivalent) propositional valuation assigns a truth value to each atom. -/
33+
abbrev Valuation (Atom : Type*) := Atom → Prop
34+
35+
/-- Evaluate a proposition under a valuation.
36+
37+
This is the propositional specialization of modal `Satisfies`, without the box case. -/
38+
def Evaluate (v : Valuation Atom) : PL.Proposition Atom → Prop
39+
| .atom x => v x
40+
| .bot => False
41+
| .imp a b => Evaluate v a → Evaluate v b
42+
| .and a b => Evaluate v a ∧ Evaluate v b
43+
| .or a b => Evaluate v a ∨ Evaluate v b
44+
45+
@[simp] theorem Evaluate_atom (v : Valuation Atom) (x : Atom) :
46+
Evaluate v (.atom x) = v x := rfl
47+
48+
@[simp] theorem Evaluate_bot (v : Valuation Atom) :
49+
Evaluate v (.bot) = False := rfl
50+
51+
@[simp] theorem Evaluate_imp (v : Valuation Atom) (a b : PL.Proposition Atom) :
52+
Evaluate v (.imp a b) = (Evaluate v a → Evaluate v b) := rfl
53+
54+
@[simp] theorem Evaluate_and (v : Valuation Atom) (a b : PL.Proposition Atom) :
55+
Evaluate v (.and a b) = (Evaluate v a ∧ Evaluate v b) := rfl
56+
57+
@[simp] theorem Evaluate_or (v : Valuation Atom) (a b : PL.Proposition Atom) :
58+
Evaluate v (.or a b) = (Evaluate v a ∨ Evaluate v b) := rfl
59+
60+
/-- A proposition is a tautology iff it is true under every valuation. -/
61+
def Tautology (φ : PL.Proposition Atom) : Prop :=
62+
∀ (v : Valuation Atom), Evaluate v φ
63+
64+
end Cslib.Logic.PL

‎Cslib/Logics/Propositional/Semantics/Bool.lean‎

Lines changed: 110 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,110 @@
1+
/-
2+
Copyright (c) 2026 Benjamin Brast-McKie. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Benjamin Brast-McKie
5+
-/
6+
7+
module
8+
9+
public import Cslib.Logics.Propositional.Semantics.Basic
10+
11+
/-! # Boolean Evaluation for Propositional Logic
12+
13+
This module defines a computable Boolean evaluation function for propositional logic,
14+
alongside the `Prop`-valued `Evaluate` from `Semantics.Basic`.
15+
16+
## Main Definitions
17+
18+
- `BoolValuation`: A Boolean propositional valuation assigns a `Bool` to each atom.
19+
- `BoolEvaluate`: Evaluate a proposition under a Boolean valuation, returning `Bool`.
20+
21+
## Main Results
22+
23+
- `BoolEvaluate_eq_iff`: Bridge lemma connecting `BoolEvaluate v φ = true` to
24+
`Evaluate (fun a => v a = true) φ`, enabling decidable evaluation.
25+
- `instDecidableBoolEvaluate`: Decidability of `Evaluate` under Boolean valuations.
26+
27+
## Design Notes
28+
29+
`BoolEvaluate` exists alongside `Evaluate` because DPLL/SAT procedures need computable
30+
`Bool` evaluation, while canonical model construction in strong completeness requires `Prop`
31+
(set membership `fun p => p ∈ S` is not decidable in general). The bridge lemma connects
32+
the two worlds: `Bool` computation to `Prop` metatheory.
33+
34+
## References
35+
36+
* [A. Chagrov, M. Zakharyaschev, *Modal Logic*][ChagrovZakharyaschev1997], Section 1.2
37+
-/
38+
39+
@[expose] public section
40+
41+
namespace Cslib.Logic.PL
42+
43+
variable {Atom : Type*}
44+
45+
/-- A Boolean propositional valuation assigns a `Bool` value to each atom. -/
46+
abbrev BoolValuation (Atom : Type*) := Atom → Bool
47+
48+
/-- Computable Boolean evaluation of a proposition; mirrors `Evaluate` with `Bool` instead of
49+
`Prop`. Use `BoolEvaluate_eq_iff` to connect results to `Evaluate`. -/
50+
def BoolEvaluate (v : BoolValuation Atom) : PL.Proposition Atom → Bool
51+
| .atom x => v x
52+
| .bot => false
53+
| .imp a b => !BoolEvaluate v a || BoolEvaluate v b
54+
| .and a b => BoolEvaluate v a && BoolEvaluate v b
55+
| .or a b => BoolEvaluate v a || BoolEvaluate v b
56+
57+
@[simp] theorem BoolEvaluate_atom (v : BoolValuation Atom) (x : Atom) :
58+
BoolEvaluate v (.atom x) = v x := rfl
59+
60+
@[simp] theorem BoolEvaluate_bot (v : BoolValuation Atom) :
61+
BoolEvaluate v (.bot) = false := rfl
62+
63+
@[simp] theorem BoolEvaluate_imp (v : BoolValuation Atom) (a b : PL.Proposition Atom) :
64+
BoolEvaluate v (.imp a b) = (!BoolEvaluate v a || BoolEvaluate v b) := rfl
65+
66+
@[simp] theorem BoolEvaluate_and (v : BoolValuation Atom) (a b : PL.Proposition Atom) :
67+
BoolEvaluate v (.and a b) = (BoolEvaluate v a && BoolEvaluate v b) := rfl
68+
69+
@[simp] theorem BoolEvaluate_or (v : BoolValuation Atom) (a b : PL.Proposition Atom) :
70+
BoolEvaluate v (.or a b) = (BoolEvaluate v a || BoolEvaluate v b) := rfl
71+
72+
/-- Bridge lemma: `BoolEvaluate v φ = true` iff `Evaluate (fun a => v a = true) φ`.
73+
The `imp` case uses `cases` on `Bool` since `!a || b = true ↔ (a = true → b = true)`
74+
is not automatic from `simp`. -/
75+
theorem BoolEvaluate_eq_iff (v : BoolValuation Atom) (φ : PL.Proposition Atom) :
76+
BoolEvaluate v φ = true ↔ Evaluate (fun a => v a = true) φ := by
77+
induction φ with
78+
| atom x => simp [BoolEvaluate, Evaluate]
79+
| bot => simp [BoolEvaluate, Evaluate]
80+
| imp a b iha ihb =>
81+
simp only [BoolEvaluate, Evaluate_imp, ← iha, ← ihb]
82+
cases BoolEvaluate v a <;> cases BoolEvaluate v b <;> simp
83+
| and a b iha ihb => simp [BoolEvaluate, Evaluate, iha, ihb]
84+
| or a b iha ihb => simp [BoolEvaluate, Evaluate, iha, ihb]
85+
86+
/-- Negation form of the bridge: `BoolEvaluate v φ = false` iff
87+
`¬ Evaluate (fun a => v a = true) φ`. -/
88+
theorem BoolEvaluate_eq_false_iff (v : BoolValuation Atom) (φ : PL.Proposition Atom) :
89+
BoolEvaluate v φ = false ↔ ¬Evaluate (fun a => v a = true) φ := by
90+
rw [← BoolEvaluate_eq_iff]
91+
cases BoolEvaluate v φ <;> simp
92+
93+
/-- Every propositional valuation with decidable atoms factors through `BoolEvaluate`. -/
94+
theorem Evaluate_eq_BoolEvaluate (v : Valuation Atom) [∀ a, Decidable (v a)]
95+
(φ : PL.Proposition Atom) :
96+
Evaluate v φ ↔ BoolEvaluate (fun a => decide (v a)) φ = true := by
97+
rw [BoolEvaluate_eq_iff]
98+
induction φ with
99+
| atom x => simp [Evaluate, decide_eq_true_eq]
100+
| bot => simp [Evaluate]
101+
| imp a b iha ihb => simp [Evaluate, iha, ihb]
102+
| and a b iha ihb => simp [Evaluate, iha, ihb]
103+
| or a b iha ihb => simp [Evaluate, iha, ihb]
104+
105+
/-- `Evaluate` under a Boolean valuation is decidable, via `BoolEvaluate_eq_iff`. -/
106+
instance instDecidableBoolEvaluate (v : BoolValuation Atom) (φ : PL.Proposition Atom) :
107+
Decidable (Evaluate (fun a => v a = true) φ) :=
108+
decidable_of_iff _ (BoolEvaluate_eq_iff v φ)
109+
110+
end Cslib.Logic.PL

0 commit comments

Comments
 (0)