Wolfgang Schwarz

Teaching mathematical logic

I taught two courses this year that I haven't taught before. One of them was our 4th-year undergraduate course on mathematical logic, "Logic, Computability, and Incompleteness". As usual, I ended up writing my own textbook. Here it is as PDF and here as HTML.

Why yet another textbook? Two reasons mainly. One is that many existing textbooks are addressed at maths students. This shows up not only in the examples and illustrations, but also in the fact that comparatively little time is spent motivating, explaining, and discussing definitions, proof ideas, or results. I wanted more of that.

The absoluteness of consistency

A somewhat appealing (albeit, to me, also somewhat obscure) view of mathematics is the pluralist doctrine that every consistent mathematical theory is true, insofar as it accurately describes some mathematical structure. I want to comment on a potential worry for this view, mentioned in (Clarke-Doane 2020): that it has implausible consequences for logic.

Gödel, Mechanism, Paradox

A famous argument, first proposed in Lucas 1961, supposedly shows that the human mind has capabilities that go beyond those of any Turing machine. In its basic form, the argument goes like this.

Let S be the set of mathematical sentences that I accept as true. S includes the axioms of Peano Arithmetic. Let S+ be the set of sentences entailed by S. Suppose for reductio that my mind is equivalent to a Turing machine. Then S is computably enumerable, and S+ is a computably axiomatizable extension of Peano Arithmetic. So Gödel's First Incompleteness Theorem applies: there is a true sentence G that is unprovable in S+. By going through Gödel's reasoning, I can see that G is true. So G is in S and thereby in S+. Contradiction!

Teaching logic: Tarski vs Mates vs "logical constants"

I'm teaching an intermediate/advanced logic course this semester. So I had to ask myself how to introduce the semantics of quantifiers, with an eye on proving soundness and completeness. The standard approach, going back to Tarski, defines a satisfaction relation between a formula, a model, and an assignment function, and then defines truth by supervaluating over all assignments. The main alternative, often found in intro logic textbooks, is Mates' approach, where ∀xA(x) is defined as true in a model M iff A(c) is true in every c-variant of M, where c is a constant not occurring in A.

Bacon on higher-order logic

In the dark old days of early logic, there was only syntax. People introduced formal languages and laid down axioms and inference rules, but there was nothing to justify these except a claim to "self-evidence". Of course, the languages were assumed to be meaningful, but there was no systematic theory of meaning, so the axioms and rules could not be justified by the meaning of the logical constants.

All this changed with the development of model theory. Now one could give a precise semantics for logical languages. The intuitive idea of entailment as necessary truth-preservation could be formalized. One could check that some proposed system of axioms and rules was sound, and one could confirm – what had been impossible before – that it was complete, so that any further, non-redundant axiom or rule would break the system's soundness.

Updated notes on counterpart semantics for modal predicate logic

In around 2009, I got interested in counterpart-theoretic interpretations of modal predicate logic. Lewis's original semantics, from Lewis (1968), has some undesirable features, due to his choice of giving the box a "strong" reading (in the sense of Kripke (1971)), but it's not hard to define a better-behaved form of counterpart semantics that gives the box its more familiar "weak" reading.

Wondering if anyone had figured out the logic determined by this semantics, I found an answer in Kutz (2000) and Kracht and Kutz (2002). I also learned that counterpart semantics seems to overcome some formal limitation of the more standard "Kripke semantics". For example, while all logics between quantified S4.3 and S5 are incomplete in Kripke semantics (as shown in Ghilardi (1991)), many are apparently complete in the "functor semantics" of Ghilardi (1992), which I do not understand but which is said to have a counterpart-theoretic flavour. Skvortsov and Shehtman (1993) present a somewhat more accessible "metaframe semantics", inspired by Ghilardi's approach, and claim that the quantified version of all canonical extensions of S4 remain canonical (and hence complete) in metaframe semantics. Kracht and Kutz argue that their – much simpler – counterpart semantics inherits these properties of functor and metaframe semantics.

Lecture notes on modal logic

I've been teaching a course called Logic 2: Modal Logics for the past few years. It's an intermediate logic course for third-year Philosophy students, all of whom have taken intro logic. I'm not entirely convinced that a second logic course should focus on modal logic, but it works OK.

One nice aspect of modal propositional logic is that models, proofs, soundness, completeness, etc. are not as trivial as in classical propositional logic, but easier than in classical predicate logic. I also like the many philosophical applications. I spend a week on epistemic logic, another on deontic logic, one on temporal logic, and one on conditionals.

Anyway, I've just uploaded my lecture notes to github, in case anyone is interested. The LaTeX source is there as well.

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.

Tree prover update

I've spent some time this summer upgrading my tree prover. The new version is here. What's new:

• support for some (normal) modal logics
• better detection of invalid formulas
• faster proof search
• nicer user interface and nicer trees
• cleaner source

I hope there aren't too many new bugs. Let me know if you find one!

Relativism and absolutism in deontic logic

Consider a world where eating doughnuts is illegal and where everyone thinks it is OK to torture animals for fun. Suppose Norman at w is eating doughnuts while torturing his pet kittens. Is he violating the laws? Is he doing something immoral?

In one sense, yes, in another, no. His doughnut eating violates the laws of w, but not the laws of our world. Conversely, his kitten torturing violates a moral code accepted at our world, but not a code accepted at w.

Duals of knowledge and belief

