To be autonomous is to be a law to oneself; autonomous agents are self-governing agents. Most of us want to be autonomous because we want to be accountable for what we do, and because it seems that if we are not the ones calling the shots, then we cannot be accountable. More importantly, perhaps, the value of autonomy is tied to the value of self-integration. We don't want to be alien to, or at war with, ourselves; and it seems that (...) when our intentions are not under our own control, we suffer from self-alienation. What conditions must be satisfied in order to ensure that we govern ourselves when we act? Philosophers have offered a wide range of competing answers to this question. (shrink)

In order to be a self-governing agent, a person must govern the process by means of which she acquires the intention to act as she does. But what does governing this process require? The standard compatibilist answers to this question all assume that autonomous actions differ from nonautonomous actions insofar as they are a more perfect expression of the agent’s agency. I challenge this conception of autonomous agents as super agents. The distinguishing feature of autonomous agents is, I argue, the (...) nonagential role they play in the formation of their intentions. I offer an account of the relevant role. (shrink)

This volume contains articles covering a broad spectrum of proof theory, with an emphasis on its mathematical aspects. The articles should not only be interesting to specialists of proof theory, but should also be accessible to a diverse audience, including logicians, mathematicians, computer scientists and philosophers. Many of the central topics of proof theory have been included in a self-contained expository of articles, covered in great detail and depth. The chapters are arranged so that the two introductory articles come first; (...) these are then followed by articles from core classical areas of proof theory; the handbook concludes with articles that deal with topics closely related to computer science. (shrink)

The original essays in this book address Harry Frankfurt's influential writing on personal identity, love, value, moral responsibility, and the freedom and ...

We believe we owe one another respect. We believe we ought to pay what we owe by treating one another ‘with respect.’ If we could understand these beliefs we would be well on the way to understanding morality itself. If we could justify these beliefs we could vindicate a central part of our moral experience.Respect comes in many varieties. We respect some people for their upright character, others for their exceptional achievements. There are people we respect as forces of nature: (...) we go to great lengths to accommodate their moods, wiles, and demands. Finally, most of us seem to respect people simply because they are people. This is the sort of respect of special interest to moral theory.In order to be worthy of this last sort of respect, it is not only sufficient but necessary that one be a person. We can, of course, take a similar attitude toward nonpersons. (shrink)

My chief aim is to explain how someone can act freely against her own best judgment. But I also have a second aim: to defend a conception of practical rationality according to which someone cannot do something freely if she believes it would be better to do something else. These aims may appear incompatible. But I argue that practical reason has the capacity to undermine itself in such a way that it produces reasons for behaving irrationally. Weakness of will is (...) possible because it is possible to conclude that one has sufficient reason to reject the verdicts of one's own reason. (shrink)

I wish more books of philosophy were like this one. It is elegantly written. It is filled with provocative claims and ingenious arguments. It is a really good read, even while it forces us to rethink many of our assumptions about practical reason and practical reasoning, morality and agency.

Cook and Reckhow defined a propositional formulation of the pigeonhole principle. This paper shows that there are Frege proofs of this propositional pigeonhole principle of polynomial size. This together with a result of Haken gives another proof of Urquhart's theorem that Frege systems have an exponential speedup over resolution. We also discuss connections to provability in theories of bounded arithmetic.

Let T be a first-order theory. A T-normal Kripke structure is one in which every world is a classical model of T. This paper gives a characterization of the intuitionistic theory T of sentences intuitionistically valid in all T-normal Kripke structures and proves the corresponding soundness and completeness theorems. For Peano arithmetic , the theory PA is a proper subtheory of Heyting arithmetic , so HA is complete but not sound for PA-normal Kripke structures.

The bounded arithmetic theory S2 is finitely axiomatized if and only if the polynomial hierarchy provably collapses. If T2i equals S2i + 1 then T2i is equal to S2 and proves that the polynomial time hierarchy collapses to ∑i + 3p, and, in fact, to the Boolean hierarchy over ∑i + 2p and to ∑i + 1p/poly.

