Journal articles: 'Proof-theoretic semantics'

1

Kahle, Reinhard, and Peter Schroeder-Heister. "Introduction: Proof-theoretic Semantics." Synthese 148, no. 3 (February 2006): 503–6. http://dx.doi.org/10.1007/s11229-004-6292-5.

Full text

APA, Harvard, Vancouver, ISO, and other styles

2

Francez, Nissim. "Views of proof-theoretic semantics: reified proof-theoretic meanings." Journal of Logic and Computation 26, no. 2 (May 30, 2014): 479–94. http://dx.doi.org/10.1093/logcom/exu035.

Full text

APA, Harvard, Vancouver, ISO, and other styles

3

Francez, Nissim. "Bilateralism in Proof-Theoretic Semantics." Journal of Philosophical Logic 43, no. 2-3 (January 10, 2013): 239–59. http://dx.doi.org/10.1007/s10992-012-9261-3.

Full text

APA, Harvard, Vancouver, ISO, and other styles

4

Stafford, Will. "Proof-Theoretic Semantics and Inquisitive Logic." Journal of Philosophical Logic 50, no. 5 (June 12, 2021): 1199–229. http://dx.doi.org/10.1007/s10992-021-09596-7.

Full text

APA, Harvard, Vancouver, ISO, and other styles

5

Chung, Inkyo. "Proof-Theoretic Semantics and Atomic Base." Korean Journal of Philosophy 125 (November 30, 2015): 57. http://dx.doi.org/10.18694/kjp.2015.11.125.57.

Full text

APA, Harvard, Vancouver, ISO, and other styles

6

Stirton, William R. "SOME PROBLEMS FOR PROOF-THEORETIC SEMANTICS." Philosophical Quarterly 58, no. 231 (April 2008): 278–98. http://dx.doi.org/10.1111/j.1467-9213.2007.506.x.

Full text

APA, Harvard, Vancouver, ISO, and other styles

7

Francez, Nissim, Roy Dyckhoff, and Gilad Ben-Avi. "Proof-Theoretic Semantics for Subsentential Phrases." Studia Logica 94, no. 3 (March 24, 2010): 381–401. http://dx.doi.org/10.1007/s11225-010-9241-y.

Full text

APA, Harvard, Vancouver, ISO, and other styles

8

Francez, Nissim, and Michael Kaminski. "A Proof-Theoretic Semantics for Exclusion." Logica Universalis 11, no. 4 (October 24, 2017): 489–505. http://dx.doi.org/10.1007/s11787-017-0179-y.

Full text

APA, Harvard, Vancouver, ISO, and other styles

9

Tait, William W. "Proof-theoretic Semantics for Classical Mathematics." Synthese 148, no. 3 (February 2006): 603–22. http://dx.doi.org/10.1007/s11229-004-6271-x.

Full text

APA, Harvard, Vancouver, ISO, and other styles

10

Schroeder-Heister, Peter. "Validity Concepts in Proof-theoretic Semantics." Synthese 148, no. 3 (February 2006): 525–71. http://dx.doi.org/10.1007/s11229-004-6296-1.

Full text

APA, Harvard, Vancouver, ISO, and other styles

11

FRANCEZ, NISSIM, and GILAD BEN-AVI. "PROOF-THEORETIC SEMANTIC VALUES FOR LOGICAL OPERATORS." Review of Symbolic Logic 4, no. 3 (September 2011): 466–78. http://dx.doi.org/10.1017/s1755020311000098.

Full text

Abstract:

The paper proposes a semantic value for the logical constants (connectives and quantifiers) within the framework of proof-theoretic semantics, basic meaning on the introduction rules of a meaning conferring natural deduction proof system. The semantic value is defined based on Frege’s Context Principle, by taking “contributions” to sentential meanings as determined by the function-argument structure as induced by a type-logical grammar. In doing so, the paper proposes a novel proof-theoretic interpretation of the semantic types, traditionally interpreted in Henkin models. The compositionality of the resulting attribution of semantic values is discussed. Elsewhere, the same method was used for defining proof-theoretic meaning of subsentential phrases in a fragment of natural language. Doing the same for (the simpler and clearer case of) logic sheds more light on the proposal.

APA, Harvard, Vancouver, ISO, and other styles

12

Piecha, Thomas, Wagner de Campos Sanz, and Peter Schroeder-Heister. "Failure of Completeness in Proof-Theoretic Semantics." Journal of Philosophical Logic 44, no. 3 (August 1, 2014): 321–35. http://dx.doi.org/10.1007/s10992-014-9322-x.

Full text

APA, Harvard, Vancouver, ISO, and other styles

13

Francez, Nissim. "A Proof-Theoretic Semantics for Adjectival Modification." Journal of Logic, Language and Information 26, no. 1 (November 4, 2016): 21–43. http://dx.doi.org/10.1007/s10849-016-9245-8.

