The work of Kurt Gödel

1976 ◽  
Vol 41 (4) ◽  
pp. 761-778 ◽  
Author(s):  
Stephen C. Kleene
Keyword(s):  
Functional Calculus ◽  
Completeness Theorem ◽  
Predicate Calculus ◽  
Closed Formula ◽  
Modern Logic ◽  
Von Neumann ◽  
First Order ◽  
Kurt Gödel ◽  
Gödel’S Completeness Theorem ◽  
Order Predicate Calculus

I first heard the name of Kurt Gödel when, as a graduate student at Princeton in the fall of 1931, I attended a colloquium at which John von Neumann was the speaker, von Neumann could have spoken on work of his own; but instead he gave an exposition of Gödel's results of formally undecidable propositions [1931].Today I shall begin with Gödel's paper [1930] on The completeness of the axioms of the functional calculus of logic, or of what we now often call “the first-order predicate calculus”, using “predicate” as synonymous with “propositional function”.Alonzo Church wrote ([1944, p. 62] and [1956, pp. 288–289]), “the first explicit formulation of the functional calculus of first order as an independent logistic system is perhaps in the first edition of Hilbert and Ackermann's Grundzüge der theoretischen Logik (1928).” Clearly, this formalism is not complete in the sense that each closed formula or its negation is provable. (A closed formula, or sentence, is a formula without free occurrences of variables.) But Hilbert and Ackermann observe, “Whether the system of axioms is complete at least in the sense that all the logical formulas which are correct for each domain of individuals can actually be derived from them is still an unsolved question.” [1928, p. 68].This question Gödel answered in the affirmative in his Ph.D. thesis (Vienna, 1930), of which the paper under discussion is a rewritten version.I shall not describe Gödel's proof. Perhaps no theorem in modern logic has been proved more often than Gödel's completeness theorem for the first-order predicate calculus. It stands at the focus of a complex of fundamental theorems, which different scholars have approached from various directions (e.g. Kleene [1967, Chapter VI]).

The Discovery of My Completeness Proofs

1996 ◽  
Vol 2 (2) ◽  
pp. 127-158 ◽  
Author(s):  
Leon Henkin
Keyword(s):  
Model Theory ◽  
Scientific Work ◽  
Completeness Theorem ◽  
Large Classes ◽  
Mathematical Structures ◽  
First Order ◽  
Kurt Gödel ◽  
Gödel’S Completeness Theorem ◽  
The Right ◽  
Mathematical Discovery

§1. Introduction. This paper deals with aspects of my doctoral dissertation which contributed to the early development of model theory. What was of use to later workers was less the results of my thesis, than the method by which I proved the completeness of first-order logic—a result established by Kurt Gödel in his doctoral thesis 18 years before.The ideas that fed my discovery of this proof were mostly those I found in the teachings and writings of Alonzo Church. This may seem curious, as his work in logic, and his teaching, gave great emphasis to the constructive character of mathematical logic, while the model theory to which I contributed is filled with theorems about very large classes of mathematical structures, whose proofs often by-pass constructive methods.Another curious thing about my discovery of a new proof of Gödel's completeness theorem, is that it arrived in the midst of my efforts to prove an entirely different result. Such “accidental” discoveries arise in many parts of scientific work. Perhaps there are regularities in the conditions under which such “accidents” occur which would interest some historians, so I shall try to describe in some detail the accident which befell me.A mathematical discovery is an idea, or a complex of ideas, which have been found and set forth under certain circumstances. The process of discovery consists in selecting certain input ideas and somehow combining and transforming them to produce the new output ideas. The process that produces a particular discovery may thus be represented by a diagram such as one sees in many parts of science; a “black box” with lines coming in from the left to represent the input ideas, and lines going out to the right representing the output. To describe that discovery one must explain what occurs inside the box, i.e., how the outputs were obtained from the inputs.

Two interpolation theorems for a predicate calculus

1971 ◽  
Vol 36 (2) ◽  
pp. 262-270
Author(s):  
Shoji Maehara ◽  
Gaisi Takeuti
Keyword(s):  
Normal Form ◽  
Completeness Theorem ◽  
Interpolation Theorem ◽  
Second Order ◽  
Predicate Calculus ◽  
Cut Elimination ◽  
First Order ◽  
Image Position ◽  
Order Predicate Calculus

A second order formula is called Π1 if, in its prenex normal form, all second order quantifiers are universal. A sequent F1, … Fm → G1 …, Gn is called Π1 if a formulais Π1If we consider only Π1 sequents, then we can easily generalize the completeness theorem for the cut-free first order predicate calculus to a cut-free Π1 predicate calculus.In this paper, we shall prove two interpolation theorems on the Π1 sequent, and show that Chang's theorem in [2] is a corollary of our theorem. This further supports our belief that any form of the interpolation theorem is a corollary of a cut-elimination theorem. We shall also show how to generalize our results for an infinitary language. Our method is proof-theoretic and an extension of a method introduced in Maehara [5]. The latter has been used frequently to prove the several forms of the interpolation theorem.

