In Good Company

The long awaited (by me, at least) article by Paolo Mancosu on the Good Company objection has been out in the Review for a few months and I missed it.  You probably didn’t, if you care about these things, but anyway:

In a recent article (Mancosu, 2009), I have explored the historical, mathematical, and philosophical issues related to the new theory of numerosities. The theory of numerosities provides a context in which to assign ‘sizes’ to infinite sets of natural numbers in such a way as to preserve the part-whole principle, namely if a set A is properly included in B then the numerosity of A is strictly less than the numerosity of B. Numerosity assignments differ from the standard assignment of size provided by Cantor’s cardinality assignments. In this paper I generalize some worries, raised by Richard Heck, emerging from the theory of numerosities to a line of thought resulting in what I call a ‘good company’ objection to Hume’s Principle (HP). The paper is centered around five main parts. The first (§3) takes a historical look at nineteenth-century attributions of equality of numbers in terms of one-one correlation and argues that there was no agreement as to how to extend such determinations to infinite sets of objects. This leads to the second part (§4) where I show that there are countably-infinite many abstraction principles that are ‘good’, in the sense that they share the same virtues of HP (or so I claim) and from which we can derive the axioms of second-order arithmetic. All the principles I present agree with HP in the assignment of numbers to finite concepts but diverge from it in the assignment of numbers to infinite concepts. The third part (§5) connects this material to a debate on Finite Hume’s Principle between Heck and MacBride. The fourth part (§6) states the ‘good company’ objection as a generalization of Heck’s objection to the analyticity of HP based on the theory of numerosities. In the same section I offer a taxonomy of possible neo-logicist responses to the ‘good company’ objection. Finally, §7 makes a foray into the relevance of this material for the issue of cross-sortal identifications for abstractions.

Hilbert’s Epsilon and Tau in Logic, Informatics and Linguistics

Organized by Université de Montpellier and LIRMM-CNRS with the support of the ANR project Polymnie, June 10-12 will see a really neat workshop on the use of epsilons and choice functions.  The program is now online; if you can, you should go.

This workshop aims at promoting work on Hilbert’s Epsilon in a number of relevant fields ranging from Philosophy and Mathematics to Linguistics and Informatics. The Epsilon and Tau operators were introduced by David Hilbert, inspired by Russell’s Iota operator for definite descriptions, as binding operators that form terms from formulae. One of their main features is that substitution with Epsilon and Tau terms expresses quantification. This leads to a calculus which is a strict and conservative extension of First Order Predicate Logic. The calculus was developed for studying first order logic in view of the program of providing a rigorous foundation of mathematics via syntactic consistency proofs. The first relevant outcomes that certainly deserve a mention are the two “Epsilon Theorems” (similar to quantifiers elimination), the first correct proof of Herbrand’s theorem or the use of Epsilon operator in Bourbaki’s Éléments de Mathématique. In nineties, renewing Russell’s ideas on definite descriptions, there has been some work on the interpretation of determiners and noun phrases with Hilbert’s epsilon. Nowadays the interest in the Epsilon substitution method has spread in a variety of fields : Mathematics, Logic, Philosophy, History of Mathematics, Linguistics, Type Theory, Computer science, Category Theory and others.

Beside the famous Grundlagen der Mathematik of Hilbert and Bernays, a general presentation of the topic can be found in the webpages of the Stanford Encyclopedia of Philosophy and Internet Encyclopedia of Philosophy.

Git for Victorianists, erm, Philosophers (pt. 4)

(Continues part 1, part 2, and part 3; fork the full text on GitHub)

Branches

Programmers are fond of using “branches” in their code. A code branch is a version of the entire project that shares it change history, but includes some changes the main branch (usually called “master”) does not (yet) contain. This is useful, for instance, when you are adding new functions to your program. The new functions may be implemented in a separate file that is added to the project, but it may also require changes in other, existing parts of the project. Until the new function is developed and tested, you don’t want to isolate these changes in a development area. After all, the other parts of the program are still used, and perhaps even continue to be developed. Adding possibly buggy code in the process of developing the new function shouldn’t interfere with development of the old, tried-and-true parts of the project. So to do that, a software project will add a “feature” branch where all the new development takes place, and when it’s complete the changes will be merged back into the “master” branch.