Full text

APA, Harvard, Vancouver, ISO, and other styles

14

Miller, Dale. "A Proof Theoretic Approach to Operational Semantics." Electronic Notes in Theoretical Computer Science 162 (September 2006): 243–47. http://dx.doi.org/10.1016/j.entcs.2005.12.089.

Full text

APA, Harvard, Vancouver, ISO, and other styles

15

Dicher, Bogdan. "On a Generality Condition in Proof-Theoretic Semantics." Theoria 83, no. 4 (October 25, 2017): 394–418. http://dx.doi.org/10.1111/theo.12131.

Full text

APA, Harvard, Vancouver, ISO, and other styles

16

DICHER, BOGDAN. "WEAK DISHARMONY: SOME LESSONS FOR PROOF-THEORETIC SEMANTICS." Review of Symbolic Logic 9, no. 3 (August 8, 2016): 583–602. http://dx.doi.org/10.1017/s1755020316000162.

Full text

Abstract:

AbstractA logical constant is weakly disharmonious if its elimination rules are weaker than its introduction rules. Substructural weak disharmony is the weak disharmony generated by structural restrictions on the eliminations. I argue that substructural weak disharmony is not a defect of the constants which exhibit it. To the extent that it is problematic, it calls into question the structural properties of the derivability relation. This prompts us to rethink the issue of controlling the structural properties of a logic by means of harmony. I argue that such a control is possible and desirable. Moreover, it is best achieved by global tests of harmony.

APA, Harvard, Vancouver, ISO, and other styles

17

Francez, Nissim, and Roy Dyckhoff. "Proof-theoretic semantics for a natural language fragment." Linguistics and Philosophy 33, no. 6 (December 2010): 447–77. http://dx.doi.org/10.1007/s10988-011-9088-3.

Full text

APA, Harvard, Vancouver, ISO, and other styles

18

Francez, Nissim. "A proof-theoretic semantics for contextual domain restriction." Journal of Language Modelling 2, no. 2 (January 12, 2015): 249. http://dx.doi.org/10.15398/jlm.v2i2.87.

Full text

APA, Harvard, Vancouver, ISO, and other styles

19

Stafford, Will. "Something Valid This Way Comes: A Study of Neologicism and Proof-Theoretic Validity." Bulletin of Symbolic Logic 28, no. 4 (December 2022): 530–31. http://dx.doi.org/10.1017/bsl.2022.16.

Full text

Abstract:

AbstractThe interplay of philosophical ambitions and technical reality have given birth to rich and interesting approaches to explain the oft-claimed special character of mathematical and logical knowledge. Two projects stand out both for their audacity and their innovativeness. These are logicism and proof-theoretic semantics. This dissertation contains three chapters exploring the limits of these two projects. In both cases I find the formal results offer a mixed blessing to the philosophical projects.Chapter 1. Is a logicist bound to the claim that as a matter of analytic truth there is an actual infinity of objects? If Hume’s Principle is analytic then in the standard setting the answer appears to be yes. Hodes’s work pointed to a way out by offering a modal picture in which only a potential infinity was posited. However, this project was abandoned due to apparent failures of cross-world predication. I re-explore this idea and discover that in the setting of the potential infinite one can interpret first-order Peano arithmetic, but not second-order Peano arithmetic. I conclude that in order for the logicist to weaken the metaphysically loaded claim of necessary actual infinities, they must also weaken the mathematics they recover.Chapter 2. There have been several recent results bringing into focus the super-intuitionistic nature of most notions of proof-theoretic validity. But there has been very little work evaluating the consequences of these results. In this chapter, I explore the question of whether these results undermine the claim that proof-theoretic validity shows us which inferences follow from the meaning of the connectives when defined by their introduction rules. It is argued that the super-intuitionistic inferences are valid due to the correspondence between the treatment of the atomic formulas and more complex formulas. And so the goals of proof-theoretic validity are not undermined.Chapter 3. Prawitz (1971) conjectured that proof-theoretic validity offers a semantics for intuitionistic logic. This conjecture has recently been proven false by Piecha and Schroeder-Heister (2019). This chapter resolves one of the questions left open by this recent result by showing the extensional alignment of proof-theoretic validity and general inquisitive logic. General inquisitive logic is a generalisation of inquisitive semantics, a uniform semantics for questions and assertions. The chapter further defines a notion of quasi-proof-theoretic validity by restricting proof-theoretic validity to allow double negation elimination for atomic formulas and proves the extensional alignment of quasi-proof-theoretic validity and inquisitive logic.Abstract prepared by Will Stafford extracted partially from the dissertation.E-mail: stafford@flu.cas.czURL: https://escholarship.org/uc/item/33c6h00c

APA, Harvard, Vancouver, ISO, and other styles

20

