We construct a faithful interpretation of ukasiewicz's logic in product logic (both propositional and predicate). Using known facts it follows that the product predicate logic is not recursively axiomatizable.We prove a completeness theorem for product logic extended by a unary connective of Baaz [1]. We show that Gödel's logic is a sublogic of this extended product logic.

We give combinatorial and computational characterizations of the NP search problems definable in the bounded arithmetic theories $T_{2}^{2}$ and $T_{3}^{2}$.

We describe a general method how to construct from a propositional proof system P a possibly much stronger proof system iP. The system iP operates with exponentially long P-proofs described "implicitly" by polynomial size circuits. As an example we prove that proof system iEF, implicit EF, corresponds to bounded arithmetic theory $V_{2}^{1}$ and hence, in particular, polynomially simulates the quantified propositional calculus G and the $\pi_{1}^{b}-consequences$ of $S_{2}^{1}$ proved with one use of exponentiation. Furthermore, the soundness of iEF is not (...) provable in $S_{2}^{1}$ . An iteration of the construction yields a proof system corresponding to $T_{2} + Exp$ and, in principle, to much stronger theories. (shrink)

We consider exponentially large finite relational structures (with the universe {0.1}ⁿ) whose basic relations are computed by polynomial size (nO(1)) circuits. We study behaviour of such structures when pulled back by P/poly maps to a bigger or to a smaller universe. In particular, we prove that: 1. If there exists a P/poly map g: {0.1} → {0.1}m, n < m, iterable for a proof system then a tautology (independent of g) expressing that a particular size n set is dominating in (...) a size 2ⁿ tournament is hard for the proof system. 2. The search problem WPHP, decoding RSA or finding a collision in a hashing function can be reduced to finding a size m homogeneous subgraph in a size 22m graph. Further we reduce the proof complexity of a concrete tautology (expressing a Ramsey property of a graph) in strong systems to the complexity of implicit proofs of implicit formulas in weak proof systems. (shrink)

Part of the appeal of the biological approach to personal identity is that it does not have to countenance spatially coincident entities. But if the termination thesis is correct and the organism ceases to exist at death, then it appears that the corpse is a dead body that earlier was a living body and distinct from but spatially coincident with the organism. If the organism is identified with the body, then the unwelcome spatial coincidence could perhaps be avoided. It is (...) argued that such an identification would be a mistake. A living organism has a different part/whole relationship and persistence conditions than the alleged body. A case will be made that the concept ‘human body’ is a conceptual mess, vague in an unprincipled manner, and that an eliminativist stance towards dead bodies is the appropriate response. CiteULike Connotea Del.icio.us What's this? (shrink)

We prove the following results: (i) PV proves NP ⊆ P/poly iff PV proves coNP ⊆ NP/O(1). (ii) If PV proves NP ⊆ P/poly then PV proves that the Polynomial Hierarchy collapses to the Boolean Hierarchy. (iii) $S_{2}^{1}$ proves NP ⊆ P/poly iff $S_{2}^{1}$ proves coNP ⊆ NP/O(log n). (iv) If $S_{2}^{1}$ proves NP ⊆ P/poly then $S_{2}^{1}$ proves that the Polynomial Hierarchy collapses to PNP[log n]. (v) If $S_{2}^{2}$ proves NP ⊆ P/poly then $S_{2}^{2}$ proves that the Polynomial Hierarchy (...) collapses to PNP. Motivated by these results we introduce a new concept in proof complexity: proof systems with advice, and we make some initial observations about them. (shrink)

T i 2 = S i +1 2 implies ∑ p i +1 ⊆ Δ p i +1 ⧸poly. S 2 and IΔ 0 ƒ are not finitely axiomatizable. The main tool is a Herbrand-type witnessing theorem for ∃∀∃ П b i -formulas provable in T i 2 where the witnessing functions are □ p i +1.

As a continuation of the work of the third author in [5], we make further observations on the features of Galois cohomology in the general model theoretic context. We make explicit the connection between forms of definable groups and first cohomology sets with coefficients in a suitable automorphism group. We then use a method of twisting cohomology (inspired by Serre’s algebraic twisting) to describe arbitrary fibres in cohomology sequences—yielding a useful “finiteness” result on cohomology sets. Applied to the special case (...) of differential fields and Kolchin’s constrained cohomology, we complete results from [3] by proving that the first constrained cohomology set of a differential algebraic group over a bounded, differentially large, field is countable. (shrink)

