Stephen Tashi said:
Summary:: For the purposes of teaching topics in mathematical logic, how can we make examples based on a computer language?
I'm not sure. But let's start out with the recognition that the statements at the core of computer programs are imperative. In contrast, logical statements are declarative. Thus the C statement "A = A && B;" specifies an operation on variable A. Whereas the logical statement "A = A ^ B" is either true or false and is equivalent to "B -> A".
Stephen Tashi said:
A computer language is not a clear example of a formal language, a formal system, or a formal logic. Can we modify the rules for a computer language to create clear examples?
My non-authoritative classification of topics in mathematical logic is:
1. Formal languages. A formal language is defined by a set of rules that define which strings of symbols are "well formed formulas" (wffs). A wff has no semantic interpretation other than being syntactically correct according the rules of the formal language. Within the context of a formal language, a wff does not represent a statement that is True or False or a mathematical function.
It seems to me that by this definition, computer programming languages are "wffs". When the compiler or interpreter processes the symbol string, it will recognize proper syntax or issue an error message. There might be some wiggle room for interpreted languages - because the interpreter might never attempt to fully parse some sections of the code. But in the case of a compiled language, the compiler will either generate object code or issue error messages - an unambiguous indication of whether the syntax has been followed.
Stephen Tashi said:
2. Formal systems: A formal system is a formal language plus a set of "production rules". If we write down an initial wff, the production rules describe permissible operations for "deriving" other wffs from the initial wff. Within the context of a formal system, there is no interpretation that wffs involved are True (or False), so the "derivations" are not mathematical proofs that deduce True statements from some initial statement that is assumed to be True.
I won't claim to be entirely clear on what you are describing, but I believe that we can describe a computer program this way. The notion of true or false is being introduced - it was not mentioned in your definition of "Formal Languages".
As I said before, computer programs are not declarative - they are imperative. When applied to a machine, they cause that machine to yield a result. Starting with a specific computer program (a wff), we can apply specific rules to transform that program into equivalent programs (other wff symbol sets) that will yield those same results. So given that a specific wff is "true", it can be transformed into other wffs that are also "true".
In fact, this operation is routinely performed on computer programs. If you start with a C program and compile it, several operations of this type are performed. First, the programming logic is parsed, categorically tabulated, and analyzed - a process which involves a major change in syntax and potentially changes to the wff imperatives themselves. Then optimizations are applied. This is a very explicit process of transforming the wff into a different but equivalent set of instructions - so a different wff has been formed with rules that assure that this new wff is just as "true" as the original. This optimized code is then provided in a variety of syntactical renditions - a buildable object module, an executable, and perhaps marco-assembly source.
So I would suggest that a computer language - especially in conjunction with functional compilers - could be considered a "Formal System" by your definition.
Stephen Tashi said:
3. Formal logics: A consistent formal two-valued logic is a formal system with additional requirements. The wffs must each be assigned exactly one of two possible values, either True or False. (As a matter of vocabulary, in a specific formal language, the wffs are assigned specific values. Speaking of "formal language" as a generality, it is a set of specific formal languages. The value assigned to a wff may vary between two different languages in that set.) The production rules must have the property that (for each specific language in the formal language) if the initial wff is True, all the wffs produced from it are True.
Given how I applied "Formal System" to a computer programing (above), all that needs to be done to meet your "Formal Logic" standard is to introduce the notion of whether a program is "true" or "false". In the case above, I simply presumed the original program (wff) to be True or False. But I believe that extending this to your definition of a "Formal System" leads to the introduction of the concept of "requirements". Given a set of requirements, a computer program can be said to be true (produces the required results) or false (fails to produce the required results). So if the required result is to produce the sequence of numbers that are the first 10,000 prime numbers, then a formal system is defined where any wff can be determined to be either true or false. Similarly, any other well-formed requirements would constitute a new "Formal System".
Stephen Tashi said:
However, that doesn't fix the problem that C is not a good example of a Formal System. So restricting it to boolean variables doesn't give us production rules.
I agree. C is not a Formal System. It is only a syntax.
