W. V. Quine. A proof procedure for quantification theory. The journal of symbolic logic, vol. 20 (1955), pp. 141–149.

1966 ◽  
Vol 31 (4) ◽  
pp. 657-657
Author(s):  
Peter Andrews

1955 ◽  
Vol 20 (2) ◽  
pp. 141-149 ◽  
Author(s):  
W. V. Quine

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.



1983 ◽  
Vol 48 (4) ◽  
pp. 1140-1144
Author(s):  
Teo Grünberg

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.



1968 ◽  
Vol 32 (4) ◽  
pp. 480-504 ◽  
Author(s):  
J. Jay Zeman

The “traditional” method of presenting the subject-matter of symbolic logic involves setting down, first of all, a basis for a propositional calculus—which basis might be a system of natural deduction, an axiom system, or a rule concerning tautologous formulas. The next step, ordinarily, consists of the introduction of quantifiers into the symbol-set of the system, and the stating of axioms or rules for quantification. In this paper I shall propose a system somewhat different from the ordinary; this system has rules for quantification and is, indeed, equivalent to classical quantification theory. It departs from the usual, however, in that it has no primitive quantifiers.



2004 ◽  
Vol 10 (3) ◽  
pp. 438-446
Author(s):  
Michael Kremer


2008 ◽  
Vol 14 (4) ◽  
pp. 553-558
Keyword(s):  




2008 ◽  
Vol 14 (3) ◽  
pp. 418-437
Author(s):  
Chris Laskowski


2009 ◽  
Vol 15 (2) ◽  
pp. 237-245
Author(s):  
Ali Enayat
Keyword(s):  


Sign in / Sign up

Export Citation Format

Share Document