Connections and higher-order logic

Abstract

Theorem proving is difficult and deals with complex phenomena. The difficulties seem to be compounded when one works with higher-order logic, but the rich expressive power of Church's formulation [10] [3] of this language makes research on theorem proving in this realm very worthwhile. In order to make significant progress on this problem, we need to try many approaches and ideas, and explore many questions. A highly relevant question is "What makes a logical formula valid?".

One approach to this question is semantic. Theorems are true because they express essential truths and thus are true in all models of the language in which they are expressed. Truth can be perceived from many perspectives, so there may be many essentially different proofs of theorems. This point of view is very appealing, but it does not shed much light on the basic question of what makes certain sentences true in all models, while others are not.

Of course, theorems are formulas which have proofs, and every proof in any logical system may provide some insight. This suggests seeing what one can learn by studying the forms proofs can take. While this may be helpful, many of the most prominent features of proofs seem to be influenced as much by the logical system in which the proof is given as by the theorem that is being proved.

We focus on trying to understand what there is about the syntactic structures of theorems that makes them valid. In the case of formulas of propositional calculus, one can test a formula for being a tautology in an explicit syntactic way. However, simply checking each line of a truth table is not really very enlightening, and we may still find ourselves asking "What is there about the structure of this formula which makes it a tautology?". Clearly the pattern of occurrences of positive and negative literals in such a formula is very important, and this leads to the theory of connections or matings [4] [1] [6]. A connection is a pair of literal-occurrences, and a mating is a set of connections, i.e., a relation between occurrences of literals. A mating is acceptable if its structure guarantees that the formula is a tautology. Perhaps much more can be said about criteria for matings to be acceptable.

This work is supported by NSF grant DCR-8402532.