Computer languages as examples in formal logic

[sbrothy]

Summary:: For the purposes of teaching topics in mathematical logic, how can we make examples based on a computer language?

I more than suspect that I'm way out of my league here, but did you consider functional languages like for instance Miranda? I'd expect such languages to convey mathematics and logic better than a messy "structured" language like C.
Regards.

 

[Stephen Tashi]

I don't know whether this helps or not, but here is an implementation of a universal program

I'm not familiar with the terminology "universal program". Does that mean an implementation of a "universal Turing machine"?

 

[SSequence]

Yes, pretty much. So, for example, I considered the universal program for the "primitive model" I described (with four basic commands) [described in a model where few extra things like macros/conditionals were added for better readability and to avoid too much repetition].

 

[strangerep]

Summary:: For the purposes of teaching topics in mathematical logic, how can we make examples based on a computer language?

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?

Are you familiar with Z and Object-Z? They are formal specification languages, built upon the mathematical concepts of sets and mappings. But they're not executable, afaik.

 

[.Scott]

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".

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.

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.

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".

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.

 

[Stephen Tashi]

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".

I agree that the nature of imperative statements sets computer languages apart from the types of formal systems that were invented before computers were common.

It seems to me that by this definition, computer programming languages are "wffs".

We have to distinguish between parsers of computer languages versus things related to the execution of their instructions. The terminology "computer language" usually includes both.

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.

This brings up the distinction between interpreters and compliers. Parsers for compilers recognize only one version of a wff. That version is a complete program. On the way to parsing code for a program they may check that segments of code form special kinds of wffs, such a variable declarations. However, it's hard to make a correspondence between the notion of the many special types of wffs used in parsers with the notion of a single type of wff that is used in formal systems.

The parsing used by interpreters uses a definition of wff that is a more interesting analogy to a formal language than the parsing used by a compiler. I'm glad you brought up interpreters.

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".

Yes, formal languages do not contain any definitions related to the "states" of wffs. There is no requirement that wff can be evaluated as being True or False - or as being 37.6 or the declaration of object.

Formal Systems also don't contain any rules about the "states" of wffs. They contain rules for producing new wffs from given wffs, but they don't contain rules saying how to use a given a"True" wff to produce another "True" wff. The concept of a "True" wff doesn't apply. The notion of "True" has to do with the state of a wff, which is not defined.

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".

I'll state the analogy differently.

A parser for a computer language can be regarded as implicitly defining a formal language. I suppose it's the technical documentation for a parser that actually defines the formal language - not the executable code for the parser. In a parser for a compiler, a wff is a valid program. In a parser for an interpreter, a wff is any text that defines an operation the interpreter can execute.

An optimizer for code implicitly defines rules for deriving one valid program in machine code from another valid program in machine code. So the technical description of an optimizer is an example of a Formal System. Similary, a code "clean-up" program that converts valid text for a program in some computer language to valid text for it in the same language implicitly defines a formal system.

If we define a computer program to be "True" if it's execution satisfies some requirements and "False" otherwise, then optimizers and code clean-up programs implicitly define Formal Logics.

 

[Stephen Tashi]

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.

What about this for an aphorism?:

Abstract math deals with "may" and computer programs deal with "must".

Which is to say that mathematics offers many possible ways to proceed from some given inputs. (e.g. from a given wff we may produce another wff, from a given premise we may deduce a particular conclusion.) The executable for a computer program defines how a machine must proceed from a given input. This is true even for computer programs that use pseudo-randomness.

 

[Stephen Tashi]

Are you familiar with Z and Object-Z? They are formal specification languages, built upon the mathematical concepts of sets and mappings. But they're not executable, afaik.

I'm not familiar with Z - or with specification languages in general. Can we make analogy between specification languages and topics that arise in the foundations of math, such as formal logics?

 

[strangerep]

I'm not familiar with Z - or with specification languages in general. Can we make analogy between specification languages and topics that arise in the foundations of math, such as formal logics?

That's not something I can answer in a short post. Probably best if you google "Introduction to Z".

 

[sbrothy]

FYI: https://arxiv.org/abs/2008.08923

Regards.

 

[.Scott]

What about this for an aphorism?:

Abstract math deals with "may" and computer programs deal with "must".

Which is to say that mathematics offers many possible ways to proceed from some given inputs. (e.g. from a given wff we may produce another wff, from a given premise we may deduce a particular conclusion.) The executable for a computer program defines how a machine must proceed from a given input. This is true even for computer programs that use pseudo-randomness.

No. Both "may" and "must" are declaratives. Computer programs are "do". They are inherently goal-oriented. It's the difference between me suggesting that a restaurant is good and me telling the restaurant to do a good job.

Or me telling you to work at the restaurant.
Once we define what constitutes "working at a restaurant", then we can determined whether you have achieved the "working at a restaurant" state.