This paper discusses lower bounds for proof length, especially as measured by number of steps (inferences). We give the first publicly known proof of Gödel's claim that there is superrecursive (in fact. unbounded) proof speedup of (i + 1)st-order arithmetic over ith-order arithmetic, where arithmetic is formalized in Hilbert-style calculi with + and · as function symbols or with the language of PRA. The same results are established for any weakly schematic formalization of higher-order logic: this allows all tautologies as (...) axioms and allows all generalizations of axioms as axioms. Our first proof of Gödel's claim is based on self-referential sentences: we give a second proof that avoids the use of self-reference based loosely on a method of Statman. (shrink)

The complexity class of [Formula: see text]-polynomial local search problems is introduced and is used to give new witnessing theorems for fragments of bounded arithmetic. For 1 ≤ i ≤ k + 1, the [Formula: see text]-definable functions of [Formula: see text] are characterized in terms of [Formula: see text]-PLS problems. These [Formula: see text]-PLS problems can be defined in a weak base theory such as [Formula: see text], and proved to be total in [Formula: see text]. Furthermore, the [Formula: (...) see text]-PLS definitions can be skolemized with simple polynomial time functions, and the witnessing theorem itself can be formalized, and skolemized, in a weak base theory. We introduce a new [Formula: see text]-principle that is conjectured to separate [Formula: see text] and [Formula: see text]. (shrink)

Samuel R. Buss and Aleksandar Ignjatović. Unprovability of Consistency Statements in Fragments of Bounded Arithmetic.

Partial consistency statements can be expressed as polynomial-size propositional formulas. Frege proof systems have polynomial-size partial self-consistency proofs. Frege proof systems have polynomial-size proofs of partial consistency of extended Frege proof systems if and only if Frege proof systems polynomially simulate extended Frege proof systems. We give a new proof of Reckhow's theorem that any two Frege proof systems p-simulate each other. The proofs depend on polynomial size propositional formulas defining the truth of propositional formulas. These are already known to (...) exist since the Boolean formula value problem is in alternating logarithmic time; this paper presents a proof of this fact based on a construction which is somewhat simpler than the prior proofs of Buss and of Buss-Cook- Gupta-Ramachandran. (shrink)

The paper proves refined feasibility properties for the disjunction property of intuitionistic propositional logic. We prove that it is possible to eliminate all cuts from an intuitionistic proof, propositional or first-order, without increasing the Horn closure of the proof. We obtain a polynomial time, interactive, realizability algorithm for propositional intuitionistic proofs. The feasibility of the disjunction property is proved for sequents containing Harrop formulas. Under hardness assumptions for NP and for factoring, it is shown that the intuitionistic propositional calculus does (...) not always have polynomial size proofs and that the classical propositional calculus provides a superpolynomial speedup over the intuitionistic propositional calculus. The disjunction property for intuitionistic propositional logic is proved to be P-hard by a reduction to the circuit value problem. (shrink)

We survey the best known lower bounds on symbols and lines in Frege and extended Frege proofs. We prove that in minimum length sequent calculus proofs, no formula is generated twice or used twice on any single branch of the proof. We prove that the number of distinct subformulas in a minimum length Frege proof is linearly bounded by the number of lines. Depthd Frege proofs ofm lines can be transformed into depthd proofs ofO(m d+1) symbols. We show that renaming (...) Frege proof systems are p-equivalent to extended Frege systems. Some open problems in propositional proof length and in logical flow graphs are discussed. (shrink)

This paper considers the computational complexity of the disjunction and existential properties of intuitionistic logic. We prove that the disjunction property holds feasibly for intuitionistic propositional logic; i.e., from a proof of A v B, a proof either of A or of B can be found in polynomial time. For intuitionistic predicate logic, we prove superexponential lower bounds for the disjunction property, namely, there is a superexponential lower bound on the time required, given a proof of A v B, to (...) produce one of A and B which is true. In addition, there is superexponential lower bound on the size of terms which fulfill the existential property of intuitionistic predicate logic. There are superexponential upper bounds for these problems, so the lower bounds are essentially optimal. (shrink)

The four authors present their speculations about the future developments of mathematical logic in the twenty-first century. The areas of recursion theory, proof theory and logic for computer science, model theory, and set theory are discussed independently.

