Showing posts with label logic. Show all posts
Showing posts with label logic. Show all posts

Friday, January 24, 2025

A Note on the Strength of Disentangled Truth-Theories

Abstract

So-called `disentangled' truth-theories are supposed to prevent assumptions about the truth of statements in the object-language from inadvertently strengthening the background syntax. In earlier work, I proved some limitative results in an attempt to show that the strategy works, but those results leave several questions unanswered. We address some of them here. We also discuss a subtlety that has so far been overlooked in discussions of these theories.

Find it here: https://philpapers.org/rec/HECANO-6

This is another short paper that is a kind of appendix to an in-progress paper on the question whether there are or could be epistemically potent proofs of consistency. It may be submitted to a journal like Thought or Analysis at some point.

Thursday, January 23, 2025

Some Remarks on 'Logical' Reflection

 Abstract:

Cezary Cieśliński has proved a result shows that highlights `logical reflection': The principle that every logically provable sentence is true. He suggests further that this result has a good deal of philosophical significance, specifically for the so-called `conservativeness argument' against deflationism. This note discusses the question to what extent Cieśliński's result generalizes, and just how strong `logical reflection' is, and suggests that the answers to these questions call the philosophical (though not the technical) significance of Cieśliński's result into doubt.  

On my website: http://rkheck.frege.org/pdf/unpublished/CieslinskiNote.pdf

On PhilPapers: https://philpapers.org/rec/HECSRO

This is a short paper, under 4000 words, which I will probably submit to Thought or Analysis. But mostly it's a kind of appendix to an in-progress paper on the question whether there can be a 'cogent' consistency proof. That one will be posted before long.

Saturday, March 18, 2017

LaTeX Notation for Numerals

It is common in meta-mathematics to use the notation n to mean the numeral for the number n, that is: S...S(0), where S is a symbol for successor and there are n S's in the numeral for n. In LaTeX, one can typeset this notation using \overline{n} in math mode. Unfortunately, this does not always look very good: The height of the bar will vary with the height of the contained character(s), so the heights of the bars in \overline{n} and \overline{k} will not match.

The solution is to use a 'strut': an invisible (because 0 width) rule that functions only to set the height of the bar:
\newlength{\numheight}
\setlength{\numheight}{\fontcharht\font`0}
\newcommand\numeral[1]{\overline{\rule{0pt}{\numheight}#1}

It would perhaps be better to use the current font in \numheight, but I've never had a problem with this in practice.

Sunday, March 5, 2017

A Bound in Gödel 1931

When teaching Gödel's famous 1931 paper on the incompleteness theorems this semester, I got hung up on one of the bounds he gives in the course of the 45 definitions of primitive recursive notions. This is the case of concatenation. Recall that Gödel here codes finite sequences via prime factorization, so the sequence <a1, ..., an> is coded as: 2a1 × ... ×pnan, where pn is the nth prime. The 'star function' is then defined as follows:
x * y = μz≤Pr[l(x) + l(y)]x+y {∀n≤l(x)(n Gl z = n Gl x) &

     ∀n≤l(y)(0<n → (n + l(x)) Gl z = n Gl y)}
Here, l(x) is the length of the sequence x; n Gl x is the nth element of that sequence. So the definition says that x * y is the least number coding a sequence that agrees with x on its first l(x) elements and agrees with y on the next l(y) elements. Of course, there is such a number (and, actually, given how "Gl" works, there are infinitely many). The bound is needed to guarantee that * is primitive recursive.

The question, though, is how the bound is supposed to work. Gödel does not often discuss his bounds, which tend to be pretty loose, but he does explain one of them in footnote 35. And if one follows the sort of reasoning Gödel uses there, then it is difficult to see how to get the bound in the above.

I asked a question about this on the Foundations of Mathematics mailing list, and Alasdair Urquhart took the bait and replied with an elegant proof showing why Gödel's bound works. I thought I'd record a version of it here, in case anyone else has a similar question.

First, we show, by a straightforward induction on n, that 2a1 × ... ×pnan ≤ pna1 + ... + an.

Now let <a1, ..., an> and <b1, ..., bm> be two sequences. The code of their concatenation is:
2a1 × ... ×pnan × pn+1b1 × ... × pn+mbm ≤ pn+ma1 + ... + an + b1 + ... + bm
Moreover,
a1 + ... + an ≤ 2a1 + ... + pnan ≤ 2a1 × ... × pnan = x
and similarly for the other sequence. (Note that the last inequality depends upon the fact that none of the ai = 0, but Gödel's coding of sequences only works for positive integers.) So
a1 + ... + an + an+1 + ... + an+m ≤ x + y
which gives Gödel's bound.

Tuesday, February 12, 2013

The Diagonal Lemma: An Informal Exposition

A couple years ago, I got a stream of emails from someone who shall remain nameless, who was completely convinced that there was something desperately wrong with the proof of the incompleteness theorem because of some kind of circularity in the diagonal lemma. I ended up writing him a long email explaining the diagonal lemma in terms of informal syntax, much as Quine does in Mathematical Logic.
I realized shortly thereafter that many of my students are in a position that is not so different. The diagonal lemma just is very hard to understand, in large part because its proof, in most expositions, in bound up with things like Gödel numbering, the representability of recursive functions, and the like, that really don't have very much to do with the diagonal lemma itself. The diagonal lemma is really a fact about syntax, not about arithmetic, and when one explains it in those terms it makes a whole lot more sense.
I therefore converted my original email into a short (five page) document that I've now used in a couple different courses. It can be found on my website.