A semantics of evidence for classical arithmetic

1995 ◽  
Vol 60 (1) ◽  
pp. 325-337 ◽  
Author(s):  
Thierry Coquand

If it is difficult to give the exact significance of consistency proofs from a classical point of view, in particular the proofs of Gentzen [2, 6], and Novikoff [14], the motivations of these proofs are quite clear intuitionistically. Their significance is then less to give a mere consistency proof than to present an intuitionistic explanation of the notion of classical truth. Gentzen for instance summarizes his proof as follows [6]: “Thus propositions of actualist mathematics seem to have a certain utility, but no sense. The major part of my consistency proof, however, consists precisely in ascribing a finitist sense to actualist propositions.” From this point of view, the main part of both Gentzen's and Novikoff's arguments can be stated as establishing that modus ponens is valid w.r.t. this interpretation ascribing a “finitist sense” to classical propositions.In this paper, we reformulate Gentzen's and Novikoff's “finitist sense” of an arithmetic proposition as a winning strategy for a game associated to it. (To see a proof as a winning strategy has been considered by Lorenzen [10] for intuitionistic logic.) In the light of concurrency theory [7], it is tempting to consider a strategy as an interactive program (which represents thus the “finitist sense” of an arithmetic proposition). We shall show that the validity of modus ponens then gets a quite natural formulation, showing that “internal chatters” between two programs end eventually.We first present Novikoff's notion of regular formulae, that can be seen as an intuitionistic truth definition for classical infinitary propositional calculus. We use this in order to motivate the second part, which presents a game-theoretic interpretation of the notion of regular formulae, and a proof of the admissibility of modus ponens which is based on this interpretation.

2012 ◽  
Vol 2012 ◽  
pp. 1-19 ◽  
Author(s):  
Guido Sciavicco

The role of time in artificial intelligence is extremely important. Interval-based temporal reasoning can be seen as a generalization of the classical point-based one, and the first results in this field date back to Hamblin (1972) and Benhtem (1991) from the philosophical point of view, to Allen (1983) from the algebraic and first-order one, and to Halpern and Shoham (1991) from the modal logic one. Without purporting to provide a comprehensive survey of the field, we take the reader to a journey through the main developments in modal and first-order interval temporal reasoning over the past ten years and outline some landmark results on expressiveness and (un)decidability of the satisfiability problem for the family of modal interval logics.


Author(s):  
Željko Ivezi ◽  
Andrew J. Connolly ◽  
Jacob T. VanderPlas ◽  
Alexander Gray ◽  
Željko Ivezi ◽  
...  

This chapter introduces the main concepts of statistical inference, or drawing conclusions from data. There are three main types of inference: point estimation, confidence estimation, and hypothesis testing. There are two major statistical paradigms which address the statistical inference questions: the classical, or frequentist paradigm, and the Bayesian paradigm. While most of statistics and machine learning is based on the classical paradigm, Bayesian techniques are being embraced by the statistical and scientific communities at an ever-increasing pace. The chapter begins with a short comparison of classical and Bayesian paradigms, and then discusses the three main types of statistical inference from the classical point of view.


2013 ◽  
Vol 15 (03) ◽  
pp. 1340019 ◽  
Author(s):  
JOAQUIN SANCHEZ-SORIANO

In this paper, we review some of the literature in which different applications to engineering problems are analyzed from a game-theoretic point of view. The revision is far from exhaustive and the sole purpose of this paper is to provide an approximate state-of-the-art on this topic. Likewise, we try throughout the paper to highlight what game theory could contribute to the study of engineering problems.


2008 ◽  
Vol 73 (4) ◽  
pp. 1433-1457 ◽  
Author(s):  
Miloš S. Kurilić ◽  
Boris Šobot

AbstractThe game is played on a complete Boolean algebra , by two players. White and Black, in κ-many moves (where κ is an infinite cardinal). At the beginning White chooses a non-zero element p ∈ . In the α-th move White chooses pα ∈ (0, p) and Black responds choosing iα ∈{0, 1}. White winsthe play iff . where and .The corresponding game theoretic properties of c.B.a.'s are investigated. So, Black has a winning strategy (w.s.) if κ ≥ π() or if contains a κ-closed dense subset. On the other hand, if White has a w.s., then κ ∈ . The existence of w.s. is characterized in a combinatorial way and in terms of forcing. In particular, if 2<κ = κ ∈ Reg and forcing by preserves the regularity of κ, then White has a w.s. iff the power 2κ is collapsed to κ in some extension. It is shown that, under the GCH, for each set S ⊆ Reg there is a c.B.a. such that White (respectively. Black) has a w.s. for each infinite cardinal κ ∈ S (resp. κ ∉ S). Also it is shown consistent that for each κ ∈ Reg there is a c.B.a. on which the game is undetermined.


2010 ◽  
Vol 3 (3) ◽  
pp. 485-519 ◽  
Author(s):  
LOES OLDE LOOHUIS ◽  
YDE VENEMA

