Gloss of "Proposition"

We employ the term "proposition" because it has fewer misleading connotations in this domain than "sentence", "assertion", "statement" or "proof goal".

It is not part of the FDL design what the structure of a proposition must be, except that it must be an expression of the general form used in the FDL, ie, a Text.

A proposition might paradigmatically be thought of as a statement with a truth condition that is understandable independently of inferences in which it occurs, but it is also possible that the significance of a proposition might depend on an inference in which it occurs. For example, there may be some sort of schematic variables that are shared by the premises and conclusion of an inference step indicating a generality such as that any way of uniformly instantiating the schematic variables throughout the inference is also a legitimate inference. A "proposition" with such schematic variables might not then really mean anything independently.

In a simple Hilbert-style system the propositions might be the kinds of formulas that could be further combined by standard sentential operators such as disjunction. In a block structured natural deduction system a proposition might be the sort of formula just mentioned combined with a context for assumptions. In a sequent calculus the propositions would be whole sequents. The FDL conception of propositional form, however, is purely programmatic, and consists simply of its role in inferences; the aforementioned notions of proposition would be instances.

When a new kind of Inference Engine is introduced into the FDL one must design the form of propositions to be used in inferences by that engine. If one were concerned solely with the individual inference then one would have an awful lot of freedom in deciding what should go into the proposition and what should go into the Justification. The basic constraint on this design is imposed by the rather natural fact that inference steps are assembled into a Proof based upon the match between propositions used as premises and conclusions, and if the same inference engine is used on a collection of inferences that can be formed into a rooted dag based on conclusion/premise matching, then the root conclusion is deemed to be a consequence of all the leaf premises. IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html