FRANCEZ, NISSIM. "ON THE NOTION OF CANONICAL DERIVATIONS FROM OPEN ASSUMPTIONS AND ITS ROLE IN PROOF-THEORETIC SEMANTICS." Review of Symbolic Logic 8, no. 2 (March 20, 2015): 296–305. http://dx.doi.org/10.1017/s1755020315000027.

Full text

Abstract:

AbstractThe paper proposes an extension of the definition of a canonical proof, central to proof-theoretic semantics, to a definition of a canonical derivation from open assumptions. The impact of the extension on the definition of (reified) proof-theoretic meaning of logical constants is discussed. The extended definition also sheds light on a puzzle regarding the definition of local-completeness of a natural-deduction proof-system, underlying its harmony.

APA, Harvard, Vancouver, ISO, and other styles

21

Zimmermann, Ernst. "Proof‐theoretic semantics of natural deduction based on inversion." Theoria 87, no. 6 (December 2021): 1651–70. http://dx.doi.org/10.1111/theo.12375.

Full text

APA, Harvard, Vancouver, ISO, and other styles

22

GIRLANDO, MARIANNA, SARA NEGRI, NICOLA OLIVETTI, and VINCENT RISCH. "CONDITIONAL BELIEFS: FROM NEIGHBOURHOOD SEMANTICS TO SEQUENT CALCULUS." Review of Symbolic Logic 11, no. 4 (June 28, 2018): 736–79. http://dx.doi.org/10.1017/s1755020318000023.

Full text

Abstract:

AbstractThe logic of Conditional Beliefs (CDL) has been introduced by Board, Baltag, and Smets to reason about knowledge and revisable beliefs in a multi-agent setting. In this article both the semantics and the proof theory for this logic are studied. First, a natural semantics forCDLis defined in terms of neighbourhood models, a multi-agent generalisation of Lewis’ spheres models, and it is shown that the axiomatization ofCDLis sound and complete with respect to this semantics. Second, it is shown that the neighbourhood semantics is equivalent to the original one defined in terms of plausibility models, by means of a direct correspondence between the two types of models. On the basis of neighbourhood semantics, a labelled sequent calculus forCDLis obtained. The calculus has strong proof-theoretic properties, in particular admissibility of contraction and cut, and it provides a decision procedure for the logic. Furthermore, its semantic completeness is used to obtain a constructive proof of the finite model property of the logic. Finally, it is shown that other doxastic operators can be easily captured within neighbourhood semantics. This fact provides further evidence of the naturalness of neighbourhood semantics for the analysis of epistemic/doxastic notions.

APA, Harvard, Vancouver, ISO, and other styles

23

Forster, Yannick, Dominik Kirst, and Dominik Wehr. "Completeness theorems for first-order logic analysed in constructive type theory." Journal of Logic and Computation 31, no. 1 (January 2021): 112–51. http://dx.doi.org/10.1093/logcom/exaa073.

Full text

Abstract:

Abstract We study various formulations of the completeness of first-order logic phrased in constructive type theory and mechanised in the Coq proof assistant. Specifically, we examine the completeness of variants of classical and intuitionistic natural deduction and sequent calculi with respect to model-theoretic, algebraic, and game-theoretic semantics. As completeness with respect to the standard model-theoretic semantics à la Tarski and Kripke is not readily constructive, we analyse connections of completeness theorems to Markov’s Principle and Weak Kőnig’s Lemma and discuss non-standard semantics admitting assumption-free completeness. We contribute a reusable Coq library for first-order logic containing all results covered in this paper.

APA, Harvard, Vancouver, ISO, and other styles

24

WIĘCKOWSKI, BARTOSZ. "RULES FOR SUBATOMIC DERIVATION." Review of Symbolic Logic 4, no. 2 (December 15, 2010): 219–36. http://dx.doi.org/10.1017/s175502031000033x.

Full text

Abstract:

In proof-theoretic semantics the meaning of an atomic sentence is usually determined by a set of derivations in an atomic system which contain that sentence as a conclusion (see, in particular, Prawitz, 1971, 1973). The paper critically discusses this standard approach and suggests an alternative account which proceeds in terms of subatomic introduction and elimination rules for atomic sentences. A simple subatomic normal form theorem by which this account of the semantics of atomic sentences and the terms from which they are composed is underpinned, shows moreover that the proof-theoretic analysis of first-order logic can be pursued also beneath the atomic level.

APA, Harvard, Vancouver, ISO, and other styles

25

de Queiroz, Ruy J. G. B. "On Reduction Rules, Meaning-as-use, and Proof-theoretic Semantics." Studia Logica 90, no. 2 (October 24, 2008): 211–47. http://dx.doi.org/10.1007/s11225-008-9150-5.

Full text

APA, Harvard, Vancouver, ISO, and other styles

26

