A proof procedure for quantification theory

1955 ◽  
Vol 20 (2) ◽  
pp. 141-149 ◽  
Author(s):  
W. V. Quine
Keyword(s):  
Simple Proof ◽  
Quantification Theory ◽  
B Method ◽  
Proof Procedure ◽  
Soundness And Completeness ◽  
Empty Universe

The purpose of this paper is to present and justify a simple proof procedure for quantification theory. The procedure will take the form of a method for proving a quantificational schema to be inconsistent, i.e., satisfiable in no non-empty universe. But it serves equally for proving validity, since we can show a schema valid by showing its negation inconsistent.Method A, as I shall call it, will appear first, followed by a more practical adaptation which I shall call B. The soundness and completeness of A will be established, and the equivalence of A and B. Method A, as will appear, is not new.The reader need be conversant with little more than the fairly conventional use (as in [8]) of such terms as ‘quantificational schema’, ‘interpretation’, ‘valid’, ‘consistent’, ‘prenex’, and my notation (as in [7]) of quasi-quotation.

A tableau system of proof for predicate-functor logic with identity

1983 ◽  
Vol 48 (4) ◽  
pp. 1140-1144
Author(s):  
Teo Grünberg
Keyword(s):  
Predicate Logic ◽  
Inference Rules ◽  
Complete Proof ◽  
Quantification Theory ◽  
First Order ◽  
Proof Procedure ◽  
Tableau System ◽  
First Order Predicate Logic

Quine has given a method for eliminating the bound variables in first-order predicate logic establishing thus a variable-free formulation called predicate-functor logic. The purpose of this paper is to give an autonomous and complete proof procedure for Quine's predicate-functor logic with identity, without presupposing axioms or inference rules for quantification theory or, for that matter, any other logic.

Modern Quantification Theory

2021 ◽  
Author(s):  
Shizuhiko Nishisato ◽  
Eric J. Beh ◽  
Rosaria Lombardo ◽  
Jose G. Clavel
Keyword(s):  
Quantification Theory

scholarly journals Kripke Semantics for Intersection Formulas

2021 ◽  
Vol 22 (3) ◽  
pp. 1-16
Author(s):  
Andrej Dudenhefner ◽  
Paweł Urzyczyn
Keyword(s):  
Kripke Semantics ◽  
Type Assignment ◽  
Soundness And Completeness

We propose a notion of the Kripke-style model for intersection logic. Using a game interpretation, we prove soundness and completeness of the proposed semantics. In other words, a formula is provable (a type is inhabited) if and only if it is forced in every model. As a by-product, we obtain another proof of normalization for the Barendregt–Coppo–Dezani intersection type assignment system.

An Automata-Theoretic Decision Procedure for Propositional Temporal Logic with Since and Until1

1992 ◽  
Vol 17 (3) ◽  
pp. 271-282
Author(s):  
Y.S. Ramakrishna ◽  
L.E. Moser ◽  
L.K. Dillon ◽  
P.M. Melliar-Smith ◽  
G. Kutty
Keyword(s):  
Temporal Logic ◽  
Decision Procedure ◽  
Linear Time ◽  
Computer Systems ◽  
Hierarchical Abstraction ◽  
Soundness And Completeness

We present an automata-theoretic decision procedure for Since/Until Temporal Logic (SUTL), a linear-time propositional temporal logic with strong non-strict since and until operators. The logic, which is intended for specifying and reasoning about computer systems, employs neither next nor previous operators. Such operators obstruct the use of hierarchical abstraction and refinement and make reasoning about concurrency difficult. A proof of the soundness and completeness of the decision procedure is given, and its complexity is analyzed.

scholarly journals Deduction in Non-Fregean Propositional Logic SCI

Axioms ◽  
2019 ◽  
Vol 8 (4) ◽  
pp. 115 ◽  
Author(s):  
Joanna Golińska-Pilarek ◽  
Magdalena Welle
Keyword(s):  
Propositional Logic ◽  
Sequent Calculus ◽  
Classical Propositional Logic ◽  
Tableau System ◽  
Soundness And Completeness