On the modal analysis of belief, 'S believes that p' is true iff p is true at all possible worlds compatible with S's belief state. So 'believes' is a necessity modal. One might expect there to be a dual possibility modal, a verb V such that 'S Vs that p' is true iff p is true at some worlds compatible with S's belief state. But there doesn't seem to be any such verb in English (or German). Why not?

What do we use if we want to say that something is compatible with someone's beliefs? Suppose at some worlds compatible with Betty's belief state, it is currently snowing. We could express this by "Betty does not believe that it is not snowing". But (for some reason) that's really hard to parse.

Validity judgments

Philosophers (and linguists) often appeal to judgments about the validity of general principles or arguments. For example, they judge that if C entails D, then 'if A then C' entails 'if A then D'; that 'it is not the case that it will be that P' is equivalent to 'it will be the case that not P'; that the principles of S5 are valid for metaphysical modality; that 'there could have been some person x such that actually x sits and actually x doesn't sit' is an unsatisfiable contradiction; and so on. In my view, such judgments are almost worthless: they carry very little evidential weight.

Small formulas with large models

Take the usual language of first-order logic from introductory textbooks, without identity and function symbols. The vast majority of sentences in this language are satisfied in models with very few individuals. You even have to make an effort to come up with a sentence that requires three or four individuals. The task is harder if you want to come up with a fairly short sentence. So I wonder, for any given number n, what is the shortest sentences that requires n individuals?

Possible worlds and non-principal ultrafilters

It is natural to think of a possible world as something like an extremely specific story or theory. Unlike an ordinary story or theory, a possible world leaves no question open. If we identify a theory with a set of propositions, a possible world could be defined as a theory T which is

1. maximally specific: T contains either P or ~P, for every proposition P;
2. consistent: T does not contain P and ~P, for any proposition P;
3. closed under conjunction and logical consequence: if T contains both P and Q, then it contains their conjunction P & Q, and if T contains P, and P entails Q, then T contains Q.

It is often useful to go in the other direction and identify propositions with sets of possible worlds. We can then analyse entailment as the subset relation, negation as complement and conjunction as intersection. Of course, we may not want to say that a world is a (non-empty) set of (consistent) propositions and also that a consistent proposition is a non-empty set of worlds, since these sets should eventually bottom out. But that doesn't seem very problematic, and it is easily fixed as long as there is a simple 1-1 correspondence between worlds and logically closed, consistent and maximally specific theories. In particular, one might suspect that on the present definitions, every logically closed, consistent and maximally specific theory uniquely corresponds to a possible world, namely the sole member of the intersection of the theory's members.

Paradoxes for "expresses the proposition"

There are familiar semantic paradoxes for "truth" and "reference", such as the Liar paradox and Berry's paradox. I would have thought that there should be similar paradoxes for "expression", i.e. for the relation between a sentence S and the proposition expressed by S. A quick duckduckgo search didn't come up with anything. Pointers?

