Formal Systems Language

Formal Systems

I don't fully understand what "Formal Systems" mathematics is all about, but I have learned some of it's terminology, which comes up in SemanticWeb technology.

My limited understanding is that this is a formalism for how we make logical arguments. It's a lot like Geometry, where you say, "because this is an axiom, and this is something we proved with other axioms, we can reason this, this, and this, and then we can prove this, which was what we wanted."

It's also is like Computer Science formalisms of computer languages. That is, where you do things like: Break a language down into the itty bitty words you can express. And then you talk about "is it grammatically correct to arrange the words in this way." And there you have the "Syntax, Semantics, and Pragmatics" split, talking about the issues in the language.

So, this is the frame of mind to be in as you read the rest of the terminology.

Here is a diagram of major terms, and some text on what they mean:

This image is public domain, released on October 15,2004 by it's creator, the author of this statement, LionKimbro.

Theory

What is called a theory here, includes the following things:

symbols - symbols and words and marks used to make expressions
well-formed formulas ("wff"s) - the expressions you can write with the symbols that make sense
axioms - expressions that you insist are true, as part of the theory
rules of inference - rules telling how you can make new expressions out of old ones

Symbols

Symbols are just marks that you use to say things in your theory.

So for example, you might have: "cat", "word", "dog", "robot", "animal", "thing", "cybernetic organism", "is a", "exists"

They don't say complete things, they just are the symbols you use.

In another theory, you might have symbols like "f", "g", "h", "*", "+", yadda yadda yadda.

Expressions

Expressions are just rows of your symbols.

Like: "(cat) (is a) (animal)"

But also: "(cat) (cat) (cat) (cat) (cat)" - doesn't necessarily have to make sense.

I suppose you could write a cool 2-D or 3-D HookupLanguage to write your symbols in.

But we'd still call it an "expression."

Well-Formed Formula (WFF)

One of the required things you have in a theory is a set of wffs.

A wff, also just called a formula, is an expression that it makes sense to say, in your theory.

Consider:

(cat) (is a) (animal)

(cat) (is a) (dog)

(cat) (dog) (dog)

Because it's all about "is this something you can say in the theory." It is not about: "is this true or false." It's only about: "Is this something you can say in the theory."

Note that the formal systems people aren't so interested in talking about: "How do you tell if this is a syntactic expression or not?" That kind of thing- Computer Scientists working on "grammars" work on that kind of thing. But these formal systems people are more interested in talking about questions like: "How do I know if such-and-such is true, given this particular theory?" That'll become clearer as you read on.

Axioms

A subset of the wffs are what we call "axioms," and this is where we get into the "what's true or false" part of the formal systems thing.

Usually it's just a very small subset of all the zillions of possible wffs that are axioms. This is sort of like- when you're describing how to count to infinity- you say, "Well, you start with 0, and then you add one, and then you add one, and then you just keep adding one." Similarly, we're going to say, "Well, you start with your axiom, and then you use your rules of inference, and then you make new wffs out of your axioms, and so on and so forth, until you know a bunch of things."

So, an axiom is something that we insist is true, as part of our theory.

Rule of Inference

The "rules of inference" are the last major part of our theory concept.

Briefly recounting, we have, in a theory,

symbols - things we can write with
wffs - things it makes sense to say
axioms - things we insist are true
and now, rules of inference

So, the "rules of inference" tell us how, with the benefit of axioms, and possibly some hypothesis, (wait for it,) we can figure out new things.

What do they look like?

Well, they have input slots, and and an output slot. You put wffs in on the inputs, and out comes a wff.

For instance, one of our rules of inference might read something like:

Input 1: (symbol A) (is a) (symbol B)
Input 2: (symbol B) (is a) (symbol C)
Output: (symbol A) (is a) (symbol C)

Or maybe something like:

Input 1: (symbol A) (exists)
Input 2: (symbol A) (is a) (symbol B)
Output: (symbol B) (exists)

