THE QUANTIFIED ARGUMENT CALCULUS

2014 ◽  
Vol 7 (1) ◽  
pp. 120-146 ◽  
Author(s):  
HANOCH BEN-YAMI
Keyword(s):  
Natural Language ◽  
Predicate Logic ◽  
Formal System ◽  
Proof System ◽  
Value Assignment ◽  
Truth Value ◽  
Necessary Existence ◽  
Modal Predicate Logic ◽  
Converse Relation ◽  
Main Ideas

AbstractI develop a formal logic in which quantified arguments occur in argument positions of predicates. This logic also incorporates negative predication, anaphora and converse relation terms, namely, additional syntactic features of natural language. In these and additional respects, it represents the logic of natural language more adequately than does any version of Frege’s Predicate Calculus. I first introduce the system’s main ideas and familiarize it by means of translations of natural language sentences. I then develop a formal system built on these principles, the Quantified Argument Calculus or Quarc. I provide a truth-value assignment semantics and a proof system for the Quarc. I next demonstrate the system’s power by a variety of proofs; I prove its soundness; and I comment on its completeness. I then extend the system to modal logic, again providing a proof system and a truth-value assignment semantics. I proceed to show how the Quarc versions of the Barcan formulas, of their converses and of necessary existence come out straightforwardly invalid, which I argue is an advantage of the modal Quarc over modal Predicate Logic as a system intended to capture the logic of natural language.

AN INTENSIONAL LEIBNIZ SEMANTICS FOR ARISTOTELIAN LOGIC

2010 ◽  
Vol 3 (2) ◽  
pp. 262-272 ◽  
Author(s):  
KLAUS GLASHOFF
Keyword(s):  
Natural Deduction ◽  
Predicate Logic ◽  
Formal System ◽  
Aristotelian Logic ◽  
Categorical Logic ◽  
Characteristic Numbers ◽  
Formal Syntax ◽  
Philosophical Standpoint ◽  
Classical Philosophy

Since Frege’s predicate logical transcription of Aristotelian categorical logic, the standard semantics of Aristotelian logic considers terms as standing for sets of individuals. From a philosophical standpoint, this extensional model poses problems: There exist serious doubts that Aristotle’s terms were meant to refer always to sets, that is, entities composed of individuals. Classical philosophy up to Leibniz and Kant had a different view on this question—they looked at terms as standing for concepts (“Begriffe”). In 1972, Corcoran presented a formal system for Aristotelian logic containing a calculus of natural deduction, while, with respect to semantics, he still made use of an extensional interpretation. In this paper we deal with a simple intensional semantics for Corcoran’s syntax—intensional in the sense that no individuals are needed for the construction of a complete Tarski model of Aristotelian syntax. Instead, we view concepts as containing or excluding other, “higher” concepts—corresponding to the idea which Leibniz used in the construction of his characteristic numbers. Thus, this paper is an addendum to Corcoran’s work, furnishing his formal syntax with an adequate semantics which is free from presuppositions which have entered into modern interpretations of Aristotle’s theory via predicate logic.

Soundness, Epistemology, and Frege’s Project

2020 ◽  
pp. 115-169
Author(s):  
Joan Weiner
Keyword(s):  
Natural Language ◽  
Formal System ◽  
Truth Predicate

Insofar as the use of natural language to introduce, discuss, and argue about features of a formal system is metatheoretic, there can be no doubt: Frege has a metatheory. But what kind of metatheory? Although the model theoretic semantics with which we are familiar today is a post-Fregean development, most believe that Frege offers a proto-soundness proof for his logic that intrinsically exploits a truth predicate and metalinguistic variables. In this chapter it is argued that he neither uses, nor has any need to use, a truth predicate or metalinguistic variables in justifications of his basic laws and rules. The purpose of the discussions that are typically understood as constituting Frege’s metatheory is, rather, elucidatory. And once we see what the aim of these particular elucidations is, we can explain Frege’s otherwise puzzling eschewal of the truth predicate in his discussions of the justification of the laws and rules of inference.

scholarly journals Program extraction applied to monadic parsing

2019 ◽  
Vol 29 (4) ◽  
pp. 487-518 ◽  
Author(s):  
Ulrich Berger ◽  
Alison Jones ◽  
Monika Seisenberger
Keyword(s):  
Natural Language ◽  
Case Studies ◽  
Proof System ◽  
Theoretic Approach ◽  
Formal Proofs ◽  
Interactive Proof ◽  
Program Extraction ◽  
Interactive Proof System

