Category Archives: research

Deontic independence challenge

Which of these 128 combinations are satisfiable in Carmo and Jones style deontic logic? (1=true, 0=false) (Here 5(c) is the strong version.)
Some possibilities are ruled out by Observation 5.1.2 that says 5(bcde) imply 5(g); and Lemma II.2.2 that says 5(abcd) imply 5(f), formalized by RJ Reiff.

5(abcdefg) Model
0000000?
0000001?
0000010?
0000011?
0000100?
0000101?
0000110?
0000111?
0001000?
0001001?
0001010?
0001011?
0001100?
0001101?
0001110?
0001111?
0010000?
0010001?
0010010?
0010011?
0010100?
0010101?
0010110?
0010111?
0011000?
0011001?
0011010?
0011011?
0011100?
0011101?
0011110?
0011111?
0100000?
0100001?
0100010?
0100011?
0100100?
0100101?
0100110?
0100111?
0101000?
0101001?
0101010?
0101011?
0101100?
0101101?
0101110?
0101111?
0110000?
0110001?
0110010?
0110011?
0110100?
0110101?
0110110?
0110111?
0111000?
0111001?
0111010?
0111011?
0111100none; Obs. 5.1.2
0111101?
0111110none; Obs. 5.1.2
0111111see: A5_not_implied
1000000?
1000001?
1000010?
1000011?
1000100?
1000101?
1000110?
1000111?
1001000?
1001001?
1001010?
1001011?
1001100?
1001101?
1001110?
1001111?
1010000?
1010001?
1010010?
1010011?
1010100?
1010101?
1010110?
1010111?
1011000?
1011001?
1011010?
1011011?
1011100?
1011101?
1011110?
1011111see: B5_not_implied’
1100000?
1100001?
1100010?
1100011?
1100100?
1100101?
1100110?
1100111?
1101000?
1101001?
1101010?
1101011?
1101100see: C5_not_implied’
1101101?
1101110?
1101111?
1110000?
1110001?
1110010?
1110011?
1110100?
1110101see theorem: strong_do_not_imply_5d_or_5f
1110110?
1110111?
1111000none; see II.2.2
1111001none; see II.2.2
1111010?
1111011see theorem: do_not_imply_5e
1111100 impossible as 5(fg) follow from 5(abcde)
1111101 impossible as 5(fg) follow from 5(abcde)
1111110 impossible as 5(fg) follow from 5(abcde)
1111111 stayAlive, alive, noObligations

Project on Github

Marginis: Formal Marginalia

Lean is a popular proof assistant.

Blueprint projects document Lean projects with Mathlib-style documentation and LaTeX/PDF support.

Here are my Lean blueprint projects:

  • Marginis – formalia marginalia for the Journal of Logic and Analysis
  • Protein folding – formalizations related to the paper Nonmonotonicity of protein folding under concatenation
  • Automatic complexity – formalized exercise solutions for my book
  • Deontic – formalized results from a paper on dyadic deontic logic
  • Jaccard – formalization of the research paper Interpolating between the Jaccard distance and an analogue of the normalized information distance (Journal of Logic and Computation, 2022)

Mathlib contributions

My selected contributions to Mathlib, the library of formalized mathematics for the proof assistant Lean:

San Luis Obispo: Logic and Analysis Special Session

Image above: View from “The P”. The P is Cal Poly’s version of the Hollywood sign and consists of a single giant letter “P”.

This Special Session of the American Mathematical Society concerns mathematical logic and mathematical analysis, honors the 18th year of the Journal of Logic and Analysis, and is organized by Bjørn Kjos-Hanssen and David A. Ross.

According to the Registrar there are three chalkboards in Room 204 of Building 38, which is where we’ll be according to the Program.

Saturday morning (8:30AM – 11AM)

8:30 Patrick Lutz
9:00 Isaac Goldbring
9:30 Timothy McNicholl
10:00 Kenny Gill
10:30 Cecelia Higgins

Saturday afternoon (3PM – 5:30PM)

Chair: Tim McNicholl
3:00 Todor Todorov
3:30 Karel Hrbacek
4:00 Janani Lakshmanan (slides presented by B. Kjos-Hanssen)
4:30 Ang Li
5:00 Noah Schweber

Sunday morning (9AM – 11AM)

Chair: Ang Li
9:00 Felix Weilacher
9:30 Yury Kudryashov
10:00 Wesley Calvert
10:30 Kenshi Miyabe

Sunday afternoon (2:30PM – 4:30PM)

2:30 Meng-Che “Turbo” Ho
3:00 Mauro Di Nasso
3:30 Lynn Scow
4:00 Forte Shinko

“A new approach to contrary-to-duty obligations” characterized

Damir Dzhafarov, Stefan Kaufmann, Bjørn Kjos-Hanssen, Dave Ripley, et al., at the 2016 ASL Annual Meeting at UConn.

Slides

José Carmo and Andrew J.I. Jones have studied contrary-to-duties obligations in a series of papers.

They develop a logical framework for scenarios such as the following:

1. There ought to be no dog.
2. If there is a dog, there ought to be a fence.

One conjecture from Carmo and Jones 1997 was refuted in a rather technical way in my 1996 term paper at University of Oslo.
The conjecture stated that one could simply add the condition
$\DeclareMathOperator{\pii}{ob}$
$$
(Z \in \pii(X)) \land
(Y \subseteq X) \land
(Y \cap Z \ne \emptyset ) \rightarrow (Z \in \pii(Y )) \tag{5e}
$$
for the conditional obligation operator ob.
In a follow-up paper (2001) they argued that (5e) could be added by weakening some other conditions.
In a new paper in Studia Logica, and presented at the Association for Symbolic Logic Annual Meeting 2016 at UConn, I argue that (5d) and (5e) are in conflict with each other. The argument is a generalization and strengthening of the 1996 argument.

2018: Benzmüller et al. have implemented Carmo and Jones’ logic in the proof assistant Isabelle and Jake Fennick’s MA project is the implementation of my follow-up paper in Isabelle.

During my sabbatical in 2025 I found a surprising characterization of Carmo and Jones’ system from their 1997 article A new approach to contrary-to-duty obligations in terms of a single forbidden world. The formal proof and accompanying paper is currently under revision with a journal.