Motivated by the problem of finding finite versions of classical incompleteness theorems, we present some conjectures that go beyond NP ≠ coNP. These conjectures formally connect computational complexity with the difficulty of proving some sentences, which means that high computational complexity of a problem associated with a sentence implies that the sentence is not provable in a weak theory, or requires a long proof. Another reason for putting forward these conjectures is that some results in proof complexity seem to be (...) special cases of such general statements and we want to formalize and fully understand these statements. Roughly speaking, we are trying to connect syntactic complexity, by which we mean the complexity of sentences and strengths of the theories in which they are provable, with the semantic concept of complexity of the computational problems represented by these sentences. -/- We have introduced the most fundamental conjectures in our earlier works. Our aim in this article is to present them in a more systematic way, along with several new conjectures, and prove new connections between them and some other statements studied before. (shrink)

We prove an exponential lower bound on the length of cutting plane proofs. The proof uses an extension of a lower bound for monotone circuits to circuits which compute with real numbers and use nondecreasing functions as gates. The latter result is of independent interest, since, in particular, it implies an exponential lower bound for some arithmetic circuits.

Suppose that Φ\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${{\it \Phi}}$$\end{document} is a consistent sentence. Then there is no Herbrand proof of ¬Φ\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\neg {\it \Phi}}$$\end{document}, which means that any Herbrand disjunction made from the prenex form of ¬Φ\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\neg {\it \Phi}}$$\end{document} is falsifiable. We show that the problem of finding such a falsifying assignment is hard in the following sense. For every (...) total polynomial search problem R, there exists a consistent Φ\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${{\it \Phi}}$$\end{document} such that finding solutions to R can be reduced to finding a falsifying assignment to an Herbrand disjunction made from ¬Φ\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\neg {\it \Phi}}$$\end{document}. It has been conjectured that there are no complete total polynomial search problems. If this conjecture is true, then for every consistent sentence Φ\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${{\it \Phi}}$$\end{document}, there exists a consistent sentence Ψ\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\Psi}$$\end{document}, such that the search problem associated with Ψ\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\Psi}$$\end{document} cannot be reduced to the search problem associated with Φ\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${{\it \Phi}}$$\end{document}. (shrink)

We define propositional quantum Frege proof systems and compare them with classical Frege proof systems.

The canonical pair of a proof system P is the pair of disjoint NP sets where one set is the set of all satisfiable CNF formulas and the other is the set of CNF formulas that have P-proofs bounded by some polynomial. We give a combinatorial characterization of the canonical pairs of depth d Frege systems. Our characterization is based on certain games, introduced in this article, that are parametrized by a number k, also called the depth. We show that (...) the canonical pair of a depth d Frege system is polynomially equivalent to the pair (Ad+2,Bd+2) where Ad+2 (respectively, Bd+1) are depth d+1 games in which Player I (Player II) has a positional winning strategy. Although this characterization is stated in terms of games, we will show that these combinatorial structures can be viewed as generalizations of monotone Boolean circuits. In particular, depth 1 games are essentially monotone Boolean circuits. Thus we get a generalization of the monotone feasible interpolation for Resolution, which is a property that enables one to reduce the task of proving lower bounds on the size of refutations to lower bounds on the size of monotone Boolean circuits. However, we do not have a method yet for proving lower bounds on the size of depth d games for d>1. (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)

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.

Linear arithmetics are extensions of Presburger arithmetic () by one or more unary functions, each intended as multiplication by a fixed element (scalar), and containing the full induction schemes for their respective languages. In this paper, we construct a model of the 2‐linear arithmetic (linear arithmetic with two scalars) in which an infinitely long initial segment of “Peano multiplication” on is ‐definable. This shows, in particular, that is not model complete in contrast to theories and that are known to satisfy (...) quantifier elimination up to disjunctions of primitive positive formulas. As an application, we show that, as a discretely ordered module over the discretely ordered ring generated by the two scalars, does not have the NIP, answering negatively a question of Chernikov and Hils. (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.

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 } $.