We study deduction systems for the weakest, extensional and two-valued non-Fregean propositional logic SCI . The language of SCI is obtained by expanding the language of classical propositional logic with a new binary connective ≡ that expresses the identity of two statements; that is, it connects two statements and forms a new one, which is true whenever the semantic correlates of the arguments are the same. On the formal side, SCI is an extension of classical propositional logic with axioms characterizing the identity connective, postulating that identity must be an equivalence and obey an extensionality principle. First, we present and discuss two types of systems for SCI known from the literature, namely sequent calculus and a dual tableau-like system. Then, we present a new dual tableau system for SCI and prove its soundness and completeness. Finally, we discuss and compare the systems presented in the paper.

scholarly journals On Polymorphic Sessions and Functions

2021 ◽  
Vol 43 (2) ◽  
pp. 1-55
Author(s):  
Bernardo Toninho ◽  
Nobuko Yoshida
Keyword(s):  
Natural Deduction ◽  
Sequent Calculus ◽  
Linear Logic ◽  
Linear Formulation ◽  
Session Types ◽  
Logical Foundation ◽  
Π Calculus ◽  
Soundness And Completeness ◽  
System F ◽  
Algebraic Representations

This work exploits the logical foundation of session types to determine what kind of type discipline for the Λ-calculus can exactly capture, and is captured by, Λ-calculus behaviours. Leveraging the proof theoretic content of the soundness and completeness of sequent calculus and natural deduction presentations of linear logic, we develop the first mutually inverse and fully abstract processes-as-functions and functions-as-processes encodings between a polymorphic session π-calculus and a linear formulation of System F. We are then able to derive results of the session calculus from the theory of the Λ-calculus: (1) we obtain a characterisation of inductive and coinductive session types via their algebraic representations in System F; and (2) we extend our results to account for value and process passing, entailing strong normalisation.

scholarly journals Study on the Attractiveness Factors of Online Courses

2019 ◽  
Vol 9 (2) ◽  
pp. 128 ◽  
Author(s):  
Jia-Xuan Han ◽  
Min-Yuan Ma
Keyword(s):  
Online Teaching ◽  
Online Courses ◽  
Rapid Development ◽  
Grid Method ◽  
Type I ◽  
Digital Learning ◽  
Key Factors ◽  
Quantification Theory ◽  
Global Trend ◽  
Education Industry

With the rapid development of online courses, digital learning has become a global trend. In this context, this study analyzed the high intake population of online courses for online affective cognition, and explored what the user’s attraction factors for online courses are. The key factors that affect consumers’ usage of online courses and the weights of impact relations are presented, aiming to provide guidance for future improvement of online courses. This study was conducted through the evaluation grid method of Miryoku engineering. In order to make the charm factors more accurate and representative, this study summarized the charm elements using the Kawakita Jiro (KJ) method, and then quantified the factors in the form of a questionnaire. Through the statistical analysis of the questionnaire and quantification theory type I, the correlation between the charm feeling and the online course as well as the weight of each item (original evaluation item) and category (specific evaluation item) were calculated. Through the research and discussion on the charm factors of online teaching, the results analyzed and integrated in this paper could give more substantive suggestions and help to the education industry.

scholarly journals A simple proof of Andrews’s 5 F 4 evaluation

2013 ◽  
Vol 36 (1-2) ◽  
pp. 165-170 ◽  
Author(s):  
Ira M. Gessel
Keyword(s):  
Simple Proof

A simple proof of existence of weak and statistical solutions of Navier–Stokes equations

1992 ◽  
Vol 436 (1896) ◽  
pp. 1-11 ◽  
Keyword(s):  
Weak Solution ◽  
Initial Data ◽  
Natural Number ◽  
Simple Proof ◽  
Stokes Equations ◽  
Galerkin Approximation ◽  
Navier Stokes ◽  
Navier Stokes Equations ◽  
Existence Proofs ◽  
Statistical Solutions

The Galerkin approximation to the Navier–Stokes equations in dimension N , where N is an infinite non-standard natural number, is shown to have standard part that is a weak solution. This construction is uniform with respect to non-standard representation of the initial data, and provides easy existence proofs for statistical solutions.

Sign in / Sign up

Export Citation Format

Share Document