12,080
edits
Changes
MyWikiBiz, Author Your Legacy — Wednesday May 01, 2024
Jump to navigationJump to searchDirectory:Jon Awbrey/Papers/Inquiry Driven Systems : Part 8 (view source)
Revision as of 18:10, 20 August 2011
, 18:10, 20 August 2011→8.4.1. Objective 1a : Propositions as Types: + text
====8.4.1. Objective 1a : Propositions as Types====
====8.4.1. Objective 1a : Propositions as Types====
In this component I investigate an important relationship that exists between two kinds of formal systems, called applicational calculi (AC's) and propositional calculi (PC's).
Expressions in an applicational calculus are called "terms" and are built up from a supply of primitive symbols called "basic terms" through the use of a binary operation called "application".
Expressions in a propositional calculus are called "propositions" and are built up from a supply of primitive symbols called "basic propositions" through the use of a stock of k ary operations called "connectives".
Exact formalization of symbolic calculi is absolutely necessary, especially if we want computers to serve as interpreters, or at least to lighten the burdens of interpretation by taking up the bit parts of formal routines. Because the problem environments where calculi develop show no signs of stopping in their growing complexity, it becomes inevitable that we turn to computers as auxiliary interpreters of formal systems, to secure their operational significance and manage the increasing complications of their practical use. But a formalized syntax, however necessary, is not enough to demonstrate utility.
A calculus is never a finished object, complete in itself, but a tool shaped to the end of interpretation.
I am using the word "interpretation" to denote the whole complex of activities through which signs acquire practical meaning. For human beings the process of interpretation is a largely automatic and usually unanalyzed affair, but it can also be highly flexible and unusually adaptive. Human language users or symbol manipulators have powers they hardly reflect on and barely understand, to entertain novel associations between signs and whatever it is that signs convey, to examine habitual assumptions about the meaning of symbols in practice.
One person can simply invite another to entertain new associations between signs and ideas or to examine old assumptions about their meaning in practice, and the other is somehow able to comply, if only for the sake of experiment and argument. But the need to supply a formal system with a computational basis, involving exact syntax, effective semantics, and computerized "pragmatics" (that is, a computer supported operational basis) requires us to analyze the process of interpretation in minute detail and on new grounds.
In use, AC's and PC's take on meaning according to a variety of interpretive rules. I am adopting an interpretation on either side that highlights the relation of interest between these two kinds of calculi and that brings the intended correspondence into sharper relief.
In both kinds of calculus the primitive symbols are distinguished as "constants" and "variables". A constant is a name for a definite object of thought, and is intended to maintain a fixed meaning throughout a given discussion. A variable is a symbol of indefinite reference, or a token without a pre assigned meaning, but is used as a site for the substitution of other expressions or as a placeholder for a multitude of conceptual objects and logical values.
Semantics. Meanings are provided or attached to symbols by means of:
1. Contexts of occurrence: the facts or rules of distribution.
2. Action induced on other symbols by means of rewrite rules:
:: generators and relations, or paraphrastic definitions.
3. Synonymy: membership in semantic equivalence classes.
4. Arbitrary fiat, external designation, or special convention.
====8.4.2. Objective 1b : Proof Styles and Developments====
====8.4.2. Objective 1b : Proof Styles and Developments====