Here is a Liar-style one I came up with myself. Assume propositions are sets of worlds (which is the case I'm interested in). Consider the sentence

E: E expresses the empty set.

If E is true, then the proposition it expresses contains the actual world, in which case E doesn't express the empty set. So E can't be true. Since we've just proved not-E from no empirical assumptions, ~E expresses the set of all worlds. Hence E expresses the empty set. So E is true. Contradiction.

Quick logic question

Suppose you add to the language of first-order logic a sentence operator L for which you stipulate that all instances of

(L(p -> q) & Lp) -> Lq

are valid and that validity is closed under prefixing L's:

if p is valid, then so is Lp.

For example, L could be the modal operator 'necessarily', or it could mean the same as ''. If it means the same as '', then

Extensionality and Leibniz' Law

Extensional contexts are usually defined as positions in a sentence at which co-refering terms can be substituted without affecting the truth-value of the sentence. So 'Cicero' occupies an extensional position in 'Cicero denounced Catiline', but not in 'Philip said that Cicero denounced Catiline'. One might think that a term t occupies an extensional position in A(t) if and only if all instances of the following schema are true:

(LL) x=y -> A(x) <-> A(y).

'x=y' is true iff 'x' and 'y' co-refer, and 'A(x) <-> A(y)' is true iff 'A(x)' and 'A(y)' have the same truth-value. So to say that all instances of (LL) are true is to say that

Diodorus and actuality

Let [] and <> express alethic necessity and alethic possibility, let @ stand for 'actually', and L for 'it is unalterable that'. We are going to prove that if something happens, then it is unalterable that it happens.

We need the following principles:

1. A <-> <>@A.
   Something is the case iff it is possibly actually the case.
2. <>A -> L<>A.
   If something is alethically possible, one cannot make it alethically impossible.
3. L(A -> B) -> (LA -> LB).
   If A -> B and A are both unalterable, then so is B.
4. If A is provable then LA.
   Logical truths are unalterable.

Here is the proof, with a sea battle for illustration.

Names and descriptions in modal logic

In the old days, it was common to exclude individual constants from quantified modal logic in favour of Russellian descriptions. I can see how this works if we have either fixed domains (the same individuals populating all worlds) or possibilist quantifiers. But in such systems individual constants don't cause much trouble anyway. Can one also make the description move in more liberal systems? I don't see how, but I guess I'm just missing something obvious.

Consider a formula "possibly, a is F". We want to replace the name "a" by a description "the A". Does the description get narrow scope ("possibly, the A is F") or wide scope ("the A is possibly F")? Either way, we seem to get the wrong result.

The absence of a logic of desire

Reinventing broken wheels is more fun than patching small punctures in functioning ones. So here are some thoughts on desires that are undistorted by knowing the relevant literature.

It seems that unlike for rational belief, there are very few formal constraints on rational desire. For instance, if you desire A & B, it doesn't follow that you should desire A: I'd like to be beaten up and get a billion dollars compensation for it, but I don't desire to be beaten up. By the same example, you may desire A without desiring the disjunction A v B. More generally, all these principles are invalid for rational desire:

Are all truths entailed by logical truths?

Sorry, the server has been down quite a lot recently. Hope it's back to normal now.

Here's the talk I gave at Kioloa. It's partly identical to the talk I gave at GAP.6 in Berlin, but with more speculative ideas towards the end and less missionary appeals in between.

Are all truths entailed by logical truths? Depends on what we mean by "all truths" and "entailed" and "logical".

Let's understand a truth to be a true sentence of English, possibly enriched by logical vocabulary. As for entailment, let's distinguish metaphysical entailment (necessarily, if P then Q) from analytical (or conceptual or a priori) entailment. The precise definition of these notions, and the differences between them, won't matter.

Kripke's (Alleged) Argument for the Necessity of Identity Statements

I have often encountered in articles, talks and classes the following argument for the necessity of true identity statements, always attributed to Kripke:

1) a = b (assumption)
2) a = a
3) a = b (from 1, 2 by Leibniz' Law)

The argument is no good, and I think it is very doubtful that Kripke ever endorsed it.

(Unary) Numerical and Proportional Quantifiers

A quick Google search didn't come up with anything, so here are a couple of questions about the definability of certain unary quantifiers.

Just as all truth-functional operators are definable in terms of the Sheffer stroke, all numerical quantifiers are definable in terms of together with truth-functional operators and identity. By a numerical quantifier I mean a quantifier like "at least one", "at least two", "exactly 17", etc.: a quantifier Q such that the truth value of QxA(x) is determined by the finite cardinality of the objects satisfying A(x).

Is "true" hyper-intensional?

While I'm on the topic of repeating well-known mistakes, here's another idea I'm certainly not the first to come up with. Consider the liar paradox:

	L := "L is not true"
1)	Suppose L is true.
2)	Then "L is not true" is true (by definition of L).
3)	Then L is not true (by the Tarski Schema).
	etc.

The inference from (1) to (2) is only valid if "... is true" is an extensional or intensional context. So couldn't one block the paradox by declaring "true" hyper-intensional?

Slingshooting against the necessity of identity

The set is the empty set if p is false, otherwise it is the set of all numbers. Hence iff either p and q are both false or p and q are both true. So

Are logical truths true?

1. Hesperus is identical to Phosophorus.
2. By modal logic, .
3. Therefore, Hesperus is necessarily identical to Phosphorus.

1. Sometimes, one is obliged to do things that are not allowed.
2. By deontic logic, .
3. Therefore, sometimes one is obliged to things that are both allowed and not allowed.

1. Necessarily, if the moon essentially consists of green cheese, then it actually consists of green cheese.
2. By provability logic, .
3. Therefore, the moon essentially consists of green cheese.

1. It is now 20 seconds past 19:00 hours.
2. It is now 30 seconds past 19:00 hours.
3. If it is now 30 seconds past 19:00 hours, it is not now 20 seconds past 19:00 hours.
4. By propositional logic, .
5. Therefore, the moon is made of green cheese.

What's wrong with these arguments? They are invalid: their premises are true, their conclusion false. In each case, the fallacy is to assume that a principle valid in some formal system is also valid when translated into English.

Suppose ZFC proves its own inconsistency

Suppose we find a proof, in ZFC, that ZFC is inconsistent. Does it follow that ZFC is inconsistent?

On the one hand, if we could infer from ZFC ~Con(ZFC) that ZFC is inconsistent, we could contrapositively infer the consistency of ZFC & Con(ZFC) from Con(ZFC); and since ZFC & Con(ZFC) obviously entails Con(ZFC), ZFC & Con(ZFC) would thereby entail its own consistency. Which it only can if it is inconsistent (Gödel's second incompleteness theorem). So it seems that we can only infer that ZFC is inconsistent from the observation that ZFC entails its own inconsistency if we presupposes that ZFC & Con(ZFC) is inconsistent.

Metaphysical Modality and S5

Note to self: I sometimes say that metaphysical modality is of S5 type, when I should rather say only that it satisfies the characteristic axiom of S5, Mp -> LMp.

It isn't clear to me that metaphysical modality obeys all the S5 principles because it isn't even clear that it obeys T. One of the problems is what to say about Lp if p contains names of objects which may exist only contingently. The two most obvious proposals are: a) Lp is true iff p holds at all worlds where the named objects exist (in this sense, Hesperus is necessarily Hesperus, even though Hesperus exists contingently); b) Lp is true if p holds at all worlds (in this sense, Hesperus is not necessarily Hesperus, but it is necessary that if Hesperus exists then Hesperus is Hesperus). Either way violates T. On (a), let "F" express the property of coexisting with Hubert Humphrey; then "L(F(Hesperus) & F(Humphrey) -> F(Hesperus)) -> L(F(Hesperus) & F(Humphrey)) -> LF(Hesperus)" is false, even though it's an axiom of T. On (b), "L(Hesperus = Hesperus -> Hesperus = Hesperus)" is false, even though it's a theorem of T.

