
44838.577006
One of the most wonderful parts of the North American Summer School for Language, Logic and Information is the opportunity it a↵ords young scholars to discuss their work with experts. By the same token, it is often inspiring for established researchers to see the creative directions in which recent work is being taken.

371150.577058
This paper deals with two issues. First, it identifies structured propositions with logical procedures. Second, it considers various rigorous definitions of the granularity of procedures, hence also of structured propositions, and comes out in favour of one of them. As for the first point, structured propositions are explicated as algorithmically structured procedures. I show that these procedures are structured wholes that are assigned to expressions as their meanings, and their constituents are subprocedures occurring in executed mode (as opposed to displayed mode). Moreover, procedures are not mere aggregates of their parts; rather, procedural constituents mutually interact. As for the second point, there is no universal criterion of the structural isomorphism of meanings, hence of cohyperintensionality, hence of synonymy for every kind of language. The positive result I present is an ordered set of rigorously defined criteria of finegrained individuation in terms of the structure of procedures. Hence procedural semantics provides a solution to the problem of the granularity of cohyperintensionality.

629513.577076
Many of us are tempted by the thought that the future is open, whereas the past is not. The future might unfold one way, or it might unfold another; but the past, having occurred, is now settled. In previous work we presented an account of what openness consists in: roughly, that the openness of the future is a matter of it being metaphysically indeterminate how things will turn out to be. We were previously concerned merely with presenting the view and exploring its consequences; we did not attempt to argue for it over rival accounts. That is what we will aim to do in this paper.

1663165.577092
The revised, surelymorenatural, disjunction elimination rule mentioned in the last post is, of course, Neil Tennant’s longstanding proposal — and the quote about the undesirability of using explosion in justifying an inference like disjunctive syllogism is from him. …

1708165.577106
The Univalent Foundations (UF) of mathematics take the point of view that spatial notions (e.g. “point” and “path”) are fundamental, rather than derived, and that all of mathematics can be encoded in terms of them. We will argue that this new point of view has important implications for philosophy, and especially for those parts of analytic philosophy that take set theory and firstorder logic as their benchmark of rigor. To do so, we will explore the connection between foundations and philosophy, outline what is distinctive about the logic of UF, and then describe new philosophical theses one can express in terms of this new logic.

1823340.57712
If mathematics is regarded as a science, then the philosophy of
mathematics can be regarded as a branch of the philosophy of science,
next to disciplines such as the philosophy of physics and the
philosophy of biology. However, because of its subject matter, the
philosophy of mathematics occupies a special place in the philosophy of
science. Whereas the natural sciences investigate entities that are
located in space in time, it is not at all obvious that this also the
case of the objects that are studied in mathematics. In addition to
that, the methods of investigation of mathematics differ markedly from
the methods of investigation in the natural sciences.

2199996.577133
Mathematical Platonists say that sets and numbers exist. But there is a standard epistemological problem: How do we have epistemic access to the sets to the extent of knowing some of the axioms they satisfy? …

2201855.577147
I'm working on a paper, "Kant Meets Cyberpunk", in which I'll argue that if we are living in a simulation  that is, if we are conscious AIs living in an artificial computational environment  then there's no particularly good reason to think that the computer that is running our simulation is a material computer. …

2511189.577163
As a new foundational language for mathematics with its very different idea as to the status of logic, we should expect homotopy type theory to shed new light on some of the problems of philosophy which have been treated by logic. In this article, definite description, and in particular its employment within mathematics, is formulated within the type theory. Homotopy type theory has been proposed as an inherently structuralist foundational language for mathematics. Using the new formulation of definite descriptions, opportunities to express ‘the structure of’ within homotopy type theory are explored, and it is shown there is little or no need for this expression.