Outline of an Introduction to Mathematical Logic IV

1959 ◽  
Vol 2 (1) ◽  
pp. 33-42
Author(s):  
Abraham Robinson
Keyword(s):  
Mathematical Logic ◽  
Completeness Theorem ◽  
Semantic Theory ◽  
Predicate Calculus ◽  
First Order ◽  
Deductive Theory ◽  
Order Predicate Calculus

The extended completeness theorem of the predicate calculas of the first order. In section 12, we developed a deductive theory of the first order predicate calculus, while in section II we dealt with the semantic theory of that calculus. We now have to consider the connection between these two theories. We recall that a sentence X can be satisfied by a structure M only if X is defined in M. Given a sentence X (a set of sentences K) we shall say that the structure M is a model of X (of K) if X is (all the sentences of K are) satisfied by M.

A reduction class containing formulas with one monadic predicate and one binary function symbol

1976 ◽  
Vol 41 (1) ◽  
pp. 45-49
Author(s):  
Charles E. Hughes
Keyword(s):  
Normal Form ◽  
Predicate Symbol ◽  
Conjunctive Normal Form ◽  
Function Symbol ◽  
Predicate Calculus ◽  
Binary Function ◽  
First Order ◽  
The Matrix ◽  
Reduction Class ◽  
Order Predicate Calculus

AbstractA new reduction class is presented for the satisfiability problem for well-formed formulas of the first-order predicate calculus. The members of this class are closed prenex formulas of the form ∀x∀yC. The matrix C is in conjunctive normal form and has no disjuncts with more than three literals, in fact all but one conjunct is unary. Furthermore C contains but one predicate symbol, that being unary, and one function symbol which symbol is binary.

On the strong semantical completeness of the intuitionistic predicate calculus

1968 ◽  
Vol 33 (1) ◽  
pp. 1-7 ◽  
Author(s):  
Richmond H. Thomason
Keyword(s):  
Model Theory ◽  
Completeness Theorem ◽  
Predicate Calculus ◽  
First Order ◽  
Semantic Tableaux ◽  
Weak Completeness ◽  
Skolem Theorem ◽  
Completeness Theorems

In Kripke [8] the first-order intuitionjstic predicate calculus (without identity) is proved semantically complete with respect to a certain model theory, in the sense that every formula of this calculus is shown to be provable if and only if it is valid. Metatheorems of this sort are frequently called weak completeness theorems—the object of the present paper is to extend Kripke's result to obtain a strong completeness theorem for the intuitionistic predicate calculus of first order; i.e., we will show that a formula A of this calculus can be deduced from a set Γ of formulas if and only if Γ implies A. In notes 3 and 5, below, we will indicate how to account for identity, as well. Our proof of the completeness theorem employs techniques adapted from Henkin [6], and makes no use of semantic tableaux; this proof will also yield a Löwenheim-Skolem theorem for the modeling.

scholarly journals On a Propositional Calculus Whose Decision Problem is Recursively Unsolvable

1970 ◽  
Vol 38 ◽  
pp. 145-152
Author(s):  
Akira Nakamura
Keyword(s):  
Decision Problem ◽  
Propositional Calculus ◽  
Predicate Calculus ◽  
Reduction Theorem ◽  
List Type ◽  
First Order ◽  
Order Predicate Calculus

The purpose of this paper is to present a propositional calculus whose decision problem is recursively unsolvable. The paper is based on the following ideas: (1) Using Löwenheim-Skolem’s Theorem and Surányi’s Reduction Theorem, we will construct an infinitely many-valued propositional calculus corresponding to the first-order predicate calculus.(2) It is well known that the decision problem of the first-order predicate calculus is recursively unsolvable.(3) Thus it will be shown that the decision problem of the infinitely many-valued propositional calculus is recursively unsolvable.

Infinitary logic and admissible sets

1969 ◽  
Vol 34 (2) ◽  
pp. 226-252 ◽  
Author(s):  
Jon Barwise
Keyword(s):  
Second Order ◽  
Order Logic ◽  
Predicate Calculus ◽  
Generalized Quantifiers ◽  
Infinitary Logic ◽  
First Order ◽  
Admissible Sets ◽  
Classical Language ◽  
Second Order Logic ◽  
Order Predicate Calculus

In recent years much effort has gone into the study of languages which strengthen the classical first-order predicate calculus in various ways. This effort has been motivated by the desire to find a language which is(I) strong enough to express interesting properties not expressible by the classical language, but(II) still simple enough to yield interesting general results. Languages investigated include second-order logic, weak second-order logic, ω-logic, languages with generalized quantifiers, and infinitary logic.

Sign in / Sign up

Export Citation Format

Share Document