Substitutional Quantifiers

Until recently, I thought that there are no quantifiers in ordinary discourse for which a substitutional interpretation is adequate, or helpful. I still think this is true for almost all cases, including quantification over fictional and intentional objects. But here are two cases where a substitutional interpretation looks ok.

First. The world can be completely described in precise vocabulary. There are no vague objects with irreducibly vague bounderies or heights or colours. Rather, for many terms, like "Mount Everest", it is indeterminate exactly which perfectly precise object they denote. But it is very natural to say that Mount Everest has vague boundaries. Instead of denying it, I'm inclined to offer some kind of reinterpretation, such as: there are different objects slightly differing in their boundaries between which "Mount Everest" is indeterminate; or: for no precise boundaries b is it true that Mount Everest has boundaries b; or: for some precise boundaries b is it indeterminate whether Mount Everest has boundaries b. All these are true, and all of them could be meant by "Mount Everest has vague boundaries".

Truth, Provability and Mathematical Realism

Sometimes I think it's unfortunate that advanced logic and metamathematics usually presuppose various mathematical truths. For instance, in discussions on mathematical realism I've heard people arguing that by the first incompleteness theorem, mathematical truth can't be identified with provability in a formal deductive system. For, those people argue, the first incompleteness theorem proves that for any reasonable formalized system of mathematics, there is a true arithmetical sentence G that is unprovable in the system.

The Antidiagonal of the Primitive Recursive Functions

Just for fun, I'm reading Peter Smith's draft of his new book on Gödel's Incompleteness Theorems. So far, it's quite enjoyable. I might say more about it later. But here is something of which I'm not sure it's correct. (I'm also not sure it's false, that's why I'm posting it here.)

Smith shows that not all computable functions are primitive recursive by proving that the antidiagonal of the p.r. functions can't be p.r., even though it is intuitively computable. Having identified the p.r. functions with functions whose implementation doesn't require unbounded loops, he then asks why the antidiagonal function doesn't satisfy that condition:

At i, A is not F

I've thought a bit more about the comments Michael Fara left last week, and I don't find my points very convincing any more. The following is partly a correction, but mostly just thinking out loud about a more general semantic question.

The general question is how to interpret sentences of the form

1) At i, A is F
2) At i, A is not F

where 'i' denotes something like a time or a place or a world. There are a dozen proposals for interpretations of (1) in the temporal case, invoking temporal parts or relations to times or whatever. Most of these proposals can be applied to other indices as well. But let's put that aside. Suppose we understand how to interpret instances of (1) in easy cases. The hard cases I have in mind are cases where A doesn't exist exactly once at i. The precise definition of these cases depends on the question I've put aside, but I hope it is reasonably clear what I mean anyway. Not existing exactly once at i means either not existing at i at all, or multiply existing at i. Plausible examples of the first kind: I do not exist in 1758; I do not exist on Alpha Centauri; I do not exist at any world containing only empty space-time. Controversial examples of the second kind: if I get split into two persons tonight, I will doubly exist tomorrow; if river R has two branches where is crosses the border to country C, R doubly exists at the border to C; if at some world, two people resemble me to exactly the same degree in all extrinsic and intrinsic respects, I doubly exist at that world.

Tableaux Trouble

I have a problem with the new, free-variables powered version of my tree prover (only existing here on my hard disk at the moment): It doesn't terminate on some valid formulas, at least not within reasonable time.

A very nice feature of ordinary tableaux is that there is a mechanical procedure for building a ("canonical") tableau that will always close as long as there is any closed tableau for the input formula. To my knowledge, no such procedure has been found for free-variable tableaux. The problem, I think, is to decide at each stage whether to apply an ordinary expansion rule or the Closure rule. For many trees, it is best to apply Closure after every expansion. But for some formulas, this procedure will leave the tree forever open. The common response to this problem is apparently to try out all possible decisions at every point, using backtracking and iterated deepening of the search space.

Translating Free-Variable Tableaux

A free-variable tableau with root

x(Fx & y~Fy)

closes after 4 nodes and 1 application of Closure. A standard tableau, on the other hand, will have at least 6 nodes because the root formula must be used twice. So translating free-variable tableaux into standard tableaux is not as easy as I once thought. I wonder if it would suffice to add a rule to the free-variable construction that forbids Closure to unify a variable with a constant that first appears after the variable on the branch.

Fara and Williamson against the Counterpart Theory

A few comments on Counterparts and Actuality by Michael Fara and Timothy Williamson (via Brian, of course).

Fara and Williamson argue that if Quantified Modal Logic is enriched by an "actually" operator, then given some further assumptions there is no correct translation scheme from QML to Counterpart Theory. Here, a correct translation scheme is one that translates theorems of QML into theorems of CT and non-theorems of QML into non-theorems of CT. (theorems of which QML? -- good question; read on.).

Solution

Here comes the solution to this year's Christmas puzzle:

First, is the story in the museum true or false? The crucial question is whether the last sentence in it is true. It goes:

*) If the story is true, the oracle finds out that it is.

Under what conditions is (*) false? It is false iff i) the story in the museum is true, but ii) the oracle doesn't find out that it is. On the other hand, since (*) is part of that very story, if (*) is false, the story is also false. So if (*) is false, the story is both true and false. So (*) can't be false.