Więckowski, Bartosz. "Intuitionistic multi-agent subatomic natural deduction for belief and knowledge." Journal of Logic and Computation 31, no. 3 (March 26, 2021): 704–70. http://dx.doi.org/10.1093/logcom/exab013.

Full text

Abstract:

Abstract This paper proposes natural deduction systems for the representation of inferences in which several agents participate in deriving conclusions about what they believe or know, where belief and knowledge are understood in an intuitionistic sense. Multi-agent derivations in these systems may involve relatively complex belief (resp. knowledge) constructions which may include forms of nested, reciprocal, shared, distributed or universal belief/knowledge as well as attitudes de dicto/re/se. The systems consist of two main components: multi-agent belief bases which assign to each agent a subatomic system that represents the agent’s beliefs concerning atomic sentences and a set of multi-agent labelled rules for logically compound formulae. Derivations in these systems normalize. Moreover, normal derivations possess the subexpression property (a refinement of the subformula property) which makes them fully analytic. Relying on the normalization result, a proof-theoretic approach to the semantics of the intensional operators for intuitionistic belief/knowledge is presented which explains their meaning entirely by appeal to the structure of derivations. Importantly, this proof-theoretic semantics is autarkic with respect to its foundations as the systems (unlike, e.g. external/labelled proof systems which internalize possible worlds truth conditions) are not defined on the basis of a possible worlds semantics. Detailed applications to a logical puzzle (McCarthy’s three wise men puzzle) and to a semantical difficulty (Geach’s problem of intentional identity), respectively, illustrate the systems. The paper also provides comparisons with other approaches to intuitionistic belief/knowledge and multi-agent natural deduction.

APA, Harvard, Vancouver, ISO, and other styles

27

Schroeder-Heister, Peter. "Proof-Theoretic Semantics, Self-Contradiction, and the Format of Deductive Reasoning." Topoi 31, no. 1 (March 31, 2012): 77–85. http://dx.doi.org/10.1007/s11245-012-9119-x.

Full text

APA, Harvard, Vancouver, ISO, and other styles

28

Kürbis, Nils. "Proof-Theoretic Semantics, a Problem with Negation and Prospects for Modality." Journal of Philosophical Logic 44, no. 6 (November 28, 2013): 713–27. http://dx.doi.org/10.1007/s10992-013-9310-6.

Full text

APA, Harvard, Vancouver, ISO, and other styles

29

Tranchini, Luca. "Proof-theoretic semantics, paradoxes and the distinction between sense and denotation." Journal of Logic and Computation 26, no. 2 (June 2, 2014): 495–512. http://dx.doi.org/10.1093/logcom/exu028.

Full text

APA, Harvard, Vancouver, ISO, and other styles

30

Piecha, Thomas, and Peter Schroeder-Heister. "Incompleteness of Intuitionistic Propositional Logic with Respect to Proof-Theoretic Semantics." Studia Logica 107, no. 1 (August 25, 2018): 233–46. http://dx.doi.org/10.1007/s11225-018-9823-7.

Full text

APA, Harvard, Vancouver, ISO, and other styles

31

Negri, Sara, and Eugenio Orlandelli. "Proof theory for quantified monotone modal logics." Logic Journal of the IGPL 27, no. 4 (May 24, 2019): 478–506. http://dx.doi.org/10.1093/jigpal/jzz015.

Full text

Abstract:

Abstract This paper provides a proof-theoretic study of quantified non-normal modal logics (NNML). It introduces labelled sequent calculi based on neighbourhood semantics for the first-order extension, with both varying and constant domains, of monotone NNML, and studies the role of the Barcan formulas in these calculi. It will be shown that the calculi introduced have good structural properties: invertibility of the rules, height-preserving admissibility of weakening and contraction and syntactic cut elimination. It will also be shown that each of the calculi introduced is sound and complete with respect to the appropriate class of neighbourhood frames. In particular, the completeness proof constructs a formal derivation for derivable sequents and a countermodel for non-derivable ones, and gives a semantic proof of the admissibility of cut.

APA, Harvard, Vancouver, ISO, and other styles

32

Poggiolesi, Francesca. "Grounding rules and (hyper-)isomorphic formulas." Australasian Journal of Logic 17, no. 1 (April 7, 2020): 70. http://dx.doi.org/10.26686/ajl.v17i1.5694.

Full text

Abstract:

An oft-defended claim of a close relationship between Gentzen inference rules and the meaning of the connectives they introduce and eliminate has given rise to a whole domain called proof-theoretic semantics, see Schroeder- Heister (1991); Prawitz (2006). A branch of proof-theoretic semantics, mainly developed by Dosen (2019); Dosen and Petric (2011), isolates in a precise mathematical manner formulas (of a logic L) that have the same meaning. These isomorphic formulas are defined to be those that behave identically in inferences. The aim of this paper is to investigate another type of recently discussed rules in the literature, namely grounding rules, and their link to the meaning of the connectives they provide the grounds for. In particular, by using grounding rules, we will refine the notion of isomorphic formulas through the notion of hyper-isomorphic formulas. We will argue that it is actually the notion of hyper-isomorphic formulas that identify those formulas that have the same meaning.