This paper proves exponential separations between depth d-LK and depth -LK for every utilizing the order induction principle. As a consequence, we obtain an exponential separation between depth d-LK and depth -LK for . We investigate the relationship between the sequence-size, tree-size and height of depth d-LK-derivations for , and describe transformations between them. We define a general method to lift principles requiring exponential tree-size -LK-refutations for to principles requiring exponential sequence-size d-LK-refutations, which will be described for the Ramsey principle (...) and d=0. From this we also deduce width lower bounds for resolution refutations of the Ramsey principle. (shrink)

We introduce new proof systems for propositional logic, simple deduction Frege systems, general deduction Frege systems, and nested deduction Frege systems, which augment Frege systems with variants of the deduction rule. We give upper bounds on the lengths of proofs in Frege proof systems compared to lengths in these new systems. As applications we give near-linear simulations of the propositional Gentzen sequent calculus and the natural deduction calculus by Frege proofs. The length of a proof is the number of lines (...) in the proof. A general deduction Frege proof system provides at most quadratic speedup over Frege proof systems. A nested deduction Frege proof system provides at most a nearly linear speedup over Frege system where by "nearly linear" is meant the ratio of proof lengths is O) where α is the inverse Ackermann function. A nested deduction Frege system can linearly simulate the propositional sequent calculus, the tree-like general deduction Frege calculus, and the natural deduction calculus. Hence a Frege proof system can simulate all those proof systems with proof lengths bounded by O). Also we show that a Frege proof of n lines can be transformed into a tree-like Frege proof of O lines and of height O. As a corollary of this fact we can prove that natural deduction and sequent calculus tree-like systems simulate Frege systems with proof lengths bounded by O. (shrink)

We give the first systematic study of strong isomorphism reductions, a notion of reduction more appropriate than polynomial time reduction when, for example, comparing the computational complexity of the isomorphim problem for different classes of structures. We show that the partial ordering of its degrees is quite rich. We analyze its relationship to a further type of reduction between classes of structures based on purely comparing for every n the number of nonisomorphic structures of cardinality at most n in both (...) classes. Furthermore, in a more general setting we address the question of the existence of a maximal element in the partial ordering of the degrees. (shrink)

A pool resolution proof is a dag-like resolution proof which admits a depth-first traversal tree in which no variable is used as a resolution variable twice on any branch. The problem of determining whether a given dag-like resolution proof is a valid pool resolution proof is shown to be NP-complete.

In this paper I consider three widespread assumptions: (1) the assumption that we are accountable for our intentional actions only if they are in some special sense ours; (2) the assumption that it is possible for us to be more or less “true to” ourselves, and that we are flawed human beings to the extent that we lack “integrity”; and (3) the assumption that we can sometimes give ourselves reasons by giving ourselves commands. I acknowledge that, as Ruediger Bittner has (...) argued, each of these assumptions is problematic, and that the failure to appreciate the problems has led many philosophers astray. I try to show, however, that it is possible to make sense of each assumption in a way that addresses Bittner’s concerns. (shrink)

In the context of a largely exploratory inquiry, I warn against oversimplifying the relationships among intuitions, emotions, principle-governed reasoning, and responsiveness to reasons. I point out that one cannot determine the normative status of some fact without determining whether a case can be made for this status. But I also note that, though reason is thus autonomous, every episode of reasoning depends causally on the way things nonnormatively are, and this makes it possible for any reasoner to challenge even her (...) most basic normative assumptions. (shrink)

We prove that the problem of determining the minimum propositional proof length is NP- hard to approximate within a factor of 2 log 1 - o(1) n . These results are very robust in that they hold for almost all natural proof systems, including: Frege systems, extended Frege systems, resolution, Horn resolution, the polynomial calculus, the sequent calculus, the cut-free sequent calculus, as well as the polynomial calculus. Our hardness of approximation results usually apply to proof length measured either by (...) number of symbols or by number of inferences, for tree-like or dag-like proofs. We introduce the Monotone Minimum (Circuit) Satisfying Assignment problem and reduce it to the problems of approximation of the length of proofs. (shrink)