LK is a natural modification of Gentzen sequent calculus for propositional logic with connectives ¬ and $\bigwedge, \bigvee$. Then for every d ≥ 0 and n ≥ 2, there is a set Td n of depth d sequents of total size O which are refutable in LK by depth d + 1 proof of size exp) but such that every depth d refutation must have the size at least exp). The sets Td n express a weaker form of the pigeonhole (...) principle. (shrink)

A proof of the (propositional) Craig interpolation theorem for cut-free sequent calculus yields that a sequent with a cut-free proof (or with a proof with cut-formulas of restricted form; in particular, with only analytic cuts) with k inferences has an interpolant whose circuit-size is at most k. We give a new proof of the interpolation theorem based on a communication complexity approach which allows a similar estimate for a larger class of proofs. We derive from it several corollaries: (1) Feasible (...) interpolation theorems for the following proof systems: (a) resolution (b) a subsystem of LK corresponding to the bounded arithmetic theory S 2 2 (α) (c) linear equational calculus (d) cutting planes. (2) New proofs of the exponential lower bounds (for new formulas) (a) for resolution ([15]) (b) for the cutting planes proof system with coefficients written in unary ([4]). (3) An alternative proof of the independence result of [43] concerning the provability of circuit-size lower bounds in the bounded arithmetic theory S 2 2 (α). In the other direction we show that a depth 2 subsystem of LK does not admit feasible monotone interpolation theorem (the so called Lyndon theorem), and that a feasible monotone interpolation theorem for the depth 1 subsystem of LK would yield new exponential lower bounds for resolution proofs of the weak pigeonhole principle. (shrink)

We consider the problem about the length of proofs of the sentences $\operatorname{Con}_S(\underline{n})$ saying that there is no proof of contradiction in S whose length is ≤ n. We show the relation of this problem to some problems about propositional proof systems.

We recall the notions of weak and strong Euler characteristics on a first order structure and make explicit the notion of a Grothendieck ring of a structure. We define partially ordered Euler characteristic and Grothendieck ring and give a characterization of structures that have non-trivial partially ordered Grothendieck ring. We give a generalization of counting functions to locally finite structures, and use the construction to show that the Grothendieck ring of the complex numbers contains as a subring the ring of (...) integer polynomials in continuum many variables. We prove the existence of a universal strong Euler characteristic on a structure. We investigate the dependence of the Grothendieck ring on the theory of the structure and give a few counter-examples. Finally, we relate some open problems and independence results in bounded arithmetic to properties of particular Grothendieck rings. (shrink)

V i 2 ⊢A iff for some term t :S i 2 ⊢ “2 i exists→ A”, a bounded first-order formula, i ≥1. V i 2 is not Π b 1 -conservative over S i 2 . Any model of V 2 not satisfying Exp satisfies the collection scheme BΣ 0 1 . V 1 3 is not Π b 1 -conservative over S 2.

We consider tautologies formed form a pseudo-random number generator, defined in Krajicek [11] and in Alekhnovich et al. [2]. We explain a strategy of proving their hardness for Extended Frege systems via a conjecture about bounded arithmetic formulated in Krajicek [11]. Further we give a purely finitary statement, in the form of a hardness condition imposed on a function, equivalent to the conjecture. This is accompanied by a brief explanation, aimed at non-specialists, of the relation between prepositional proof (...) complexity and bounded arithmetic. (shrink)

In this classic work David Bohm, writing clearly and without technical jargon, develops a theory of quantum physics which treats the totality of existence as an unbroken whole.

For all i ≥ 1, Ti+11 is not ∀Σb2-conservative over Ti1.

In this innovative study, Lea David critically investigates the relationship between human rights and memory, suggesting that, instead of understanding human rights in a normative fashion, human rights should be treated as an ideology. Conceptualizing human rights as an ideology gives us useful theoretical and methodological tools to recognize the real impact human rights has on the ground. David traces the rise of the global phenomenon that is the human rights memorialization agenda, termed 'Moral Remembrance', and explores what (...) happens once this agenda becomes implemented. Based on evidence from the Western Balkans and Israel/Palestine, she argues that the human rights memorialization agenda does not lead to a better appreciation of human rights but, contrary to what would be expected, it merely serves to strengthen national sentiments, divisions and animosities along ethnic lines, and leads to the new forms of societal inequalities that are closely connected to different forms of corruptions. (shrink)

