Mathematical Logic Seminar Abstracts Winter 2011

We explore the idea of getting at the logical constants, or at least the constants, of a language by 'extracting' them from a given consequence relation, taken as primitive. Under minimal assumptions, we show that (a) this gives the expected constants for familiar consequence relations in logic, and (b) the extraction operation is an inverse, in a suitable sense, to the Bolzano-Tarski style method of defining a consequence relation from any set of symbols taken as constants. This is joint work with Denis Bonnay.

Omega-rule was introduced by W. Buchhlolz to give a proof-theoretic analysis of \Pi-1-1-comprehension. The rule is used to expand second order existential introduction rule into an infinite figure. However Buchholz's cut-elimination theorem is restricted to derivations with an arithmetical end-sequent. We describe a version of this approach which works for arbitrary sequents.

Part I surveyed a variety of recursive ordinal notation systems and their relationships that have been used in proof theory, including those built up from below and applied in predicative and metapredicative proof theory, as well as those generated from above and that have been applied to the proof theory of impredicative formal systems. The latter ordinal notations make prima facie essential use of names of uncountable regular ordinals and require collapsing arguments to identify them with countable ordinals.

In this continuation, I describe another approach not requiring either uncountable ordinals or collapsing arguments but using finite and transfinite types over the countable ordinals. This approach takes one a certain distance into impredicative proof theory. Though some 40 years old, it has hardly been exploited and deserves renewed consideration.

We will review the 2009 JSL paper by Avigad and Towsner giving a new functional interpretation of ID1, the theory of arithmetic extended with one positive inductive definition. We will outline the steps of interpretations in the paper, and then focus our attention on the functional translation itself.

The importance of modeling reasoning agents in economics is widely recognized by economists. However, the treatment of such reasoning has evolved in a particular manner due to the particular questions economists study and the evolution of the field. In this talk I will provide an overview of the evolution of modeling economic agents' reasoning. The talk will cover reasoning in microeconomics prior to the widespread use of game theory, the evolution of reasoning in game theory, when and how the two merged and how research on reasoning agents advanced since. I will attempt to explain the forces driving the particular evolution of modeling reasoning agents and distinguish between some idiosyncrasies that are essential to economics and those that beg modification and present research opportunities.

I will present a simpler and cleaner version of a proof (c. 1960) of the termination of the epsilon substitution method for first-order arithmetic.

Continuing the theme of applications of logic to economics, I will present a paper by Giacomo Bonanno entitled "Modal Logic and Game Theory: Two Alternative Approaches" (Risk Decision and Policy, 7, December 2002, pp. 309-324). The purpose of the paper is to demonstrate that modal logic is a natural choice as a formal language of specification for games, and in more ways than one. Bonnano considers two views of game theory and its solution concepts: solution concepts as a description of rational behavior, and solution concepts as a recommendation to rational agents. In the first case, Bonnano shows how a modal language, interpreted as a logic of belief, can capture the intuitive connection between common belief of rationality and the iterated deletion of dominated strategies as a logical validity. In the second case, Bonnano shows how a modal language, now interpreted as a logic of ability, can be used to characterize the notion of Nash Equilibrium in strategic-form games and characterize the recommendation of a "backward induction" strategy in extensive form games.