We give a uniform proof of the theorems of Yao and Beigel–Tarui representing ACC predicates as constant depth circuits with MODm\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\hbox {MOD}_{m}$$\end{document} gates and a symmetric gate. The proof is based on a relativized, generalized form of Toda’s theorem expressed in terms of closure properties of formulas under bounded universal, existential and modular counting quantifiers. This allows the main proofs to be expressed in terms of formula classes instead of Boolean circuits. (...) The uniform version of the Beigel–Tarui theorem is then obtained automatically via the Furst–Saxe–Sipser and Paris–Wilkie translations. As a special case, we obtain a uniform version of Razborov and Smolensky’s representation of AC0[p]\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\hbox {AC}^{0}[p]$$\end{document} circuits. The paper is partly expository, but is also motivated by the desire to recast Toda’s theorem, the Beigel–Tarui theorem, and their proofs into the language of bounded arithmetic. However, no knowledge of bounded arithmetic is needed. (shrink)

Originating from work in operations research the cutting plane refutation systemCP is an extension of resolution, where unsatisfiable propositional logic formulas in conjunctive normal form are recognized by showing the non-existence of boolean solutions to associated families of linear inequalities. Polynomial sizeCP proofs are given for the undirecteds-t connectivity principle. The subsystemsCP q ofCP, forq≥2, are shown to be polynomially equivalent toCP, thus answering problem 19 from the list of open problems of [8]. We present a normal form theorem forCP (...) 2-proofs and thereby for arbitraryCP-proofs. As a corollary, we show that the coefficients and constant terms in arbitrary cutting plane proofs may be exponentially bounded by the number of steps in the proof, at the cost of an at most polynomial increase in the number of steps in the proof. The extensionCPLE +, introduced in [9] and there shown top-simulate Frege systems, is proved to be polynomially equivalent to Frege systems. Lastly, since linear inequalities are related to threshold gates, we introduce a new threshold logic and prove a completeness theorem. (shrink)

We refine the constructions of Ferrante-Rackoff and Solovay on iterated definitions in first-order logic and their expressibility with polynomial size formulas. These constructions introduce additional quantifiers; however, we show that these extra quantifiers range over only finite sets and can be eliminated. We prove optimal upper and lower bounds on the quantifier complexity of polynomial size formulas obtained from the iterated definitions. In the quantifier-free case and in the case of purely existential or universal quantifiers, we show that Ω quantifiers (...) are necessary and sufficient. The last lower bounds are obtained with the aid of the Yao-Håstad switching lemma. (shrink)

We believe we owe one another respect. We believe we ought to pay what we owe by treating one another ‘with respect.’ If we could understand these beliefs we would be well on the way to understanding morality itself. If we could justify these beliefs we could vindicate a central part of our moral experience.Respect comes in many varieties. We respect some people for their upright character, others for their exceptional achievements. There are people we respect as forces of nature: (...) we go to great lengths to accommodate their moods, wiles, and demands. Finally, most of us seem to respect people simply because they are people. This is the sort of respect of special interest to moral theory.In order to be worthy of this last sort of respect, it is not only sufficient but necessary that one be a person. We can, of course, take a similar attitude toward nonpersons. (shrink)

This paper investigates provability and non-provability of well-foundedness of ordinal notations in weak theories of bounded arithmetic. We define a notion of well-foundedness on bounded domains. We show that T21 and S22 can prove the well-foundedness on bounded domains of the ordinal notations below 0 and Γ0. As a corollary, the class of polynomial local search problems, PLS, can be augmented with cost functions that take ordinal values below 0 and Γ0 without increasing the class PLS.

This paper investigates provability and non-provability of well-foundedness of ordinal notations in weak theories of bounded arithmetic. We define a notion of well-foundedness on bounded domains. We show that T21 and S22 can prove the well-foundedness on bounded domains of the ordinal notations below 0 and Γ0. As a corollary, the class of polynomial local search problems, PLS, can be augmented with cost functions that take ordinal values below 0 and Γ0 without increasing the class PLS.

We extend results of Bonet, Buss and Pitassi on Bondy’s Theorem and of Nozaki, Arai and Arai on Bollobás’ Theorem by proving that Frankl’s Theorem on the trace of sets has quasipolynomial size Frege proofs. For constant values of the parametert, we prove that Frankl’s Theorem has polynomial size AC0-Frege proofs from instances of the pigeonhole principle.