This is not a situation that a run-of-the-mill collaborative writing project will encounter. But it is useful to understand what branches are, because behind the scenes, Git’s functionality for dealing with branches is what’s behind most of the features discussed so far. For instance, pulling changes from a remote repository in fact uses this functionality. If your repository is linked to a remote, the content of the remote is actually a branch of your repository, “origin/master”. The git fetch command updates the content of this branch to the content of the remote. The git merge command allows you to merge a branch into another, e.g., git merge origin/master would merge the content of the “origin/master” branch into the current “master” branch. An that’s actually what git pull does: first git fetch to update the “origin/master” branch, then git merge origin/master to merge the remote changes into your local “master” branch. Similarly, merging a pull request is a combination of a git fetch the contents of your contributor’s repository into a, say, “gitonaut/master” branch, and then merging that branch into your own “master” branch. GitHub and GitLab do this behind the scenes when you click on the “merge pull request” button, you can also do it by hand. A situation where you might want to do that is if you want to adjust the changes made by your contributor before merging into the “master” branch.

There are other situations when branches might be helpful. One is analogous to the “feature” branch in a software project. Suppose you are working on a collaborative book project (such as the Open Logic Text), and you want to add a chapter on a new topic. You will star writing the chapter in a separate file, of course. But there are perhaps other areas of the book that will be affected, e.g., the table of contents, cross-references, the bibliography, the index. While your new chapter is not yet read for prime time, you may still want to exclude any mention of the new material. Someone printing the text shouldn’t have to print your half-baked ideas and placeholder bibliography entries. At the same time, /you/ do want to be able to see what the book will look like with all the new cross-references etc. The solution is to work on your new chapter in a branch. When your new chapter is ready, you can then merge your branch into “master”. Before it is ready, any changes to the master branch can also be merged into your “feature” branch, so the copy of the project in which you’re working on the new chapter will also include all the changes you or other people make to other parts of the text.

Another possible application of branches is when you want to develop a slightly different version of your project. For instance, say you are co-authoring a paper using git, and you’re ready to send it to a conference. You can start a new branch, and anonymize the paper on that branch. That’s the version you submit. You get some feedback at the conference which you incorporate, and fix some typos or add a reference or two to the master branch. Now you want to send it to a journal. You’ve made changes to the original paper, but it does take some effort to anonymize it. Rather than anonymize it again, you can just switch to the anonymized branch, marge the changes from the master branch, and have an updated but still anonymized version of the paper.

Let’s see how this works in action. Suppose you want to prepare a version of this paper for a slightly different audience, e.g., Victorianists instead of philosophers. We are going to keep the Victorianist version on a branch, “victorianists”.

To make a new branch, say

git branch victorianists

To switch to work on the branch, say

git checkout victorianists

Now any change you make and commit will be committed to the “victorianists” branch, instead of the “master” branch. If you say git push, Git will first complain that your new branch has no matching branch on GitHub.

fatal: The current branch victorianists has no upstream branch.
To push the current branch and set the remote as upstream, use

    git push --set-upstream origin victorianists

After you do that, your remote will be updated with a matching branch, and you can push the branch to the GitHub repository. You can make the changes to the text required on the branch, e.g., change references to LaTeX to TEI-XML. You can look at what that would like here.

To add more material to the text, or to fix typos, you probably want to switch back to the “master” branch.

git checkout master

Now the file will be reset to the version on the “master” branch. Any changes you commit from here on will be recorded in the “master” version, but not in the “victorianists” version. You can merge those changes into the “victorianists” branch using

git checkout victorianists
git merge master

so the Victorianists also get the added content and corrections.

Branches are useful sometimes, it’s good to understand how they work because that’s how many of Git’s features work “behind the scenes”, but they can also be confusing. If you do work with branches, you have to be extra careful to make sure you commit your changes to the right branches, and that you merge changes from the “master” branch regularly to avoid having to do it manually when the branches get too far out of sync. It’s now also very important to git pull often, othrwise you will have to merge changes from the remote not just into “master” but also into your feature branches.

 