Liberal thinkers of the eighteenth and nineteenth centuries were alert to the political costs and human cruelties involved in European colonialism, but they also thought that European expansion held out progressive possibilities. In Progress, Pluralism, and Politics David Williams examines the colonial and anti-colonial arguments of Adam Smith, Immanuel Kant, Jeremy Bentham, and L.T. Hobhouse. Williams locates their ambivalent attitude towards European conquest and colonial rule in a set of tensions between the impact of colonialism on European states, the (...) possibilities of progress in distant and diverse places, and the relationship between universalism and cultural pluralism. In so doing he reveals some of the central ambiguities that characterize the ways that liberal thought has dealt with the reality of an illiberal world. Of particular importance are appeals to various forms of universal history, attempts to mediate between the claims of identity and the reality of difference, and the different ways of thinking about the achievement of liberal goods in other places. Pointing to key elements in still ongoing debates within liberal states about how they should relate to illiberal places, Progress, Pluralism, and Politics enriches the discussion on political thought and the relationship between liberalism and colonialism. (shrink)

We define the notion of a combinatorics of a first order structure, and a relation of covering between first order structures and propositional proof systems. Namely, a first order structure M combinatorially satisfies an L-sentence Φ iff Φ holds in all L-structures definable in M. The combinatorics Comb(M) of M is the set of all sentences combinatorially satisfied in M. Structure M covers a propositional proof system P iff M combinatorially satisfies all Φ for which the associated sequence of propositional (...) formulas 〈Φ〉 n , encoding that Φ holds in L-structures of size n, have polynomial size P-proofs. That is, Comb(M) contains all Φ feasibly verifiable in P. Finding M that covers P but does not combinatorially satisfy Φ thus gives a super polynomial lower bound for the size of P-proofs of 〈Φ〉 n . We show that any proof system admits a class of structures covering it; these structures are expansions of models of bounded arithmetic. We also give, using structures covering proof systems R * (log) and PC, new lower bounds for these systems that are not apparently amenable to other known methods. We define new type of propositional proof systems based on a combinatorics of (a class of) structures. (shrink)

We define a first-order extension LK(CP) of the cutting planes proof system CP as the first-order sequent calculus LK whose atomic formulas are CP-inequalities ∑ i a i · x i ≥ b (x i 's variables, a i 's and b constants). We prove an interpolation theorem for LK(CP) yielding as a corollary a conditional lower bound for LK(CP)-proofs. For a subsystem R(CP) of LK(CP), essentially resolution working with clauses formed by CP- inequalities, we prove a monotone interpolation theorem (...) obtaining thus an unconditional lower bound (depending on the maximum size of coefficients in proofs and on the maximum number of CP-inequalities in clauses). We also give an interpolation theorem for polynomial calculus working with sparse polynomials. The proof relies on a universal interpolation theorem for semantic derivations [16, Theorem 5.1]. LK(CP) can be viewed as a two-sorted first-order theory of Z considered itself as a discretely ordered Z-module. One sort of variables are module elements, another sort are scalars. The quantification is allowed only over the former sort. We shall give a construction of a theory LK(M) for any discretely ordered module M (e.g., LK(Z) extends LK(CP)). The interpolation theorem generalizes to these theories obtained from discretely ordered Z-modules. We shall also discuss a connection to quantifier elimination for such theories. We formulate a communication complexity problem whose (suitable) solution would allow to improve the monotone interpolation theorem and the lower bound for R(CP). (shrink)

For any countable nonstandard modelM of a sufficiently strong fragment of arithmeticT, and any nonstandard numbersa, c εM, M⊨c≦a, there is a modelK ofT which agrees withM up toa and such that inK there is a proof of contradiction inT with Gödel number $ \leqq 2^{a^c } $.

Thus, Meyers provides a valuable account, not only of current medical attitudes, but also of relevant case and statute law as it stands at present.

We prove an exponential lower bound on the size of proofs in the proof system operating with ordered binary decision diagrams introduced by Atserias, Kolaitis and Vardi [2]. In fact, the lower bound applies to semantic derivations operating with sets defined by OBDDs. We do not assume any particular format of proofs or ordering of variables, the hard formulas are in CNF. We utilize (somewhat indirectly) feasible interpolation. We define a proof system combining resolution and the OBDD proof system.