APA, Harvard, Vancouver, ISO, and other styles

33

VAN BENTHEM, JOHAN, NICK BEZHANISHVILI, SEBASTIAN ENQVIST, and JUNHUA YU. "INSTANTIAL NEIGHBOURHOOD LOGIC." Review of Symbolic Logic 10, no. 1 (December 19, 2016): 116–44. http://dx.doi.org/10.1017/s1755020316000447.

Full text

Abstract:

AbstractThis paper explores a new language of neighbourhood structures where existential information can be given about what kind of worlds occur in a neighbourhood of a current world. The resulting system of ‘instantial neighbourhood logic’ INL has a nontrivial mix of features from relational semantics and from neighbourhood semantics. We explore some basic model-theoretic behavior, including a matching notion of bisimulation, and give a complete axiom system for which we prove completeness by a new normal form technique. In addition, we relate INL to other modal logics by means of translations, and determine its precise SAT complexity. Finally, we discuss proof-theoretic fine-structure of INL in terms of semantic tableaux and some expressive fine-structure in terms of fragments, while discussing concrete illustrations of the instantial neighborhood language in topological spaces, in games with powers for players construed in a new way, as well as in dynamic logics of acquiring or deleting evidence. We conclude with some coalgebraic perspectives on what is achieved in this paper. Many of these final themes suggest follow-up work of independent interest.

APA, Harvard, Vancouver, ISO, and other styles

34

LAKIN, MATTHEW R., and ANDREW M. PITTS. "Contextual equivalence for inductive definitions with binders in higher order typed functional programming." Journal of Functional Programming 23, no. 6 (November 2013): 658–700. http://dx.doi.org/10.1017/s0956796813000245.

Full text

Abstract:

AbstractCorrect handling of names and binders is an important issue in meta-programming. This paper presents an embedding of constraint logic programming into the αML functional programming language, which provides a provably correct means of implementing proof search computations over inductive definitions involving names and binders modulo α-equivalence. We show that the execution of proof search in the αML operational semantics is sound and complete with regard to the model-theoretic semantics of formulae, and develop a theory of contextual equivalence for the subclass of αML expressions which correspond to inductive definitions and formulae. In particular, we prove that αML expressions, which denote inductive definitions, are contextually equivalent precisely when those inductive definitions have the same model-theoretic semantics. This paper is a revised and extended version of the conference paper (Lakin, M. R. & Pitts, A. M. (2009) Resolving inductive definitions with binders in higher-order typed functional programming. InProceedings of the 18th European Symposium on Programming (ESOP 2009), Castagna, G. (ed), Lecture Notes in Computer Science, vol. 5502. Berlin, Germany: Springer-Verlag, pp. 47–61) and draws on material from the first author's PhD thesis (Lakin, M. R. (2010)An Executable Meta-Language for Inductive Definitions with Binders. University of Cambridge, UK).

APA, Harvard, Vancouver, ISO, and other styles

35

ZHANG, YU. "The computational SLR: a logic for reasoning about computational indistinguishability." Mathematical Structures in Computer Science 20, no. 5 (October 2010): 951–75. http://dx.doi.org/10.1017/s0960129510000265.

Full text

Abstract:

Computational indistinguishability is a notion in complexity-theoretic cryptography and is used to define many security criteria. However, in traditional cryptography, proving computational indistinguishability is usually informal and becomes error-prone when cryptographic constructions are complex. This paper presents a formal proof system based on an extension of Hofmann's SLR language, which can capture probabilistic polynomial-time computations through typing and is sufficient for expressing cryptographic constructions. In particular, we define rules that directly justify the computational indistinguishability between programs, and then prove that these rules are sound with respect to the set-theoretic semantics, and thus the standard definition of security. We also show that it is applicable in cryptography by verifying, in our proof system, Goldreich and Micali's construction of a pseudorandom generator, and the equivalence between next-bit unpredictability and pseudorandomness.

APA, Harvard, Vancouver, ISO, and other styles

36

Eklund, Peter W. "Research developments in multiple inheritance with exceptions." Knowledge Engineering Review 9, no. 1 (March 1994): 21–55. http://dx.doi.org/10.1017/s0269888900006561.

Full text

Abstract:

AbstractThe inheritance problem can be simply stated: for any instantiation of an inheritance network, say a specific hierarchy Γ, find a conclusion set for Γ. In other words, find out what is logically entailed by Γ. This can be done in two ways: either by defining a deductive or proof theoretic definition to determine what paths are entailed by a network; or by translating the individual links in the network to a more general nonmonotonic logic and using its model and proof theory to generate entailments that correspond to what one would expect from “viewing” the inheritance hierarchy. Two approaches to a solution to the inheritance problem structure this paper. The first is widely known as the “path-based” or “proof theoretic”, and the second, the “Model-based” or “model theoretic”. The two approaches result in both a different interpretation of default links as well as a variation in the entailment strategy for a solution to teh inheritance problem. In either case, the entailments produced need some intuitive interpretation, which can be either credulous or skeptical. The semantics of both skeptical and credulous inheritance reasoners are examined.

APA, Harvard, Vancouver, ISO, and other styles

37

Coquand, Thierry. "A semantics of evidence for classical arithmetic." Journal of Symbolic Logic 60, no. 1 (March 1995): 325–37. http://dx.doi.org/10.2307/2275524.

Full text

Abstract:

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.

APA, Harvard, Vancouver, ISO, and other styles

38

Ambler, Simon. "A categorical approach to the semantics of argumentation." Mathematical Structures in Computer Science 6, no. 2 (April 1996): 167–88. http://dx.doi.org/10.1017/s0960129500000931.

Full text

Abstract:

Argumentation is a proof theoretic paradigm for reasoning under uncertainty. Whereas a ‘proof’ establishes its conclusion outright, an ‘argument’ can only lend a measure of support. Thus, the process of argumentation consists of identifying all the arguments for a particular hypothesis φ, and then calculating the support for φ from the weight attached to these individual arguments. Argumentation has been incorporated as the inference mechanism of a large scale medical expert system, the ‘Oxford System of Medicine’ (OSM), and it is therefore important to demonstrate that the approach is theoretically justified. This paper provides a formal semantics for the notion of argument embodied in the OSM. We present a categorical account in which arguments are the arrows of a semilattice enriched category. The axioms of a cartesian closed category are modified to give the notion of an ‘evidential closed category’, and we show that this provides the correct enriched setting in which to model the connectives of conjunction (&) and implication (⇒).Finally, we develop a theory of ‘confidence measures’ over such categories, and relate this to the Dempster-Shafer theory of evidence.

APA, Harvard, Vancouver, ISO, and other styles

39

OLKHOVIKOV, GRIGORY K., and PETER SCHROEDER-HEISTER. "ON FLATTENING ELIMINATION RULES." Review of Symbolic Logic 7, no. 1 (January 23, 2014): 60–72. http://dx.doi.org/10.1017/s1755020313000385.

Full text

Abstract:

AbstractIn proof-theoretic semantics of intuitionistic logic it is well known that elimination rules can be generated from introduction rules in a uniform way. If introduction rules discharge assumptions, the corresponding elimination rule is a rule of higher level, which allows one to discharge rules occurring as assumptions. In some cases, these uniformly generated elimination rules can be equivalently replaced with elimination rules that only discharge formulas or do not discharge any assumption at all—they can be flattened in a terminology proposed by Read. We show by an example from propositional logic that not all introduction rules have flat elimination rules. We translate the general form of flat elimination rules into a formula of second-order propositional logic and demonstrate that our example is not equivalent to any such formula. The proof uses elementary techniques from propositional logic and Kripke semantics.

APA, Harvard, Vancouver, ISO, and other styles

40

MAREK, V. W., and J. B. REMMEL. "Guarded resolution for Answer Set Programming." Theory and Practice of Logic Programming 11, no. 1 (March 24, 2010): 111–23. http://dx.doi.org/10.1017/s1471068410000062.

Full text

Abstract:

AbstractWe investigate a proof system based on a guarded resolution rule and show its adequacy for the stable semantics of normal logic programs. As a consequence, we show that Gelfond–Lifschitz operator can be viewed as a proof-theoretic concept. As an application, we find a propositional theory EP whose models are precisely stable models of programs. We also find a class of propositional theories 𝓒P with the following properties. Propositional models of theories in 𝓒P are precisely stable models of P, and the theories in 𝓒T are of the size linear in the size of P.

APA, Harvard, Vancouver, ISO, and other styles

41

Zhang, Yizhou, and Nada Amin. "Reasoning about “reasoning about reasoning”: semantics and contextual equivalence for probabilistic programs with nested queries and recursion." Proceedings of the ACM on Programming Languages 6, POPL (January 16, 2022): 1–28. http://dx.doi.org/10.1145/3498677.

Full text

Abstract:

Metareasoning can be achieved in probabilistic programming languages (PPLs) using agent models that recursively nest inference queries inside inference queries. However, the semantics of this powerful, reflection-like language feature has defied an operational treatment, much less reasoning principles for contextual equivalence. We give formal semantics to a core PPL with continuous distributions, scoring, general recursion, and nested queries. Unlike prior work, the presence of nested queries and general recursion makes it impossible to stratify the definition of a sampling-based operational semantics and that of a measure-theoretic semantics—the two semantics must be defined mutually recursively. A key yet challenging property we establish is that probabilistic programs have well-defined meanings: limits exist for the step-indexed measures they induce. Beyond a semantics, we offer relational reasoning principles for probabilistic programs making nested queries. We construct a step-indexed, biorthogonal logical-relations model. A soundness theorem establishes that logical relatedness implies contextual equivalence. We demonstrate the usefulness of the reasoning principles by proving novel equivalences of practical relevance—in particular, game-playing and decisionmaking agents. We mechanize our technical developments leading to the soundness proof using the Coq proof assistant. Nested queries are an important yet theoretically underdeveloped linguistic feature in PPLs; we are first to give them semantics in the presence of general recursion and to provide them with sound reasoning principles for contextual equivalence.

APA, Harvard, Vancouver, ISO, and other styles

42

Sambin, Giovanni. "Pretopologies and completeness proofs." Journal of Symbolic Logic 60, no. 3 (September 1995): 861–78. http://dx.doi.org/10.2307/2275761.

Full text

Abstract:

Pretopologies were introduced in [S], and there shown to give a complete semantics for a propositional sequent calculus BL, here called basic linear logic, as well as for its extensions by structural rules, ex falso quodlibet or double negation. Immediately after Logic Colloquium '88, a conversation with Per Martin-Löf helped me to see how the pretopology semantics should be extended to predicate logic; the result now is a simple and fully constructive completeness proof for first order BL and virtually all its extensions, including the usual, or structured, intuitionistic and classical logic. Such a proof clearly illustrates the fact that stronger set-theoretic principles and classical metalogic are necessary only when completeness is sought with respect to a special class of models, such as the usual two-valued models.To make the paper self-contained, I briefly review in §1 the definition of pretopologies; §2 deals with syntax and §3 with semantics. The completeness proof in §4, though similar in structure, is sensibly simpler than that in [S], and this is why it is given in detail. In §5 it is shown how little is needed to obtain completeness for extensions of BL in the same language. Finally, in §6 connections with proofs with respect to more traditional semantics are briefly investigated, and some open problems are put forward.

APA, Harvard, Vancouver, ISO, and other styles

43

Peregrin, Jaroslav. "What Logics Mean: From Proof Theory to Model-Theoretic Semantics, by James W. Garson." Australasian Journal of Philosophy 93, no. 3 (January 19, 2015): 613–16. http://dx.doi.org/10.1080/00048402.2014.995682.

Full text

APA, Harvard, Vancouver, ISO, and other styles

44

Avigad, Jeremy. "Forcing in Proof Theory." Bulletin of Symbolic Logic 10, no. 3 (September 2004): 305–33. http://dx.doi.org/10.2178/bsl/1102022660.

Full text

Abstract:

AbstractPaul Cohen's method of forcing, together with Saul Kripke's related semantics for modal and intuitionistic logic, has had profound effects on a number of branches of mathematical logic, from set theory and model theory to constructive and categorical logic. Here, I argue that forcing also has a place in traditional Hilbert-style proof theory, where the goal is to formalize portions of ordinary mathematics in restricted axiomatic theories, and study those theories in constructive or syntactic terms. I will discuss the aspects of forcing that are useful in this respect, and some sample applications. The latter include ways of obtaining conservation results for classical and intuitionistic theories, interpreting classical theories in constructive ones, and constructivizing model-theoretic arguments.

APA, Harvard, Vancouver, ISO, and other styles

45

LANZET, RAN. "A THREE-VALUED QUANTIFIED ARGUMENT CALCULUS: DOMAIN-FREE MODEL-THEORY, COMPLETENESS, AND EMBEDDING OF FOL." Review of Symbolic Logic 10, no. 3 (May 8, 2017): 549–82. http://dx.doi.org/10.1017/s1755020317000053.

Full text

Abstract:

AbstractThis paper presents an extended version of the Quantified Argument Calculus (Quarc). Quarc is a logic comparable to the first-order predicate calculus. It employs several nonstandard syntactic and semantic devices, which bring it closer to natural language in several respects. Most notably, quantifiers in this logic are attached to one-place predicates; the resulting quantified constructions are then allowed to occupy the argument places of predicates. The version presented here is capable of straightforwardly translating natural-language sentences involving defining clauses. A three-valued, model-theoretic semantics for Quarc is presented. Interpretations in this semantics are not equipped with domains of quantification: they are just interpretation functions. This reflects the analysis of natural-language quantification on which Quarc is based. A proof system is presented, and a completeness result is obtained. The logic presented here is capable of straightforward translation of the classical first-order predicate calculus, the translation preserving truth values as well as entailment. The first-order predicate calculus and its devices of quantification can be seen as resulting from Quarc on certain semantic and syntactic restrictions, akin to simplifying assumptions. An analogous, straightforward translation of Quarc into the first-order predicate calculus is impossible.