The Museum of the Myth (Another Christmas Puzzle)

The Museum of the Myth is not very comprehensive. In fact, it only contains a single story:

The Museum of the Myth is not very comprehensive. In fact, it only contains a single story. The story is not particularly exciting. Moreover, some people wonder whether it is actually false. If not, it would of course be incorrectly classified as a myth. So one day, the oracle is asked about the story. Luckily, the oracle is quite reliable: if the story is true, it undoubtedly finds out that it is.

The story is not particularly exciting. Moreover, some people wonder whether it is actually false. If not, it would of course be incorrectly classified as a myth. So one day, the oracle is asked about the story. Does it find out whether it is true?

Unhelpful Trees

Today I wondered about the connection between

Under certain ideal conditions, something is conceivable iff it is possible

and

Something is possible iff it is conceivable under certain ideal conditions.

So I asked my tree prover whether

1) y(Iyx(PxCxy))x(Pxy(IyCxy))

2) x(Pxy(IyCxy))y(Iyx(PxCxy)).

Substitutional Quantification

What's the difference between substitutional and objectual quantification? I'll use the old-fashioned round brackets for objectual quantifiers and square brackets for substitutional quantifiers. The standard interpretations are

OB) (x)A is true under an interpretation I iff for some new constant t, A(x/t) is true under all interpretations I' that differ from I at most in what they assign to t.

SUB) [x]A is true under an interpretation I iff for all constants t, A(x/t) is true under I.

Assume that predication (and the truth functors) is interpreted in one of the usual ways, for instance by ruling that Ft is true under I iff I(t) is in I(F). Then if (x)A is true under any interpretation, [x]A is also true under that interpretation. The converse holds iff every interpretation assigns every object in the domain to some constant.

Gödel's Ontological Proof

Let K be a class of sets such that whenever x is in K and x is a subset of y, then y is also in K. It follows that if the empty set is in K, then every set is in K. Let's rule this out by stipulating that some set is not in K. Thus every set that is in K is not empty. So instead of saying outright that some set is not empty we can instead say that it is in K, which sounds less controversial but really comes down to the same thing.

I think this is the trick in Gödel's ontological proof of god. His class K is the class of 'positive' properties, where properties are individuated intensionally. Gödel claims 1) that whenever some property Q is necessarily implied by a positive property P, then property Q is also positive (which is just the closure principle above), and 2) that not all properties are positive. On these assumptions saying that a property is positive means saying that it is not empty, that is, not necessarily uninstantiated. Hence when Gödel says that 3) necessary existence is a positive property he in effect says that a necessary being possibly exists, which in turn means that a necessary being actually exists.

The fallacy is to assume that there is any class of ('positive') properties satisfying (1)-(3).

Semantics and Model Theory

At first, I thought teaching students an informal semantics for predicate logic was only a compromise we had to choose because the real thing, formal model theory, is just too difficult for beginners. But now I'm inclined to believe that the informal semantics is itself the real thing. Maybe for those of us who have no quarrals with set theory, the difference is only superficial since both accounts assign the same truth conditions to all sentences, and truth conditions are all that matters. But that's not quite true. For example, when we talk about all sets (or all classes, or all things whatsoever), standard model theory is in trouble. I think it's silly to conclude that we can't really talk about all sets or classes or things. We obviously can do so in English, and we can also do so in (interpreted) first-order logic.

The Ordinary Conception of Logical Consequence

Another note on FOL75: In his talk, Wilfried Hodges argued that the logician's conception of logical consequence differs a lot from the ordinary conception. One of his points was that not all valid arguments are valid in any of our technical senses because the latter don't account for conceptual implication. That's of course true. But Hodges also claimed that consultation of Google shows that the ordinary conception of logical consequence is even further away from what most logicians think. For if one excludes results from sites about philosophy and logic the top results (e.g. 1, 2, 3, 4, 5) all look like this (from 5):

Detecting Satisfiability with Free-Variable Tableaux

Recently I suggested the following restriction on free-variable tableaux:

The gamma rule must not be applied if the result of its previous application has not yet been replaced by the closure rule.

I think I've now found a proof that the restriction preserves completeness:

Let (GAMMA) be a gamma-node that has been expanded with a variable y even though the free variable x introduced by the previous expansion is still on the tree. I'll show that before the elimination of x, every branch that can be closed by some unifier U can also be closed by a unifier U' that does not contain y in any way (that is, y is neither in the domain nor in the range of the unification, nor does it occur as an argument of anything in the range of the unification.) Hence the expansion with y is completely useless before the elimination of x.

Before the y-expansion, no branch at any stage contains y. After the y-expansion, every open subbranch of (GAMMA) contains the formula created by the y-expansion, let's call it F(y). Among these branches select the one that first gets closed by some unifier U containing y in any way. Now I'll show that, whenever at some stage a formula G(y) containing y occurs on this branch, we can extend the branch by adding the same formula with every occurrence of y replaced by x.