Let g be a map defined as the Nisan–Wigderson generator but based on an NP ∩ coNP -function f. Any string b outside the range of g determines a propositional tautology τb expressing this fact. Razborov [27] has conjectured that if f is hard on average for P/poly then these tautologies have no polynomial size proofs in the Extended Frege system EF. We consider a more general Statement that the tautologies have no polynomial size proofs in any propositional proof system. (...) This is equivalent to the statement that the complement of the range of g contains no infinite NP set. We prove that Statement is consistent with Cook' s theory PV and, in fact, with the true universal theory T PV in the language of PV. If PV in this consistency statement could be extended to "a bit" stronger theory then Razborov's conjecture would follow, and if TPV could be added too then Statement would follow. We discuss this problem in some detail, pointing out a certain form of reflection principle for propositional logic, and we introduce a related feasible disjunction property of proof systems. (shrink)

Let L be a first-order language and Φ and ψ two $\Sigma _{1}^{1}$ L-sentences that cannot be satisfied simultaneously in any finite L-structure. Then obviously the following principle Chain L,Φ,ψ (n,m) holds: For any chain of finite L-structures C 1 ,...,C m with the universe [n] one of the following conditions must fail: 1. $C_{1}\vDash \Phi $ , 2. C i ≅ C i+1 , for i = 1,...,m — 1, 3. $C_{m}\vDash \Psi $ . For each fixed L and (...) parameters n,m the principle Chain L,Φ,ψ (n,m) can be encoded into a propositional DNF formula of size polynomial in n,m. For any language L containing only constants and unary predicates we show that there is a constant c L such that the following holds: If a constant depth Frege system in DeMorgan language proves Chain L,Φ,ψ (n, c L · n) by a size s proof then the class of finite L-structures with universe [n] satisfying Φ can be separated from the class of those L-structures on [n] satisfying ψ by a depth 3 formula of size $2^{{\rm log}(s)^{O(1)}}$ and with bottom fan-in ${\rm log}(s)^{O(1)}$. (shrink)

A method for constructing Boolean-valued models of some fragments of arithmetic was developed in Krajíček (Forcing with Random Variables and Proof Complexity, London Mathematical Society Lecture Notes Series, Cambridge University Press, Cambridge, 2011), with the intended applications in bounded arithmetic and proof complexity. Such a model is formed by a family of random variables defined on a pseudo-finite sample space. We show that under a fairly natural condition on the family [called compactness in Krajíček (Forcing with Random Variables and Proof (...) Complexity, London Mathematical Society Lecture Notes Series, Cambridge University Press, Cambridge, 2011)] the resulting structure has a property that is naturally interpreted as saturation for existential types. We also give an example showing that this cannot be extended to universal types. (shrink)

The feasible interpolation theorem for semantic derivations from [J. Krajíček, Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic, J. Symbolic Logic 62 457–486] allows to derive from some short semantic derivations of the disjointness of two [Formula: see text] sets [Formula: see text] and [Formula: see text] a small communication protocol computing the Karchmer–Wigderson multi-function [Formula: see text] associated with the sets, and such a protocol further yields a small circuit separating [Formula: see text] from (...) [Formula: see text]. When [Formula: see text] is closed upwards, the protocol computes the monotone Karchmer–Wigderson multi-function [Formula: see text] and the resulting circuit is monotone. Krajíček [Interpolation by a game, Math. Logic Quart. 44 450–458] extended the feasible interpolation theorem to a larger class of semantic derivations using the notion of a real communication complexity. In this paper, we generalize the method to a still larger class of semantic derivations by allowing randomized protocols. We also introduce an extension of the monotone circuit model, monotone circuits with a local oracle, that does correspond to communication protocols for [Formula: see text] making errors. The new randomized feasible interpolation thus shows that a short semantic derivation of the disjointness of [Formula: see text], [Formula: see text] closed upwards, yields a small randomized protocol for [Formula: see text] and hence a small monotone CLO separating the two sets. This research is motivated by the open problem to establish a lower bound for proof system [Formula: see text] operating with clauses formed by linear Boolean functions over [Formula: see text]. The new randomized feasible interpolation applies to this proof system and also to cutting planes CP, to small width resolution over CP of Krajíček [Discretely ordered modules as a first-order extension of the cutting planes proof system, J. Symbolic Logic 63 1582–1596] ) and to random resolution RR of Buss, Kolodziejczyk and Thapen [Fragments of approximate counting, J. Symbolic Logic 79 496–525]. The method does not yield yet lengths-of-proofs lower bounds; for this it is necessary to establish lower bounds for randomized protocols or for monotone CLOs. (shrink)