Libertarian philosophy asserts that only the initiation of physical force against persons or property, or the threat thereof, is inherently illegitimate. A corollary to this assertion is that all forms of speech, including fraudulent advertising, are not invasive and therefore should be considered legitimate. On the other hand, fraudulent advertising can be viewed as implicit theft under the theory of contract: if a seller accepts money knowing that his product does not have some of its advertised characteristics, he acquires the (...) property title to the customer’s money without voluntary consent, which is theft. The balance between these two logical extensions of property rights—the right of free speech and the right of contract—lies somewhere in the area of communication philosophy, and can be explained through understanding the role of communication in human interactions. Advertising is a form of communication that may convey important information about the conditions of the proposed contract. These conditions are expressed in particular words that may have different meanings in different circumstances. Therefore to determine whether a particular example or “misinterpretation” is mere sophistry or a type of fraud, the judicial system has to approach each issue on a case-by-case basis. The border between legal and illegal should be determined by precedents and by expectations based on commonly accepted definitions of terms—what people commonly understand by the words and other forms of communication they use. (shrink)

Out of the broad variety of Cusanus' work, this book discusses six of his writings, careful not to isolate them from the whole of his work. It instead presents them against the maturation of Cusanus' thinking as it developed from his first sermons up to his shortest philosophical text De apice theoriae. The texts in question are De docta ignorantia, De coniecturis, Idiota de mente, De beryllo, Trialogus de possest and De apice theoriae. In the search for God, or rather (...) in Cusanus' lifetime eff orts to have his spirit touch the fi rst principle and the basis of all things, new perspectives on the world and man within would open up for Cusanus. Respecting this basic intention of Cusanus' thinking, the author primarily deals with Cusanus' ontotheological (metaphysical) claims and, in their context, turns his attention to the cosmological, or anthropologico-gnoseological opinions. (shrink)

In my comment on Katerina Ierodiakonou’s paper, I outline my understanding of the programme of De anima and how it bears on Aristotle’s discussion of the transparent in De anima 2.7, in contrast with his discussion of the transparent in De sensu 3. I then explore Aristotle’s notion of transparency and sketch an alternative to Ierodiakonou’s interpretation of Aristotle’s views as to how colours are generated in physical objects. At the end, I raise two objections to Alexander’s interpretation of the (...) transparent as discussed by Ierodiakonou. (shrink)

Kniha obsahuje články, studie, úvahy a memoárové texty, publikované v různých časopisech a sbornících v letech 1971 až 2010.

Chapter One: Constructions. Entities, constructions, and functions When one travels from Los Angeles to New York, going, say, by way of St. Louis, Chicago, ...

Traxler, Pickering, and Clifton found that ambiguous sentences are read faster than their unambiguous counterparts. This so-called ambiguity advantage has presented a major challenge to classical theories of human sentence comprehension because its most prominent explanation, in the form of the unrestricted race model, assumes that parsing is non-deterministic. Recently, Swets, Desmet, Clifton, and Ferreira have challenged the URM. They argue that readers strategically underspecify the representation of ambiguous sentences to save time, unless disambiguation is required by task demands. When (...) disambiguation is required, however, readers assign sentences full structure—and Swets et al. provide experimental evidence to this end. On the basis of their findings, they argue against the URM and in favor of a model of task-dependent sentence comprehension. We show through simulations that the Swets et al. data do not constitute evidence for task-dependent parsing because they can be explained by the URM. However, we provide decisive evidence from a German self-paced reading study consistent with Swets et al.'s general claim about task-dependent parsing. Specifically, we show that under certain conditions, ambiguous sentences can be read more slowly than their unambiguous counterparts, suggesting that the parser may create several parses, when required. Finally, we present the first quantitative model of task-driven disambiguation that subsumes the URM, and we show that it can explain both Swets et al.'s results and our findings. (shrink)