|Proposition||- an expression used as a conclusion or premise of an
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
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
When a new kind of