David Charles presents a major new study of Aristotle's views on meaning, essence, necessity, and related topics. These interconnected views are central to Aristotle's metaphysics, philosophy of language, and philosophy of science, and are also highly relevant to current philosophical debates. Charles aims to reach a clear understanding of Aristotle's claims and arguments, to assess their truth, and to evaluate their importance to ancient and modern philosophy.

A Ramsey statement denoted \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${n \longrightarrow (k)^2_2}$$\end{document} says that every undirected graph on n vertices contains either a clique or an independent set of size k. Any such valid statement can be encoded into a valid DNF formula RAM(n, k) of size O(nk) and with terms of size \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\left(\begin{smallmatrix}k\\2\end{smallmatrix}\right)}$$\end{document}. Let rk be the minimal n for which the statement holds. We prove that (...) RAM(rk, k) requires exponential size constant depth Frege systems, answering a problem of Krishnamurthy and Moll [15]. As a consequence of Pudlák’s work in bounded arithmetic [19] it is known that there are quasi-polynomial size constant depth Frege proofs of RAM(4k, k), but the proof complexity of these formulas in resolution R or in its extension R(log) is unknown. We define two relativizations of the Ramsey statement that still have quasi-polynomial size constant depth Frege proofs but for which we establish exponential lower bound for R. (shrink)

We show that the feasible interpolation property is robust for some proof systems but not for others.

We study from the proof complexity perspective the proof search problem : •Is there an optimal way to search for propositional proofs?We note that, as a consequence of Levin’s universal search, for any fixed proof system there exists a time-optimal proof search algorithm. Using classical proof complexity results about reflection principles we prove that a time-optimal proof search algorithm exists without restricting proof systems iff a p-optimal proof system exists.To characterize precisely the time proof search algorithms need for individual formulas (...) we introduce a new proof complexity measure based on algorithmic information concepts. In particular, to a proof system P we attach information-efficiency function $i_P$ assigning to a tautology a natural number, and we show that: • $i_P$ characterizes time any P-proof search algorithm has to use on $\tau $,•for a fixed P there is such an information-optimal algorithm,•a proof system is information-efficiency optimal iff it is p-optimal,•for non-automatizable systems P there are formulas $\tau $ with short proofs but having large information measure $i_P$.We isolate and motivate the problem to establish unconditional super-logarithmic lower bounds for $i_P$ where no super-polynomial size lower bounds are known. We also point out connections of the new measure with some topics in proof complexity other than proof search. (shrink)

We investigate the possibility to characterize (multi) functions that are Σ b i -definable with small i (i = 1, 2, 3) in fragments of bounded arithmetic T 2 in terms of natural search problems defined over polynomial-time structures. We obtain the following results: (1) A reformulation of known characterizations of (multi)functions that are Σ b 1 - and Σ b 2 -definable in the theories S 1 2 and T 1 2 . (2) New characterizations of (multi)functions that are (...) Σ b 2 - and Σ b 3 -definable in the theory T 2 2 . (3) A new non-conservation result: the theory T 2 2 (α) is not ∀Σ b 1 (α)-conservative over the theory S 2 2 (α). To prove that the theory T 2 2 (α) is not ∀Σ b 1 (α)-conservative over the theory S 2 2 (α), we present two examples of a Σ b 1 (α)-principle separating the two theories: (a) the weak pigeonhole principle WPHP (a 2 , f, g) formalizing that no function f is a bijection between a 2 and a with the inverse g, (b) the iteration principle Iter (a, R, f) formalizing that no function f defined on a strict partial order ( $\{0,\dots,a\}$ , R) can have increasing iterates. (shrink)

Beneath the stylized violence and thrilling car crashes, the Mad Max films consider universal questions about the nature of human life, order and anarchy, justice and moral responsibility, society and technology, and ultimately, human redemption. In Mad Max and Philosophy, a diverse team of political scientists, historians, and philosophers investigates the underlying themes of the blockbuster movie franchise, following Max as he attempts to rebuild himself and the world. -/- This book guides you through the barren wastelands of a post-apocalyptic (...) future as you explore ethics and politics in The Wasteland, the importance of costumes and music, humankind's relationship with nature, commerce, gender, religion, madness, and more. (shrink)