Git for Philosophers (pt. 3)

(Continues part 1 and part 2; fork the full text on GitHub)

Forks and Pull Requests

If you have push access to a repository, you can sync your local clone with the remte on GitHub or GitLab directly. But many projects do allow push access only to a select group of people to make sure noone breaks anything. There are some larger collaborative writing projects like this, e.g., the HoTT Book and the Open Logic Text. You may wish to set up a project in such a way, to allow others to use, improve, and contribute to your project but while retaining control. Git is set up for this kind of scenario, it is called the “fork and pull” model of collaboration. In the fork and pull model, your collaorators each work on their own fork of the repository. Forking your repository is easy: both GitHub and GitLab display a fork button on the repository page. Your contributor clicks on that button, and a complete copy of the repository appears in their own GitHub/GitLab user space. If your repository lives at github.com/reader/project then their fork will live at github.com/collaborator/project. Instead of cloning the author/project repository, and pushing to it directly, they clone the collaborator/project repository and work on that private copy.

The collaborator/project repository is a complete copy, but it is not automatically kept in sync with reader/project. If your collaborator wants to have changes to your repository included also in their forks, they have to do this explicitly. If you have forked a repository, e.g., you have your own fork reader/OpenLogic of the OpenLogicProject/OpenLogic, you also have to explicitly merge changes into your fork from the original repository. You do this on your local clone on your own computer. Suppose you have cloned the reader/OpenLogic repository (your own fork) on your computer’s harddrive. It is already set up with a remote, your fork on GitHub. Pulling and pushin usually happen between your local clone and the remote fork reader/OpenLogic. To sync changes from the original OpenLogicProject/OpenLogic repository, you have to add it as anoter remote:

git remote add upstream https://github.com/OpenLogicProject/OpenLogic.git

Here upstream is the traditional name given to the original remote repository (vs. origin which is the remote repository on your own GitHub account, which happens to be a fork). Of course, the URL will point to whichever upstream repository you want to track.

Now you can tell Git to pull changes, not from the remote origin but from upstream, and merge them into your local repository using the command

git pull upstream master

Your local clone of reader/OpenLogic contains all the changes from the upstream OpenLogicProject/OpenLogic. To update these changes also in your own fork on GitHub, simply say

git push

Having a copy of a repository, and keeping it up-to-date with the original, “upstream” version, is only half the fun. The real advantage of being able to edit your own /fork/ — rather than just your own /copy/ — is that your additions and corrections can be incorporated back into the source repository. For instance, you might want to correct a typo, help with some copyediting, or, in a collaborative project, contribute additional material. The editors of the source repository may want to retain control over who gets to contribute what, and so they don’t give push access to anyone. But you can work on your own fork, and make those corrections and additions there first.

When you are done, you can send a /pull request/ to the owners of the source repository. GitHub/GitLab remember from which repository your fork was created, and will display if your fork contains changes not in the upstream source repository. Here’s what user gitonaut sees after they’ve added some material to their fork of this file:

GitHub fork view

When your fork is “ahead” of the original repository, you can send a /pull request/: alert the owners of the source repository that your fork contains changes which they might want to pull, i.e., merge into their repository.

Creating pull request

The pull request shows up as an “issue” in the GitHub view of the source repository. The owners of the original repository can see who sent the pull request, read the description, look at the line-by-line changes in all affected files. For instance, the pull request adding a paragraph above in this file by gitonaut looked like this:

Viewing changes in pull request

The repository owners can respond to the pull request with a comment, e.g., asking for clarification or explaining why they can’t merge the proposed changes. It is also possible to add comments to individual lines in the commits making up the pull request. If the changes in the pull request are simple and do not conflict with any changes that have meanwhile been made to the source repository, GitHub will show a button that allows the repository owner to merge the changes automatically. Your contribution can be easily incorporated into the repository in this way. The history of the files you changed will contain a record of the change merged via the pull request, and you will be listed among the contributors to the files you changed. For instance, this file now lists gitonaut as a contributor, and the “blame” view of the file shows the contributions made by gitonaut.

