Axis from FOLDOC

(AADL) A language allowing concise modular specification of multiprocessor architectures from the compiler/operating-system interface level down to chip level. AADL is rich enough to specify target architectures while providing a concise model for clocked microarchitectures.

["AADL: A Net-Based Specification Method for Computer Architecture Design", W. Damm et al in Languages for Parallel Architectures, J.W. deBakker ed, Wiley, 1989].

Last updated: 2003-06-30

axiomatic semantics

<theory>

A set of assertions about properties of a system and how they are effected by program execution. The axiomatic semantics of a program could include pre- and post-conditions for operations. In particular if you view the program as a state transformer (or collection of state transformers), the axiomatic semantics is a set of invariants on the state which the state transformer satisfies.

E.g. for a function with the type:

 sort_list :: [T] -> [T]

we might give the precondition that the argument of the function is a list, and a postcondition that the return value is a list that is sorted.

One interesting use of axiomatic semantics is to have a language that has a finitely computable sublanguage that is used for specifying pre and post conditions, and then have the compiler prove that the program will satisfy those conditions.

Last updated: 1995-11-09

axiomatic set theory

<theory>

One of several approaches to set theory, consisting of a formal language for talking about sets and a collection of axioms describing how they behave.

There are many different axiomatisations for set theory. Each takes a slightly different approach to the problem of finding a theory that captures as much as possible of the intuitive idea of what a set is, while avoiding the paradoxes that result from accepting all of it, the most famous being Russell's paradox.

The main source of trouble in naive set theory is the idea that you can specify a set by saying whether each object in the universe is in the "set" or not. Accordingly, the most important differences between different axiomatisations of set theory concern the restrictions they place on this idea (known as "comprehension").

Zermelo Fränkel set theory, the most commonly used axiomatisation, gets round it by (in effect) saying that you can only use this principle to define subsets of existing sets.

NBG (von Neumann-Bernays-Goedel) set theory sort of allows comprehension for all formulae without restriction, but distinguishes between two kinds of set, so that the sets produced by applying comprehension are only second-class sets. NBG is exactly as powerful as ZF, in the sense that any statement that can be formalised in both theories is a theorem of ZF if and only if it is a theorem of ZFC.

MK (Morse-Kelley) set theory is a strengthened version of NBG, with a simpler axiom system. It is strictly stronger than NBG, and it is possible that NBG might be consistent but MK inconsistent.

NF ("New Foundations"), a theory developed by Willard Van Orman Quine, places a very different restriction on comprehension: it only works when the formula describing the membership condition for your putative set is "stratified", which means that it could be made to make sense if you worked in a system where every set had a level attached to it, so that a level-n set could only be a member of sets of level n+1. (This doesn't mean that there are actually levels attached to sets in NF). NF is very different from ZF; for instance, in NF the universe is a set (which it isn't in ZF, because the whole point of ZF is that it forbids sets that are "too large"), and it can be proved that the Axiom of Choice is false in NF!

ML ("Modern Logic") is to NF as NBG is to ZF. (Its name derives from the title of the book in which Quine introduced an early, defective, form of it). It is stronger than ZF (it can prove things that ZF can't), but if NF is consistent then ML is too.

Last updated: 2003-09-21

Axiom of Choice

<logic>

(AC, or "Choice") An axiom of set theory:

If X is a set of sets, and S is the union of all the elements of X, then there exists a function f:X -> S such that for all non-empty x in X, f(x) is an element of x.

In other words, we can always choose an element from each set in a set of sets, simultaneously.

Function f is a "choice function" for X - for each x in X, it chooses an element of x.

Most people's reaction to AC is: "But of course that's true! From each set, just take the element that's biggest, stupidest, closest to the North Pole, or whatever". Indeed, for any finite set of sets, we can simply consider each set in turn and pick an arbitrary element in some such way. We can also construct a choice function for most simple infinite sets of sets if they are generated in some regular way. However, there are some infinite sets for which the construction or specification of such a choice function would never end because we would have to consider an infinite number of separate cases.

For example, if we express the real number line R as the union of many "copies" of the rational numbers, Q, namely Q, Q+a, Q+b, and infinitely (in fact uncountably) many more, where a, b, etc. are irrational numbers no two of which differ by a rational, and

  Q+a == {q+a : q in Q}

we cannot pick an element of each of these "copies" without AC.

An example of the use of AC is the theorem which states that the countable union of countable sets is countable. I.e. if X is countable and every element of X is countable (including the possibility that they're finite), then the sumset of X is countable. AC is required for this to be true in general.

Even if one accepts the axiom, it doesn't tell you how to construct a choice function, only that one exists. Most mathematicians are quite happy to use AC if they need it, but those who are careful will, at least, draw attention to the fact that they have used it. There is something a little odd about Choice, and it has some alarming consequences, so results which actually "need" it are somehow a bit suspicious, e.g. the Banach-Tarski paradox. On the other side, consider Russell's Attic.

AC is not a theorem of Zermelo Fränkel set theory (ZF). Gödel and Paul Cohen proved that AC is independent of ZF, i.e. if ZF is consistent, then so are ZFC (ZF with AC) and ZF(~C) (ZF with the negation of AC). This means that we cannot use ZF to prove or disprove AC.

Last updated: 2003-07-11

Axiom of Comprehension

<logic>

An axiom schema of set theory which states: if P(x) is a property then

 {x : P}

is a set. I.e. all the things with some property form a set.

Acceptance of this axiom leads to Russell's Paradox which is why Zermelo set theory replaces it with a restricted form.

Last updated: 1995-03-31

axiom schema

<logic>

A formula in the language of an axiomatic system, containing one or more. These metasyntactic variables (or "schematic variables") that stand for terms or subformulae. An example is the Axiom of Comprehension.

Last updated: 2009-02-10

Nearby terms:

AWT ♦ aXe ♦ AXIOM ♦ axiom ♦ AXIOM* ♦ Axiomatic Architecture Description Language

Try this search on Wikipedia, Wiktionary, Google, OneLook.