At the stage immediately after the y-expansion, the only formula containing y is F(y). And because (GAMMA) has previously also been expanded with x, and x has not yet been eliminated, the branch also contains F(x). Next, assume that G(y) occurs at some later stage of the branch. Then it has been introduced either by application of an ordinary alpha-delta rule or by the closure rule. If it has been introduced by application of an alpha-delta rule then we can just as well derive G(x) from the corresponding ancestor with x instead of y (which exists by induction hypothesis). Now for the closure rule. Assume first this application of closure does not close the branch (but rather some other branch). Then by assumption, the applied unifier does not contain y in any way, Moreover, it does not replace x by anything else. So in particular, it will not introduce any new occurrences of y in any formula, and it will not replace any occurrences of x and y. Hence if G(y) is the result of applying this unifier to some formula G'(y), then G(x) is the result of applying the unifier to the corresponding formula G'(x).

Assume finally that the branch is now closed by application of some unifier U that contains y in any way. Let C1, -C2 be the unified complementory pair. (At least one of C1, C2 contains y, otherwise U wouldn't be minimal.) Then as we've just shown, the branch also contains the pair C1(y/x), -C2(y/x). Let U' be like U except that every occurrence of y (in its domain or range or in an argument of anything in its range) is replaced by x. Clearly, if U unifies C1 and C2, then U' unifies C1(y/x), C2(y/x).

In the other posting I also mentioned that this restriction can't detect the satisfiability of x((Fx y Fy) Gx), which the Herbrand restriction on standard tableaux can. (A simpler example is x((Fx Fa) Ga).) These cases can be dealt with by simply incorporating the Herbrand restriction into the Free Variable system:

Restrict the Gamma Rule?

The following restriction might be a way out of the problems I mentioned in my last posting:

The gamma rule must not be applied if the result of its previous application has not yet been replaced by the Closure rule.

(The gamma rule deals with and formulae; the Closure rule is the rule that allows to replace dummy constants by real constants iff that leads to the closure of at least one branch.)

Counter-Models and Free-Variable Tableau Systems

I'm half-way into programming a more efficient tree prover, based on free-variable tableaux. But now I'm not sure any more if this is really what I want.

The basic idea in free-variable tableaux is that you use dummy constants to instantiate universally quantified formulas, and only replace these dummy constants by real constants if this allows you to close a branch. In automatised tableaux, this dramatically decreases the steps required for certain proofs. For example, my old tree prover internally creates an 860-node tree to prove xy(Fxy zFzz) x y Fxy x Fxx, whereas a free-variable system only needs 12 nodes.

An Impossible Question

A while ago, I asked: "Could Frege's ontology be a Henkin model?". I now believe that this question doesn't make sense: A standard model of second-order logic is a (standard) Henkin model. I should have asked: "Could Frege's ontology be a non-standard Henkin model?". Even this question is, uh, questionable, because the late Frege would have certainly rejected both a standard and a Henkin semantics, as both of these employ singular terms to denote the semantic values of function expressions. So I should rather have asked: "Are Frege's logical and semantical theses satisfiable in a non-standard Henkin model?" But now, I guess, the answer is trivially Yes, because nothing you can say in higher-order logic rules out a non-standard Henkin interpretation. However, my question was not meant to be trivial. I wanted to know whether Frege is comitted to there being more concepts (values of second-order quantifiers) than objects (values of first-order quantifiers), a claim that is true in standard models, but not in some non-standard models of any (really?)* second-order theory. Unfortunately, this question can't even be asked without violating Frege's semantical theses. As he himself notes in a letter to Russell:

I Got Hit On The Battleground God

Battleground God says that there are three contradictions in my views about God. Of course I don't believe my views are contradictory. Here are the alleged contradictions:

First, I accepted both of the following as true:

4. Any being which it is right to call God must want there to be as little suffering in the word as is possible.

12. If God exists she could make it so that everything now considered sinful becomes morally acceptable and everything that is now considered morally good becomes sinful.

Is this a contradiction? I'm not quite sure whether (12) is an indicative or a subjunctive conditional, but I think if it was subjunctive it would have to go "If God existed ..." or "If God would exist ...". So I think it's meant to be indicative (in the sense of "If God exists, then it is the case that: She could ..."). Like most people, I find it difficult to evaluate indicative conditionals with false antecedents, but at least for today I felt like embracing the Grice-Jackson-Lewis view that they are true. The website complained that I "say that God could make it so that everything now considered sinful becomes morally acceptable". But that's not what I said!

What does Russell's Paradox Teach in Semantics?

On Friday, I wrote:

Conclusion 2: If we want to avoid Bradley's regress, there is no reasonable way to defend the principle that every meaningful expression of our language has a semantic value. (Russell's paradox is an independent argument for the same conclusion.)

Today, I was trying to prove the statement in brackets. This is more difficult than I had thought.

Semantic paradoxes usually (always?) arise out of an unrestricted application of schemas like

Could Frege's Ontology be a Henkin Model?

Frege uses second-order quantification in both his formal and informal works. So far, I have always assumed that his second-order logic is standard second-order logic. But couldn't it also be second-order logic with Henkin semantics, which would in fact be a kind of first-order logic (compact, complete and skolem-löwenheimish)? Unfortunately, I know far too little about second-order logic to answer this question.

