We verify that the Maple model from 1996 is actually a canon₃_II model.
Thus the definition of canon_II was foreshadowed in 1996;
In this example canon_II can be characterized as the model obtain by a certain greedy algorithm
for A5-C5 and automatically satisfies E5.
Limited Principle of Explosion:
If C is at least somewhat desirable
and the most desirable (A) is violated then C is obligatory.
This is paradoxical if a is the best world, then b, then c.
- basic₁ {n : ℕ} {A B X : Finset (Fin n)} : X ⊆ Finset.univ → X ∩ A ≠ ∅ → Ob_chisholm_b A B (A, X)
- basic₂ {n : ℕ} {A B X : Finset (Fin n)} : X ⊆ Aᶜ → X ∩ B ≠ ∅ → Ob_chisholm_b A B (B, X)
- B5 {n : ℕ} {A B X Y Z : Finset (Fin n)} : Ob_chisholm_b A B (X, Y) → X ∩ Y = Z ∩ Y → Ob_chisholm_b A B (Z, Y)
Instances For
- basic₁ {n : ℕ} {A B X : Finset (Fin n)} : X ⊆ Finset.univ → X ∩ A ≠ ∅ → Ob_chisholm_bdf A B (A, X)
- basic₂ {n : ℕ} {A B X : Finset (Fin n)} : X ⊆ Aᶜ → X ∩ B ≠ ∅ → Ob_chisholm_bdf A B (B, X)
- B5 {n : ℕ} {A B X Y Z : Finset (Fin n)} : Ob_chisholm_bdf A B (X, Y) → X ∩ Y = Z ∩ Y → Ob_chisholm_bdf A B (Z, Y)
- D5 {n : ℕ} {A B X Y Z : Finset (Fin n)} : Y ⊆ X → Ob_chisholm_bdf A B (Y, X) → X ⊆ Z → Ob_chisholm_bdf A B (Z \ X ∪ Y, Z)
- F5 {n : ℕ} {A B X Y Z : Finset (Fin n)} : Ob_chisholm_bdf A B (X, Y) → Ob_chisholm_bdf A B (X, Z) → Ob_chisholm_bdf A B (X, Y ∪ Z)
Instances For
Since canon₂_II also satisfies A B C E G we can furthermore characterize it as the least model of those axioms and B5 and these Oughts. It is remarkable that A, C, E, G do not add anything to this least model.
least model of also of
canon₂_II A B C E G B canon₂ A B C D B D F
What are the least models of the paradoxical ABCDEFG and ABCEFG?
We need to assume A ⊆ B, perhaps relevant to referee's question,
although it was already in least_model_canon₂_II.
The contribution of this theorem is to obtain canon₂_II as equal to a certain closure,
not just satisfying a "least model" predicate.
January 5, 2026.
canon₂ is the minimal model satisfying certain Ought's and B5, D5, F5. Actually F5 follows from B5, C5, D5, A5 (Lemma II-2-2) although here we do not need to assume C5.
June 6, 2025
- basic {α : Type u_1} {𝒜 : Set (Set α)} {R : Type u_2} {rule : R → Rule α} {s : Set α} : s ∈ 𝒜 → Closure 𝒜 rule s
- apply {α : Type u_1} {𝒜 : Set (Set α)} {R : Type u_2} {rule : R → Rule α} (r : R) (p : (rule r).params) : (∀ (i : (rule r).ι), Closure 𝒜 rule ((rule r).premise_set p i)) → Closure 𝒜 rule ((rule r).conclusion p)
Instances For
General setup for CJ rules #
- basic {α : Type u_1} {𝒜 : Finset (Finset α × Finset α)} {rule : Finset (closure_rule α)} {s : Finset α × Finset α} : s ∈ 𝒜 → closure_under 𝒜 rule s
- apply {α : Type u_1} {𝒜 : Finset (Finset α × Finset α)} {rule : Finset (closure_rule α)} (r : closure_rule α) (hr : r ∈ rule) (sets : sets_instance α r.numSets r.P) (h : ∀ (i : Fin r.num_in), closure_under 𝒜 rule (r.premises sets i)) : closure_under 𝒜 rule (r.conclusion sets)
Instances For
If we add more rules then the closure becomes larger.
Equations
- One or more equations did not get rendered due to their size.
Instances For
This shows, together with earlier results, how to express canon₂_II as a closure under a set of operators.
The closure of a set under some operations can be defined
in a very noneffective way as the intersection of all closed sets.
Second, it can be defined in a recursively enumerable way in terms of
being generated by some operations. Sometimes, it can be characterized
even more concretely in a quantifier-free way, like here.
For example, in a vector space over F_2 the subspace generated by v
is just {v,0}.
Equations
- disjointUnionRule α = { params := DisjointUnionParams α, ι := Fin 2, premise_set := DisjointUnionParams.s, conclusion := fun (p : DisjointUnionParams α) => p.s 0 ∪ p.s 1 }
Instances For
A version of least_model_canon₂ that mentions only
older axioms than F5.