Show description

23–38, 2000. c Springer-Verlag Berlin Heidelberg 2000 24 Melvin Fitting semantics, these two are equivalent exactly when k denotes, so it is non-denoting terms that force us to use such machinery classically. Frege noted an analogous problem with intentional contexts, and introduced the notions of “sense” and “denotation” to deal with it. Roughly, this gives terms two kinds of values, what they denote, and what they mean. Of course this is loose. But the introduction of a scoping mechanism also turns out to be of considerable use here.

Occurrences of parameters in a formula are not counted as free occurrences. Further, if we refer to a variable, it is assumed it is not a parameter. If we need to speak about a parameter, we will explicitly say so. To state the existential tableau rules, we use the following convention. Suppose Φ(αt ) is a formula in which the variable αt , of type t, may have free occurrences. And suppose pt is a parameter of type t. Then Φ(pt ) is the result of replacing all free occurrences of αt with occurrences of pt .

N are grounded terms, we refer to the formula as grounded. Example 2. X (X) (P) ⊃ X(x)] is a predicate abstract, hence a term. X (X) 2 (P1 ) ⊃ X(x)] is an extended term. X (X) 2 (P1 ) ⊃ X(x)] 3 is. The presence of a prefix σ on a subterm is intended to indicate that we are thinking about the object the subterm denotes at the world that σ denotes. Since not all subterms may have been intuitively evaluated at a particular stage of a proof, there might be subterms that have not been prefixed.