1. Suppose you have strong evidence that L are the true laws of nature, where L is
a system of deterministic laws. You also have strong evidence that the universe
started in the exact microstate P. Your have a choice of either affirming or
denying the conjunction of L and P. You want to speak truly. What should you do?

Intuitively, you should affirm. But what would happen if you denied?

Since L is deterministic, L & P either logically entails that you affirm, or it
logically entails that you don't affirm. Let's consider both possibilities.

Until recently, the Stanford Encyclopedia of Philosophy didn't have anything on
counterpart theory. The editors thought the topic isn't worth an entry of its
own, but at least it now has a section in the entry on "David Lewis's Metaphysics". This isn't ideal, since counterpart-theoretic approaches to
intensional constructions are best seen as metaphysically non-committal. But
it's better than nothing.

I also wrote an "appendix" to the entry with an overview over
counterpart-theoretic interpretations of quantified modal logic. It
explains some unusual features of counterpart-theoretic logics, how they arise,
and how they could be avoided.

By the way, here's another problem my prover can't solve (in reasonable time):

Show: ∀y∃z∀x(Fxz ↔ x=y) → ¬∃w∀x(Fxw ↔ ∀u(Fxu → ∃y(Fyu ∧ ¬∃z(Fzu ∧ Fzy))))

This is problem 54 in Pelletier 1986. It is a pure first-order adaptation of a
little theorem proved in Montague 1955. Montague gives a fairly simple proof.
His proof uses the Cut rule, which the tableau method doesn't have. I've tried
to construct a tableau proof by hand, but failed.

This might be a nice example of a relatively straightforward fact that can be
proved easily with Cut, but not without.

It's been quiet here. I haven't had much time or energy for philosophy since the
pandemic turned me into a stay-at-home dad on top of the regular job(s). At
least teaching has finally come to an end a few weeks ago. I've used my newly
found free time to build support for identity into the tree prover.

This is something I've wanted to do for a long time. Every five years or so I
look into it, but give up because it's too hard. Here I'll explain the
challenges, and the approach I chose.

Logic textbooks usually introduce two rules for handling identity: "Leibniz'
Law" (in both directions) and a rule that allows closing branches on which there
is a node of the form ¬t=t. These rules go back to Jeffrey 1967.