(Right? So, if you said a cat exists, and a cat is an animal, then an animal exists, too.)

Schema

The blueprints for the rules of inference are called "schema."

i.e.- you know, where we just wrote "Input 1 is such-and-such, and then Input 2 is such-and-such, and then the output it such-and-such"- that description is called a "schema."

And you can think of it as a "template" or a "pattern" that you describe the rules of inference in.

You can use symbols, and place-holders for symbols, like "symbol A" or "symbol B", in the schema.

(Side note: In Mozilla, they use RDF. And in their XUL, you can write rules which use this schema idea, so you can tell how to transform from raw RDF into HTML, and words, and stuff like that. It's very cool.)

Hypothesis

A "hypothesis" is an idea, in the form of a wff, that we are temporarily entertaining.

Like, for instance, suppose we said something like: "Well, let's suppose that (cat) (exists). Would that mean that (animal) (exists)? How about (dog) (exists)?"

See? It's part of the game we're constructing: We're making a thing called a theory, that you can use to try out hypothesis, and see if such-and-such is true or not. And this is call called "formal systems. You almost certinaly already know all these ideas, we're just attaching a super-strong language to it.

You might wonder: "Well, why not make those things just axioms, like in Geometry, and then we don't have to add in this idea of "hypothesis.""

But this is like a computer program: The axioms are like constants, and the hypotheses is like variables. We're using a thing that we're calling the theory like a function, that you call with some hypothesis, and you see if it can prove a particular wff for you or not, by the rules of inference. (The result would be called a proof of derivation.)

So the answer is, "We want to say these things are fixed (axioms), but these things are variable (hypothesis)."

X "is Deducable from" Y "in Theory" T

So, you have a bunch of hypothesis Y1, Y2, Y3, Y..., Yn, and then you say, "Is this thing X- is that true or not, in theory T?"

So, I might say:

Hypothesis Y: (cat) exists
I'm wondering if X: (thing) exists
My theory is "T".

And so, if you plug in hypothesis Y into your theory T, is it true or not that X is true?

If it is, then you say: "Yes, it's true. X is deducable from Y in theory T."

Our theory might include things like:

axiom: (cat) (is a) (animal)
axiom: (animal) (is a) (thing)
rule of inference: (A) (exists), (A) (is a) (B), then: (B) (exists)
rule of inference: (A) (is a) (B), (B) (is a) (C), then: (A) (is a) (C)

Plugging in hypothesis (cat) (exists), we should be able to get out (thing) (exists).

Proof of Derivation

The result comes as a proof of derivation.

Each line of a proof of derivation is made of either:

an axiom
a hypothesis
a "direct consequence" from some rule of derivation over the previous lines

So, for example, our proof of derivation might look like:

(cat) (is a) (animal) - axiom
(animal) (is a) (thing) - axiom
(cat) (is a) (thing) - direct consequence
(cat) (exists) - hypothesis
(thing) (exists) - direct consequence

This is a proof of derivation that (thing) (exists) by our example theory.

Page Notes

This was written by LionKimbro, after studying a page, "Formal Systems - Definitions."

The first revision of this page in the ESW wiki was written entirely by LionKimbro, the author writing this sentence, and this first revision of this page is hereby placed into the public domain. That is, you are free to use this revision (the first revision) of this page for any purpose that you like. That includes the graphic image used as well.

Versions beyond the first may have been edited by other people, and I can't really say whether they put their contributions into the public domain or not. So, use the first version of the page, and you're safe.

-- LionKimbro DateTime(2004-10-17T09:32:38Z)

Not Described, Diagramed

Theorem (basically, any true statement can get from just the axioms)
Monotonic Theorem
Compact Theorem
Interpretation - seems like voodoo, given the Formal Systems - Definition description
Model
Complete Theory
Sound Theory
Complete Computation Method
Decidable Theory
Consistent Theory
"First Order Predicate Calculus (Logic)"

Discussion

( none yet )