Vienna Circle Exhibition

As part of the 650-year celebration of the University of Vienna, the Institute Vienna Circle is putting on an exhibition on the Vienna Circle. The exhibition opens tomorrow.

A central part of our exhibition will be devoted to the history of the racist and political persecution of intellectuals and scholars, leading to the exodus of the Vienna Circle and the brutal suppression of Vienna’s ‘Golden Autumn’. Many of the central topics of the Vienna Circle are still with us. There is  a direct line leading from the abstract investigations of Carnap and Gödel on symbolic logic to programmed computers and the algorithms governing our life today. The ‘Vienna pictorial statistics’ of Neurath led to the pictograms that  continue to direct  streams of passengers all over the world. The Circle also had close contacts with eminent writers and architects. There was  a tight connection with quantum physics and with Albert Einstein (Schlick was Einstein’s prophet and ‘Hausphilosoph’, and Gödel became Einstein’s best friend). … The exhibition will deal with the extraordinary intellectual and cultural feats that led to the emergence of the Vienna Circle. At the same time, it will also take a closer look at the terrible ravages of political fanaticism and anti-semitism, and the ruthless destruction of a pinnacle of exact thinking.  Last not least, the exhibition will  reveal the international impact that the Vienna Circle would have.

You may not be able to attend the exhibition itself, but there will be a catalog, and Fritz Stadler’s The Vienna Circle is out soon in a 2nd edition.

Karl Sigmund, Sie nannten sich Der Wiener Kreis: Exaktes Denken am Rand des Untergangs. Springer

Christoph Limbeck-Lilienau, Friedrich Stadler, The Vienna Circle: Texts and Pictures at an Exhibition. LIT Verlag

Friedrich Stadler, The Vienna Circle: Studies in the Origins, Development, and Influence of Logical Empiricism. 2nd ed. Springer

(Related: Gödel’s Vienna)

Git for Philosophers (pt. 2)

Continues Git for Philosophers (pt. 1)

Collaborative Writing with Git