2741996.577176
J. D. Hamkins and J. Reitz, “The settheoretic universe $V$ is not necessarily a classforcing extension of HOD,” ArXiv eprints, 2017. (manuscript under review)
Citation arχiv
@ARTICLE{HamkinsReitz:ThesettheoreticuniverseisnotnecessarilyaforcingextensionofHOD,
author = {Joel David Hamkins and Jonas Reitz},
title = {The settheoretic universe $V$ is not necessarily a classforcing extension of HOD},
journal = {ArXiv eprints},
year = {2017},
volume = {},
number = {},
pages = {},
month = {September},
note = {manuscript under review},
abstract = {},
keywords = {},
source = {},
doi = {},
eprint = {1709.06062},
archivePrefix = {arXiv},
primaryClass = {math.LO},
url = {http://jdh.hamkins.org/theuniverseneednotbeaclassforcingextensionofhod},
}
Abstract. …

2933774.57719
An action is something that takes place in the world, and that makes a difference to what the world looks like. Thus, actions are maps from states of the world to new states of the world. Actions can be of various kinds. The action of spilling coffee changes the state of your trousers. The action of telling a lie to your friend changes your friends state of mind (and maybe the state of your soul). The action of multiplying two numbers changes the state of certain registers in your computer. Despite the differences between these various kinds of actions, we will see that they can all be covered under the same logical umbrella.

3013675.577204
In this paper, we study the conditions under which existence of interpolants (for quantifierfree formulae) is modular, in the sense that it can be transferred from two firstorder theories T1, T2 to their combination T1∪T2. We generalize to the nondisjoint signatures case the results from [3]. As a surprising application, we relate the Horn combinability criterion of this paper to superamalgamability conditions known from propositional logic and we use this fact to derive old and new results concerning fusions transfer of interpolation properties in modal logic.

3049117.577217
In this tutorial, the meaning of natural language is analysed along the lines proposed by Gottlob Frege and Richard Montague. In building meaning representations, we assume that the meaning of a complex expression derives from the meanings of its components. Typed logic is a convenient tool to make this process of composition explicit. Typed logic allows for the building of semantic representations for formal languages and fragments of natural language in a compositional way. The tutorial ends with the discussion of an example fragment, implemented in the functional programming language Haskell Haskell Team; Jones [2003].

3062491.577231
Prima facie, there is an incompatibility between God’s alleged omnipotence and impeccability. I argue that this incompatibility is more than prima facie. Attempts to avoid this appearance of incompatibility by allowing that there are commonplace states of affairs that an omnipotent being cannot bring about are unsuccessful. Instead, we should accept that God is not omnipotent. This is acceptable since it is a mistake to hold that omnipotence is a perfection. God’s moral perfection should be privileged over God’s potency properties—and the same is true of human beings as well.

3170608.577244
Last weekend, I gave a talk on big numbers, as well as a Q&A about quantum computing, at Festivaletteratura: one of the main European literary festivals, held every year in beautiful and historic Mantua, Italy. …

3230087.577257
By “alternative set theories” we mean systems of set
theory differing significantly from the dominant ZF
(ZermeloFrankel set theory) and its close relatives (though we will
review these systems in the article). Among the systems we will review
are typed theories of sets, Zermelo set theory and its variations, New
Foundations and related systems, positive set theories, and
constructive set theories. An interest in the range of alternative set
theories does not presuppose an interest in replacing the dominant set
theory with one of the alternatives; acquainting ourselves with
foundations of mathematics formulated in terms of an alternative
system can be instructive as showing us what any set theory (including
the usual one) is supposed to do for us.

3230142.577271
We would like to arrive at a single coherent pair of credences in X and X. Perhaps we wish to use these to set our own credences; or perhaps we wish to publish them in a report of the WHO as the collective view of expert epidemiologists; or perhaps we wish to use them in a decisionmaking process to determine how medical research funding should be allocated in 2018. Given their expertise, we would like to use Amira’s and Benito’s credences when we are coming up with ours. However, there are two problems. First, Amira and Benito disagree — they assign different credences to X and different credences to X. Second, Amira and Benito are incoherent — they each assign credences to X and X that do not sum to 1. How, then, are we to proceed? There are natural ways to aggregate different credence functions; and there are natural ways to fix incoherent credence functions. Thus, we might fix Amira and Benito first and then aggregate the fixes; or we might aggregate their credences first and then fix up the aggregate. But what if these two disagree, as we will see they are sometimes wont to do? Which should we choose? To complicate matters further, there is a natural way to do both at once — it makes credences coherent and aggregates them all at the same time. What if this onestep procedure disagrees with one or other or both of the twostep procedures, fixthenaggregate and aggregatethenfix? In what follows, I explore when such disagreement arises and what the conditions are that guarantee that they will not. Then I will explain how these results may be used in philosophical arguments. I begin, however, with an overview of the paper.

3283636.577284
Quite often verification tasks for distributed systems are accomplished via counter abstractions. Such abstractions can sometimes be justified via simulations and bisimulations. In this work, we supply logical foundations to this practice, by a specifically designed technique for second order quantifier elimination. Our method, once applied to specifications of verification problems for parameterized distributed systems, produces integer variables systems that are ready to be modelchecked by current SMTbased tools. We demonstrate the feasibility of the approach with a prototype implementation and first experiments.

3521593.577298
In a series of posts a few months ago (here, here, and here), I explored a particular method by which we might aggregate expert credences when those credences are incoherent. The result was this paper, which is now forthcoming in Synthese. …

3581514.577311
This paper describes a decision procedure for disjunctions of conjunctions of antiprenex normal forms of pure firstorder logic (FOLDNFs) that do not contain ∨ within the scope of quantifiers. The disjuncts of these FOLDNFs are equivalent to prenex normal forms whose quantifierfree parts are conjunctions of atomic and negated atomic formulae (= Herbrand formulae). In contrast to the usual algorithms for Herbrand formulae, neither skolemization nor unification algorithms with function symbols are applied. Instead, a procedure is described that rests on nothing but equivalence transformations within pure firstorder logic (FOL). This procedure involves the application of a calculus for negative normal forms (the NNFcalculus) with A ⊣⊢ A ∧ A (= ∧I) as the sole rule that increases the complexity of given FOLDNFs. The described algorithm illustrates how, in the case of Herbrand formulae, decision problems can be solved through a systematic search for proofs that reduce the number of applications of the rule ∧I to a minimum in the NNFcalculus. In the case of Herbrand formulae, it is even possible to entirely abstain from applying ∧I. Finally, it is shown how the described procedure can be used within an optimized general search for proofs of contradiction and what kind of questions arise for a ∧Iminimal proof strategy in the case of a general search for proofs of contradiction.

3623468.577324
A mainstay assumption in naturallanguage semantics is that if  clauses bind indexical argumentplaces in thenclauses. Unfortunately, recent work (compare Santorio 2012) suggests that if clauses can somehow act to ‘shift the context’. On the framework of Kaplan’s ‘Demonstratives’ (Kaplan 1977), that would be ‘monstrous’ and somehow impossible ‘in English’. The superseding framework of Lewis’s ‘Index, context, and content’ (Lewis 1980) instead maintains that an indexical argumentplace is just one that is bindable (compare Stalnaker 2014, ch. 1), but maintains that these are rare—whereas the lesson of recent work is that they are pervasive.

3630522.577338
This paper reveals two fallacies in Turing’s undecidability proof of firstorder logic (FOL), namely, (i) an “extensional fallacy”: from the fact that a sentence is an instance of a provable FOL formula, it is inferred that a meaningful sentence is proven, and (ii) a “fallacy of substitution”: from the fact that a sentence is an instance of a provable FOL formula, it is inferred that a true sentence is proven. The first fallacy erroneously suggests that Turing’s proof of the nonexistence of a circlefree machine that decides whether an arbitrary machine is circular proves a significant proposition. The second fallacy suggests that FOL is undecidable.

3803645.577351
“Curry’s paradox”, as the term is used by
philosophers today, refers to a wide variety of paradoxes of
selfreference or circularity
that trace their modern
ancestry to Curry (1942b) and Löb
(1955) .^{[ 1 ]}
The common characteristic of these socalled Curry paradoxes is the
way they exploit a notion of implication, entailment or consequence,
either in the form of a connective or in the form of a predicate. Curry’s paradox arises in a number of different domains. Like
Russell’s paradox, it can take
the form of a paradox of
set theory or the theory of properties. But it can also take the form
of a semantic paradox, closely akin to the
Liar paradox.

3917565.577364
The divine attributes of omniscience and omnipotence have faced objections to their very consistency. Such objections rely on reasoning parallel to the semantic paradoxes such as the Liar or the settheoretic paradoxes like Russell’s paradox. With the advent of paraconsistent logics, dialetheism — the view that some contradictions are true — became a major player in the search for a solution to such paradoxes. This paper explores whether dialetheism, armed with the tools of paraconsistent logics, has the resources to respond to the objections levelled against the divine attributes.

4034427.577378
When we design a complex system, we often start with a rough outline and fill in details later, one step at a time. And if the system is supposed to be adaptive, these details may need to changed as the system is actually being used! …

4266964.577391
By Eric Schwitzgebel and Ivan GonzalezCabrera
Elite Englishlanguage philosophy journals cite almost exclusively Englishlanguage sources, while elite Chineselanguage philosophy journals cite from a range of linguistic traditions. …

4271382.577406
Let me start with a few quick announcements before the main entrée:
First, the website haspvsnpbeensolved.com is now live! Thanks so much to my friend Adam Chalmers for setting it up. Please try it out on your favorite P vs. NP solution paper—I think you’ll be impressed by how well our secret validation algorithm performs. …

4322634.577419
In the context of language, selfreference is used to denote
a statement that refers to itself or its own referent. The most famous
example of a selfreferential sentence is the liar sentence:
“This sentence is not true.” Selfreference is often used
in a broader context as well. For instance, a picture could be
considered selfreferential if it contains a copy of itself (see the
animated image above); and a piece of literature could be considered
selfreferential if it includes a reference to the work itself. In
philosophy, selfreference is primarily studied in the context of
language.

5107848.577433
N. Barton, A. E. Caicedo, G. Fuchs, J. D. Hamkins, and J. Reitz, “Innermodel reflection principles.” (manuscript under review)
Citation arχiv
@ARTICLE{BartonCaicedoFuchsHamkinsReitz:Innermodelreflectionprinciples,
author = {Neil Barton and Andr\'es Eduardo Caicedo and Gunter Fuchs and Joel David Hamkins and Jonas Reitz},
title = {Innermodel reflection principles},
journal = {},
year = {},
volume = {},
number = {},
pages = {},
month = {},
note = {manuscript under review},
abstract = {},
keywords = {},
source = {},
doi = {},
eprint = {1708.06669},
archivePrefix = {arXiv},
primaryClass = {math.LO},
url = {http://jdh.hamkins.org/innermodelreflectionprinciples},
}
Abstract. …

5166062.577446
Last time I introduced typed operads. A typed operad has a bunch of operations for putting together things of various types and getting new things of various types. This is a very general idea! But in the CASCADE project we’re interested in something more specific: networks. …