Abstract This article outlines a proof-theoretic approach to developing correct and terminating monadic parsers. Using modified realizability, we extract formally verified and terminating programs from formal proofs. By extracting both primitive parsers and parser combinators, it is ensured that all complex parsers built from these are also correct, complete and terminating for any input. We demonstrate the viability of our approach by means of two case studies: we extract (i) a small arithmetic calculator and (ii) a non-deterministic natural language parser. The work is being carried out in the interactive proof system Minlog.

A Semantic Map for Indoor Robot Navigation Based on Predicate Logic

2020 ◽  
Vol 11 (1) ◽  
pp. 1-21
Author(s):  
Hengsheng Wang ◽  
Jin Ren
Keyword(s):  
Natural Language ◽  
Indoor Environment ◽  
Robot Navigation ◽  
Predicate Logic ◽  
Constraint Satisfaction Problem ◽  
Real Data ◽  
Main Concern ◽  
Building Structure ◽  
Topological Map ◽  
Semantic Map

Interacting with mobile robots through natural language is the main concern of this article, which focuses on the semantic meaning of concepts used in natural language instructions to navigate robots indoors. Assuming the building structure is the prior knowledge of the robot and the robot has the ability of navigating itself locally to avoid collision with the environment, the building structure is represented with predicate logic on SWI-Prolog as the database of the indoor environment, which is called semantic map in this paper, in which the basic predicate clauses are based on two kinds of entities, namely ‘area' and ‘node.' The area names (in natural language convention) of indoor environment are organized with an ontology and are defined in the semantic map which includes the geometric information of areas and connection relationships between areas. With the semantic map database, functions for robot navigation, like a topological map, path planning, and self-localization, are realized through reasoning by properly designed predicates based on constraint satisfaction problem (CSP). An example building is given to show the idea proposed in this article, the real data of which was used to establish the semantic map, and the predicates for navigation functions worked well on SWI-Prolog.

A Probabilistic Propositional Logic System is an Event Semantics for Classical Formal System of Propositional Calculus

2013 ◽  
Vol 427-429 ◽  
pp. 1917-1923
Author(s):  
Hong Lan Liu ◽  
De Zheng Zhang
Keyword(s):  
Formal System ◽  
Propositional Calculus ◽  
Semantic Interpretation ◽  
Probabilistic Logic ◽  
Value Functions ◽  
Event Semantics ◽  
Set Inclusion ◽  
Set Operations ◽  
Truth Value ◽  
Logic System

The well formed formulas (wffs) in classical formal system of propositional calculus (CPC) are only some formal symbols, whose meanings are given by an interpretation. A probabilistic logic system, based on a probabilistic space, is an event semantics for CPC, in which set operations are the semantic interpretations for connectives, event functions are the semantic interpretations for wffs, the event (set) inclusion is the semantic interpretation for tautological implication, and the event equality = is the semantic interpretation for tautological equivalence. CPC is applicable to probabilistic propositions completely. Event calculus instead of truth value (probability) calculus can be performed in CPC because there arent truth value functions (operators) to interpret all connectives correctly.

The complexity of the modal predicate logic of “true in every transitive model of ZF”

1997 ◽  
Vol 62 (4) ◽  
pp. 1371-1378
Author(s):  
Vann McGee
Keyword(s):  
Lower Bound ◽  
Set Theory ◽  
Predicate Logic ◽  
Alternative Conception ◽  
Predicate Calculus ◽  
Modal Formula ◽  
Sentential Calculus ◽  
Transitive Model ◽  
Modal Predicate Logic

Robert Solovay [8] investigated the version of the modal sentential calculus one gets by taking “□ϕ” to mean “ϕ is true in every transitive model of Zermelo-Fraenkel set theory (ZF).” Defining an interpretation to be a function * taking formulas of the modal sentential calculus to sentences of the language of set theory that commutes with the Boolean connectives and sets (□ϕ)* equal to the statement that ϕ* is true in every transitive model of ZF, and stipulating that a modal formula ϕ is valid if and only if, for every interpretation *, ϕ* is true in every transitive model of ZF, Solovay obtained a complete and decidable set of axioms.In this paper, we stifle the hope that we might continue Solovay's program by getting an analogous set of axioms for the modal predicate calculus. The set of valid formulas of the modal predicate calculus is not axiomatizable; indeed, it is complete .We also look at a variant notion of validity according to which a formula ϕ counts as valid if and only if, for every interpretation *, ϕ* is true. For this alternative conception of validity, we shall obtain a lower bound of complexity: every set which is in the set of sentences of the language of set theory true in the constructible universe will be 1-reducible to the set of valid modal formulas.

Sign in / Sign up

Export Citation Format

Share Document