< 704 older entries Home

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.

## Counterpart theory in the SEP

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.

## A difficult tableau proof

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.

## Identity (equality) in automated semantic tableaux

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.

 < 704 older entries Home