Are there any second-order statements that are satisfiable in standard semantics, but not in Henkin semantics? (I guess there must be: Wouldn't second-order logic with standard semantics have to be complete otherwise? Not sure.) If so, do any of Frege's theorems belong to these?

Exercises and Puzzles II

I've finally managed to introduce the provability predicate and its properties without mentioning representability and recursiveness. The exercise is then to derive Löb's theorem and Gödel's incompleteness theorems. Unfortunately these deductions are not as simple as I thought they were. Probably too difficult for an introductory book.

I've also just made up this puzzle, which is not very difficult I think. ("Not very difficult" even in the ordinary sense of "not very difficult", not only in the David Chalmers sense.)

Exercises and Puzzles

I'm still doing exercises for the logic book. This is rather unpleasant because I have to use Microsoft Word. Getting back to Word after using reasonable document formats (like LaTeX) and editors (like Alpha) for a while is a very frustrating experience.

At the moment, I'm trying to find nice and simple versions of Gödel's Theorems that still leave something formal to prove (like deducing Löb's Theorem from provability properties). This turns out to be difficult because I don't have the space to introduce the concepts of representability and recursiveness.

Stealing Ideas (and a very difficult logic puzzle)

First, the puzzle:

In a certain country there are two Gods, called A and B. One of them (A or B, you don't know which) only tells the truth, the other one only falsehoods. One day you meet a God in this country and want to find out whether it's A or B. You're only allowed to ask a single yes/no question. Unfortunately, you don't understand the language of the Gods (even though they understand yours). All you know is that their words for "yes" and "no" are "qwer" and "poiu", but you don't know which of these means "yes", and which "no". With what question will you be able to find out whether it's A or B you're talking to?

I can't really say that I have made up this puzzle. Well, I have made it up, but I took all the main ingredients from puzzles by George Boolos, who himself owes them mainly to Raymond Smullyan and a computer scientist whose name I forgot.

Speculations on the Origin of "Incorrect" Quantifier Rules

The fact that it turned out so difficult to explain my question in sci.logic made me have a closer look at common axiomatic systems of the kind I was critizising. This was a good idea, because I found out that the systems used by Mendelson and Hodges are not of that kind after all. The only such system is the one used by Kutschera and Breitkopf, and as their logic book is German (and post-war), it is not surprising that nobody understood my problem. It is however interesting to compare the Kutschera/Breitkopf system with the systems of Mendelson, Hodges and others:

Why use incorrect rules of inference?

Call for logicians: I have to convince Prof. Beckermann to drop an incorrect rule of inference from the axiomatic system for predicate logic used in his logic book. The incorrect rule is that from

A B

one may derive

A x B(t/x)

provided that t does not occur in A.

What Montague Pointed Out

Today I found Montague's paper, and it turns out that I was wrong. Well, Field's presentation was not entirely correct: We shouldn't take Robinson arithmetic itself as R, but some extension of it that contains an additional primitive predicate "True" (T, for short). The extension need not say anything about this predicate. This is why T needn't represent truth in R. (If R says nothing about T, T either represents nothing at all or the inconsistent property, depending on how precisely we define representation.) Montague then shows, very much like Field, that any theory that contains R -- no matter if it's axiomatizable or not --, as well as every instance of

Truth, Field, Montague, and Robinson Arithmetic

So I've started to actually read Field's papers. Unfortunately I already got stuck on page 4 of "The Semantic Paradoxes and the Paradoxes of Truth". Field there discusses the following restriction of the naive truth schema:

T**) If True(p) then p.

He notes that this is rather weak, since it doesn't even imply that there are any truths at all. Hence, he says, one would presumably add principles like

Non-Standard Escape Routes

I've been busy working on the logic book, playing with music software, meeting friends, lazing around, looking after Magdalena (who was ill again), protesting against the war, and thinking that it was a good idea to have voted for Livingstone (as I did when I lived in London). I hope to get back to philosophy soon.

Teaching Predicate Logic

I'm thinking about how to introduce the semantics of predicate logic to beginning philosophy students. In particular, I'm interested in the interpretation of predicates and quantifiers. Last year in logic class, it seemed that most students were rather unhappy with the formal recursion on truth we were teaching them.

So I've just picked 15 random logic textbooks to see how they are doing it.

Group 1 (functions and sets): Interpretations are introduced as entities that assign to each n-ary predicate symbol a class of n-tuples of elements of the domain. (Machover, Beckermann, Bostock, Newton-Smith, Mendelson, Kutschera, Allen/Hand, Bühler)

Even More Thoughts about Thoughts

In my last posting, I argued that to escape the cardinality problem for thoughts Frege perhaps has to give up

1) For any things there is at least one concept under which all and only those things fall.

Now (1) is clearly false if, as I think, all there is are objects -- that is, if it makes sense to quantify over absolutely everything. But if not, as Frege thinks, denying (1) is not an option. A concept is a function from things to truth values. Given that functions are not themselves things, how could there fail to be such functions?

Too Many Thoughts

A while ago, I was discussing Adam Rieger's alleged paradox in Frege's ontology (here, here, and here). I'm still confident that the Russellian version of the paradox can be blocked. But on second thought, the cardinality version of the paradox appears to be much more difficult. Here it is again.

1) For any things there is at least one concept under which all and only those things fall.

2) For each of these concepts, there exists the thought that Ben Lomond falls under it.

3) All these thoughts are different.

4) All thoughts are objects.

From (1)-(3) it follows that there are more thoughts than objects (2^k if k is the number of objects), contradicting (4).

A Quine