Collaborative writing presents similar issues as collaborative programming: different people making changes to the same document from different locations. Sending the document back and forth is inefficient: only one person can work on it at a time, and there is a risk of changes being made in parallel which are then either overlooked or which are hard to reconcile. Collaborative editing tools (e.g., Google Docs for Word documents, shared LaTeX editors like ShareLaTeX and Overleaf help if you’re using those formats, but have their own drawbacks (e.g., they can’t be used offline). Simply keeping your shared Document in a Dropbox folder is a partial solution, but the doesn’t solve the issue of conflicting changes to your shared document. Dropbox assumes that you know what you’re doing. So if you make a change to a document on your office desktop, and then make a change to the same document on your laptop, the later change will silently overwrite the former. If for some reason you didn’t update the file on your laptop with the changes from your office desktop (say, if you were without an internet connection), these changes will be gone from the document when you save it the second time. The changes will be preserved in a previous version of the document, since Dropbox keeps every intermediate version — but it might take you a while to notice that your change got lost, and it might take you a while to find the most recent version of the file on Dropbox that still has it.

Dropbox is a bit more careful when two different users make changes to the same document in a shared Dropbox folder. If your collaborator has edited the file while you were away, you will see the changes automatically. But if you’ve had your file open in an editor while your collaborator has made changes — perhaps even with your laptop asleep! — Dropbox will realize that there may be a conflict between your version of the document and your collaborator’s. But it won’t know what to do. Rather than overwrite one of your changes, Dropbox will make a copy of the file you’re working on simultaneously, and leave you to figure out which version is more up-to-date and how to reconcile the two copies into one. So if author A and author B are both working on a document, author A adds a sentence to the introduction and at the same time author B adds a sentence to the conclusion, your shared Dropbox folder will suddenly contain a second version of the document, document (author B's conflicted copy).doc, say. It will contain the additional sentence in the conclusion, but not author A’s additional sentence in the introduction, and document.doc will contain author A’s sentence but not author B’s. Dropbox will leave it to you to figure out who has made what change where and how to reconcile them and integrate the two documents into a single one. This is annoying and complicated, especially if the conflict goes unnoticed for a while.

Using Git helps you avoid these problems to the extent it is possible to avoid them.

When you have set up a repository for your writing project (say, containing a LaTeX document plus a BibTeX file for references), you can edit the files, commit your changes to generate a new revision, and periodically push your revisions to the remote repository on GitHub or GitLab. If you are working on the project with someone else, you can give them access to the repository as well. If they have push access, they can send their own revisions to the shared repository just like you do.

Git keeps track of the state of your own local repository and the remote on GitHub/GitLab. The command

git status

will prompt Git to display the status of your repository: which branch you are on (typically, this is the master branch, but more about branches later), whether your local version of the repository is up to date with the remote or not, which files have changes that are waiting to be committed, and which files are untracked. If you have commits that you have not pushed to the remote yet, Git will report something like “Your branch is ahead of ‘origin/master’ by 1 commit.” The remote repository is usually called origin, and the remote branch that corresponds to your local master branch is then called origin/master. It might happen that your branch is behind the remote: if your collaborator has pushed changes to the shared remote, there will be commits on the remote that you don’t yet have in your local repository. Before you can push your changes, you will have to incorporate your collaborators’ changes into your own local version of your paper.

If your document is under Git control, you have to pull changes from the shared repository before you see what your co-author has done. By the same token, you and they have to remember to push new commits to the repository, or there won’t be any changes to pull. In the crucial case where you have both made changes at the same time, however, Git will handle the discrepancies gracefully.

In the best case scenario, you and your co-author have edited the same file, but you haven’t edited the same part of the file: say, they added a footnote to the introduction, you have cleaned up a passage in a middle section. If they have committed their changes and pushed to the shared remote, Git won’t let you push your changes. You’ll get an error message like

! [rejected]        master -> master (fetch first)

If your changes do not conflict (were not made to the same line of text), Git can fix this automatically. Just say

git pull

Git will then download (“fetch”) the changes from the remote and automatically merge them with your version of the repository, creating a new revision which includes both your changes and the older changes by your co-author. Your repository is now ahead of the remote by one commit (the act of merging your co-authors changes with your own created a new revision), and you can push the combined changes to the remote.

If you did happen to both make changes that cannot be merged automatically, Git will alert you to this fact:

CONFLICT (content): Merge conflict in <filenames>
Automatic merge failed; fix conflicts and then commit the result.

Instead of letting you fend for yourself in figuring out what has changed and where, Git will tell you exactly what you have to fix. The files with editing conflicts will now contain the conflicting lines, indicating your and their changes, e.g.:

<<<<<<< HEAD
what you wrote
=======
what your co-author wrote
>>>>>>> hash code of your co-author's commit

in the relevant place in the document. Fix up just that part of the document. Then say git commit -a. Your local repository now contains a conflict-free version of both your changes, which is ahead of the shared repository by one commit, and Git will again let you push to the remote. When your co-author returns to work and says git pull, they will have the merged, clean version of the document.

Note that your intervention is only required if both you and your co-author have made changes to the very same line of text, otherwise Git will merge the changes automatically. This includes the case where one of you adds a paragraph and the other one cuts text somewhere else in the file: after git pull the file will have the new paragraph but the text you deleted will still be gone.

(Continued in part 3; Read, fork, or download the full document on GitHub.)

Nerdiest Paper Ever? Green, Rossberg, Ebert on the Typography of Frege’s Grundgesetze

In the most recent issue of the Bulletin, J. J. Green, Marcus Rossberg and Philip Ebert discuss the typography of Frege’s Grundgesetze.

J. J. Green, Marcus Rossberg and Philip A. Ebert, “The Convenience of the Typesetter; Notation and Typography in Frege’s Grundgesetze der Arithmetik”, Bulletin of Symbolic Logic, vol. 21, no. 1, 15–30, Mar. 2015. (doi, pdf)

(Found on J. J. Green’s page on Frege, which also includes a Grundgesetze font and a link to a complete digital edition of the German original. The website for the Grundgesetze translation project is here.)