Jan Aldert Bergstra

The paper is well-motivated and fairly easy to read. The issues and unclarities which the author mentions and is concerned about abound in educational texts on elementary arithmetic. Nevertheless, it is not easy to understand what precisely is the no...

Proposition algebra is based on Hoare’s conditional, a ternary connective comparable to if–then–else and used in the context of propositional logic. Conditional statements are composed from atomic propositions (propositional variables), constants for the Boolean truth values, and the conditional. In previous work, various equational axiomatisations have been defined, each of which leads to a so-called valuation congruence. The weakest of these is “free valuation congruence” and the strongest is “static valuation congruence”, which is equivalent to propositional logic. Free valuation congruence is axiomatised by four simple equational axioms, and we use evaluation trees to give a simple semantics: two conditional statements are free valuation congruent if, and only if, they have equal evaluation trees. Increasingly stronger valuation congruences arise by adding axioms to the four that define free valuation congruence: repetition-proof, contractive, memorising, and static valuation congruence. We prove that each such valuation congruence C can be characterised using a transformation on evaluation trees: two conditional statements are C-valuation congruent if, and only if, their C-transformed evaluation trees are equal. In order to prove that these transformations preserve the congruence property, we use normalisation functions: two conditional statements are C-valuation congruent if, and only if, the C-normalisation function returns equal images. Our framework provides the first comprehensive tree-based semantics that unifies all major valuation congruences in proposition algebra, offering both conceptual clarity and practical decision procedures.

Categorial gender theory is concerned with frameworks for categorizing human individuals in terms of gender and gender-related notions. A survey of gender frameworks is presented. We observe two alternative ways of conveying similar information: one via features and the other via process algebraic descriptions of gender lifecycles. The development of categorial gender theory is compared with the Formal Gender Theory that was previously developed in collaboration with Laurens Buijs.

To avoid the risk of problems to do with division by zero (DbZ), arithmetical texts involving division use what may be called traditional conventions on DbZ. Earlier, we developed a method for exploring these conventions using informal notions of legal and illegal texts, which are used to analyse simple fragments of arithmetical texts. We showed how these texts can be transformed into logical formulae over special total algebras, called common meadows, that are able to approximate partiality but in a total world. The subtleties of the legal/illegal distinction call for further development of these mathematical methods. Here we examine a more complex type of text, namely proof by contradiction, in which inconsistent assumptions can coexist with DbZ. We formulate more advanced criteria of legality for this case. We introduce a three-valued logic to capture the resulting semiformal conventions that is based on a notion we call frugal equality for partial operators. We apply the method to a proof of the Bayes-Price Theorem in probability theory, whose proof has DbZ issues.

Following earlier work we proceed with a detailed investigation of genocide accusations which we consider to constitute a particular class of extreme accusations. We focus on controversial real-time accusations of episodal genocide. We find that the logic of genocide and the logic of genocide accusations interact in complicated ways, and that there is a plausible use for a new term: tribocide. Tribocide entails the visible and often detrimental effect of genocide on the victims, while abstracting from the perpetrator's plans, motives, and intentions, as well as from side-effects which may be advantageous from the perpetrator's perspective. Importantly, validating a tribocide accusation is simpler than validating a genocide accusation because the focus is exclusively on the victim's perspectives.

Following up earlier work on accusations, we proceed with a detailed investigation of a particular class of extreme accusations called genocide accusations. We focus on real time accusations of episodal genocide, meant to bring the target behaviour of the accusee to an end, or to contribute to its termination. We derive conditions under which issuing such accusations may be justified.