When I take a break from philosophy I often find myself creating utterly useless computer programs. Today, for example, I've spent some hours on Quines. A Quine is a program that outputs its own source code. (Quines are so called because Quine, in "The Ways of Paradox" if I recall correctly, introduced the self-denoting expression "'appended to its own quotation' appended to its own quotation".) Making Quines is a lot of fun, and also a good training to avoid use/mention mistakes. I've just written several JavaScript Quines. Here is a particularly neat one (try it!):

Better trees, big trees

Sometime before christmas, Greg Restall spotted a bug in my tree prover and noticed that it didn't work with Internet Explorer on MacOS X. These problems should now be fixed. I've also started working on an implementation of proofs with identity and function symbols, but I'm not sure if I'll ever finish it.

I actually wrote the tree prover to check the results of another script, which is what I vaguely talk about in the Feedback section. This is what that other script would calculate if I'd ever get it done:

Solutions

Back to life. Here is the solution to the Christmas puzzles:

1. The king said that one day somebody will find a sound proof that he hasn't always said the truth. Now either this is true or it isn't. If it isn't, the king hasn't always said the truth. If it is, somebody will find such a proof, and since the conlusion of any sound proof is true, again the king hasn't always said the truth. So in any case, the king hasn't always said the truth.

2. The king had uttered only two sentences. By the above argument we know that one of them must be false. But we also know that the first one was true: Somebody really found the requested argument. So the second sentence must have been the false one. It said that the person who finds the argument will get the kingdom. Hence it was logically impossible to give the kingdom to the court jester.

A Christmas Puzzle

I'm too sick to blog. In the meantime, here is a puzzle I've made up for the second edition of Ansgar Beckermann's Einführung in die Logik. In fact, it's two puzzles.

Once upon a time an old and reticent king made the following announcement: "One day somebody will find a deductively sound argument proving that I haven't always said the truth. To this person I will bequeath my kindom." It was the court jester who first presented such an argument. How did the argument go?

Soon afterwards, the king died, and it came to be known that the above announcement was in fact the only sentences the king had spoken in his entire life. Thereafter, the court jester was refused the kingdom -- for logical reasons. Why?

Locating the paradox

Brian Weatherson correctly argues that, since premise 2 of argument Z is analytically true, it can be simplified to

Argument Z':
1. If the conclusion of argument Z' is true, then argument Z' isn't sound.
Therefore: Argument Z' isn't sound.

The paradox then arises in two different ways. First, for premise 1 to be false, it must be the case that 'Argument Z isn't sound' is true and argument Z is sound.

Second, and more interestingly, the falseness of premise 1 analytically implies that argument Z is sound, which in turn analytically implies that all premises of argument Z are true, which implies that premise 1 is true.

This second paradox can be further simplified to:

Argument Z'':
1. Argument Z'' isn't sound.
Therefore: Snow is white or snow isn't white.

A paradoxical argument

An argument is called sound if it is deductively valid and its premises are true. Now consider the following argument, which I'll dub 'argument Z':

1. If the conclusion of argument Z is true, then argument Z isn't sound.
2. If the conclusion of argument Z is not true, then argument Z isn't sound.
Therefore: Argument Z isn't sound.

Is argument Z sound? (If not, which premise is false?)

A true contradiction?

Let S be the sentence "S contains a quantifier that does not range over everything".

S (and every utterance of S) is contradictory. Interestingly, it is so even if the quantifier in S really does not range over everything. From which it follows that either there are true contradictions, or "S contains a quantifier that does not range over everything" is not true iff S contains a quantifier that does not range over everything.

Idle remarks on Russell's paradox and higher-order entities

Okay, as promised here comes the third and last part of my little series on Rieger's paradox. I will first describe a general version of Russell's paradox, of which Rieger's is a special case. Then I'll discuss whether Frege is already prey to the paradox by his admission of too many concepts. Whether he is will depend on whether it makes sense to say that there are entities which are not first-order entities. I'm sorry that there is probably nothing new in all this.

First, the general version of Russell's paradox.

Is Frege save?

Yesterday, I argued that Frege can escape Rieger's Paradox if it is allowed that the thought that Fb might equal the thought that Gb (briefly, [Fb]=[Gb]) even if F and G are not coextensive.

In particular, to escape the paradox there has to be a concept F, such that [Fb]=[Ob] even though O([Ob]) and F([Ob]). O, recall, is defined thus:

O(x) iff F(x=[Fb]Fx)

I did not say how this F might look like. Here is a good candidate:

Saving Frege from another contradiction

In the October issue of Analysis, Adam Rieger presents the following paradox in Frege's ontology.

For any object b and first order concept F, there is the thought [Fb] that b falls under F. Let Con and Obj be functions that yield the (referents of the) constituents of such thoughts: Con([Fb])=F, and Obj([Fb])=b. We stipulate moreover that 'b' shall denote the mountain Ben Lomond, and define O ("ordinary") as follows:

Tree Proof Generator Update

I've spent some more time on the Tree Proof Generator. The algorithm is now a lot faster, more information is displayed during calculation, and there are new buttons to control the drawing.

This formula (the last one on the Examples page) is quite interesting: After the quantifiers have all been dealt with, there are 36 formulas on the tree that have to be broken down by the truth-functional rules. I let it run for several hours. When finally Mozilla ran out of memory it had developed just 25 of those 36 formulas, building a tree with 179797 nodes!

I've got that formula from David Bostock's very fine book "Intermediate Logic", where he says that "the tedium of writing out a completed tableau" for this formula would be "very considerable" (p.177). Indeed.