APA, Harvard, Vancouver, ISO, and other styles

46

Francez, Nissim. "On a Distinction of Two Facets of Meaning and its Role in Proof-theoretic Semantics." Logica Universalis 9, no. 1 (March 2015): 121–27. http://dx.doi.org/10.1007/s11787-015-0118-8.

Full text

APA, Harvard, Vancouver, ISO, and other styles

47

DELZANNO, G., D. GALMICHE, and M. MARTELLI. "A specification logic for concurrent object-oriented programming." Mathematical Structures in Computer Science 9, no. 3 (June 1999): 253–86. http://dx.doi.org/10.1017/s0960129599002789.

Full text

Abstract:

This paper focuses on the use of linear logic as a specification language for the operational semantics of advanced concepts of programming such as concurrency and object-orientation. Our approach is based on a refinement of linear logic sequent calculi based on the proof-theoretic characterization of logic programming. A well-founded combination of higher-order logic programming and linear logic will be used to give an accurate encoding of the traditional features of concurrent object-oriented programming languages, whose corner-stone is the notion of encapsulation.

APA, Harvard, Vancouver, ISO, and other styles

48

STÄRK, ROBERT F. "CUT-PROPERTY AND NEGATION AS FAILURE." International Journal of Foundations of Computer Science 05, no. 02 (June 1994): 129–64. http://dx.doi.org/10.1142/s0129054194000086.

Full text

Abstract:

What is the semantics of Negation-as-Failure in logic programming? We try to answer this question by proof-theoretic methods. A rule based sequent calculus is used in which a sequent is provable if, and only if, it is true in all three-valued models of the completion of a logic program. The main theorem is that proofs in the sequent calculus can be transformed into SLDNF-computations if, and only if, a program has the cut-property. A fragment of the sequent calculus leads to a sound and complete semantics for SLDNF-resolution with substitutions. It turns out that this version of SLDNF-resolution is sound and complete with respect to three-valued possible world models of the completion for arbitrary logic programs and arbitrary goals. Since we are dealing with possibly nonterminating computations and constructive proofs, three-valued possible world models seem to be an appropriate semantics.

APA, Harvard, Vancouver, ISO, and other styles

49

RUMBERG, ANTJE. "BOLZANO’S CONCEPT OF GROUNDING (ABFOLGE) AGAINST THE BACKGROUND OF NORMAL PROOFS." Review of Symbolic Logic 6, no. 3 (July 3, 2013): 424–59. http://dx.doi.org/10.1017/s1755020313000154.

Full text

Abstract:

AbstractIn this paper, I provide a thorough discussion and reconstruction of Bernard Bolzano’s theory of grounding and a detailed investigation into the parallels between his concept of grounding and current notions of normal proofs. Grounding (Abfolge) is an objective ground-consequence relation among true propositions that is explanatory in nature. The grounding relation plays a crucial role in Bolzano’s proof-theory, and it is essential for his views on the ideal buildup of scientific theories. Occasionally, similarities have been pointed out between Bolzano’s ideas on grounding and cut-free proofs in Gentzen’s sequent calculus. My thesis is, however, that they bear an even stronger resemblance to the normal natural deduction proofs employed in proof-theoretic semantics in the tradition of Dummett and Prawitz.

APA, Harvard, Vancouver, ISO, and other styles

50

Valliappan, Nachiappan, Fabian Ruch, and Carlos Tomé Cortiñas. "Normalization for fitch-style modal calculi." Proceedings of the ACM on Programming Languages 6, ICFP (August 29, 2022): 772–98. http://dx.doi.org/10.1145/3547649.

Full text

Abstract:

Fitch-style modal lambda calculi enable programming with necessity modalities in a typed lambda calculus by extending the typing context with a delimiting operator that is denoted by a lock. The addition of locks simplifies the formulation of typing rules for calculi that incorporate different modal axioms, but each variant demands different, tedious and seemingly ad hoc syntactic lemmas to prove normalization. In this work, we take a semantic approach to normalization, called normalization by evaluation (NbE), by leveraging the possible-world semantics of Fitch-style calculi to yield a more modular approach to normalization. We show that NbE models can be constructed for calculi that incorporate the K, T and 4 axioms of modal logic, as suitable instantiations of the possible-world semantics. In addition to existing results that handle 𝛽-equivalence, our normalization result also considers 𝜂-equivalence for these calculi. Our key results have been mechanized in the proof assistant Agda. Finally, we showcase several consequences of normalization for proving meta-theoretic properties of Fitch-style calculi as well as programming-language applications based on different interpretations of the necessity modality.

APA, Harvard, Vancouver, ISO, and other styles

Journal articles on the topic 'Proof-theoretic semantics'

Create a spot-on reference in APA, MLA, Chicago, Harvard, and other styles