Browse Prior Art Database

Making Infinite Structures Appear Finite in First Order Logic

IP.com Disclosure Number: IPCOM000128706D
Original Publication Date: 1976-Dec-31
Included in the Prior Art Database: 2005-Sep-16
Document File: 28 page(s) / 49K

Publishing Venue

Software Patent Institute

Related People

Richard E. Ladner: AUTHOR [+3]

Abstract

This paper is mostly definitional in nature. The recent work of Ferrante [3 1, Rackoff [7 Tenney [8 ], and Ladner [5 ], and the earlier work of Ehrenfeucht [2 ] and Lauchli (6 has demonstrated the usefulness of model theoretic games in showing the efficient decidability of certain first order logical theories. We attempt to unify this method under a single notation and concept. To do so we extend the notions of first order structure, truth in such structures, and first order games played on such structures. The inspiration for this paper lies in the Ph.D. theses of Ferrante [ 3] and Rackoff [7 ]. Many of the results we mention can be found in some form in one thesis or the other. In Section 1 we give the basic definitions we use. In Section 2 we define first order games and relate games to the notion of truth. In Section 3 we use the model theoretic games to help analyze the computational complexity of several logical theories that were considered by Ferrante [3 1.

This text was extracted from a PDF file.
This is the abbreviated version, containing approximately 13% of the total text.

Page 1 of 28

THIS DOCUMENT IS AN APPROXIMATE REPRESENTATION OF THE ORIGINAL.

Making Infinite Structures Appear Finite in First Order Logic

Richard E. Ladner

Department of Computer Science University of Washington Seattle, Washington 98195 U. S. A. (Telephone: 206-543--9347)

76-10-09

Research supported by NSF Grant No. GJ-43264. This paper is mostly definitional in nature. The recent work of Ferrante [3 1, Rackoff [7 Tenney [8 ], and Ladner [5 ], and the earlier work of Ehrenfeucht [2 ] and Lauchli (6 has demonstrated the usefulness of model theoretic games in showing the efficient decidability of certain first order logical theories. We attempt to unify this method under a single notation and concept. To do so we extend the notions of first order structure, truth in such structures, and first order games played on such structures.

The inspiration for this paper lies in the Ph.D. theses of Ferrante [ 3] and Rackoff [7 ]. Many of the results we mention can be found in some form in one thesis or the other.

In Section 1 we give the basic definitions we use. In Section 2 we define first order games and relate games to the notion of truth. In Section 3 we use the model theoretic games to help analyze the computational complexity of several logical theories that were considered by Ferrante [3 1.

1. Preliminaries

The first order logical symbols are

(Equation Omitted)

A first order language, L, is a finite set of relation symbols and function symbols. If R is a relation symbol then r(R) -~ 1 denotes its rank (unary, binary, ternary, ...);likewise if f is a function symbol then r(f) ~! 0 denotes its rank.

Function symbols of rank 0 are called constant symbols.

As a matter of notation we define a[i:j] to be the sequence

(Equation Omitted)

where

(Equation Omitted)

. All the notions we will define are relative to an arbitrary language L and as such will have a prefix "L-" attached. This prefix is dropped when no confusion should arise.

We define L-terms inductively along with their depth and length.

University of Washington Page 1 Dec 31, 1976

Page 2 of 28

Making Infinite Structures Appear Finite in First Order Logic

(tl) for all

(Equation Omitted)

is a term of depth 0 and length

(Equation Omitted)

(the length of v I is the length of i written in binary notation) and if c is a constant symbol then c is a term of depth 0 and length 1.

(t2) if f is a function symbol of rank

(Equation Omitted)

in L, and Tfl:r(f)] are terms of depth d[l:r(f)] and length Z[l:r(f)) respectively then

(Equation Omitted)

is a term of depth max(d[l:r(f)])+ 1 and

r(f) length

(Equation Omitted)

We define L-formulas inductively along with their quantifier depth and length.

(fl) if T 1 and T 2 are L-terms of length k 1 and k 2 respectively, then

(Equation Omitted)

is a formula of quantifier depth 0 and length

(Equation Omitted)

(f2) if R is a relation symbol in L and T[l:r(R)l are L-terms of length

(Equation Omitted)

respectively, then

(Equation Omitted)

is a

r(R) formula of quantifier...