We study a generalization of the standard syntax and game-theoretic semantics of logic, which is based on a duality between two players, to a multiplayer setting. We define propositional and modal languages of multiplayer formulas, and provide them with a semantics involving a multiplayer game. Our focus is on the notion of equivalence between two formulas, which is defined by saying that two formulas are equivalent if under each valuation, the set of players with a winning strategy is the same in the two respective associated games. We provide a derivation system which enumerates the pairs of equivalent formulas, both in the propositional case and in the modal case. Our approach is algebraic: We introduce multiplayer algebras as the analogue of Boolean algebras, and show, as the corresponding analog to Stone’s theorem, that these abstract multiplayer algebras can be represented as concrete ones which capture the game-theoretic semantics. For the modal case we prove a similar result. We also address the computational complexity of the problem whether two given multiplayer formulas are equivalent. In the propositional case, we show that this problem is co-NP-complete, whereas in the modal case, it is PSPACE-hard.


1984 ◽  
Vol 49 (1) ◽  
pp. 192-203 ◽  
Author(s):  
Nicolas D. Goodman

Questions about the constructive or effective character of particular arguments arise in several areas of classical mathematics, such as in the theory of recursive functions and in numerical analysis. Some philosophers have advocated Lewis's S4 as the proper logic in which to formalize such epistemic notions. (The fundamental work on this is Hintikka [4].) Recently there have been studies of mathematical theories formalized with S4 as the underlying logic so that these epistemic notions can be expressed. (See Shapiro [7], Myhill [5], and Goodman [2]. The motivation for this work is discussed in Goodman [3].) The present paper is a contribution to the study of the simplest of these theories, namely first-order arithmetic as formalized in S4. Following Shapiro, we call this theory epistemic arithmetic (EA). More specifically, we show that EA is a conservative extension of Hey ting's arithmetic HA (ordinary first-order intuitionistic arithmetic). The question of whether EA is conservative over HA was raised but left open in Shapiro [7].The idea of our proof is as follows. We interpret EA in an infinitary propositional S4, pretty much as Tait, for example, interprets classical arithmetic in his infinitary classical propositional calculus in [8]. We then prove a cut-elimination theorem for this infinitary propositional S4. A suitable version of the cut-elimination theorem can be formalized in HA. For cut-free infinitary proofs, there is a reflection principle provable in HA. That is, we can prove in HA that if there is a cut-free proof of the interpretation of a sentence ϕ then ϕ is true. Combining these results shows that if the interpretation of ϕ is provable in EA, then ϕ is provable in HA.


1951 ◽  
Vol 16 (3) ◽  
pp. 204-204 ◽  
Author(s):  
Alan Rose

There has recently been developed a method of formalising any fragment of the propositional calculus, subject only to the condition that material implication is a primitive function of the fragmentary system considered. Tarski has stated, without proof, that when implication is the only primitive function a formulation which is weakly complete (i.e., has as theorems all expressible tautologies) is also strongly complete (i.e., provides for the deduction of any expressible formula from any which is not a tautology). The methods used by Henkin suggest the following proof of theTheorem. If in a fragment of the propositional calculus material implication can be defined in terms of the primitive functions, then any weakly complete formalisation of the fragmentary system which has for rules of procedure the substitution rule and modus ponens is also strongly complete.


2016 ◽  
Vol 9 (3) ◽  
pp. 429-455
Author(s):  
LUCA BELLOTTI

AbstractWe consider the consistency proof for a weak fragment of arithmetic published by von Neumann in 1927. This proof is rather neglected in the literature on the history of consistency proofs in the Hilbert school. We explain von Neumann’s proof and argue that it fills a gap between Hilbert’s consistency proofs for the so-called elementary calculus of free variables with a successor and a predecessor function and Ackermann’s consistency proof for second-order primitive recursive arithmetic. In particular, von Neumann’s proof is the first rigorous proof of the consistency of an axiomatization of the first-order theory of a successor function.


Author(s):  
Andrey Krushinskiy

For a long time, leading European thinkers have denied systematic, theoretical and rational nature of Chinese traditional thinking, unpretentiously reading it as banal moralizing (“moral philosophy,” at best – “moral metaphysics,” etc.), not supported by any proper philosophical discourse. However, the habitual socioethical label conceals a much deeper problematic of strategic thinking. At its center, there is the question of choosing all sorts of strategies: from everyday life to special technical ones, from personal existential choice to fateful state decisions. The concept of a winning strategy is emblematized by the dramatic plot of a deadly risk (“stepping on a tiger’s tail”) but under certain conditions with guaranteed happy end. The strategy of harmony (he 和), which is miraculous in its effectiveness, is proposed as a exemplary strategy. It allows you to “step on the tiger’s tail” with impunity (lü hu wei履 虎尾). From the point of view of strategic thinking, the criterion of cognitive value of reasoning is its effectiveness (in the context of a particular game), and the most effective is unmistakable prediction, i.e. the ability to predict the outcome of future developments with the help of reasoning. In the ideal case (under certain conditions), prognostic reasoning becomes not just plausible but 100% reliable that is an apodictic true inference. Therefore, the highest cognitive status in the Chinese intellectual tradition is endowed with guaranteed error-free prognostic reasoning. This type of reasoning, where the reliability of foresight is guaranteed by the implementation of a certain winning strategy, can be called the prognostic form of deduction. As a result, the dynamism of Chinese logic, which relies on a deliberate staging of the future (sometimes with the help of stratagems of varying degrees of cunning), is strikingly different from the static nature of the classical image of logic (both traditional and modern), where logic is no more than a static guardian of correctness of reasoning. On the contrary, the Chinese concept of logic focuses on deriving consequences from strategic considerations regarding the future, actively and purposefully shaped by the subject who at the same time constructing both himself and the world around him.


Sign in / Sign up

Export Citation Format

Share Document